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

[Jonas Almström Duregård]

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 <ajs at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>