The Coq mailing list

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

Dear Amin,

Thank you for your hint. I did indeed notice that comp_snoc_refl could
be proved using UIP (or Streicher_K) of which JMeq_eq is a consequence.
But I think it is possible to prove it without using an axiom ... though
it is very cumbersome: you have to commute eq_rect with constructors
and as already said, unification is of no help here. 
I will post the proof if I manage to finish it. 

Dear Daniel,

I am impressed by your *very elegant* solution which involves shifting
the predicate. This completely avoids having to prove properties on
identity types. In some way, it makes me think of the dependently
typed implementation of pure lambda calculus.
Thank your very much for your input, it is perfect.

Dominique

----- Mail original -----
> De: "Amin Timany" 
> <amintimany AT gmail.com>
> À: 
> coq-club AT inria.fr
> Envoyé: Mardi 16 Juin 2015 17:49:30
> Objet: Re: [Coq-Club] Snoc list recursion principle
> 
> Hi,
> 
> I din’t try to prove comp_snoc_refl below but I guess it is not directly
> provable in Coq (requires some axioms). As you mentioned working with proofs
> of equalities is usually very cumbersome. Here is my attempt at defining
> list_rev_rect, list_rev_rect_nil and list_rev_rect_snoc:
> 
> Require Import Coq.Lists.List.
> Require Import Coq.Logic.JMeq.
> 
> 
> 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 *)
> 
> Definition rev_lem : forall {A : Type} (l : list A) (a : A), rev (l ++ a ::
> nil) = a :: (rev l).
> Proof.
>   induction l.
>   reflexivity.
>   intros a'.
>   cbn.
>   rewrite IHl.
>   trivial.
> Defined.
> 
> 
> Definition RI : forall {A : Type} (l : list A), rev (rev l) = l.
> Proof.
>   induction l.
>   reflexivity.
>   cbn.
>   rewrite rev_lem.
>   rewrite IHl.
>   trivial.
> Defined.
> 
> Definition RI_snoc : forall {A : Type} (l : list A) (x : A) (H : rev (rev l)
> = l), rev (rev (l\\x)) = (l\\x).
> Proof.
>   intros A l x H.
>   unfold snoc.
>   rewrite rev_lem.
>   cbn.
>   rewrite H.
>   trivial.
> Defined.
>   
> 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.
>  Proof.
>    intros l.
>    rewrite <- RI.
>    induction (rev l) as [|h rl].
>    assumption.
>    cbn.
>    apply Psnoc.
>    trivial.
> Defined.
> 
>  Fact list_rev_rect_nil : list_rev_rect nil = Pnil.
>  Proof.
>    trivial.
>  Qed.
> 
>  Fact list_rev_rect_snoc l x :
>       list_rev_rect (l\\x) = Psnoc _ x (list_rev_rect l).
>  Proof.
>    unfold list_rev_rect.
>    unfold list_rect, eq_rect.
>    apply JMeq_eq.
>    destruct (RI l).
>    destruct (RI (rev (rev l) \\ x)).
>    etransitivity.
>    {
>      rewrite (RI l).
>      unfold snoc.
>      rewrite rev_lem.
>      trivial.
>    }
>    trivial.
>  Qed.
> 
> End list_rev_rect.
> 
> I didn’t spent much time on it. list_rev_rect is defined by a proof and can
> be simplified by hand. Note that I have here used JMeq_eq which is an axiom.
> 
> Regards,
> Amin
> 
> 
> > On 16 Jun 2015, at 14:54, Dominique Larchey-Wendling
> > <dominique.larchey-wendling AT loria.fr>
> >  wrote:
> > 
> > Dear Pierre,
> > 
> > Thanks for your hint. However I did try to apply the list_rect
> > recursion principle on the reverse list (rev l) but I get the
> > same problems as the one that occur in the following code.
> > Mainly, the problem is concentrated in the proof of
> > 
> >  comp_snoc_refl l y x : comp_snoc y (l\\x)
> >                       = existT _ x (exist _ (y :: l) eq_refl)
> > 
> > which states that 2 identity proofs are identical ... if
> > you destruct the list l several times, "auto" succeeds on the "nil"
> > case each time and leave the "cons" case open.
> > 
> > Thus I think this goal is provable by induction on l but
> > managing proofs of equality of identity proofs is horribly
> > painful. In particular, the unification algorithm of Coq
> > fails most of the time so you have to enter terms by
> > hand ...
> > 
> > Thank you anyway for your hint but to me, it does not seem
> > to solve the problem I am interested in, which is obtaining
> > the 3 following results :
> > 
> >  list_rev_rect, list_rev_rect_nil and list_rev_rect_cons
> > 
> > Best regards,
> > 
> > Dominique Larchey-Wendling
> > 
> > ---------------------------------
> > 
> > Require Import Arith.
> > Require Import List.
> > Require Import Wf.
> > Require Import Wellfounded.
> > 
> > Set Implicit Arguments.
> > 
> > Notation "l '\\' x" := (l++x::nil) (at level 59, left associativity).
> > 
> > Section list_utils.
> > 
> >  Variable X : Type.
> > 
> >  Fact app_assoc (l m k : list X) : (l++m)++k = l++(m++k).
> >  Proof.
> >    induction l as [ | x l ]; simpl.
> >    reflexivity.
> >    rewrite IHl; reflexivity.
> >  Defined.
> > 
> >  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.
> > 
> >  Fact last_snoc x l y: last x (l\\y) = y.
> >  Proof.
> >    revert x; induction l; intros; simpl; auto.
> >  Defined.
> > 
> >  Fixpoint beg (x : X) l :=
> >    match l with
> >      | nil  => nil
> >      | y::l => x::beg y l
> >    end.
> > 
> >  Fact beg_snoc x l y : beg x (l\\y) = x::l.
> >  Proof.
> >    revert x; induction l as [ | a ? IH ]; intros; simpl; auto.
> >    rewrite (IH a); reflexivity.
> >  Defined.
> > 
> >  Fact beg_last_snoc x l : (beg x l)\\(last x l) = x::l.
> >  Proof.
> >    revert x; induction l as [ | y ? IH ]; intros x; simpl.
> >    reflexivity.
> >    specialize (IH y).
> >    rewrite <- IH.
> >    apply (app_assoc (x::nil)).
> >  Defined.
> > 
> >  Fact snoc_inj_beg l l' (x x' : X) : l\\x = l'\\x' -> l = l'.
> >  Proof.
> >    intros H.
> >    generalize (beg_snoc x l x) (beg_snoc x l' x').
> >    rewrite H; clear H; intros H; rewrite H.
> >    injection 1; auto.
> >  Defined.
> > 
> >  Fact snoc_inj_last l l' (x x' : X) : l\\x = l'\\x' -> x = x'.
> >  Proof.
> >    intros H.
> >    rewrite <- (last_snoc x l x), <- (last_snoc x l' x').
> >    f_equal; assumption.
> >  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.
> > 
> >  Fact comp_snoc_refl l y x : comp_snoc y (l\\x) = existT _ x (exist _ (y 
> > ::
> >  l) eq_refl).
> >  Proof.
> >    unfold comp_snoc.
> > 
> >    (* It is difficult to prove that equation but the following
> >       tactic succeed i.e. it leaves only one goal *)
> > 
> >    do 10 (destruct l as [ | ? l ]; auto).
> > 
> >    (* hence an inductive proof on l should be feasible but I get stuck
> >       with unmanageable equations between equality proofs *)
> > 
> >  Admitted.
> > 
> >  Definition 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.
> > 
> > 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.
> >    intros l.
> >    induction l as [ | x l IH ] using rev_ind.
> >    constructor.
> >    intros [] (? & H); discriminate H.
> >    constructor.
> >    intros m (y & Hm).
> >    apply snoc_inj_beg in Hm.
> >    subst; assumption.
> >  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; unfold F.
> >    auto.
> >  Qed.
> > 
> >  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.
> >    f_equal.
> >    apply comp_snoc_refl.
> >  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; auto.
> >  Qed.
> > 
> > End list_rev_rect.
> > 
> > Print Assumptions list_rev_rect_snoc.
> 
>