coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Adam Chlipala <adamc AT csail.mit.edu>
- To: Hendrik Tews <tews AT os.inf.tu-dresden.de>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] prove forall(l : ilist 0), l = Nil ?
- Date: Wed, 17 Oct 2012 09:48:24 -0400
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.
- [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.