coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Different eliminations of existentials

From: Taral <taralx AT gmail.com>
To: Luke Palmer <lrpalmer AT gmail.com>
Cc: coq-club <coq-club AT pauillac.inria.fr>
Subject: Re: [Coq-Club] Different eliminations of existentials
Date: Sat, 24 Jan 2009 11:12:43 -0800
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type:content-transfer-encoding; b=VSNI1bQtPP5TKCECjd2z41CBpqz2VE4ra1pB9+p458Na8wf1mskwR5jQAb8AqaGhC9 nblMxSNKIN0HbQaeSzujGPpqRJB+5C3NrFR1dWVW0IkNj5N5y2nH4K8GpIYZlOhSUXNV tHJ9ybBXNjLdCyEQYgcHuVsvhKRfKdDWd0kOU=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On Sat, Jan 24, 2009 at 6:48 AM, Luke Palmer
<lrpalmer AT gmail.com>
wrote:
> 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 :-)

I'm almost certain the answer is no, and it has something to do with
(a) the fact that the injection tactic doesn't work on propositional
inductive types and (b) you can't eliminate from Prop (eq) to Set
(nat).

I *can* prove that ex_intro (fun x : nat => even x) x XH = ex_intro
(fun x : nat => even x) y YH.

--
Taral
<taralx AT gmail.com>
"Please let me know if there's any further trouble I can give you."
-- Unknown

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