Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Snoc list recursion principle


Chronological Thread 
  • 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



Archive powered by MHonArc 2.6.18.

Top of Page