<?xml version="1.0" encoding="UTF-8" ?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">

<html xmlns="http://www.w3.org/1999/xhtml" xml:lang="en" lang="en">

<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8" />
<meta name="viewport" content="width=device-width, initial-scale=1.0">
<title>nbloomf.blog - Addition</title>
<link rel="stylesheet" type="text/css" href="../../css/default.css" />
<link rel="icon" href="../../raw/gfx/icon/favicon-32.png" />
<link rel="apple-touch-icon-precomposed" sizes="57x57" href="../../raw/gfx/icon/favicon-57.png" />
<link rel="apple-touch-icon-precomposed" sizes="114x114" href="../../raw/gfx/icon/favicon-114.png" />
<link rel="apple-touch-icon-precomposed" sizes="152x152" href="../../raw/gfx/icon/favicon-152.png" />
<script type="text/javascript" src="http://cdn.mathjax.org/mathjax/latest/MathJax.js?config=TeX-AMS-MML_HTMLorMML">
</script>
</head>

<body>
<div id="header">
  <div id="logo">
    <a href="../../index.html">nbloomf</a>
  </div>
  <div id="navigation">
    <a href="../../index.html">Home</a>
    <a href="../../pages/about.html">About</a>
    <a href="../../pages/projects.html">Projects</a>
    <a href="../../archive.html">Blog</a>
  </div>
</div>

<div id="content">
<h1>Addition</h1>
<!-- BEGIN CONTENT -->


<div class="info">
Posted on 2014-06-01 by nbloomf
</div>


<div class="info tags">Tags: <a href="../../tag/arithmetic-made-difficult.html">arithmetic-made-difficult</a>, <a href="../../tag/literate-haskell.html">literate-haskell</a></div>


<!-- LaTeX Macros for Arithmetic Made Difficult -->
<div class="invisible">
<!-- proof structure -->
\(\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}\)

<!-- booleans -->
\(\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)}\)

<!-- functions -->
\(\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}}\)


<!-- predicates -->
\(\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}}}\)

<!-- tuples -->
\(\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}}\)

<!-- disjoint unions -->
\(\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}}\)

<!-- natural numbers -->
\(\newcommand{\nats}{\mathbb{N}}\)
\(\newcommand{\zero}{\mathsf{0}}\)
\(\newcommand{\next}{\mathsf{next}}\)
\(\newcommand{\unnext}{\mathsf{unnext}}\)
\(\newcommand{\iszero}{\mathsf{isZero}}\)
\(\newcommand{\prev}{\mathsf{prev}}\)

<!-- natural number recursion -->
\(\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}}\)

<!-- natural number arithmetic -->
\(\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}}\)

<!-- categories -->
\(\newcommand{\dom}{\mathsf{dom}}\)
\(\newcommand{\cod}{\mathsf{cod}}\)

<!-- lists -->
\(\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}}\)

<!-- list recursion -->
\(\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}}\)

<!-- list arithmetic -->
\(\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}}\)
</div>
<!-- End LaTeX Macros for Arithmetic Made Difficult -->

<p class="post-info">This page is part of a series on <a href="../../pages/amd.html">Arithmetic Made Difficult</a>.</p>

<p class="post-info">This post is literate Haskell; you can load <a href="https://raw.githubusercontent.com/nbloomf/nbloomf.md/master/posts/arithmetic-made-difficult/Plus.lhs">the source</a> into GHCi and play along.</p>

<hr />

