Note that "all (True ==)" is logically equivalent to "all id" and to the "and" function from the prelude.
A more general approach based on type classes, the function taut takes a boolean function and determines (by exhaustive search) if it is a tautology: class BooleanFunction a where taut :: a -> Bool instance BooleanFunction Bool where taut = id instance (Bounded a,Enum a, BooleanFunction b) => BooleanFunction (a -> b) where taut f = and $ map (taut . f) $ enumFrom minBound unifier = taut transitivity On 22 May 2010 19:37, Alexander Solla <a...@2piix.com> wrote: > > 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) > _______________________________________________ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe > > _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
