coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club]Problems proving equality of proof terms of inductively defined predicate.

chronological Thread

From: "Roland Zumkeller" <Roland.Zumkeller AT polytechnique.fr>
To: eelis AT eelis.net
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club]Problems proving equality of proof terms of inductively defined predicate.
Date: Thu, 8 Jun 2006 18:11:21 +0200
Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=beta; d=gmail.com; h=received:message-id:date:from:sender:to:subject:cc:in-reply-to:mime-version:content-type:content-transfer-encoding:content-disposition:references:x-google-sender-auth; b=GsIWqbP+c48u4NbCfXk7B8BI2ETn5+FnomnYAb5PNu4RZ76Miri/ltnc2ERALJTvAXZHI+LSIjECshlnYoBkWOIQC0sJ+rnSLtAChmJlNC+vbJRy+1vtkyN9y73HgdPx9omnAQEWoRnHVUAmF/fhUOGpUW26PsbsvbRTyBsOFMM=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On 04/06/06, Eelis van der Weegen
<eelis AT eelis.net>
wrote:

Is the following provable? If it is, how? If it isn't, why not? :

Inductive P : nat -> Prop := C0 : P 0 | C1 : P 1.

This is almost the same problem that Fabrice encountered yesterday, so
I can copy my code:

Theorem A: forall (x: P 0), x = C0.

intros; refine(
match x as x0 return forall H, eq_rect _ P x0 _ H = C0 with
| C0 => _
| C1 => _
end (refl_equal _)).
Require Import Eqdep_dec.
intros; pattern H; apply K_dec_set.
decide equality.
apply refl_equal.
intros; discriminate.
Qed.

Best,

Roland

--
http://www.lix.polytechnique.fr/~zumkeller/

[Coq-Club]Problems proving equality of proof terms of inductively defined predicate., Eelis van der Weegen
- Re: [Coq-Club]Problems proving equality of proof terms of inductively defined predicate., Roland Zumkeller
- Re: [Coq-Club]Problems proving equality of proof terms of inductively defined predicate., David Nowak