2010/5/21 R J
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
This one depends on what you mean by rigorous. But you would have to have lemmas showing that && and || correspond to the predicate logic notions. I would do this by cases: x = True: (True && True) || (not True && not True) ... True || False True x = False (False && False) || (not False && not False) ... False || True 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
Yes, given the lemmas about && and ||, this is rigorous. You can prove those lemmas by case analysis.
Theorem (transitivity): For all x, y, z `elem` Bool, if x == y, and y == z, then x == z. Proof: ?
My first hunch here is to try the following lemma: Lemma: if (x == y) = True if and only if x = y. where == is the version you defined, and = is regular equality from logic, if you are allowed to rely on that. I would prove this by cases. At this point, you can convert transitivity of == to transitivity of =, which is assumed by the axioms. You could do the same for the other proofs you asked about instead of brute-forcing them. If you aren't allowed such magic, then I guess you could do all 8 cases of x, y, and z (i.e. proof by truth table). Somebody else might have a cleverer idea. Luke