The Coq mailing list

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

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