Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Problem using Lemma as a coercion

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Problem using Lemma as a coercion


chronological Thread 
  • 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








Archive powered by MhonArc 2.6.16.

Top of Page