The Coq mailing list

[Yakov Zaytsev <yakov AT yakov.cc>]

(*Now I'm confused :-). [Zle] is defined as follows. 
Why then it does not have type [Zle : Z -> Z -> Prop -> Prop] because of 
application of [not]?*)
Print Zle.
(* Zle = fun x y : Z => not (eq (Zcompare x y) Gt) *)
(*      : Z -> Z -> Prop *)
Check Zle.
(* Zle *)
(*      : Z -> Z -> Prop *)
Check not.
(* not *)
(*      : Prop -> Prop *)
(*I'm Haskell user.)

On Mar 19, 2010, at 3:41 PM, Adam Chlipala wrote:

> Yakov Zaytsev wrote:
>> I used omega to solve this inequality
>> 
>>    Lemma zgtz : not (0 > 0).
>> 
>> Now I can't get what does resulting term mean
>> 
>>    Require Import Arith.
>>    (*Require Import Omega.*)
>>    Require Import Coq.ZArith.auxiliary. (* Zgt_left *)
>>    Require Import Coq.ZArith.Znat. (* inj_gt *)
>>    Parameter H: 0 > 0.
>>    Definition left := Zgt_left 0 0 (inj_gt 0 0 H).
>>    Definition zgtz := left (eq_refl Gt).
>> 
>> Left doesn't have arrow type, does it!? Why is zgtz well-typed then?
> 
> In fact, [left] _does_ have a function type.  Its type is a call to [Zle], 
> which evaluates to an expression built with [<>], which evaluates to the 
> negation of an [=] fact.  A negation is encoded as a function returning 
> [False] proofs.