The Coq mailing list

[Amin Timany <amintimany AT gmail.com>]

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.