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
signature.asc
Description: This is a digitally signed message part
_______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
