Or

Posted on 2018-01-17 by nbloomf

Tags: arithmetic-made-difficult, literate-haskell

$\newcommand{\hyp}[2]{\stackrel{\tiny\text{hyp}}{#2}}$ $\newcommand{\let}[2]{\stackrel{\tiny\text{let}}{#2}}$ $\newcommand{\a}{a}$ $\newcommand{\b}{b}$ $\newcommand{\c}{c}$ $\newcommand{\p}{p}$ $\newcommand{\q}{q}$ $\newcommand{\r}{r}$ $\newcommand{\s}{s}$ $\newcommand{\x}{x}$ $\newcommand{\y}{y}$ $\newcommand{\z}{z}$ $\newcommand{\bool}{\mathbb{B}}$ $\newcommand{\btrue}{\mathsf{true}}$ $\newcommand{\bfalse}{\mathsf{false}}$ $\newcommand{\bnot}{\mathsf{not}}$ $\newcommand{\band}{\mathbin{\mathsf{and}}}$ $\newcommand{\bor}{\mathbin{\mathsf{or}}}$ $\newcommand{\bimpl}{\mathbin{\mathsf{impl}}}$ $\newcommand{\beq}{\mathsf{eq}}$ $\newcommand{\bif}[3]{\mathsf{if}\left(#1,#2,#3\right)}$ $\newcommand{\id}{\mathsf{id}}$ $\newcommand{\compose}{\mathsf{compose}}$ $\newcommand{\const}{\mathsf{const}}$ $\newcommand{\apply}{\mathsf{apply}}$ $\newcommand{\flip}{\mathsf{flip}}$ $\newcommand{\flipB}{\mathsf{flip2}}$ $\newcommand{\flipC}{\mathsf{flip3}}$ $\newcommand{\flipD}{\mathsf{flip4}}$ $\newcommand{\flipE}{\mathsf{flip5}}$ $\newcommand{\clone}{\mathsf{clone}}$ $\newcommand{\cloneC}{\mathsf{clone3}}$ $\newcommand{\composeAonB}{\mathsf{compose1on2}}$ $\newcommand{\composeAonC}{\mathsf{compose1on3}}$ $\newcommand{\composeAonD}{\mathsf{compose1on4}}$ $\newcommand{\composeBonA}{\mathsf{compose2on1}}$ $\newcommand{\composeBonB}{\mathsf{compose2on2}}$ $\newcommand{\composeConA}{\mathsf{compose3on1}}$ $\newcommand{\ptrue}{\mathsf{ptrue}}$ $\newcommand{\pfalse}{\mathsf{pfalse}}$ $\newcommand{\pnot}{\mathsf{pnot}}$ $\newcommand{\pand}{\mathbin{\mathsf{pand}}}$ $\newcommand{\por}{\mathbin{\mathsf{por}}}$ $\newcommand{\pimpl}{\mathbin{\mathsf{pimpl}}}$ $\newcommand{\fst}{\mathsf{first}}$ $\newcommand{\snd}{\mathsf{second}}$ $\newcommand{\dup}{\mathsf{dup}}$ $\newcommand{\tup}{\mathsf{tup}}$ $\newcommand{\tSwap}{\mathsf{swap}_{\times}}$ $\newcommand{\tPair}{\mathsf{pair}_{\times}}$ $\newcommand{\tAssocL}{\mathsf{assocL}_{\times}}$ $\newcommand{\tAssocR}{\mathsf{assocR}_{\times}}$ $\newcommand{\tupL}{\mathsf{tupL}}$ $\newcommand{\tupR}{\mathsf{tupR}}$ $\newcommand{\uncurry}{\mathsf{uncurry}}$ $\newcommand{\curry}{\mathsf{curry}}$ $\newcommand{\lft}{\mathsf{left}}$ $\newcommand{\rgt}{\mathsf{right}}$ $\newcommand{\either}{\mathsf{either}}$ $\newcommand{\uSwap}{\mathsf{swap}_{+}}$ $\newcommand{\uPair}{\mathsf{pair}_{+}}$ $\newcommand{\uAssocL}{\mathsf{assocL}_{+}}$ $\newcommand{\uAssocR}{\mathsf{assocR}_{+}}$ $\newcommand{\isLft}{\mathsf{isLeft}}$ $\newcommand{\isRgt}{\mathsf{isRight}}$ $\newcommand{\nats}{\mathbb{N}}$ $\newcommand{\zero}{\mathsf{0}}$ $\newcommand{\next}{\mathsf{next}}$ $\newcommand{\unnext}{\mathsf{unnext}}$ $\newcommand{\iszero}{\mathsf{isZero}}$ $\newcommand{\prev}{\mathsf{prev}}$ $\newcommand{\natrec}{\mathsf{natrec}}$ $\newcommand{\simprec}{\mathsf{simprec}}$ $\newcommand{\bailrec}{\mathsf{bailrec}}$ $\newcommand{\mutrec}{\mathsf{mutrec}}$ $\newcommand{\dnatrec}{\mathsf{dnatrec}}$ $\newcommand{\normrec}{\mathsf{normrec}}$ $\newcommand{\findsmallest}{\mathsf{findsmallest}}$ $\newcommand{\mnormrec}{\mathsf{mnormrec}}$ $\newcommand{\nequal}{\mathsf{eq}}$ $\newcommand{\nplus}{\mathsf{plus}}$ $\newcommand{\ntimes}{\mathsf{times}}$ $\newcommand{\nleq}{\mathsf{leq}}$ $\newcommand{\ngeq}{\mathsf{geq}}$ $\newcommand{\nminus}{\mathsf{minus}}$ $\newcommand{\nmax}{\mathsf{max}}$ $\newcommand{\nmin}{\mathsf{min}}$ $\newcommand{\ndivalg}{\mathsf{divalg}}$ $\newcommand{\nquo}{\mathsf{quo}}$ $\newcommand{\nrem}{\mathsf{rem}}$ $\newcommand{\ndiv}{\mathsf{div}}$ $\newcommand{\ngcd}{\mathsf{gcd}}$ $\newcommand{\ncoprime}{\mathsf{coprime}}$ $\newcommand{\nlcm}{\mathsf{lcm}}$ $\newcommand{\nmindiv}{\mathsf{mindiv}}$ $\newcommand{\nisprime}{\mathsf{isPrime}}$ $\newcommand{\npower}{\mathsf{power}}$ $\newcommand{\nchoose}{\mathsf{choose}}$ $\newcommand{\dom}{\mathsf{dom}}$ $\newcommand{\cod}{\mathsf{cod}}$ $\newcommand{\lists}[1]{\mathsf{List}(#1)}$ $\newcommand{\nil}{\mathsf{nil}}$ $\newcommand{\cons}{\mathsf{cons}}$ $\newcommand{\uncons}{\mathsf{uncons}}$ $\newcommand{\isnil}{\mathsf{isNil}}$ $\newcommand{\tail}{\mathsf{tail}}$ $\newcommand{\head}{\mathsf{head}}$ $\newcommand{\foldr}{\mathsf{foldr}}$ $\newcommand{\foldl}{\mathsf{foldl}}$ $\newcommand{\tacunfoldN}{\mathsf{tacunfoldN}}$ $\newcommand{\unfoldN}{\mathsf{unfoldN}}$ $\newcommand{\dfoldr}{\mathsf{dfoldr}}$ $\newcommand{\cfoldr}{\mathsf{cfoldr}}$ $\newcommand{\bfoldr}{\mathsf{bfoldr}}$ $\newcommand{\dbfoldr}{\mathsf{dbfoldr}}$ $\newcommand{\lfoldr}{\mathsf{lfoldr}}$ $\newcommand{\snoc}{\mathsf{snoc}}$ $\newcommand{\revcat}{\mathsf{revcat}}$ $\newcommand{\rev}{\mathsf{rev}}$ $\newcommand{\last}{\mathsf{last}}$ $\newcommand{\cat}{\mathsf{cat}}$ $\newcommand{\addlength}{\mathsf{addlength}}$ $\newcommand{\length}{\mathsf{length}}$ $\newcommand{\head}{\mathsf{head}}$ $\newcommand{\at}{\mathsf{at}}$ $\newcommand{\map}{\mathsf{map}}$ $\newcommand{\range}{\mathsf{range}}$ $\newcommand{\zip}{\mathsf{zip}}$ $\newcommand{\zipPad}{\mathsf{zipPad}}$ $\newcommand{\unzip}{\mathsf{unzip}}$ $\newcommand{\prefix}{\mathsf{prefix}}$ $\newcommand{\suffix}{\mathsf{suffix}}$ $\newcommand{\lcp}{\mathsf{lcp}}$ $\newcommand{\lcs}{\mathsf{lcs}}$ $\newcommand{\all}{\mathsf{all}}$ $\newcommand{\any}{\mathsf{any}}$ $\newcommand{\tails}{\mathsf{tails}}$ $\newcommand{\inits}{\mathsf{inits}}$ $\newcommand{\filter}{\mathsf{filter}}$ $\newcommand{\elt}{\mathsf{elt}}$ $\newcommand{\addcount}{\mathsf{addcount}}$ $\newcommand{\count}{\mathsf{count}}$ $\newcommand{\repeat}{\mathsf{repeat}}$ $\newcommand{\sublist}{\mathsf{sublist}}$ $\newcommand{\infix}{\mathsf{infix}}$ $\newcommand{\select}{\mathsf{select}}$ $\newcommand{\unique}{\mathsf{unique}}$ $\newcommand{\delete}{\mathsf{delete}}$ $\newcommand{\dedupeL}{\mathsf{dedupeL}}$ $\newcommand{\dedupeR}{\mathsf{dedupeR}}$ $\newcommand{\common}{\mathsf{common}}$ $\newcommand{\disjoint}{\mathsf{disjoint}}$ $\newcommand{\sublists}{\mathsf{sublists}}$ $\newcommand{\take}{\mathsf{take}}$ $\newcommand{\drop}{\mathsf{drop}}$ $\newcommand{\takeBut}{\mathsf{takeBut}}$ $\newcommand{\dropBut}{\mathsf{dropBut}}$ $\newcommand{\takeWhile}{\mathsf{takeWhile}}$ $\newcommand{\dropWhile}{\mathsf{dropWhile}}$

This page is part of a series on Arithmetic Made Difficult.

This post is literate Haskell; you can load the source into GHCi and play along.

{-# LANGUAGE NoImplicitPrelude #-}
module Or (
  or, _test_or, main_or
) where

import Testing
import Booleans
import Not
import And

Finally, $\bor$.

We define $\bor : \bool \rightarrow \bool \rightarrow \bool$ by \[\bor(p,q) = \bif{p}{\btrue}{\bif{q}{\btrue}{\bfalse}}.\]

In Haskell:

or :: (Boolean b) => b -> b -> b
or p q = ifThenElse p true (ifThenElse q true false)

We can compute $\bor$ explicitly.

We have \[\begin{eqnarray*} \bor(\btrue,\btrue) & = & \btrue \\ \bor(\btrue,\bfalse) & = & \btrue \\ \bor(\bfalse,\btrue) & = & \btrue \\ \bor(\bfalse,\bfalse) & = & \bfalse. \end{eqnarray*}\]

Note that \[\begin{eqnarray*} & & \bor(\btrue,\btrue) \\ & \href{/posts/arithmetic-made-difficult/Or.html#def-or} = & \bif{\btrue}{\btrue}{\bif{\btrue}{\btrue}{\bfalse}} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & \btrue \end{eqnarray*}\] that \[\begin{eqnarray*} & & \bor(\btrue,\bfalse) \\ & \href{/posts/arithmetic-made-difficult/Or.html#def-or} = & \bif{\btrue}{\btrue}{\bif{\bfalse}{\btrue}{\bfalse}} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & \btrue \end{eqnarray*}\] that \[\begin{eqnarray*} & & \bor(\bfalse,\btrue) \\ & \href{/posts/arithmetic-made-difficult/Or.html#def-or} = & \bif{\bfalse}{\btrue}{\bif{\btrue}{\btrue}{\bfalse}} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & \bif{\bfalse}{\btrue}{\btrue} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & \btrue \end{eqnarray*}\] and that \[\begin{eqnarray*} & & \bor(\bfalse,\bfalse) \\ & \href{/posts/arithmetic-made-difficult/Or.html#def-or} = & \bif{\bfalse}{\btrue}{\bif{\bfalse}{\btrue}{\bfalse}} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & \bif{\bfalse}{\btrue}{\bfalse} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & \bfalse \end{eqnarray*}\] as claimed.

_test_or_true_true :: (Boolean b, Equal b)
  => b -> Test Bool
_test_or_true_true p =
  testName "or(true,true) == true" $
  eq (or true true) (true `withTypeOf` p)


_test_or_true_false :: (Boolean b, Equal b)
  => b -> Test Bool
_test_or_true_false p =
  testName "or(true,false) == true" $
  eq (or true false) (true `withTypeOf` p)


_test_or_false_true :: (Boolean b, Equal b)
  => b -> Test Bool
_test_or_false_true p =
  testName "or(false,true) == true" $
  eq (or false true) (true `withTypeOf` p)


_test_or_false_false :: (Boolean b, Equal b)
  => b -> Test Bool
_test_or_false_false p =
  testName "or(false,false) == false" $
  eq (or false false) (false `withTypeOf` p)

$\btrue$ absorbs under $\bor$.

For all $a \in \bool$, we have \[\bor(\btrue,a) = \bor(a,\btrue) = \btrue.\]

If $a = \btrue$, we have \[\begin{eqnarray*} & & \bor(\btrue,\btrue) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-eval-true-true} = & \btrue \end{eqnarray*}\] and if $a = \bfalse$ we have \[\begin{eqnarray*} & & \bor(\btrue,\bfalse) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-eval-true-false} = & \btrue \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-eval-false-true} = & \bor(\bfalse,\btrue) \end{eqnarray*}\] as claimed.

_test_or_true :: (Boolean b, Equal b)
  => b -> Test (b -> Bool)
_test_or_true b =
  testName "or(true,p) == true" $
  \p -> eq (or true p) (true `withTypeOf` b)

$\bfalse$ is neutral under $\bor$.

For all $a \in \bool$, we have \[\bor(\bfalse,a) = \bor(a,\bfalse) = a.\]

If $a = \btrue$, we have \[\begin{eqnarray*} & & \bor(\bfalse,\btrue) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-eval-false-true} = & \btrue \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-eval-true-false} = & \bor(\btrue,\bfalse) \end{eqnarray*}\] and if $a = \bfalse$ we have \[\begin{eqnarray*} & & \bor(\bfalse,\bfalse) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-eval-false-false} = & \bfalse \end{eqnarray*}\] as claimed.

