Creating a tactic for 'destructing' a list by last element?

Question

Sometimes, I have a context in which I have some l : list X, and I want to prove the goal by proving that (1) If l = [], the goal holds, and (2) If l = l' ++ [x], the goal still holds.

This usually takes the form of a proof pattern. For example,

Goal forall {X} (l : list X), True.
  Proof.
    intros.
    destruct (unsnoc l) as [ [l' x] | ] eqn:E.
    2 : {
      rewrite unsnoc_None in E. subst l. 
      (* now all instances of l have been replaced with []*)
      
      exact I.
    } {
      rewrite unsnoc_Some in E.
      (* now we have l = l' ++ [x] *)

      exact I.
    }
  Qed.

How can I write a tactic unsnoc_destruct l as [ E l' x] which does generate this proof structure for me?

I tried the following, but it has the wrong order of goals, and I cannot seem to suggest better variable names using an as clause.

Ltac unsnoc_destruct l :=
  let E := fresh "E" l in
  let x := fresh "x" in
  let l' := fresh "l'" in
  destruct (unsnoc l) as [ [x l'] | ] eqn:E;
  [ 
    rewrite -> unsnoc_Some in E
  | rewrite unsnoc_None in E; subst l ].

---

Including definitions and proofs used in the question above:

Require Import Coq.Lists.List.
Import ListNotations.

Fixpoint unsnoc {X : Type} (l : list X) : option (list X * X) :=
   match l with
   | [] => None
   | x :: l' => match unsnoc l' with
     | None => Some ([], x)
     | Some (l'', x') => Some (x :: l'', x')
     end
   end.
 
 Lemma last_inversion {A : Type} : forall (x y : A) xs ys,
     xs ++ [x] = ys ++ [y] -> xs = ys /\ x = y.
 Proof.
   intros. apply (f_equal (@rev A)) in H.
   repeat rewrite (rev_app_distr) in H.
   simpl in H. inversion H. apply (f_equal (@rev A)) in H2.
   repeat rewrite rev_involutive in H2.
   auto.
 Qed.
 
 Lemma unsnoc_spec {X : Type} : forall (l : list X) (l' : list X),
   (forall x, unsnoc l = Some (l', x) <-> l = l' ++ [x])
   /\ (unsnoc l = None <-> l = []).
 Proof.
   induction l.
   - simpl. intros. repeat split. try discriminate.
     intros. destruct l'; discriminate.
   - destruct (unsnoc l) eqn:E.
     + destruct p as [l1 x1].
       intros. split.
       * intros. simpl. rewrite E. 
         specialize (IHl l1).
         destruct IHl as [IHl1 IHl2].
         specialize (IHl1 x1).
         assert (l = l1 ++ [x1]) as H. {
           apply IHl1. auto.
         }
         rewrite H. 
         split. intros.
         ** inversion H0.  auto. 
         ** intros. 
            replace (a :: l1 ++ [x1]) with ((a :: l1) ++ [x1]) in H0 by auto.
            apply last_inversion in H0. destruct H0. subst. auto.
       * intros. split; [ | discriminate].
         simpl. rewrite E. intros. inversion H.
     + simpl.
        assert (l = []) as H. {
         specialize (IHl []) as [IHl1 IHl2].
         apply IHl2. auto.
        }
        subst l. simpl.
        repeat split; try discriminate.
        * intros. inversion H. subst. reflexivity.
        * intros. 
          replace ([a]) with ([] ++ [a]) in H by auto.
          apply last_inversion in H. destruct H. subst. auto.
 Qed.
 
 Lemma unsnoc_Some {X : Type} : forall (l : list X) (l' : list X) (x : X),
   (unsnoc l = Some (l', x) <-> l = l' ++ [x]).
 Proof.
   intros. apply unsnoc_spec.
 Qed.
 
 Lemma unsnoc_None {X : Type} : forall (l : list X),
   (unsnoc l = None <-> l = []).
 Proof.
   intros. apply unsnoc_spec. exact [].
 Qed.

Answer 1

A fun way is to express the destructuring as something resembling an induction principle. For example, you can define "snoc induction" like this:

From Coq Require Import List.
Import ListNotations.

Definition snoc {A:Type} (xh : list A) (x : A) : list A := xh ++ [x].

Lemma list_snoc_ind {A:Type} (P : list A -> Prop) :
  P [] ->
  (forall xh x, P xh -> P (snoc xh x)) ->
  forall l, P l.
Proof.
  intros Pnil Psnoc l.
  rewrite <- rev_involutive.
  induction (rev l) as [|xh xr IH]. 1: easy.
  now apply Psnoc.
Qed.

Lemma list_snoc_destruct {A:Type} (P : list A -> Prop) :
  P [] ->
  (forall xh x, P (snoc xh x)) ->
  forall l, P l.
Proof. intros Pnil Psnoc. eapply list_snoc_ind; easy. Qed.

If you leave out the inductive hypothesis, you get a "destruction scheme," like list_snoc_destruct.

The induction tactic now allows you to use this instead of the default induction scheme. In general, induction .. using scheme allows you to use scheme, as long as scheme looks "close enough" to an induction principle.

This then allows you to do the match like in this example:

Goal forall A (l:list A), l = nil \/ exists hd tl, l = snoc hd tl.
Proof.
  intros A la.
  induction la as [|xh x] using list_snoc_destruct.
  - now left.
  - right. do 2 eexists. reflexivity.
Qed.

Answer 2

Here is a solution that feels more like destruct than induction:

Ltac _unsnoc_destruct l x l':=
  let x := fresh x in
  let l' := fresh l' in
  (destruct (unsnoc_dest l) as [[x [l']]|]) ; subst l.

Tactic Notation "unsnoc_destruct" constr(l) "as" ident(x) ident(l') := _unsnoc_destruct l x l'.

Variable (P : forall {X}, list X -> Prop).

Goal forall X (l : list X), P l.
Proof.
  intros X l.
  unsnoc_destruct l as x l'.
  (* 2 Goals: P (l' ++ [x]) and P [] *) 
  Undo.
  unsnoc_destruct l as y z.
  (* 2 Goals: P (y ++ [z]) and P [] *) 

Note the use of Tactic Notation to wrap the tactic, that itself handles the naming. Ultimately, the core tactic is a one-liner (destruct (unsnoc_dest l) as [[x [l']]|]) ; subst., so you might even just use that – although it is probably less readable.

(On a side-note, the quantification on l' outside of the conjunct in your statement of unsnoc_spec is strange.)