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)