The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

How about this:

Require Import List.

Definition snoc {A:Type} (l:list A) (x:A) :=

l ++ x :: nil.

Fixpoint snoc_rect {A:Type} (P:list A -> Type)

  (Pnil : P nil) (Psnoc : forall (l : list A) (x : A),

                  P l -> P (snoc l x))

  (l : list A) : P l :=

match l with

| nil => Pnil

| a :: l0 => snoc_rect (fun l' => P (a :: l'))

               (Psnoc nil a Pnil)

               (fun l' x X => Psnoc (a :: l') x X)

               l0

end.

Lemma snoc_rect_base : forall (A:Type) (P:list A->Type) Pnil Psnoc,

  snoc_rect P Pnil Psnoc nil = Pnil.

Proof.

reflexivity.

Qed.

Lemma snoc_rect_step : forall (A:Type) (P:list A->Type)

  Pnil Psnoc x l, snoc_rect P Pnil Psnoc (snoc l x) =

                  Psnoc l x (snoc_rect P Pnil Psnoc l).

Proof.

intros. revert P Pnil Psnoc x. induction l.

+ reflexivity.

+ simpl. intros. apply IHl with (P := fun l' => P (a :: l')).

Qed.

-- 

Daniel Schepler