[Haskell-cafe] Re: Proof question -- (==) over Bool

[Alexander Solla]

On May 22, 2010, at 1:32 AM, Jon Fairbairn wrote:

> Since Bool is a type, and all Haskell types include ⊥, you need
> to add conditions in your proofs to exclude it.

Not really.  Bottom isn't a value, so much as an expression for  
computations that don't refer to "real" values.  It's close enough to  
be treated as a value in many contexts, but this isn't one of them.

Proof by pattern matching (i.e., proof by truth table) is sufficient  
to ensure that bottom (as a value) isn't included.  After all, the  
Bool type is enumerable.  At least in principle.

So perhaps the constructive Haskell proof would go something like:

-- Claim to prove
transitivity :: Bool -> Bool -> Bool -> Bool
transitivity x y z = if (x == y) && (y && z) then x == z else True

-- "The" proof
unifier :: Bool
unifier = all (True ==) $ [ transitivity x y z | x <- [ True, False ]
                                                , y <- [ True, False ]
                                                , z <- [ True, False ] ]

This includes some syntactic sugar R J might not be "entitled" to, but  
the intent is pretty clear.  We are programmatically validating that  
every assignment of truth values to the sentence "if (x == y) && (y &&  
z) then x == z" is true.  (The theorem is "vacuously true" for  
assignments where the antecedent of the conditional is false)
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20100522/935758a5/attachment.html