The Coq mailing list

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

Hi all

using the tactic "inversion H." on a hypothesis of the form

H :  a :: L = b :: L

gives us that a is equal to b. But how can we do the same when we have a function instead of a constructor? Such as in the case of snoc (from Pierce's software foundations, code fragment below).

H : snoc L a = snoc L b

inversion does not work; is there some easy way, possibly through a tactic, to do this? or must one just prove lemmas?

Thanks in advance.

Best
Chris

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) ..).

Fixpoint snoc (l : natlist) (v : nat) : natlist :=

  match l with

  | [] => [v]

  | h :: t => h :: snoc t v

  end.

Fixpoint rev (l:natlist) : natlist := 

  match l with

  | nil    => nil

  | h :: t => snoc (rev t) h

  end.

Fixpoint app (l1 l2 : natlist) : natlist := 

  match l1 with

  | nil    => l2

  | h :: t => h :: (app t l2)

  end.

Notation "x ++ y" := (app x y) 

                     (right associativity, at level 60).

Axiom snoc_append : forall (l:natlist) (n:nat),

  snoc l n =  l ++ [n].

Axiom emp_snoc : forall a L, [] = snoc L a -> False.

Goal forall (l1 l2 : natlist), rev l1 = rev l2 -> l1 = l2.

Proof with auto.

  induction l1 as [|n1 l1], l2  as [|n2 l2] ; simpl; intros...

  apply emp_snoc in H. contradiction.

  symmetry in H.

  apply emp_snoc in H. contradiction.

  inversion H. (* no effect *)

  repeat rewrite snoc_append in H.

  inversion H. (* no effect *)

  admit.

Qed.