<div class="sourceCode" id="cb1"><pre class="sourceCode literate haskell"><code class="sourceCode haskell"><a class="sourceLine" id="cb1-1" data-line-number="1"><span class="ot">{-# LANGUAGE NoImplicitPrelude #-}</span></a>
<a class="sourceLine" id="cb1-2" data-line-number="2"><span class="kw">module</span> <span class="dt">Plus</span></a>
<a class="sourceLine" id="cb1-3" data-line-number="3">  ( plus, _test_plus, main_plus</a>
<a class="sourceLine" id="cb1-4" data-line-number="4">  ) <span class="kw">where</span></a>
<a class="sourceLine" id="cb1-5" data-line-number="5"></a>
<a class="sourceLine" id="cb1-6" data-line-number="6"><span class="kw">import</span> <span class="dt">Testing</span></a>
<a class="sourceLine" id="cb1-7" data-line-number="7"><span class="kw">import</span> <span class="dt">Functions</span></a>
<a class="sourceLine" id="cb1-8" data-line-number="8"><span class="kw">import</span> <span class="dt">Booleans</span></a>
<a class="sourceLine" id="cb1-9" data-line-number="9"><span class="kw">import</span> <span class="dt">NaturalNumbers</span></a>
<a class="sourceLine" id="cb1-10" data-line-number="10"><span class="kw">import</span> <span class="dt">SimpleRecursion</span></a></code></pre></div>
<p>So far we’ve characterized the natural numbers via a unique mapping <span class="math display">\[\natrec(\ast)(\ast) : \nats \rightarrow A,\]</span> and we defined another parameterized mapping <span class="math display">\[\simprec(\ast)(\ast) : \nats \times A \rightarrow B.\]</span> From now on, when we want to define a mapping with one of these signatures, these prepackaged recursive maps may come in handy. What’s more, we can use the universal properties of these maps to define them in terms of <em>desired behavior</em>.</p>
<p>Natural number addition has signature <span class="math inline">\(\nats \times \nats \rightarrow \nats\)</span>, so we might hope to define addition in terms of <span class="math inline">\(\simprec(\ast)(\ast)\)</span>. To do this, we need to find mappings <span class="math inline">\(\varphi : \nats \rightarrow \nats\)</span> and <span class="math inline">\(\mu : \nats \times \nats \times \nats \rightarrow \nats\)</span> that make <span class="math inline">\(\simprec(\varphi)(\mu)\)</span> act like addition. For example, we want <span class="math inline">\(\next\)</span> to act like <span class="math inline">\(+1\)</span>, and <span class="math display">\[n = \zero + n = \simprec(\varphi)(\mu)(\zero,n) = \varphi(n),\]</span> and</p>
<p><span class="math display">\[\begin{eqnarray*}
(m+n)+1
  &amp; = &amp; (m+1)+n \\
  &amp; = &amp; \simprec(\varphi)(\mu)(\next(m),n) \\
  &amp;     \href{/posts/arithmetic-made-difficult/SimpleRecursion.html#def-simprec-next}
    = &amp; \mu(m,n,\simprec(\varphi)(\mu)(m,n)) \\
  &amp; = &amp; \mu(m,n,m+n).
\end{eqnarray*}\]</span></p>
<p>With this in mind, we define a binary operation <span class="math inline">\(\nplus\)</span> on <span class="math inline">\(\nats\)</span> as follows.</p>
<div class="definition">
<p>Let <span class="math inline">\(\mu : \nats \times \nats \times \nats \rightarrow \nats\)</span> be given by <span class="math inline">\(\mu(k,a,b) = \next(b)\)</span>. We then define <span class="math inline">\(\nplus : \nats \times \nats \rightarrow \nats\)</span> by <span class="math display">\[\nplus = \simprec(\id)(\mu).\]</span></p>
<p>In Haskell:</p>
<div class="sourceCode" id="cb2"><pre class="sourceCode literate haskell"><code class="sourceCode haskell"><a class="sourceLine" id="cb2-1" data-line-number="1"><span class="ot">plus ::</span> (<span class="dt">Natural</span> n) <span class="ot">=&gt;</span> n <span class="ot">-&gt;</span> n <span class="ot">-&gt;</span> n</a>
<a class="sourceLine" id="cb2-2" data-line-number="2">plus <span class="fu">=</span> simpleRec id mu</a>
<a class="sourceLine" id="cb2-3" data-line-number="3">  <span class="kw">where</span> mu _ _ b <span class="fu">=</span> next b</a></code></pre></div>
</div>
<p>Since <span class="math inline">\(\nplus\)</span> is defined in terms of simple recursion, it is the unique solution to a set of functional equations.</p>
<div class="corollary">
<p><span id="cor-plus-up"></span><span id="cor-plus-up-zero"></span><span id="cor-plus-up-next"></span> <span class="math inline">\(\nplus\)</span> is the unique map <span class="math inline">\(f : \nats \times \nats \rightarrow \nats\)</span> with the property that for all <span class="math inline">\(a,b \in \nats\)</span>, we have <span class="math display">\[\left\{\begin{array}{l}
 f(\zero,b) = b \\
 f(\next(a),b) = \next(f(a,b)).
\end{array}\right.\]</span></p>
<div class="test">
<div class="sourceCode" id="cb3"><pre class="sourceCode literate haskell"><code class="sourceCode haskell"><a class="sourceLine" id="cb3-1" data-line-number="1"><span class="ot">_test_plus_zero_left ::</span> (<span class="dt">Natural</span> n, <span class="dt">Equal</span> n)</a>
<a class="sourceLine" id="cb3-2" data-line-number="2">  <span class="ot">=&gt;</span> <span class="dt">Proxy</span> n <span class="ot">-&gt;</span> (n <span class="ot">-&gt;</span> n <span class="ot">-&gt;</span> n) <span class="ot">-&gt;</span> <span class="dt">Test</span> (n <span class="ot">-&gt;</span> <span class="dt">Bool</span>)</a>
<a class="sourceLine" id="cb3-3" data-line-number="3">_test_plus_zero_left _ f <span class="fu">=</span></a>
<a class="sourceLine" id="cb3-4" data-line-number="4">  testName <span class="st">&quot;f(0,b) == b&quot;</span> <span class="fu">$</span></a>
<a class="sourceLine" id="cb3-5" data-line-number="5">  \b <span class="ot">-&gt;</span> eq (f zero b) b</a>
<a class="sourceLine" id="cb3-6" data-line-number="6"></a>
<a class="sourceLine" id="cb3-7" data-line-number="7"></a>
<a class="sourceLine" id="cb3-8" data-line-number="8"><span class="ot">_test_plus_next_left ::</span> (<span class="dt">Natural</span> n, <span class="dt">Equal</span> n)</a>
<a class="sourceLine" id="cb3-9" data-line-number="9">  <span class="ot">=&gt;</span> <span class="dt">Proxy</span> n <span class="ot">-&gt;</span> (n <span class="ot">-&gt;</span> n <span class="ot">-&gt;</span> n) <span class="ot">-&gt;</span> <span class="dt">Test</span> (n <span class="ot">-&gt;</span> n <span class="ot">-&gt;</span> <span class="dt">Bool</span>)</a>
<a class="sourceLine" id="cb3-10" data-line-number="10">_test_plus_next_left _ f <span class="fu">=</span></a>
<a class="sourceLine" id="cb3-11" data-line-number="11">  testName <span class="st">&quot;f(next(a),b) == next(f(a,b))&quot;</span> <span class="fu">$</span></a>
<a class="sourceLine" id="cb3-12" data-line-number="12">  \a b <span class="ot">-&gt;</span> eq (f (next a) b) (next (f a b))</a></code></pre></div>
</div>
</div>
<p>Next we establish a version of the universal property of <span class="math inline">\(\nplus\)</span> with the arguments reversed.</p>
<div class="theorem">
<p><span id="thm-plus-zero-right"></span><span id="thm-plus-next-right"></span> The following hold for all natural numbers <span class="math inline">\(a\)</span> and <span class="math inline">\(b\)</span>.</p>
<ol type="1">
<li><span class="math inline">\(\nplus(a,\zero) = a\)</span>.</li>
<li><span class="math inline">\(\nplus(a,\next(b)) = \next(\nplus(a,b))\)</span>.</li>
</ol>
<div class="proof">
<ol type="1">
<li>We proceed by induction on <span class="math inline">\(a\)</span>. For the base case, we have <span class="math inline">\(\nplus(\zero,\zero) = \zero\)</span> by the universal property of <span class="math inline">\(\nplus\)</span>. For the inductive step, suppose we have <span class="math inline">\(\nplus(a,\zero) = a\)</span> for some <span class="math inline">\(a \in \nats\)</span>. Then <span class="math display">\[\begin{eqnarray*}
 &amp;   &amp; \nplus(\next(a),\zero) \\
 &amp;     \href{/posts/arithmetic-made-difficult/Plus.html#cor-plus-up-next}
= &amp; \next(\nplus(a,\zero)) \\
 &amp;     \hyp{\nplus(a,\zero) = a}
= &amp; \next(a)
\end{eqnarray*}\]</span> as needed.</li>
<li>We proceed by induction on <span class="math inline">\(a\)</span>. For the base case, note that <span class="math display">\[\nplus(\zero,\next(b)) = \next(b).\]</span> For the inductive step, suppose we have <span class="math inline">\(\next(\nplus(a,b)) = \nplus(a,\next(b))\)</span> for all <span class="math inline">\(b\)</span> for some <span class="math inline">\(a\)</span>. Then <span class="math display">\[\begin{eqnarray*}
 &amp;   &amp; \nplus(\next(a),\next(b)) \\
 &amp;     \href{/posts/arithmetic-made-difficult/Plus.html#cor-plus-up-next}
= &amp; \next(\nplus(a,\next(b))) \\
 &amp;     \hyp{\next(\nplus(a,b)) = \nplus(a,\next(b))}
= &amp; \next(\next(\nplus(a,b))) \\
 &amp;     \href{/posts/arithmetic-made-difficult/Plus.html#cor-plus-up-next}
= &amp; \next(\nplus(\next(a),b))
\end{eqnarray*}\]</span> as needed.</li>
</ol>
</div>
<div class="test">
<div class="sourceCode" id="cb4"><pre class="sourceCode literate haskell"><code class="sourceCode haskell"><a class="sourceLine" id="cb4-1" data-line-number="1"><span class="ot">_test_plus_zero_right ::</span> (<span class="dt">Natural</span> n, <span class="dt">Equal</span> n)</a>
<a class="sourceLine" id="cb4-2" data-line-number="2">  <span class="ot">=&gt;</span> <span class="dt">Proxy</span> n <span class="ot">-&gt;</span> (n <span class="ot">-&gt;</span> n <span class="ot">-&gt;</span> n) <span class="ot">-&gt;</span> <span class="dt">Test</span> (n <span class="ot">-&gt;</span> <span class="dt">Bool</span>)</a>
<a class="sourceLine" id="cb4-3" data-line-number="3">_test_plus_zero_right _ f <span class="fu">=</span></a>
<a class="sourceLine" id="cb4-4" data-line-number="4">  testName <span class="st">&quot;plus(a,0) == a&quot;</span> <span class="fu">$</span></a>
<a class="sourceLine" id="cb4-5" data-line-number="5">  \a <span class="ot">-&gt;</span> eq (f a zero) a</a>
<a class="sourceLine" id="cb4-6" data-line-number="6"></a>
<a class="sourceLine" id="cb4-7" data-line-number="7"></a>
<a class="sourceLine" id="cb4-8" data-line-number="8"><span class="ot">_test_plus_next_right ::</span> (<span class="dt">Natural</span> n, <span class="dt">Equal</span> n)</a>
<a class="sourceLine" id="cb4-9" data-line-number="9">  <span class="ot">=&gt;</span> <span class="dt">Proxy</span> n <span class="ot">-&gt;</span> (n <span class="ot">-&gt;</span> n <span class="ot">-&gt;</span> n) <span class="ot">-&gt;</span> <span class="dt">Test</span> (n <span class="ot">-&gt;</span> n <span class="ot">-&gt;</span> <span class="dt">Bool</span>)</a>
<a class="sourceLine" id="cb4-10" data-line-number="10">_test_plus_next_right _ f <span class="fu">=</span></a>
<a class="sourceLine" id="cb4-11" data-line-number="11">  testName <span class="st">&quot;next(plus(a,b)) == plus(a,next(b))&quot;</span> <span class="fu">$</span></a>
<a class="sourceLine" id="cb4-12" data-line-number="12">  \a b <span class="ot">-&gt;</span> eq (f a (next b)) (next (f a b))</a></code></pre></div>
</div>
</div>
<p><span class="math inline">\(\nplus\)</span> is associative and commutative.</p>
<div class="theorem">
<p><span id="thm-plus-associative"></span><span id="thm-plus-commutative"></span> The following hold for all natural numbers <span class="math inline">\(a\)</span>, <span class="math inline">\(b\)</span>, and <span class="math inline">\(c\)</span>.</p>
<ol type="1">
<li><span class="math inline">\(\nplus(\nplus(a,b),c) = \nplus(a,\nplus(b,c))\)</span>.</li>
<li><span class="math inline">\(\nplus(a,b) = \nplus(b,a)\)</span>.</li>
</ol>
<div class="proof">
<ol type="1">
<li>We will show this by induction on <span class="math inline">\(a\)</span>. For the base case, note that <span class="math display">\[\nplus(\nplus(\zero,b),c) = \nplus(b,c) = \nplus(\zero,\nplus(b,c)).\]</span> For the inductive step, suppose the result holds for some <span class="math inline">\(a\)</span>. Then <span class="math display">\[\begin{eqnarray*}
 &amp;   &amp; \nplus(\nplus(\next(a),b),c) \\
 &amp;     \href{/posts/arithmetic-made-difficult/Plus.html#cor-plus-up-next}
= &amp; \nplus(\next(\nplus(a,b)),c) \\
 &amp;     \href{/posts/arithmetic-made-difficult/Plus.html#cor-plus-up-next}
= &amp; \next(\nplus(\nplus(a,b),c)) \\
 &amp;     \hyp{\nplus(a,\nplus(b,c)) = \nplus(\nplus(a,b),c)}
= &amp; \next(\nplus(a,\nplus(b,c))) \\
 &amp;     \href{/posts/arithmetic-made-difficult/Plus.html#cor-plus-up-next}
= &amp; \nplus(\next(a),\nplus(b,c))
\end{eqnarray*}\]</span> as needed.</li>
<li>We proceed by induction on <span class="math inline">\(a\)</span>. For the base case, note that <span class="math display">\[\nplus(\zero,b) = b = \nplus(b,\zero).\]</span> For the inductive step, suppose the result holds for some <span class="math inline">\(a\)</span>. Then we have <span class="math display">\[\begin{eqnarray*}
 &amp;   &amp; \nplus(\next(a),b) \\
 &amp;     \href{/posts/arithmetic-made-difficult/Plus.html#cor-plus-up-next}
= &amp; \next(\nplus(a,b)) \\
 &amp;     \hyp{\nplus(a,b) = \nplus(b,a)}
= &amp; \next(\nplus(b,a)) \\
 &amp;     \href{/posts/arithmetic-made-difficult/Plus.html#thm-plus-next-right}
= &amp; \nplus(b,\next(a))
\end{eqnarray*}\]</span> as needed.</li>
</ol>
</div>
<div class="test">
<div class="sourceCode" id="cb5"><pre class="sourceCode literate haskell"><code class="sourceCode haskell"><a class="sourceLine" id="cb5-1" data-line-number="1"><span class="ot">_test_plus_associative ::</span> (<span class="dt">Natural</span> n, <span class="dt">Equal</span> n)</a>
<a class="sourceLine" id="cb5-2" data-line-number="2">  <span class="ot">=&gt;</span> <span class="dt">Proxy</span> n <span class="ot">-&gt;</span> (n <span class="ot">-&gt;</span> n <span class="ot">-&gt;</span> n) <span class="ot">-&gt;</span> <span class="dt">Test</span> (n <span class="ot">-&gt;</span> n <span class="ot">-&gt;</span> n <span class="ot">-&gt;</span> <span class="dt">Bool</span>)</a>
<a class="sourceLine" id="cb5-3" data-line-number="3">_test_plus_associative _ f <span class="fu">=</span></a>
<a class="sourceLine" id="cb5-4" data-line-number="4">  testName <span class="st">&quot;plus(plus(a,b),c) == plus(a,plus(b,c))&quot;</span> <span class="fu">$</span></a>
<a class="sourceLine" id="cb5-5" data-line-number="5">  \a b c <span class="ot">-&gt;</span> eq (f (f a b) c) (f a (f b c))</a>
<a class="sourceLine" id="cb5-6" data-line-number="6"></a>
<a class="sourceLine" id="cb5-7" data-line-number="7"></a>
<a class="sourceLine" id="cb5-8" data-line-number="8"><span class="ot">_test_plus_commutative ::</span> (<span class="dt">Natural</span> n, <span class="dt">Equal</span> n)</a>
<a class="sourceLine" id="cb5-9" data-line-number="9">  <span class="ot">=&gt;</span> <span class="dt">Proxy</span> n <span class="ot">-&gt;</span> (n <span class="ot">-&gt;</span> n <span class="ot">-&gt;</span> n) <span class="ot">-&gt;</span> <span class="dt">Test</span> (n <span class="ot">-&gt;</span> n <span class="ot">-&gt;</span> <span class="dt">Bool</span>)</a>
<a class="sourceLine" id="cb5-10" data-line-number="10">_test_plus_commutative _ f <span class="fu">=</span></a>
<a class="sourceLine" id="cb5-11" data-line-number="11">  testName <span class="st">&quot;plus(a,b) == plus(b,a)&quot;</span> <span class="fu">$</span></a>
<a class="sourceLine" id="cb5-12" data-line-number="12">  \a b <span class="ot">-&gt;</span> eq (f a b) (f b a)</a></code></pre></div>
</div>
</div>
<p>And <span class="math inline">\(\nplus\)</span> is cancellative.</p>
<div class="theorem">
<p><span id="thm-plus-left-cancel"></span><span id="thm-plus-right-cancel"></span> The following hold for all natural numbers <span class="math inline">\(a\)</span>, <span class="math inline">\(b\)</span>, and <span class="math inline">\(c\)</span>.</p>
<ol type="1">
<li>If <span class="math inline">\(\nplus(c,a) = \nplus(c,b)\)</span> then <span class="math inline">\(a = b\)</span>.</li>
<li>If <span class="math inline">\(\nplus(a,c) = \nplus(b,c)\)</span> then <span class="math inline">\(a = b\)</span>.</li>
</ol>
<div class="proof">
<ol type="1">
<li>We proceed by induction on <span class="math inline">\(c\)</span>. For the base case, note that if <span class="math inline">\(\nplus(\zero,a) = \nplus(\zero,b)\)</span>, then we have <span class="math display">\[a = \nplus(\zero,a) = \nplus(\zero,b) = b.\]</span> For the inductive step, suppose the result holds for some <span class="math inline">\(c\)</span>. Now if <span class="math display">\[\nplus(\next(c),a) = \nplus(\next(c),b),\]</span> then <span class="math display">\[\next(\nplus(c,a)) = \next(\nplus(c,b))\]</span> so that <span class="math display">\[\nplus(c,a) = \nplus(c,b)\]</span> and thus <span class="math inline">\(a = b\)</span> as needed.</li>
<li>If <span class="math display">\[\nplus(a,c) = \nplus(b,c),\]</span> then <span class="math display">\[\nplus(c,a) = \nplus(c,b),\]</span> and so <span class="math inline">\(a = b\)</span> as claimed.</li>
</ol>
</div>
<div class="test">
<div class="sourceCode" id="cb6"><pre class="sourceCode literate haskell"><code class="sourceCode haskell"><a class="sourceLine" id="cb6-1" data-line-number="1"><span class="ot">_test_plus_cancellative_left ::</span> (<span class="dt">Natural</span> n, <span class="dt">Equal</span> n)</a>
<a class="sourceLine" id="cb6-2" data-line-number="2">  <span class="ot">=&gt;</span> <span class="dt">Proxy</span> n <span class="ot">-&gt;</span> (n <span class="ot">-&gt;</span> n <span class="ot">-&gt;</span> n) <span class="ot">-&gt;</span> <span class="dt">Test</span> (n <span class="ot">-&gt;</span> n <span class="ot">-&gt;</span> n <span class="ot">-&gt;</span> <span class="dt">Bool</span>)</a>
<a class="sourceLine" id="cb6-3" data-line-number="3">_test_plus_cancellative_left _ f <span class="fu">=</span></a>
<a class="sourceLine" id="cb6-4" data-line-number="4">  testName <span class="st">&quot;if plus(c,a) == plus(c,b) then a == b&quot;</span> <span class="fu">$</span></a>
<a class="sourceLine" id="cb6-5" data-line-number="5">  \a b c <span class="ot">-&gt;</span> <span class="kw">if</span> eq (f c a) (f c b)</a>
<a class="sourceLine" id="cb6-6" data-line-number="6">    <span class="kw">then</span> eq a b</a>
<a class="sourceLine" id="cb6-7" data-line-number="7">    <span class="kw">else</span> true</a>
<a class="sourceLine" id="cb6-8" data-line-number="8"></a>
<a class="sourceLine" id="cb6-9" data-line-number="9"></a>
<a class="sourceLine" id="cb6-10" data-line-number="10"><span class="ot">_test_plus_cancellative_right ::</span> (<span class="dt">Natural</span> n, <span class="dt">Equal</span> n)</a>
<a class="sourceLine" id="cb6-11" data-line-number="11">  <span class="ot">=&gt;</span> <span class="dt">Proxy</span> n <span class="ot">-&gt;</span> (n <span class="ot">-&gt;</span> n <span class="ot">-&gt;</span> n) <span class="ot">-&gt;</span> <span class="dt">Test</span> (n <span class="ot">-&gt;</span> n <span class="ot">-&gt;</span> n <span class="ot">-&gt;</span> <span class="dt">Bool</span>)</a>
<a class="sourceLine" id="cb6-12" data-line-number="12">_test_plus_cancellative_right _ f <span class="fu">=</span></a>
<a class="sourceLine" id="cb6-13" data-line-number="13">  testName <span class="st">&quot;if plus(a,c) == plus(b,c) then a == b&quot;</span> <span class="fu">$</span></a>
<a class="sourceLine" id="cb6-14" data-line-number="14">  \a b c <span class="ot">-&gt;</span> <span class="kw">if</span> eq (f a c) (f b c)</a>
<a class="sourceLine" id="cb6-15" data-line-number="15">    <span class="kw">then</span> eq a b</a>
<a class="sourceLine" id="cb6-16" data-line-number="16">    <span class="kw">else</span> true</a></code></pre></div>
</div>
</div>
<p>Of course we will eventually prefer to say <span class="math inline">\(a + b\)</span> instead of <span class="math inline">\(\nplus(a,b)\)</span>. But we’ll avoid the more familiar notation until we’re convinced that <span class="math inline">\(\nplus\)</span> really does act just like the usual <span class="math inline">\(+\)</span>, since familiar notation can easily lull us into using theorems we haven’t proven yet.</p>
<h2 id="testing">Testing</h2>
<p>Suite:</p>
<div class="sourceCode" id="cb7"><pre class="sourceCode literate haskell"><code class="sourceCode haskell"><a class="sourceLine" id="cb7-1" data-line-number="1">_test_plus</a>
<a class="sourceLine" id="cb7-2" data-line-number="2"><span class="ot">  ::</span> (<span class="dt">Typeable</span> n, <span class="dt">Natural</span> n, <span class="dt">Equal</span> n, <span class="dt">Show</span> n, <span class="dt">Arbitrary</span> n)</a>
<a class="sourceLine" id="cb7-3" data-line-number="3">  <span class="ot">=&gt;</span> <span class="dt">Int</span> <span class="ot">-&gt;</span> <span class="dt">Int</span> <span class="ot">-&gt;</span> <span class="dt">Proxy</span> n <span class="ot">-&gt;</span> (n <span class="ot">-&gt;</span> n <span class="ot">-&gt;</span> n) <span class="ot">-&gt;</span> <span class="dt">IO</span> ()</a>
<a class="sourceLine" id="cb7-4" data-line-number="4">_test_plus size cases pn f <span class="fu">=</span> <span class="kw">do</span></a>
<a class="sourceLine" id="cb7-5" data-line-number="5">  labelTestArgs1 <span class="st">&quot;plus&quot;</span> pn</a>
<a class="sourceLine" id="cb7-6" data-line-number="6">  <span class="kw">let</span> args <span class="fu">=</span> testArgs size cases</a>
<a class="sourceLine" id="cb7-7" data-line-number="7"></a>
<a class="sourceLine" id="cb7-8" data-line-number="8">  runTest args (_test_plus_zero_left pn f)</a>
<a class="sourceLine" id="cb7-9" data-line-number="9">  runTest args (_test_plus_next_left pn f)</a>
<a class="sourceLine" id="cb7-10" data-line-number="10">  runTest args (_test_plus_zero_right pn f)</a>
<a class="sourceLine" id="cb7-11" data-line-number="11">  runTest args (_test_plus_next_right pn f)</a>
<a class="sourceLine" id="cb7-12" data-line-number="12">  runTest args (_test_plus_associative pn f)</a>
<a class="sourceLine" id="cb7-13" data-line-number="13">  runTest args (_test_plus_commutative pn f)</a>
<a class="sourceLine" id="cb7-14" data-line-number="14">  runTest args (_test_plus_cancellative_left pn f)</a>
<a class="sourceLine" id="cb7-15" data-line-number="15">  runTest args (_test_plus_cancellative_right pn f)</a></code></pre></div>
<p>Main:</p>
<div class="sourceCode" id="cb8"><pre class="sourceCode literate haskell"><code class="sourceCode haskell"><a class="sourceLine" id="cb8-1" data-line-number="1"><span class="ot">main_plus ::</span> <span class="dt">IO</span> ()</a>
<a class="sourceLine" id="cb8-2" data-line-number="2">main_plus <span class="fu">=</span> <span class="kw">do</span></a>
<a class="sourceLine" id="cb8-3" data-line-number="3">  _test_plus <span class="dv">100</span> <span class="dv">100</span> (<span class="dt">Proxy</span><span class="ot"> ::</span> <span class="dt">Proxy</span> <span class="dt">Unary</span>) plus</a></code></pre></div>



<!-- END CONTENT -->
</div>

<div id="footer"></div>
</body>
</html>
