coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Problem using Lemma as a coercion

From: Georgi Guninski <guninski AT guninski.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Problem using Lemma as a coercion
Date: Sun, 12 Jun 2011 08:23:55 +0300
Header: best read with a sniffer

I have problem using a Lemma as a coercion.

Trying this, get stuck on goal "coer a" and can't compute/unfold it:

(* Definition coer := fun a:True => Prop. *)
Lemma coer: True->Prop.
intro. exact True.
Qed.

Coercion coer: True >-> Sortclass.

Lemma lemma_true: forall a : True,a.
intro. compute. exact True. (*can't prove it*)
Qed.

How to prove it ?

If I use the definition instead of the lemma as a coercion, the proof works.

Thank you.

--
joro

[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