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

[Maciej Piechotka]

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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 836 bytes
Desc: This is a digitally signed message part
Url : http://www.haskell.org/pipermail/haskell-cafe/attachments/20100522/65411b9b/attachment-0001.bin