The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

I forgot, you might also consider the following code:
=====================================================
Parameter A:Set.
Require Import Bool.

Record ilist_ {S : Set} : Set :=
  { head : A
  ; tail : S
  }.

Fixpoint ilist (n : nat) : Set :=
  match n with
  | O => unit
  | S n => @ilist_ (ilist n)
  end.

Lemma ilist_0 : forall(l : ilist 0), l = tt.
Proof. intros []; split. Qed.

Lemma ilist_S : forall (n : nat) (l : ilist (S n)),
    exists (a : A) (tl : ilist n), l = {| head := a; tail := tl |}.
Proof. intros n [a tl]; exists a; exists tl; split. Qed.

Definition ilist_eq (a_eq : A -> A -> bool)
: forall n1 n2, ilist n1 -> ilist n2 -> bool :=
  fix ilist_eq n1 n2 :=
  match n1, n2 with
  | O, O => fun _ _ => true
  | S n1, S n2 => fun (l1 : ilist (S n1))
                      (l2 : ilist (S n2)) =>
                      a_eq (head l1) (head l2) &&
                      ilist_eq n1 n2 (tail l1) (tail l2)
  | _, _ => fun _ _ => false
  end.

Lemma ilist_eq_correct :
  forall(a_eq : A -> A -> bool)(n : nat)(l1 : ilist n)(l2 : ilist n),
    (forall(a1 a2 : A), a_eq a1 a2 = true <-> a1 = a2) ->
      (ilist_eq a_eq n n l1 l2 = true <-> l1 = l2).
Proof.
  intros a_eq n l1 l2 H; induction n as [|n IHn]; simpl.
    destruct l1; destruct l2; split; split.
  generalize (H (head l1) (head l2)).
  generalize (IHn (tail l1) (tail l2)).
  clear.
  intros [L1 L2].
  intros [A1 A2].
  split.
    clear A2 L2.
    destruct (a_eq (head l1) (head l2)); simpl.
      intros H; generalize (L1 H); generalize (A1 (eq_refl true));
clear. destruct l1 as [h1 t1]; simpl; intros; subst.
      destruct l2 as [h2 t2]; simpl.
      split.
    clear; intros H; exfalso.
    change (match false with false => False | true => True end).
    rewrite H; clear.
    split.
  clear A1 L1; intros; subst.
  rewrite (A2 (eq_refl (head l2))); clear A2; simpl.
  apply L2.
  split.
Qed.
==================================================================
Here, ilist is not the one you used, but an isomorphic one, in which
pattern matching is easier. The final proof is long only because I show
how to proceed step by step. I can produce shorter scripts.

Le Wed, 17 Oct 2012 15:09:06 +0200,
Hendrik Tews 
<tews AT os.inf.tu-dresden.de>
 a écrit :

> Hi,
> 
> I am working with length-indexed lists, as they are described in
> CPDT:
> 
>   Variable A : Set.
> 
>   Inductive ilist : nat -> Set :=
>     | Nil : ilist 0
>     | Cons : forall n, A -> ilist n -> ilist (S n).
> 
> I have a proof where I cannot destruct some ilist, therefore I
> tried to prove the following two obvious facts:
> 
>   Lemma ilist_0 : forall(l : ilist 0), l = Nil.
> 
>   Lemma ilist_S : forall(n : nat)(l : ilist (S n)),
>     exists(a : A)(tl : ilist n), l = Cons n a tl.
> 
> However, I can only prove these by using UIP_refl, ie. uniqueness
> of reflexive identity proofs (full sources attached below).
> 
> Could somebody give me a hint on how to prove these lemmas
> without using axioms?
> 
> I need this for the correctness prove of an decidable equality
> predicate on ilists:
> 
>   Fixpoint ilist_eq(a_eq : A -> A -> bool)
>                    (n1 n2 : nat)(l1 : ilist n1)(l2 : ilist n2) :
> bool := match (l1, l2) with
>       | (Nil, Nil) => true
>       | (Cons n1 a1 l1, Cons n2 a2 l2) => 
>          a_eq a1 a2 && ilist_eq a_eq n1 n2 l1 l2
>       | _ => false
>     end.
> 
>   Lemma ilist_eq_correct :
>     forall(a_eq : A -> A -> bool)(n : nat)(l1 : ilist n)(l2 : ilist
> n), (forall(a1 a2 : A), a_eq a1 a2 = true <-> a1 = a2) ->
>         (ilist_eq a_eq n n l1 l2 = true <-> l1 = l2).
> 
> If there are no axiom-free proofs for the two lemmas above, I
> would appreciate any hints on how to prove ilist_eq_correct
> without axioms.
> 
> Bye,
> 
> Hendrik
>