coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

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