_test_or_false :: (Boolean b, Equal b)
  => b -> Test (b -> Bool)
_test_or_false _ =
  testName "or(false,p) == p" $
  \p -> eq (or false p) p

$\bor$ interacts with $\bnot$.

For all $a \in \bool$, we have $\bor(p,\bnot(p)) = \btrue$.

If $a = \btrue$, we have \[\begin{eqnarray*} & & \bor(\btrue,\bnot(\btrue)) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-true-left} = & \btrue \end{eqnarray*}\] and if $a = \bfalse$ we have \[\begin{eqnarray*} & & \bor(\bfalse,\bnot(\bfalse)) \\ & \href{/posts/arithmetic-made-difficult/Not.html#thm-not-false} = & \bor(\bfalse,\btrue) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-eval-false-true} = & \btrue \end{eqnarray*}\] as claimed.

_test_or_not :: (Boolean b, Equal b)
  => b -> Test (b -> Bool)
_test_or_not b =
  testName "or(p,not(p)) == true" $
  \p -> eq (or p (not p)) (true `withTypeOf` b)

$\bor$ is idempotent.

For all $a \in \bool$, we have $\bor(a,a) = a$.

If $a = \btrue$ we have \[\begin{eqnarray*} & & \bor(\btrue,\btrue) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-eval-true-true} = & \btrue \end{eqnarray*}\] and if $a = \bfalse$ then \[\begin{eqnarray*} & & \bor(\bfalse,\bfalse) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-eval-false-false} = & \bfalse \end{eqnarray*}\] as claimed.

