coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Snoc list recursion principle
- Date: Mon, 15 Jun 2015 15:25:40 +0200
- Organization: LORIA
Dear all, and especially experts in dependent types / computations with identity proofs.
I am trying to write a snoc list (aka reverse list) recursion
principle *with its associated fixpoint equations*.
There is a snoc list induction principle in the standard library
(check rev_ind in List.v) but there are no associated fixpoint
equations (because it is an induction principle in Prop).
I would like to obtain something like:
(*************************************************************)
Definition snoc X l (x:X) := l++x::nil.
Notation "l '\\' x" := (snoc l x) (at level 59, left associativity).
(* dependently typed snoc recursion principle *)
Section list_rev_rect.
Variable (X : Type) (P : list X -> Type).
Variable Pnil : P nil.
Variable Psnoc : forall l x, P l -> P (l\\x).
Definition list_rev_rect : forall l, P l.
Admitted.
Fact list_rev_rect_nil : list_rev_rect nil = Pnil.
Admitted.
Fact list_rev_rect_snoc l x :
list_rev_rect (l\\x) = Psnoc x (list_rev_rect l).
Admitted.
End list_rev_rect.
(*************************************************************)
I have some code developed towards this end. Mainly you have
to make identity proofs transparent and carefully compute
equations between identity proofs but I get stuck at some
point with too complicated equations.
May be there is some easy solution that I am unaware of. I could
post my partial developments for this problem if my question
turns out to be non trivial.
Thank you very much in advance,
Dominique Larchey-Wendling
- [Coq-Club] Snoc list recursion principle, Dominique Larchey-Wendling, 06/15/2015
- Re: [Coq-Club] Snoc list recursion principle, Pierre Courtieu, 06/15/2015
Archive powered by MHonArc 2.6.18.