<html>
<head>
<style><!--
.hmmessage P
{
margin:0px;
padding:0px
}
body.hmmessage
{
font-size: 10pt;
font-family:Verdana
}
--></style>
</head>
<body class='hmmessage'>
I'm trying to prove that (==) is reflexive, symmetric, and transitive over the Bools, given this definition:<div><br></div><div><div>(==) :: Bool -> Bool -> Bool</div><div>x == y = (x && y) || (not x && not y)</div><div><br></div><div>My question is: are the proofs below for reflexivity and symmetricity rigorous, and what is the proof of transitivity, which eludes me? Thanks.</div><div> </div><div>Theorem (reflexivity): For all x `elem` Bool, x == x.</div><div><br></div><div>Proof:</div><div><br></div><div> x == x</div><div> = {definition of "=="}</div><div> (x && x) || (not x && not x)</div><div> = {logic (law of the excluded middle)}</div><div> True</div><div><br></div><div>Theorem (symmetricity): For all x, y `elem` Bool, if x == y, then y == x.</div><div><br></div><div>Proof:</div><div><br></div><div> x == y</div><div> = {definition of "=="}</div><div> (x && y) || (not x && not y)</div><div> = {lemma: "(&&)" is commutative}</div><div> (y && x) || (not x && not y)</div><div> = {lemma: "(&&)" is commutative}</div><div> (y && x) || (not y && not x)</div><div> = {definition of "=="}</div><div> y == x</div><div><br></div><div>Theorem (transitivity): For all x, y, z `elem` Bool, if x == y, and y == z,</div><div>then x == z.</div><div><br></div><div>Proof: ?</div></div> <br /><hr />Hotmail has tools for the New Busy. Search, chat and e-mail from your inbox. <a href='http://www.windowslive.com/campaign/thenewbusy?ocid=PID28326::T:WLMTAGL:ON:WL:en-US:WM_HMP:042010_1' target='_new'>Learn more.</a></body>
</html>