_test_or_idempotent :: (Boolean b, Equal b)
  => b -> Test (b -> Bool)
_test_or_idempotent _ =
  testName "or(p,p) == p" $
  \p -> eq (or p p) p

$\bor$ is commutative.

For all $a,b \in \bool$, we have $\bor(a,b) = \bor(b,a)$.

If $a = \btrue$ we have \[\begin{eqnarray*} & & \bor(\btrue,b) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-true-left} = & \btrue \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-true-right} = & \bor(b,\btrue) \end{eqnarray*}\] and if $a = \bfalse$ we have \[\begin{eqnarray*} & & \bor(\bfalse,b) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-false-left} = & b \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-false-right} = & \bor(b,\bfalse) \end{eqnarray*}\] as claimed.

_test_or_commutative :: (Boolean b, Equal b)
  => b -> Test (b -> b -> Bool)
_test_or_commutative _ =
  testName "or(p,q) == or(q,p)" $
  \p q -> eq (or p q) (or q p)

$\bor$ is associative.

For all $a,b,c \in \bool$, we have \[\bor(\bor(a,b),c) = \bor(a,\bor(b,c)).\]

If $a = \btrue$ we have \[\begin{eqnarray*} & & \bor(\bor(a,b),c) \\ & \let{a = \btrue} = & \bor(\bor(\btrue,b),c) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-true-left} = & \bor(\btrue,c) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-true-left} = & \btrue \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-true-left} = & \bor(\btrue,\bor(b,c)) \end{eqnarray*}\] as claimed. If $a = \bfalse$, we have \[\begin{eqnarray*} & & \bor(\bor(a,b),c) \\ & \let{a = \bfalse} = & \bor(\bor(\bfalse,b),c) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-false-left} = & \bor(b,c) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-false-left} = & \bor(\bfalse,\bor(b,c)) \end{eqnarray*}\] as claimed.

