Implies

Posted on 2018-01-18 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 Implies (
  impl, _test_impl, main_impl
) where

import Testing
import Booleans
import Not
import And
import Or

Next we define implication on booleans.

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

In Haskell:

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

\(\bimpl\) is equivalent to an \(\bor\).

For all \(p,q \in \bool\), we have \[\bimpl(p,q) = \bor(\bnot(p),q).\]

If \(p = \bfalse\), we have \[\begin{eqnarray*} & & \bimpl(\bfalse,q) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#def-implies} = & \bif{\bfalse}{q}{\btrue} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & \btrue \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-true-left} = & \bor(\btrue,q) \\ & \href{/posts/arithmetic-made-difficult/Not.html#thm-not-false} = & \bor(\bnot(\bfalse),q) \end{eqnarray*}\] as needed. Suppose then that \(p = \btrue\). Then \[\begin{eqnarray*} & & \bimpl(\btrue,q) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#def-implies} = & \bif{\btrue}{q}{\btrue} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & q \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-false-left} = & \bor(\bfalse,q) \\ & \href{/posts/arithmetic-made-difficult/Not.html#thm-not-true} = & \bor(\bnot(\btrue),q) \end{eqnarray*}\] as needed.

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

\(\bfalse\) implies anything.

If \(p \in \bool\), we have \(\bimpl(\bfalse,p) = \btrue\).

We have \[\begin{eqnarray*} & & \bimpl(\bfalse,p) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-or} = & \bor(\bnot(\bfalse),p) \\ & \href{/posts/arithmetic-made-difficult/Not.html#thm-not-false} = & \bor(\btrue,p) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-true-left} = & \btrue \end{eqnarray*}\] as claimed.

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

\(\bfalse\) interacts with \(\bimpl\) in the right argument.

If \(p \in \bool\), we have \(\bimpl(p,\bfalse) = \bnot(p)\).

We have \[\begin{eqnarray*} & & \bimpl(p,\bfalse) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-or} = & \bor(\bnot(p),\bfalse) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-false-right} = & \bnot(p) \end{eqnarray*}\] as claimed.

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

\(\btrue\) is left-neutral.

For all \(p \in \bool\) we have \(\bimpl(\btrue,p) = p\).

We have \[\begin{eqnarray*} & & \bimpl(\btrue,p) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-or} = & \bor(\bnot(\btrue),p) \\ & \href{/posts/arithmetic-made-difficult/Not.html#thm-not-true} = & \bor(\bfalse,p) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-false-left} = & p \end{eqnarray*}\] as claimed.

_test_impl_true_hyp :: (Boolean b, Equal b)
  => b -> Test (b -> Bool)
_test_impl_true_hyp _ =
  testName "impl(true,p) == p" $
  \p -> eq (impl true p) p

\(\btrue\) is right-absorptive.

If \(p \in \bool\), we have \(\bimpl(p,\btrue) = \btrue\).

We have \[\begin{eqnarray*} & & \bimpl(p,\btrue) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-or} = & \bor(\bnot(p),\btrue) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-true-right} = & \btrue \end{eqnarray*}\] as claimed.

_test_impl_true_conc :: (Boolean b, Equal b)
  => b -> Test (b -> Bool)
_test_impl_true_conc _ =
  testName "impl(p,true) == true" $
  \p -> eq (impl p true) true

\(\bimpl\) is… idemp-constant? Not sure what to call this.

If \(p \in \bool\) we have \(\bimpl(p,p) = \btrue\).

If \(p = \btrue\), we have \[\begin{eqnarray*} & & \bimpl(\btrue,\btrue) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-or} = & \bor(\bnot(\btrue),\btrue) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-true-right} = & \btrue \end{eqnarray*}\] as claimed. If \(p = \bfalse\), we have \[\begin{eqnarray*} & & \bimpl{\bfalse,\bfalse} \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-false-hyp} = & \btrue \end{eqnarray*}\] as claimed.

_test_impl_reflexive :: (Boolean b, Equal b)
  => b -> Test (b -> Bool)
_test_impl_reflexive _ =
  testName "impl(p,p) == true" $
  \p -> eq (impl p p) true

\(\bimpl\) is antisymmetric.

For all \(p,q \in \bool\) we have \(\bor(\bimpl(p,q),\bimpl(q,p))\).

We have \[\begin{eqnarray*} & & \bor(\bimpl(p,q),\bimpl(q,p)) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-or} = & \bor(\bor(\bnot(p),q),\bimpl(q,p)) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-or} = & \bor(\bor(\bnot(p),q),\bor(\bnot(q),p)) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-associative} = & \bor(\bnot(p),\bor(q,\bor(\bnot(q),p))) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-associative} = & \bor(\bnot(p),\bor(\bor(q,\bnot(q)),p)) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-not} = & \bor(\bnot(p),\bor(\btrue,p)) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-true-left} = & \bor(\bnot(p),\btrue) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-true-right} = & \btrue \end{eqnarray*}\] as needed.

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

