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

[Luke Palmer]

2010/5/21 R J <rj248842 at 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