Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Snoc list recursion principle

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Snoc list recursion principle


Chronological Thread 
  • From: Daniel Schepler <dschepler AT gmail.com>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Snoc list recursion principle
  • Date: Tue, 16 Jun 2015 09:58:49 -0700

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



Archive powered by MHonArc 2.6.18.

Top of Page