I'm trying to prove that (==) is reflexive, symmetric, and transitive over the
Bools, given this definition:
(==) :: Bool -> Bool -> Boolx == y =
(x && y) || (not x && not y)
My question is: are the proofs below for reflexivity and symmetricity
rigorous, and what is the proof of transitivity, which eludes me? Thanks.
Theorem (reflexivity): For all x `elem` Bool, x == x.
Proof:
x == x = {definition of "=="} (x && x) || (not x && not x) =
{logic (law of the excluded middle)} True
Theorem (symmetricity): For all x, y `elem` Bool, if x == y, then y == x.
Proof:
x == y = {definition of "=="} (x && y) || (not x && not y) =
{lemma: "(&&)" is commutative} (y && x) || (not x && not y) = {lemma:
"(&&)" is commutative} (y && x) || (not y && not x) = {definition of
"=="} y == x
Theorem (transitivity): For all x, y, z `elem` Bool, if x == y, and y ==
z,then x == z.
Proof: ?
_________________________________________________________________
Hotmail has tools for the New Busy. Search, chat and e-mail from your inbox.
http://www.windowslive.com/campaign/thenewbusy?ocid=PID28326::T:WLMTAGL:ON:WL:en-US:WM_HMP:042010_1_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
