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