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
