Albert Y. C. Lai trebla at vex.net
Thu Sep 2 13:59:02 EDT 2010

```On 10-09-02 12:10 PM, Stephen Sinclair wrote:
> Sorry to go a bit off topic, but I find it funny that I never really
> noticed you could perform less-than or greater-than comparisons on
> Bool values.  What's the semantic reasoning behind allowing relative
> comparisons on booleans?  In what context would you use it?  It seems
> to me a throwback to C's somewhat arbitrary assumption that False=0
> and True=1.

A boolean algebra is also a lattice. The lattice order reflects
implication. If the boolean algebra is furthermore 2-valued, the order
is total too. The only possible dispute among people is over False<=True
vs True<=False, i.e., should "<=" be "implies" or "implied by". But it
is always correct to pick one and stick with it. This is useful wherever
implication is useful. Suppose you wrote two functions and you now want
to prove or quickcheck-test that they are extensionally equal, except
you only care about arguments satisfying an assumption. You are checking

(p x) implies (f x == g x)

(p x) <= (f x == g x)

Implication is pervasively useful, but people pervasively
underappreciate it; they avoid to think in terms of implication when the
essence is implication. For example, some people say: you can use "not
(p x) || f x == g x". To that, I reply firstly: you can use solely NAND
too, why don't you try that. And I reply secondly: implication is more
direct, one single operator for the pervasive assume-guarantee paradigm,
minimum boilerplate. There is no need to bring in negation.
```