On Sat, 2010-05-22 at 00:15 +0000, R J wrote:
I'm trying to prove that (==) is reflexive, symmetric, and transitive over the Bools, given this definition:
(==) :: Bool -> Bool -> Bool x == 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
I'd add additional step: x == x <=> (x && x) || (not x && not x) <=> x || not x <=> T def A && A = A A || not A = T However it depends on your level - the more advanced you are the more step you can omit.
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: ?
For example by cases in Y (assume Y is true and prove it correct and then assume Y is false and prove it correct. As in logic where there is law of excluded middle Y have to be true or false it holds). It took around 7 lines. Regards