The Coq mailing list

[roconnor AT theorem.ca]

On Mon, 2 May 2005, Roland Zumkeller wrote:

> Fixpoint le (a b : nat) { struct a } : Prop :=
> match a, b with
> | S a, S b => le a b
> | S _, O => False
> | O, _ => True
> end.

I suggest going further and defining le to be

Fixpoint le (a b : nat) { struct a } : bool :=
match a, b with
| S a, S b => le a b
| S _, O => false
| O, _ => true
end.

and making Is_true a coercion from bool to Prop.

In fact I suggest going further still and defining

Definition comparisonLt a : bool :=
match a with
| Lt => true
| Eq => false
| Gt => false
end.

Definition lt (a b:nat) := comparisionLt (a ?= b).

Actually, I suggest going still further and abstracting out nat, and
putting this in a module that can be applied in all situations where you
have a decidable comparison function: postive, N, nat, Z, rational, lists
of decidable types, polynomials of decideable types...

-- 
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''