The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Thanks a lot. Since it is that "short", I suppose it could be included into the Standard Library without

problem. Because there is only rev_ind which is snoc_rect limited to (P : X -> Prop) and without

fixpoint equations.

Dominique

---

De: "Daniel Schepler" <dschepler AT gmail.com>
À: "Coq Club" <coq-club AT inria.fr>
Envoyé: Mardi 16 Juin 2015 18:58:49
Objet: Re: [Coq-Club] Snoc list recursion principle

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