The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Coq users,

 

the definition of Z.le in the standard library is:

 

Z.le = fun x y : Z => (x ?= y)%Z <> Gt

     : Z -> Z -> Prop

 

which is a computing definition. For unknown x and y this computes to a rather lengthy term mapping the Z compare to the one for positives. This makes this definition unusable e.g. for dependent types like:

 

Definition t := { x : Z | 0 <= x < mod }.

 

because if one does computation on instances of such a type, the < and <= are expanded (results in roughly 100 lines).

 

Since for most other types (like nat) < is a relation (an inductive prop) rather than a function, I wonder why it was done like this for Z and what advantages this has.

 

My opinion is that there are computing (bool valued) and non-computing (Prop valued) versions of < and that there is a good reason for having both.

 

Best regards,

 

Michael

 

Michael Soegtrop
iCDG (Intel Communications & Devices Group)

PRD PSE SBA SWR (Software Reliability)
Principal Software Reliability

 

Phone: +49 (0)89 99 8853-60431
Mobile: +49 (0)172 81 62 56 2
michael.soegtrop AT intel.com

 

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928