coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Different eliminations of existentials

From: Luke Palmer <lrpalmer AT gmail.com>
To: coq-club <coq-club AT pauillac.inria.fr>
Subject: [Coq-Club] Different eliminations of existentials
Date: Sat, 24 Jan 2009 07:48:13 -0700
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:date:message-id:subject:from:to:content-type; b=ixt2ErXqSN4r5jj38/HG628B+xpTUAIi8GAG+uX8ZdS4XKB8z4R/dgreJ02WElsSyH rDIKn8mJ/eElR0Z5uEZkOnqAQzpD6FX97KEh9iZy8AtblEJ//EXG07afrOB/CpfK7mzS GXpuB08YuZoffkX6EltbrHe3gT/PJZ4coyjHk=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

I'm working on a core theory for a programming language, and I'm wondering if existentials are a good way to encode "differentness" of types.

So formally, my question is this. Let's say I have:

Goal (exists x, even x) -> True.
intro.
elim H ; intros x XH.
elim H ; intros y YH.

At this point, the proof state is:

H : exists x : nat, even x
x : nat
XH : even x
y : nat
YH : even y
______________________________________(1/1)
False

Is it possible, from here or in another capacity, to prove that x = y? Shouldn't it follow from the fact that an existential has to have a witness? Remember, the answer I want is "no", so come up with a "yes" or "maybe" in any way possible :-)

Thanks!
Luke

[Coq-Club] Different eliminations of existentials, Luke Palmer
- Re: [Coq-Club] Different eliminations of existentials, Taral