The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 10/17/2012 09:09 AM, Hendrik Tews wrote:
> 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).
>    

The "Universes and Axioms" chapter of CPDT covers axiom-avoidance 
techniques that make short work of this problem.  Most likely I don't 
give precisely your example in CPDT, though.

Here's one theorem equivalent to your two.  I'll leave it up to the 
"Universes and Axioms" discussion to elaborate on the techniques used here.

  Theorem ilist_eta : forall n (ls : ilist n),
    match n return ilist n -> Prop with
      | O => fun ls => ls = Nil
      | S _ => fun ls => exists x ls', ls = Cons _ x ls'
    end ls.
    destruct ls; eauto.
  Qed.