coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] prove forall(l : ilist 0), l = Nil ?
- Date: Wed, 17 Oct 2012 15:19:55 +0200
Using Case0 and CaseS in
http://coq.inria.fr/distrib/V8.4/stdlib/Coq.Vectors.VectorDef.html
are answers to your problem.
I'm sure it is tackled by CPDT (maybe later in the book).
Pierre B.
On 17/10/2012 15:09, Hendrik Tews wrote:
> 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
>
- [Coq-Club] prove forall(l : ilist 0), l = Nil ?, Hendrik Tews, 10/17/2012
- Re: [Coq-Club] prove forall(l : ilist 0), l = Nil ?, Pierre Boutillier, 10/17/2012
- Re: [Coq-Club] prove forall(l : ilist 0), l = Nil ?, Adam Chlipala, 10/17/2012
- Re: [Coq-Club] prove forall(l : ilist 0), l = Nil ?, AUGER Cédric, 10/17/2012
- Re: [Coq-Club] prove forall(l : ilist 0), l = Nil ?, AUGER Cédric, 10/17/2012
Archive powered by MHonArc 2.6.18.