_test_or_associative :: (Boolean b, Equal b)
  => b -> Test (b -> b -> b -> Bool)
_test_or_associative _ =
  testName "or(or(p,q),r) == or(p,or(q,r))" $
  \p q r -> eq (or (or p q) r) (or p (or q r))

DeMorgan’s laws hold for $\bor$, $\band$, and $\bnot$.

The following hold for all $a,b,c \in \bool$.

$\bnot(\band(a,b)) = \bor(\bnot(a),\bnot(b))$.
$\bnot(\bor(a,b)) = \band(\bnot(a),\bnot(b))$.

If $a = \btrue$, we have \[\begin{eqnarray*} & & \bnot(\band(a,b)) \\ & \let{a = \btrue} = & \bnot(\band(\btrue,b)) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-true-left} = & \bnot(b) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-false-left} = & \bor(\bfalse,\bnot(b)) \\ & \href{/posts/arithmetic-made-difficult/Not.html#thm-not-true} = & \bor(\bnot(\btrue),\bnot(b)) \\ & \let{a = \btrue} = & \bor(\bnot(a),\bnot(b)) \end{eqnarray*}\] as claimed. If $a = \bfalse$, we have \[\begin{eqnarray*} & & \bnot(\band(a,b)) \\ & \let{a = \bfalse} = & \bnot(\band(\bfalse,b)) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-false-left} = & \bnot(\bfalse) \\ & \href{/posts/arithmetic-made-difficult/Not.html#thm-not-false} = & \btrue \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-true-left} = & \bor(\btrue,\bnot(b)) \\ & \href{/posts/arithmetic-made-difficult/Not.html#thm-not-false} = & \bor(\bnot(\bfalse),\bnot(b)) \\ & \let{a = \bfalse} = & \bor(\bnot(a),\bnot(b)) \end{eqnarray*}\] as claimed.
If $a = \btrue$, we have \[\begin{eqnarray*} & & \bnot(\bor(a,b)) \\ & \let{a = \btrue} = & \bnot(\bor(\btrue,b)) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-true-left} = & \bnot(\btrue) \\ & \href{/posts/arithmetic-made-difficult/Not.html#thm-not-true} = & \bfalse \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-false-left} = & \band(\bfalse,\bnot(b)) \\ & \href{/posts/arithmetic-made-difficult/Not.html#thm-not-true} = & \band(\bnot(\btrue),\bnot(b)) \\ & \let{a = \btrue} = & \band(\bnot(a),\bnot(b)) \end{eqnarray*}\] as claimed. If $b = \bfalse$, we have \[\begin{eqnarray*} & & \bnot(\bor(a,b)) \\ & \let{a = \bfalse} = & \bnot(\bor(\bfalse,b)) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-false-left} = & \bnot(b) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-true-left} = & \band(\btrue,\bnot(b)) \\ & \href{/posts/arithmetic-made-difficult/Not.html#thm-not-false} = & \band(\bnot(\bfalse),\bnot(b)) \\ & \let{a = \bfalse} = & \band(\bnot(a),\bnot(b)) \end{eqnarray*}\] as claimed.

_test_not_and :: (Boolean b, Equal b)
  => b -> Test (b -> b -> Bool)
_test_not_and _ =
  testName "not(and(p,q)) == or(not(p),not(q))" $
  \p q -> eq (not (and p q)) (or (not p) (not q))


_test_not_or :: (Boolean b, Equal b)
  => b -> Test (b -> b -> Bool)
_test_not_or _ =
  testName "not(or(p,q)) == and(not(p),not(q))" $
  \p q -> eq (not (or p q)) (and (not p) (not q))

$\band$ and $\bor$ distribute over each other.

The following hold for all $a,b,c \in \bool$.

$\band(a,\bor(b,c)) = \bor(\band(a,b),\band(a,c))$.
$\bor(a,\band(b,c)) = \band(\bor(a,b),\bor(a,c))$.

If $a = \btrue$, we have \[\begin{eqnarray*} & & \band(a,\bor(b,c)) \\ & \let{a = \btrue} = & \band(\btrue,\bor(b,c)) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-true-left} = & \bor(b,c) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-true-left} = & \bor(\band(\btrue,b),c) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-true-left} = & \bor(\band(\btrue,b),\band(\btrue,c)) \\ & \let{a = \btrue} = & \bor(\band(a,b),\band(a,c)) \end{eqnarray*}\] as claimed. If $a = \bfalse$, we have \[\begin{eqnarray*} & & \band(a,\bor(b,c)) \\ & \let{a = \bfalse} = & \band(\bfalse,\bor(b,c)) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-false-left} = & \bfalse \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-false-left} = & \bor(\bfalse,\bfalse) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-false-left} = & \bor(\band(\bfalse,b),\bfalse) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-false-left} = & \bor(\band(\bfalse,b),\band(\bfalse,c)) \\ & \let{a = \bfalse} = & \bor(\band(a,b),\band(a,c)) \end{eqnarray*}\] as claimed.
If $a = \btrue$, we have \[\begin{eqnarray*} & & \bor(a,\band(b,c)) \\ & \let{a = \btrue} = & \bor(\btrue,\band(b,c)) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-true-left} = & \btrue \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-eval-true-true} = & \band(\btrue,\btrue) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-true-left} = & \band(\bor(\btrue,b),\btrue) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-true-left} = & \band(\bor(\btrue,b),\bor(\btrue,c)) \\ & \let{a = \btrue} = & \band(\bor(a,b),\bor(a,c)) \end{eqnarray*}\] as claimed. If $a = \bfalse$, we have \[\begin{eqnarray*} & & \bor(a,\band(b,c)) \\ & \let{a = \bfalse} = & \bor(\bfalse,\band(b,c)) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-false-left} = & \band(b,c) \\ & = & \band(b,\bor(\bfalse,c)) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-false-left} = & \band(\bor(\bfalse,b),\bor(\bfalse,c)) \\ & \let{a = \bfalse} = & \band(\bor(a,b),\bor(a,c)) \end{eqnarray*}\] as claimed.

