The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hi, would this help?

Pierre

-----

Require Import List.

Section rev.

  Variable A:Type.

Function rev' (l : list A) : list A :=

  match l with

  | nil => nil

  | x :: l' => rev' l' ++ x :: nil

  end.

Check rev'_rect.

Check rev'_equation.

2015-06-15 15:25 GMT+02:00 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