The Coq mailing list

[Hendrik Tews <tews AT os.inf.tu-dresden.de>]

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

Attachment: ilist.v
Description: Binary data