\(\bimpl\) is left-commutative.

For all \(p,q,r \in \bool\) we have \[\bimpl(p,\bimpl(q,r)) = \bimpl(q,\bimpl(p,r)).\]

We have \[\begin{eqnarray*} & & \bimpl(p,\bimpl(q,r)) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-or} = & \bor(\bnot(p),\bimpl(q,r)) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-or} = & \bor(\bnot(p),\bor(\bnot(q),r)) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-associative} = & \bor(\bor(\bnot(p),\bnot(q)),r) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-commutative} = & \bor(\bor(\bnot(q),\bnot(p)),r) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-associative} = & \bor(\bnot(q),\bor(\bnot(p),r)) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-or} = & \bor(\bnot(q),\bimpl(p,r)) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-or} = & \bimpl(q,\bimpl(p,r)) \end{eqnarray*}\] as claimed.

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

\(\bimpl\) has a kind of transitivity.

For all \(p,q,r \in \bool\) we have \[\bimpl(\bimpl(p,q),\bimpl(\bimpl(q,r),\bimpl(p,r))).\]

If \(p = \bfalse\), we have \[\begin{eqnarray*} & & \bimpl(\bimpl(p,q),\bimpl(\bimpl(q,r),\bimpl(p,r))) \\ & \let{p = \bfalse} = & \bimpl(\bimpl(\bfalse,q),\bimpl(\bimpl(q,r),\bimpl(\bfalse,r))) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-false-hyp} = & \bimpl(\btrue,\bimpl(\bimpl(q,r),\bimpl(\bfalse,r))) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-false-hyp} = & \bimpl(\btrue,\bimpl(\bimpl(q,r),\btrue)) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-true-hyp} = & \bimpl(\bimpl(q,r),\btrue) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-or} = & \bor(\bnot(\bimpl(q,r)),\btrue) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-true-right} = & \btrue \end{eqnarray*}\] as claimed. If \(p = \btrue\), we have \[\begin{eqnarray*} & & \bimpl(\bimpl(p,q),\bimpl(\bimpl(q,r),\bimpl(p,r))) \\ & \let{p = \btrue} = & \bimpl(\bimpl(\btrue,q),\bimpl(\bimpl(q,r),\bimpl(\btrue,r))) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-true-hyp} = & \bimpl(q,\bimpl(\bimpl(q,r),\bimpl(\btrue,r))) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-true-hyp} = & \bimpl(q,\bimpl(\bimpl(q,r),r)) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-left-commutative} = & \bimpl(\bimpl(q,r),\bimpl(q,r)) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-self} = & \btrue \end{eqnarray*}\] as claimed.

_test_impl_transitive :: (Boolean b, Equal b)
  => b -> Test (b -> b -> b -> Bool)
_test_impl_transitive _ =
  testName "impl(impl(p,q),impl(impl(q,r),impl(p,r)))" $
  \p q r -> isTrue $ impl (impl p q) (impl (impl q r) (impl p r))

\(\bimpl\) has a kind of distributivity.

For all \(p,q,r \in \bool\) we have \[\bimpl(\bimpl(p,\bimpl(q,r)),\bimpl(\bimpl(p,q),\bimpl(p,r))).\]

If \(p = \bfalse\), we have \[\begin{eqnarray*} & & \bimpl(\bimpl(p,\bimpl(q,r)),\bimpl(\bimpl(p,q),\bimpl(p,r))) \\ & \let{p = \bfalse} = & \bimpl(\bimpl(\bfalse,\bimpl(q,r)),\bimpl(\bimpl(\bfalse,q),\bimpl(\bfalse,r))) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-false-hyp} = & \bimpl(\btrue,\bimpl(\bimpl(\bfalse,q),\bimpl(\bfalse,r))) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-false-hyp} = & \bimpl(\btrue,\bimpl(\btrue,\bimpl(\bfalse,r))) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-false-hyp} = & \bimpl(\btrue,\bimpl(\btrue,\btrue)) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-true-hyp} = & \bimpl(\btrue,\btrue) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-true-hyp} = & \btrue \end{eqnarray*}\] Suppose instead that \(p = \btrue\). Now \[\begin{eqnarray*} & & \bimpl(\bimpl(p,\bimpl(q,r)),\bimpl(\bimpl(p,q),\bimpl(p,r))) \\ & \let{p = \btrue} = & \bimpl(\bimpl(\btrue,\bimpl(q,r)),\bimpl(\bimpl(\btrue,q),\bimpl(\btrue,r))) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-true-hyp} = & \bimpl(\bimpl(q,r),\bimpl(\bimpl(\btrue,q),\bimpl(\btrue,r))) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-true-hyp} = & \bimpl(\bimpl(q,r),\bimpl(q,\bimpl(\btrue,r))) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-true-hyp} = & \bimpl(\bimpl(q,r),\bimpl(q,r)) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-self} = & \btrue \end{eqnarray*}\] as claimed.

