The Coq mailing list

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

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.