---
title: Or
author: nbloomf
date: 2018-01-17
tags: arithmetic-made-difficult, literate-haskell
slug: or
---

> {-# LANGUAGE NoImplicitPrelude #-}
> module Or (
>   or, _test_or, main_or
> ) where
> 
> import Testing
> import Booleans
> import Not
> import And

Finally, $\bor$.

:::::: definition ::
[]{#def-or}
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.

:::::: theorem :::::
[]{#thm-or-eval}[]{#thm-or-eval-true-true}[]{#thm-or-eval-true-false}[]{#thm-or-eval-false-true}[]{#thm-or-eval-false-false}
We have
$$\begin{eqnarray*}
\bor(\btrue,\btrue)   & = & \btrue \\
\bor(\btrue,\bfalse)  & = & \btrue \\
\bor(\bfalse,\btrue)  & = & \btrue \\
\bor(\bfalse,\bfalse) & = & \bfalse.
\end{eqnarray*}$$

::: proof ::::::::::
Note that
$$\begin{eqnarray*}
 &   & \bor(\btrue,\btrue) \\
 &     \href{@or@#def-or}
   = & \bif{\btrue}{\btrue}{\bif{\btrue}{\btrue}{\bfalse}} \\
 &     \href{@booleans@#cor-if-true}
   = & \btrue
\end{eqnarray*}$$
that
$$\begin{eqnarray*}
 &   & \bor(\btrue,\bfalse) \\
 &     \href{@or@#def-or}
   = & \bif{\btrue}{\btrue}{\bif{\bfalse}{\btrue}{\bfalse}} \\
 &     \href{@booleans@#cor-if-true}
   = & \btrue
\end{eqnarray*}$$
that
$$\begin{eqnarray*}
 &   & \bor(\bfalse,\btrue) \\
 &     \href{@or@#def-or}
   = & \bif{\bfalse}{\btrue}{\bif{\btrue}{\btrue}{\bfalse}} \\
 &     \href{@booleans@#cor-if-true}
   = & \bif{\bfalse}{\btrue}{\btrue} \\
 &     \href{@booleans@#cor-if-false}
   = & \btrue
\end{eqnarray*}$$
and that
$$\begin{eqnarray*}
 &   & \bor(\bfalse,\bfalse) \\
 &     \href{@or@#def-or}
   = & \bif{\bfalse}{\btrue}{\bif{\bfalse}{\btrue}{\bfalse}} \\
 &     \href{@booleans@#cor-if-false}
   = & \bif{\bfalse}{\btrue}{\bfalse} \\
 &     \href{@booleans@#cor-if-false}
   = & \bfalse
\end{eqnarray*}$$
as claimed.
::::::::::::::::::::

::: test :::::::::::

> _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$.

:::::: theorem :::::
[]{#thm-or-true}[]{#thm-or-true-left}[]{#thm-or-true-right}
For all $a \in \bool$, we have $$\bor(\btrue,a) = \bor(a,\btrue) = \btrue.$$

::: proof ::::::::::
If $a = \btrue$, we have
$$\begin{eqnarray*}
 &   & \bor(\btrue,\btrue) \\
 &     \href{@or@#thm-or-eval-true-true}
   = & \btrue
\end{eqnarray*}$$
and if $a = \bfalse$ we have
$$\begin{eqnarray*}
 &   & \bor(\btrue,\bfalse) \\
 &     \href{@or@#thm-or-eval-true-false}
   = & \btrue \\
 &     \href{@or@#thm-or-eval-false-true}
   = & \bor(\bfalse,\btrue)
\end{eqnarray*}$$
as claimed.
::::::::::::::::::::

::: test :::::::::::

> _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$.

:::::: theorem :::::
[]{#thm-or-false}[]{#thm-or-false-left}[]{#thm-or-false-right}
For all $a \in \bool$, we have $$\bor(\bfalse,a) = \bor(a,\bfalse) = a.$$

::: proof ::::::::::
If $a = \btrue$, we have
$$\begin{eqnarray*}
 &   & \bor(\bfalse,\btrue) \\
 &     \href{@or@#thm-or-eval-false-true}
   = & \btrue \\
 &     \href{@or@#thm-or-eval-true-false}
   = & \bor(\btrue,\bfalse)
\end{eqnarray*}$$
and if $a = \bfalse$ we have
$$\begin{eqnarray*}
 &   & \bor(\bfalse,\bfalse) \\
 &     \href{@or@#thm-or-eval-false-false}
   = & \bfalse
\end{eqnarray*}$$
as claimed.
::::::::::::::::::::

::: test :::::::::::

> _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$.

:::::: theorem :::::
[]{#thm-or-not}
For all $a \in \bool$, we have $\bor(p,\bnot(p)) = \btrue$.

::: proof ::::::::::
If $a = \btrue$, we have
$$\begin{eqnarray*}
 &   & \bor(\btrue,\bnot(\btrue)) \\
 &     \href{@or@#thm-or-true-left}
   = & \btrue
\end{eqnarray*}$$
and if $a = \bfalse$ we have
$$\begin{eqnarray*}
 &   & \bor(\bfalse,\bnot(\bfalse)) \\
 &     \href{@not@#thm-not-false}
   = & \bor(\bfalse,\btrue) \\
 &     \href{@or@#thm-or-eval-false-true}
   = & \btrue
\end{eqnarray*}$$
as claimed.
::::::::::::::::::::

::: test :::::::::::

> _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.

:::::: theorem :::::
[]{#thm-or-idempotent}
For all $a \in \bool$, we have $\bor(a,a) = a$.

::: proof ::::::::::
If $a = \btrue$ we have
$$\begin{eqnarray*}
 &   & \bor(\btrue,\btrue) \\
 &     \href{@or@#thm-or-eval-true-true}
   = & \btrue
\end{eqnarray*}$$
and if $a = \bfalse$ then
$$\begin{eqnarray*}
 &   & \bor(\bfalse,\bfalse) \\
 &     \href{@or@#thm-or-eval-false-false}
   = & \bfalse
\end{eqnarray*}$$
as claimed.
::::::::::::::::::::

::: test :::::::::::

> _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.

:::::: theorem :::::
[]{#thm-or-commutative}
For all $a,b \in \bool$, we have $\bor(a,b) = \bor(b,a)$.

::: proof ::::::::::
If $a = \btrue$ we have
$$\begin{eqnarray*}
 &   & \bor(\btrue,b) \\
 &     \href{@or@#thm-or-true-left}
   = & \btrue \\
 &     \href{@or@#thm-or-true-right}
   = & \bor(b,\btrue)
\end{eqnarray*}$$
and if $a = \bfalse$ we have
$$\begin{eqnarray*}
 &   & \bor(\bfalse,b) \\
 &     \href{@or@#thm-or-false-left}
   = & b \\
 &     \href{@or@#thm-or-false-right}
   = & \bor(b,\bfalse)
\end{eqnarray*}$$
as claimed.
::::::::::::::::::::

::: test :::::::::::

> _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.

:::::: theorem :::::
[]{#thm-or-associative}
For all $a,b,c \in \bool$, we have $$\bor(\bor(a,b),c) = \bor(a,\bor(b,c)).$$

::: proof ::::::::::
If $a = \btrue$ we have
$$\begin{eqnarray*}
 &   & \bor(\bor(a,b),c) \\
 &     \let{a = \btrue}
   = & \bor(\bor(\btrue,b),c) \\
 &     \href{@or@#thm-or-true-left}
   = & \bor(\btrue,c) \\
 &     \href{@or@#thm-or-true-left}
   = & \btrue \\
 &     \href{@or@#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{@or@#thm-or-false-left}
   = & \bor(b,c) \\
 &     \href{@or@#thm-or-false-left}
   = & \bor(\bfalse,\bor(b,c))
\end{eqnarray*}$$
as claimed.
::::::::::::::::::::

::: test :::::::::::

> _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$.

:::::: theorem :::::
[]{#thm-demorgan}[]{#thm-demorgan-not-and}[]{#thm-demorgan-not-or}
The following hold for all $a,b,c \in \bool$.

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

::: proof ::::::::::
1. If $a = \btrue$, we have
$$\begin{eqnarray*}
 &   & \bnot(\band(a,b)) \\
 &     \let{a = \btrue}
   = & \bnot(\band(\btrue,b)) \\
 &     \href{@and@#thm-and-true-left}
   = & \bnot(b) \\
 &     \href{@or@#thm-or-false-left}
   = & \bor(\bfalse,\bnot(b)) \\
 &     \href{@not@#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{@and@#thm-and-false-left}
   = & \bnot(\bfalse) \\
 &     \href{@not@#thm-not-false}
   = & \btrue \\
 &     \href{@or@#thm-or-true-left}
   = & \bor(\btrue,\bnot(b)) \\
 &     \href{@not@#thm-not-false}
   = & \bor(\bnot(\bfalse),\bnot(b)) \\
 &     \let{a = \bfalse}
   = & \bor(\bnot(a),\bnot(b))
\end{eqnarray*}$$
as claimed.
2. If $a = \btrue$, we have
$$\begin{eqnarray*}
 &   & \bnot(\bor(a,b)) \\
 &     \let{a = \btrue}
   = & \bnot(\bor(\btrue,b)) \\
 &     \href{@or@#thm-or-true-left}
   = & \bnot(\btrue) \\
 &     \href{@not@#thm-not-true}
   = & \bfalse \\
 &     \href{@and@#thm-and-false-left}
   = & \band(\bfalse,\bnot(b)) \\
 &     \href{@not@#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{@or@#thm-or-false-left}
   = & \bnot(b) \\
 &     \href{@and@#thm-and-true-left}
   = & \band(\btrue,\bnot(b)) \\
 &     \href{@not@#thm-not-false}
   = & \band(\bnot(\bfalse),\bnot(b)) \\
 &     \let{a = \bfalse}
   = & \band(\bnot(a),\bnot(b))
\end{eqnarray*}$$
as claimed.
::::::::::::::::::::

::: test :::::::::::

> _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.

:::::: theorem :::::
[]{#thm-and-or-distribute}[]{#thm-or-and-distribute}
The following hold for all $a,b,c \in \bool$.

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

::: proof ::::::::::
1. If $a = \btrue$, we have
$$\begin{eqnarray*}
 &   & \band(a,\bor(b,c)) \\
 &     \let{a = \btrue}
   = & \band(\btrue,\bor(b,c)) \\
 &     \href{@and@#thm-and-true-left}
   = & \bor(b,c) \\
 &     \href{@and@#thm-and-true-left}
   = & \bor(\band(\btrue,b),c) \\
 &     \href{@and@#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{@and@#thm-and-false-left}
   = & \bfalse \\
 &     \href{@or@#thm-or-false-left}
   = & \bor(\bfalse,\bfalse) \\
 &     \href{@and@#thm-and-false-left}
   = & \bor(\band(\bfalse,b),\bfalse) \\
 &     \href{@and@#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.
2. If $a = \btrue$, we have
$$\begin{eqnarray*}
 &   & \bor(a,\band(b,c)) \\
 &     \let{a = \btrue}
   = & \bor(\btrue,\band(b,c)) \\
 &     \href{@or@#thm-or-true-left}
   = & \btrue \\
 &     \href{@and@#thm-and-eval-true-true}
   = & \band(\btrue,\btrue) \\
 &     \href{@or@#thm-or-true-left}
   = & \band(\bor(\btrue,b),\btrue) \\
 &     \href{@or@#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{@or@#thm-or-false-left}
   = & \band(b,c) \\
 & = & \band(b,\bor(\bfalse,c)) \\
 &     \href{@or@#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 :::::::::::

> _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.

:::::: theorem :::::
[]{#thm-or-is-if}
If $p,q \in \bool$, we have $$\bif{p}{\btrue}{q} = \bor(p,q).$$

::: proof ::::::::::
If $p = \btrue$, we have
$$\begin{eqnarray*}
 &   & \bif{\btrue}{\btrue}{q} \\
 &     \href{@booleans@#cor-if-true}
   = & \btrue \\
 &     \href{@or@#thm-or-true-left}
   = & \bor(\btrue,q)
\end{eqnarray*}$$
and if $p = \bfalse we have
$$\begin{eqnarray*}
 &   & \bif{\bfalse}{\btrue}{q} \\
 &     \href{@booleans@#cor-if-false}
   = & q \\
 &     \href{@or@#thm-or-false-left}
   = & \bor(\bfalse,q)
\end{eqnarray*}$$
as needed.
::::::::::::::::::::

::: test :::::::::::

> _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$.

:::::: theorem :::::
[]{#thm-or-if-hyp}
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}.$$

::: proof ::::::::::
If $p = \btrue$, we have
$$\begin{eqnarray*}
 &   & \bif{\bor(p,q)}{a}{b} \\
 &     \let{p = \btrue}
   = & \bif{\bor(\btrue,q)}{a}{b} \\
 &     \href{@or@#thm-or-true-left}
   = & \bif{\btrue}{a}{b} \\
 &     \href{@booleans@#cor-if-true}
   = & a \\
 &     \href{@booleans@#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{@or@#thm-or-false-left}
   = & \bif{q}{a}{b} \\
 &     \href{@booleans@#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 :::::::::::

> _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