_test_impl_distributive :: (Boolean b, Equal b)
  => b -> Test (b -> b -> b -> Bool)
_test_impl_distributive _ =
  testName "impl(impl(p,impl(q,r)),impl(impl(p,q),impl(p,r)))" $
  \p q r -> isTrue $ impl (impl p (impl q r)) (impl (impl p q) (impl p r))

\(\bimpl\) interacts with \(\band\).

For all \(p,q,r,s \in \bool\), if \(\bimpl(p,r)\) and \(\bimpl(q,s)\), then \(\bimpl(\band(p,q),\band(r,s))\).

If \(p = \bfalse\), we have \[\begin{eqnarray*} & & \bimpl(\band(\bimpl(p,r),\bimpl(q,s)),\bimpl(\band(p,q),\band(r,s))) \\ & \let{p = \bfalse} = & \bimpl(\band(\bimpl(\bfalse,r),\bimpl(q,s)),\bimpl(\band(\bfalse,q),\band(r,s))) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-false-hyp} = & \bimpl(\band(\btrue,\bimpl(q,s)),\bimpl(\band(\bfalse,q),\band(r,s))) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-false-left} = & \bimpl(\band(\btrue,\bimpl(q,s)),\bimpl(\bfalse,\band(r,s))) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-false-hyp} = & \bimpl(\band(\btrue,\bimpl(q,s)),\btrue) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-or} = & \bor(\bnot(\band(\btrue,\bimpl(q,s))),\btrue) \\ & \href{/posts/arithmetic-made-difficult/Or.html#thm-or-true-right} = & \btrue \end{eqnarray*}\] as claimed. suppose \(p = \btrue\). If \(r = \bfalse\), we have \[\begin{eqnarray*} & & \bimpl(\band(\bimpl(p,r),\bimpl(q,s)),\bimpl(\band(p,q),\band(r,s))) \\ & \let{p = \btrue} = & \bimpl(\band(\bimpl(\btrue,r),\bimpl(q,s)),\bimpl(\band(\btrue,q),\band(r,s))) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-true-left} = & \bimpl(\band(\bimpl(\btrue,r),\bimpl(q,s)),\bimpl(q,\band(r,s))) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-true-hyp} = & \bimpl(\band(r,\bimpl(q,s)),\bimpl(q,\band(r,s))) \\ & \let{r = \bfalse} = & \bimpl(\band(\bfalse,\bimpl(q,s)),\bimpl(q,\band(\bfalse,s))) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-false-left} = & \bimpl(\bfalse,\bimpl(q,\band(\bfalse,s))) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-false-hyp} = & \btrue \end{eqnarray*}\] as claimed. If \(r = \btrue\), we have \[\begin{eqnarray*} & & \bimpl(\band(\bimpl(p,r),\bimpl(q,s)),\bimpl(\band(p,q),\band(r,s))) \\ & \let{p = \btrue} = & \bimpl(\band(\bimpl(\btrue,r),\bimpl(q,s)),\bimpl(\band(\btrue,q),\band(r,s))) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-true-left} = & \bimpl(\band(\bimpl(\btrue,r),\bimpl(q,s)),\bimpl(q,\band(r,s))) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-true-hyp} = & \bimpl(\band(r,\bimpl(q,s)),\bimpl(q,\band(r,s))) \\ & \let{r = \btrue} = & \bimpl(\band(\btrue,\bimpl(q,s)),\bimpl(q,\band(\btrue,s))) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-true-left} = & \bimpl(\bimpl(q,s),\bimpl(q,\band(\btrue,s))) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-true-left} = & \bimpl(\bimpl(q,s),\bimpl(q,s)) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-self} = & \btrue \end{eqnarray*}\] as claimed.

_test_impl_and_compatible
  :: (Boolean b, Equal b)
  => b -> Test (b -> b -> b -> b -> Bool)
_test_impl_and_compatible _ =
  testName "if and(impl(p,r),impl(q,s)) then impl(and(p,q),and(r,s))" $
  \p q r s -> isTrue $ ifThenElse (and (impl p r) (impl q s))
    (impl (and p q) (and r s))
    (true)

\(\bimpl\) interacts with \(\band\) and \(\bif{\ast}{\ast}{\ast}\).

Let \(p,q,r \in \bool\). If \(\bimpl(r,q)\), then \[\bif{\band(p,q)}{\btrue}{r} = \bif{p}{q}{r}.\]

If \(q = \btrue\) then \[\begin{eqnarray*} & & \bimpl(\bimpl(r,q),\beq(\bif{\band(p,q)}{\btrue}{r},\bif{p}{q}{r})) \\ & \let{q = \btrue} = & \bimpl(\bimpl(r,\btrue),\beq(\bif{\band(p,\btrue)}{\btrue}{r},\bif{p}{\btrue}{r})) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-true-conc} = & \bimpl(\btrue,\beq(\bif{\band(p,\btrue)}{\btrue}{r},\bif{p}{\btrue}{r})) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-true-right} = & \bimpl(\btrue,\beq(\bif{p}{\btrue}{r},\bif{p}{\btrue}{r})) \\ & \href{/posts/arithmetic-made-difficult/Testing.html#thm-eq-reflexive} = & \bimpl(\btrue,\btrue) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-true-hyp} = & \btrue \end{eqnarray*}\] as claimed. If \(q = \bfalse\) and \(r = \bfalse\), we have \[\begin{eqnarray*} & & \bimpl(\bimpl(r,q),\beq(\bif{\band(p,q)}{\btrue}{r},\bif{p}{q}{r})) \\ & \let{q = \bfalse} = & \bimpl(\bimpl(r,\bfalse),\beq(\bif{\band(p,\bfalse)}{\btrue}{r},\bif{p}{\bfalse}{r})) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-false-conc} = & \bimpl(\bnot(r),\beq(\bif{\band(p,\bfalse)}{\btrue}{r},\bif{p}{\bfalse}{r})) \\ & \href{/posts/arithmetic-made-difficult/And.html#thm-and-false-right} = & \bimpl(\bnot(r),\beq(\bif{\bfalse}{\btrue}{r},\bif{p}{\bfalse}{r})) \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & \bimpl(\bnot(r),\beq(r,\bif{p}{\bfalse}{r})) \\ & \let{r = \bfalse} = & \bimpl(\bnot(\bfalse),\beq(\bfalse,\bif{p}{\bfalse}{\bfalse})) \\ & \href{/posts/arithmetic-made-difficult/Not.html#thm-not-false} = & \bimpl(\btrue,\beq(\bfalse,\bif{p}{\bfalse}{\bfalse})) \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#thm-if-same} = & \bimpl(\btrue,\beq(\bfalse,\bfalse)) \\ & \href{/posts/arithmetic-made-difficult/Testing.html#thm-eq-reflexive} = & \bimpl(\btrue,\btrue) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-true-hyp} = & \btrue \end{eqnarray*}\] as claimed. And if \(q = \bfalse\) and \(r = \btrue\), we have \[\begin{eqnarray*} & & \bimpl(\bimpl(r,q),\beq(\bif{\band(p,q)}{\btrue}{r},\bif{p}{q}{r})) \\ & \let{q = \bfalse} = & \bimpl(\bimpl(r,\bfalse),\beq(\bif{\band(p,\bfalse)}{\btrue}{r},\bif{p}{\bfalse}{r})) \\ & \let{r = \btrue} = & \bimpl(\bimpl(\btrue,\bfalse),\beq(\bif{\band(p,\bfalse)}{\btrue}{\btrue},\bif{p}{\bfalse}{\btrue})) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-true-hyp} = & \bimpl(\bfalse,\beq(\bif{\band(p,\bfalse)}{\btrue}{\btrue},\bif{p}{\bfalse}{\btrue})) \\ & \href{/posts/arithmetic-made-difficult/Implies.html#thm-implies-false-hyp} = & \btrue \end{eqnarray*}\] as claimed.

_test_impl_and_if :: (Boolean b, Equal b)
  => b -> Test (b -> b -> b -> Bool)
_test_impl_and_if _ =
  testName "if impl(r,q) then if(and(p,q),true,r) == if(p,q,r)" $
  \p q r -> if isTrue (impl r q)
    then eq
      (ifThenElse (and p q) true r)
      (ifThenElse p q r)
    else true

Testing

Suite:

_test_impl ::
  ( TypeName b, Boolean b, Arbitrary b, Show b, Equal b
  ) => b -> Int -> Int -> IO ()
_test_impl p size cases = do
  testLabel1 "implies" p

  let args = testArgs size cases

  runTest args (_test_impl_or p)
  runTest args (_test_impl_false_hyp p)
  runTest args (_test_impl_false_conc p)
  runTest args (_test_impl_true_hyp p)
  runTest args (_test_impl_true_conc p)
  runTest args (_test_impl_reflexive p)
  runTest args (_test_impl_total p)
  runTest args (_test_impl_antecedents_commute p)
  runTest args (_test_impl_transitive p)
  runTest args (_test_impl_distributive p)
  runTest args (_test_impl_and_compatible p)
  runTest args (_test_impl_and_if p)

Main:

main_impl :: IO ()
main_impl = _test_impl (true :: Bool) 20 100