_test_and_or :: (Boolean b, Equal b)
  => b -> Test (b -> b -> b -> Bool)
_test_and_or _ =
  testName "and(p,or(q,r)) == or(and(p,q),and(p,r))" $
  \p q r -> eq (and p (or q r)) (or (and p q) (and p r))


_test_or_and :: (Boolean b, Equal b)
  => b -> Test (b -> b -> b -> Bool)
_test_or_and _ =
  testName "or(p,and(q,r)) == and(or(p,q),or(p,r))" $
  \p q r -> eq (or p (and q r)) (and (or p q) (or p r))

$\bif{\ast}{\ast}{\ast}$ on booleans is equivalent to an or.

If $p,q \in \bool$, we have \[\bif{p}{\btrue}{q} = \bor(p,q).\]

If $p = \btrue$, we have \[\begin{eqnarray*} & & \bif{\btrue}{\btrue}{q} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & \btrue \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-true-left} = & \bor(\btrue,q) \end{eqnarray*}\] and if $p = we have \[\begin{eqnarray*} & & \bif{\bfalse}{\btrue}{q} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & q \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-false-left} = & \bor(\bfalse,q) \end{eqnarray*}\] as needed.

_test_if_or :: (Equal a)
  => a -> Test (Bool -> Bool -> Bool)
