coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Snoc list recursion principle, Dominique Larchey-Wendling, 06/16/2015
- Re: [Coq-Club] Snoc list recursion principle, Amin Timany, 06/16/2015
- Re: [Coq-Club] Snoc list recursion principle, Dominique Larchey-Wendling, 06/16/2015
- Re: [Coq-Club] Snoc list recursion principle, Dominique Larchey-Wendling, 06/17/2015
- Re: [Coq-Club] Snoc list recursion principle, Matthieu Sozeau, 06/17/2015
- Re: [Coq-Club] Snoc list recursion principle, Dominique Larchey-Wendling, 06/17/2015
- Re: [Coq-Club] Snoc list recursion principle, Dominique Larchey-Wendling, 06/16/2015
- Re: [Coq-Club] Snoc list recursion principle, Daniel Schepler, 06/16/2015
- Re: [Coq-Club] Snoc list recursion principle, Dominique Larchey-Wendling, 06/16/2015
- Re: [Coq-Club] Snoc list recursion principle, Amin Timany, 06/16/2015
Archive powered by MHonArc 2.6.18.