2010/5/21 R J <rj248...@hotmail.com>:
> 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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