_test_if_or _ =
  testName "if(p,true,q) == or(p,q)" $
  \p q -> eq (if p then true else q) (or p q)

$\bif{\ast}{\ast}{\ast}$ interacts with $\bor$.

Let $A$ be a set with $a,b \in A$, and let $p,q \in \bool$. Then we have \[\bif{p}{a}{\bif{q}{a}{b}} = \bif{\bor(p,q)}{a}{b}.\]

If $p = \btrue$, we have \[\begin{eqnarray*} & & \bif{\bor(p,q)}{a}{b} \\ & \let{p = \btrue} = & \bif{\bor(\btrue,q)}{a}{b} \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-true-left} = & \bif{\btrue}{a}{b} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & a \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & \bif{\btrue}{a}{\bif{q}{a}{b}} \\ & \let{p = \btrue} = & \bif{p}{a}{\bif{q}{a}{b}} \end{eqnarray*}\] as needed, and if $p = \bfalse$ we have \[\begin{eqnarray*} & & \bif{\bor(p,q)}{a}{b} \\ & \let{p = \bfalse} = & \bif{\bor(\bfalse,q)}{a}{b} \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-false-left} = & \bif{q}{a}{b} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & \bif{\bfalse}{a}{\bif{q}{a}{b}} \\ & \let{p = \bfalse} = & \bif{p}{a}{\bif{q}{a}{b}} \end{eqnarray*}\] as needed.

