coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club]Equality problem.

From: "Adam Koprowski" <adam.koprowski AT gmail.com>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club]Equality problem.
Date: Mon, 10 Apr 2006 15:03:32 +0200
Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=beta; d=gmail.com; h=received:message-id:date:from:to:subject:mime-version:content-type; b=rNDhTYep/sdt4mso7sBwyFg9zqmjiFI0gsoLl8NI3oEH4pGZzlXHGg5ByIZAajZyaS+vqEyr8wJnN5D+JyJOW3oypGNSFh4J0ZlGd/Yug3eUSILcrXfbacERHK/wng/OQ8jeqJ9scyp1zxpy5SuuSlnsHsyKBIgf7n3LeMDefME=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hello everybody,

During my work in Coq I encountered something that looks rather as an elementary problem but I got stucked on it nevertheless. Here is the relevant snippet:

Variable A: Set.
Inductive Test: Set :=
| Elem: A -> Test
| Pair: Test -> Test -> Test.

Fact discr: forall a b, ~a = Pair a b.
Proof. ?

How can one prove discr? I tried all varations of discriminate, injection etc. I could think of. Or is this equality not valid intuitionistically? Any indications why? Any help appreciated!

Adam Koprowski

--
=====================================================
Adam.Koprowski AT gmail.com, ICQ: 3204612
http://www.win.tue.nl/~akoprows
The difference between impossible and possible
lies in determination (Tommy Lasorda)
=====================================================

[Coq-Club]Equality problem., Adam Koprowski
- Re: [Coq-Club]Equality problem., roconnor
- Re: [Coq-Club]Equality problem., Xavier Leroy
- Re: [Coq-Club]Equality problem., Andrew McCreight
- Re: [Coq-Club]Equality problem., Jean-Marc Notin
- Re: [Coq-Club]Equality problem., Conor McBride