coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jean-Francois Monin <jean-francois.monin AT imag.fr>
- To: Georgi Guninski <guninski AT guninski.com>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Problem using Lemma as a coercion
- Date: Mon, 13 Jun 2011 12:29:11 +0200
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=sender:date:from:to:cc:subject:message-id:references:mime-version :content-type:content-disposition:in-reply-to:user-agent; b=kreWmbWbado5OMqhM2/4lMRtyFW7GS6f1NRA6w2Prz7Wc57hJk18JddaifnpStBtPw 4MAR7yLlECe3cDQIY3bZRnGKsBIU9MvFFwDQO09vV2axubn9ml5BOAbFJbYnLkE6kZMT mPAESNC9yX5SdAl182c0ts5qCNZLw98V5nneE=
On Mon, Jun 13, 2011 at 10:26:05AM +0300, Georgi Guninski wrote:
> is the following code cheating?
>
> Lemma coer: True->Prop.
> intro. exact False.
> Defined.
>
> (*vvv provably correct per [Defined] *)
> Coercion coer: True >-> Sortclass.
>
> Lemma true_false: forall a : True, a ->False.
> intro. compute. intro. contradiction.
> Qed.
You can make it even simpler:
Lemma true_false: forall a : True, a ->False.
intros; assumption.
Qed.
Or even:
Lemma true_false: forall a : True, a ->False.
trivial.
Qed.
So what?
There is no problem unless you can prove:
Lemma pb: False.
Here you just prove False in a non-empty environment (which happens to
contain a hypothesis of type False). This kind of situation --
non-empty inconsistent environment -- is very common in real proofs,
and of course is harmless.
JF
--
Jean-Francois Monin
LIAMA Project FORMES, CNRS & Universite de Grenoble 1
Office 3-605, FIT, Tsinghua University
Haidian District, Beijing 100084, CHINA
Tel: +86 10 62 79 69 79 ext 605
Fax@LIAMA:
+86 10 6264 7458
- [Coq-Club] Problem using Lemma as a coercion, Georgi Guninski
- Re: [Coq-Club] Problem using Lemma as a coercion,
Adam Chlipala
- Re: [Coq-Club] Problem using Lemma as a coercion,
Georgi Guninski
- Re: [Coq-Club] Problem using Lemma as a coercion,
Adam Chlipala
- Re: [Coq-Club] Problem using Lemma as a coercion,
Randy Pollack
- Re: [Coq-Club] Problem using Lemma as a coercion, Adam Chlipala
- Re: [Coq-Club] Problem using Lemma as a coercion, Georgi Guninski
- Re: [Coq-Club] Problem using Lemma as a coercion,
Georgi Guninski
- Re: [Coq-Club] Problem using Lemma as a coercion, Jean-Francois Monin
- Re: [Coq-Club] Problem using Lemma as a coercion,
Randy Pollack
- Re: [Coq-Club] Problem using Lemma as a coercion,
Adam Chlipala
- Re: [Coq-Club] Problem using Lemma as a coercion,
Georgi Guninski
- Re: [Coq-Club] Problem using Lemma as a coercion,
Adam Chlipala
Archive powered by MhonArc 2.6.16.