_test_if_or_nest :: (Equal a)
  => a -> Test (a -> a -> Bool -> Bool -> Bool)
_test_if_or_nest _ =
  testName "if(or(p,q),a,b) == if(p,a,if(q,a,b))" $
  \a b p q -> eq
    (if or p q then a else b)
    (if p then a else if q then a else b)

Testing

Suite:

_test_or ::
  ( Equal a, Arbitrary a, CoArbitrary a, Show a, TypeName a
  , Boolean b, Arbitrary b, Show b, Equal b, TypeName b
  )
  => b -> a -> Int -> Int -> IO ()
_test_or p x size cases = do
  testLabel2 "or" p x

  let args = testArgs size cases

  runTest args (_test_or_true_true p)
  runTest args (_test_or_true_false p)
  runTest args (_test_or_false_true p)
  runTest args (_test_or_false_false p)

  runTest args (_test_or_true p)
  runTest args (_test_or_false p)
  runTest args (_test_or_not p)
  runTest args (_test_or_idempotent p)
  runTest args (_test_or_commutative p)
  runTest args (_test_or_associative p)

  runTest args (_test_not_and p)
  runTest args (_test_not_or p)
  runTest args (_test_and_or p)
  runTest args (_test_or_and p)

  runTest args (_test_if_or x)
  runTest args (_test_if_or_nest x)

Main:

main_or :: IO ()
main_or = _test_or (true :: Bool) (true :: Bool) 20 100