Fwd: Add fixity for (==) and (/=)

[Dannyu NDos]

---------- Forwarded message ---------
From: Dannyu NDos <ndospark320 at gmail.com>
Date: 2018년 9월 17일 (월) 오후 6:18
Subject: Re: Add fixity for (==) and (/=)
To: <david.feuer at gmail.com>


Proof by truth table (F is False, T is True):
p q r (p == q) (q == r) ((p == q) == r) (p == (q == r))
F F F        T        T               F               F
F F T        T        F               T               T
F T F        F        F               T               T
F T T        F        T               F               F
T F F        F        T               T               T
T F T        F        F               F               F
T T F        T        F               F               F
T T T        T        T               T               T
That proves associativity of (==).

Also note that p /= q ≡ not p == q. Proof:
p q (p /= q) (not p) (not p == q)
F F        F       T            F
F T        T       T            T
T F        T       F            T
T T        F       F            F
And by symmetry of (/=), p /= q ≡ p == not q.

Then:
(p /= q) /= r ≡ (not p == q) == not r ≡ not p == (q == not r) ≡ p /= (q /=
r).
Hence (/=) is associative.

Q.E.D.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20180917/bfa73d8a/attachment.html>