The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi,
  just an idea, many of those proofs are probably already part of the HoTT/Coq library (formulated with different constant names though).

-- Matthieu

On Wed, Jun 17, 2015 at 5:13 PM Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr> wrote:

Dear Amin,

I did finish the proof of equality of two identity proofs *without*
using any axiom. I had to generate a lemma about the commutativity
of eq_rect with exist, and another for the composition of eq_rect
with itself (the proof of those lemmas are trivial but finding
them isn't ...)

So here is the completed proof of the list_rev_rect recursion
operator with its two fixpoint equations.

-----------------------------------------------------------------

Require Import Arith.       (* for lt_wf *)
Require Import List.
Require Import Wf.
Require Import Wellfounded.

Set Implicit Arguments.

Section f_eq2. (* f_equal2 is forever Opaque because of Qed, this is not
the case for f_equal *)

   Variable (X Y Z K : Type) (op : X -> Y -> Z).

   Definition f_eq2 (x1 x2 : X) (y1 y2 : Y) (Ex : x1 = x2) (Ey : y1 =
y2) : op x1 y1 = op x2 y2.
   Proof. subst; reflexivity. Defined.

   Fact f_eq2_refl_left (x : X) (y1 y2 : Y) (Ey : y1 = y2) : f_eq2
eq_refl Ey = f_equal (op x) Ey.
   Proof. subst; reflexivity. Qed.

   Fact f_eq2_refl_right (x1 x2 : X) (y : Y) (Ex : x1 = x2) : f_eq2 Ex
eq_refl = f_equal (fun x => op x y) Ex.
   Proof. subst; reflexivity. Qed.

End f_eq2.

Section exist_fun. (* exist and existT are functional *)

   Variables (X : Type) (P : X -> Type) (Q : X -> Prop).

   Implicit Types x y : X.

   Fact existT_fun x y (H : x = y) tx ty : eq_rect x P tx y H = ty ->
existT P x tx = existT P y ty.
   Proof.
     subst; simpl; intros; subst; reflexivity.
   Qed.

   Fact exist_fun x y (H : x = y) tx ty : eq_rect x Q tx y H = ty ->
exist Q x tx = exist Q y ty.
   Proof.
     subst; simpl; intros; subst; reflexivity.
   Qed.

End exist_fun.

Section eq_utils.

   Variables (X Y Z K : Type) (R : Z -> K -> Type) (op : X -> Y -> Z).

   Implicit Types (x : X) (y : Y).

   (* substitution of an identity with itself equals eq_refl *)

   Fact eq_rect_eq_simpl x1 x2 (H : x1 = x2) : eq_rect _ (fun z => z =
x2) H _ H = eq_refl.
   Proof.
     subst; reflexivity.
   Qed.

   (* eq_rect composed with another eq_rect *)

   Section eq_rect_rect.

     Variables (x1 x2 : X) (y1 y2 : Y) (k : K) (Ex : x1 = x2) (Ey : y1 =
y2) (H : R (op x1 y1) k).

     Fact eq_rect_rect : eq_rect x1 (fun a => R (op a y2) k) (eq_rect y1
(fun a => R (op x1 a) k) H _ Ey) _ Ex
                       = eq_rect (op x1 y1) (fun a => R a k) H _ (f_eq2
op Ex Ey).
     Proof.
       subst; reflexivity.
     Qed.

   End eq_rect_rect.

   (* eq_rect commutes with exist in some particular case *)

   Section eq_rect_exist.

     Variables (Q : X -> X -> Y -> Prop).

     Variable (x1 x2 : X) (y : Y) (Hx : x1 = x2) (HQ : Q x1 x2 y).

     Fact eq_rect_exist_comm : eq_rect _ (fun u => { y' | Q u x2 y' })
(exist _ y HQ) _ Hx
                             = exist _ y (eq_rect _ (fun u => Q u x2 y)
HQ _ Hx).
     Proof.
       subst; reflexivity.
     Qed.

   End eq_rect_exist.

End eq_utils.

Notation "l '\\' x" := (l++x::nil) (at level 59, left associativity).
Notation snoc := (fun l x => l\\x).

Section list_utils.

   Variable X : Type.

   Fact snoc_length l (x : X) : length (l\\x) = S (length l).
   Proof.
     rewrite app_length, plus_comm; auto.
   Qed.

   Fixpoint last (x : X) l :=
     match l with
       | nil  => x
       | y::l => last y l
     end.

   Fixpoint beg (x : X) l :=
     match l with
       | nil  => nil
       | y::l => x::beg y l
     end.

   (* proofs by induction are possible but fixpoints simplify much better
      when computing with proofs

      it is VERY IMPORTANT to control precisely your proof terms so that
      you are actually able to show properties of this proof terms ...

      and of course, you cannot use Opaque lemmas to prove those ...
   *)

   Fixpoint last_snoc x l y { struct l } : last x (l\\y) = y.
   Proof.
     destruct l as [ | a l ]; simpl.
     reflexivity.
     apply last_snoc.
   Defined.

   Fixpoint beg_snoc x l y { struct l } : beg x (l\\y) = x::l.
   Proof.
     destruct l as [ | a l ]; simpl.
     reflexivity.
     apply f_equal, beg_snoc.
   Defined.

   Fixpoint beg_last_snoc x l { struct l } : beg x l \\ last x l = x::l.
   Proof.
     destruct l as [ | a l ]; simpl.
     reflexivity.
     apply f_equal, beg_last_snoc.
   Defined.

   Definition comp_snoc (x : X) l : { y : _ & { l' | l'\\y = x::l } }.
   Proof.
     exists (last x l), (beg x l).
     apply beg_last_snoc.
   Defined.

   Section comp_snoc_refl.

     Implicit Type x : X.

     Let cons_snoc_comm x l1 l2 y1 y2 (Hl : l1 = l2) (Hy : y1 = y2) :
            f_equal (cons x) (f_eq2 snoc Hl Hy) = f_eq2 snoc (f_equal
(cons x) Hl) Hy.
     Proof.
       subst; reflexivity.
     Qed.

     Let beg_last_snoc_prop x l y : beg_last_snoc x (l \\ y) = f_eq2
snoc (beg_snoc x l y) (last_snoc x l y).
     Proof.
       revert x.
       induction l as [ | a l IH ]; intros x; auto.
       change ((a::l)\\y) with (a::l\\y).
       specialize (IH a).
       simpl; rewrite IH.
       apply (cons_snoc_comm x (beg_snoc a l y) (last_snoc a l y)).
     Qed.

     Fact comp_snoc_refl l y x : comp_snoc y (l\\x) = existT _ x (exist
_ (y :: l) eq_refl).
     Proof.
       unfold comp_snoc.
       apply existT_fun             with (H := last_snoc y l x).
       rewrite eq_rect_exist_comm   with (Q := fun z a m => m\\z =
y::l\\a).
       apply exist_fun              with (H := beg_snoc y l x).
       rewrite eq_rect_rect         with (op := snoc).
       rewrite <- beg_last_snoc_prop.
       apply eq_rect_eq_simpl.
     Qed.

   End comp_snoc_refl.

End list_utils.

(* 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).

   Let snoc_rel (l m : list X) := exists x, m = l\\x.

   Let wf_snoc_rel : well_founded snoc_rel.
   Proof.
     apply wf_incl with (R2 := fun m l => length m < length l).
     intros m l (x & H); subst; rewrite snoc_length; auto.
     apply wf_inverse_image, lt_wf.
   Qed.

   Let snoc_dec (ll : list X) : (ll = nil) + { x : _ & { l | l\\x = ll } }.
   Proof.
     destruct ll as [ | x l ].
     left; reflexivity.
     right; apply comp_snoc.
   Defined.

   Let snoc_dec_refl (x : X) l : snoc_dec (l\\x) = inr (existT _ x
(exist _ l eq_refl)).
   Proof.
     unfold snoc_dec.
     destruct l as [ | y l ];
     simpl; auto.
     rewrite comp_snoc_refl.
     reflexivity.
   Qed.

   Let F l (f : forall m, snoc_rel m l -> P m) : P l.
   Proof.
     destruct (snoc_dec l) as [ H | (x & m & H) ]; subst.
     apply Pnil.
     apply Psnoc, f.
     exists x; auto.
   Defined.

   Definition list_rev_rect := Fix wf_snoc_rel _ F.

   Fact list_rev_rect_fix l : list_rev_rect l = F (fun m _ =>
list_rev_rect m).
   Proof.
     unfold list_rev_rect at 1.
     rewrite Fix_eq; auto.
     clear l.
     intros l f g H; unfold F.
     destruct (snoc_dec l) as [ | (x & m & H')]; subst;
       unfold eq_rect_r; simpl; f_equal; auto.
   Qed.

   Fact list_rev_rect_nil : list_rev_rect nil = Pnil.
   Proof.
     rewrite list_rev_rect_fix; reflexivity.
   Qed.

   Fact list_rev_rect_snoc l x : list_rev_rect (l\\x) = Psnoc x
(list_rev_rect l).
   Proof.
     rewrite list_rev_rect_fix; unfold F.
     rewrite snoc_dec_refl; reflexivity.
   Qed.

End list_rev_rect.

Print list_rev_rect.
Print Assumptions list_rev_rect_snoc.