The Coq mailing list

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

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).

If you are not very familiar with dependant type, try rather:

Inductive ilist (n : nat) : Set :=
 | Nil : n = 0 -> ilist n
 | Cons : forall m, n = S m -> A -> ilist m -> ilist n.

Things can become a lot easier.

> 
> 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 will tell you how to do for ilist_0, ilist_S will then be an easy
task.

Lemma ilist_0 : forall(l : ilist 0), l = Nil.
exact (fun l => match l with Nil => eq_refl _ | _ => I end).
Qed.

I am pretty sure you didn't understood how it works.
I learned rather recently (I posted a mail on it on the list) that Coq
has become more clever than it was and does not require annotations it
used to need anymore.

The first thing to do is to be able to prove:

Lemma ilist_0_ : forall n (l : ilist n),
  match n as n0 return list n0 -> Prop with
  | O => fun l => l = Nil
  | S m => fun l => True
  end.

To prove that, "destruct l" gives two cases, one with l=Nil and thus
n=0, leading to have to prove "(fun l => l = Nil) Nil", and one with
l=Cons a m, leading to have to prove "(fun l => True) (Cons a m)".
None of them is hard.

Then your ilist_0 is simply (ilist_0_ O).

You can even try to prove:

Lemma ilist_ : forall n (l : ilist n),
  match n as n0 return list n0 -> Prop with
  | O => fun l => l = Nil
  | S m => fun l => exists a tl, l = Cons a tl
  end.

Which will make you prove easily "ilist_0" and "ilist_S".

Now for my first answer, when you write:

fun l => match l with Nil => eq_refl _ | _ => I end,

Coq infers:

fun (l : ilist O) => match l as l0 in ilist n
                     return match n with O => l0 = Nil
                                       | S m => True
                                       end
                     with Nil => @eq_refl (ilist 0) Nil
                        | Cons _ _ => I
                        end.

> 
> 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.

So forget my first recommendation for that purpose (although with my
proposed alternative, as equality on nat is decidable your goal will
still be provable, but it won't be as easy if you want to understand
each part of the proof).

> 
> Bye,
> 
> Hendrik
>