Fwd: Add fixity for (==) and (/=)
Dannyu NDos
ndospark320 at gmail.com
Mon Sep 17 09:20:37 UTC 2018
---------- 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>
More information about the Libraries
mailing list