The Coq mailing list

[Georgi Guninski <guninski AT guninski.com>]

On Sun, Jun 12, 2011 at 09:15:02AM -0400, Adam Chlipala wrote:
> Georgi Guninski wrote:
> >Are lemma proved coercions considered cheating that violates Pollack
> >consistency?
> 
> I think the issue of coercions should be considered independently of
> the way the coercion functions are defined.
> 
> I haven't read a definition of Pollack consistency.  To me, the
> relevant question is about the proper form for displaying theorem
> statements, so that we can develop high confidence that they mean
> what we think they mean.  I don't think such a form should support
> implicit coercions at all.  (I never use coercions in theorem
> statements.)


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.

-- 
joro