The Coq mailing list

[Christopher Ernest Sally <christopherernestsally AT gmail.com>]

Thank you, Daniel and Julien!

That helps a lot, especially Function which is new to me.

Best

Chris

On 8 December 2013 03:52, <forest AT ensiie.fr> wrote:

Or .....
you can use Function which will allow you to reason easily on snoc (see
code bellow)


Hope this help,

Julien

Inductive natlist : Type :=  nil : natlist | cons : nat -> natlist ->
natlist.
Notation "x :: l" := (cons x l) (at level 60, right associativity).
Notation "[ ]" := nil.
Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).

Function snoc (l : natlist) (v : nat) : natlist :=
  match l with
  | [] => [v]
  | h :: t => h :: snoc t v
  end.

(* Function defines many principles on snoc including
   - induction principle to be used alone or via functional induction
   - some lemmas to allow functionnal inversion
*)

Lemma snoc_nil_discr : forall (l : natlist) (v : nat),
  snoc l v <> nil.
Proof.
  intros.
  intro.
  (* functionnal inversion is the functionnal version of inversion.  *)
  functional inversion H.
Qed.

Lemma snoc_inj : forall (l1 l2 : natlist) (v1 v2 : nat),
  snoc l1 v1 = snoc l2 v2 -> l1 = l2 /\ v1 = v2.
Proof.
  intros l1 l2 v1 v2;revert l2 v2.
  (* functional induction will apply the snoc_rect induction principle
  on the current goal as induction should apply nat_ind on a goal *)
 functional induction (snoc l1 v1);intros l2 v2 H.
  - functional inversion H;clear H.
    + auto.
    + subst.
      functional inversion H5.
  - functional inversion H;clear H.
    + subst.
      functional inversion H4.
    + subst.
      destruct (IHn _ _ H5).
      subst.
      auto.
Qed.