1258 lines
133 KiB
HTML
1258 lines
133 KiB
HTML
<!DOCTYPE html>
|
||
<html lang="en"><head>
|
||
<meta charset="utf-8">
|
||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||
<meta name="viewport" content="width=device-width, initial-scale=1">
|
||
<title>Induction: Proof by Induction | Programming Language Foundations in Agda
|
||
</title><!-- Begin Jekyll SEO tag v2.6.1 -->
|
||
<meta name="generator" content="Jekyll v3.9.0" />
|
||
<meta property="og:title" content="Induction: Proof by Induction" />
|
||
<meta property="og:locale" content="en_US" />
|
||
<meta name="description" content="Programming Language Foundations in Agda" />
|
||
<meta property="og:description" content="Programming Language Foundations in Agda" />
|
||
<link rel="canonical" href="https://plfa.github.io/20.07/Induction/" />
|
||
<meta property="og:url" content="https://plfa.github.io/20.07/Induction/" />
|
||
<meta property="og:site_name" content="Programming Language Foundations in Agda" />
|
||
<script type="application/ld+json">
|
||
{"url":"https://plfa.github.io/20.07/Induction/","headline":"Induction: Proof by Induction","description":"Programming Language Foundations in Agda","@type":"WebPage","@context":"https://schema.org"}</script>
|
||
<!-- End Jekyll SEO tag -->
|
||
<link rel="stylesheet" href="/20.07/assets/main.css"></head>
|
||
<body><header class="site-header" role="banner">
|
||
|
||
<div class="wrapper">
|
||
|
||
<a class="site-title" href="/20.07/">Programming Language Foundations in Agda
|
||
</a>
|
||
|
||
<nav class="site-nav">
|
||
<span class="menu-icon">
|
||
<svg viewBox="0 0 18 15" width="18px" height="15px">
|
||
<path fill="#424242" d="M18,1.484c0,0.82-0.665,1.484-1.484,1.484H1.484C0.665,2.969,0,2.304,0,1.484l0,0C0,0.665,0.665,0,1.484,0 h15.031C17.335,0,18,0.665,18,1.484L18,1.484z"/>
|
||
<path fill="#424242" d="M18,7.516C18,8.335,17.335,9,16.516,9H1.484C0.665,9,0,8.335,0,7.516l0,0c0-0.82,0.665-1.484,1.484-1.484 h15.031C17.335,6.031,18,6.696,18,7.516L18,7.516z"/>
|
||
<path fill="#424242" d="M18,13.516C18,14.335,17.335,15,16.516,15H1.484C0.665,15,0,14.335,0,13.516l0,0 c0-0.82,0.665-1.484,1.484-1.484h15.031C17.335,12.031,18,12.696,18,13.516L18,13.516z"/>
|
||
</svg>
|
||
</span>
|
||
|
||
<div class="trigger">
|
||
<a class="page-link" href="/20.07/">The Book</a>
|
||
<a class="page-link" href="/20.07/Announcements/">Announcements</a>
|
||
<a class="page-link" href="/20.07/GettingStarted/">Getting Started</a>
|
||
<a class="page-link" href="/20.07/Citing/">Citing</a>
|
||
<a class="page-link" href="https://agda-zh.github.io/PLFA-zh/">中文</a>
|
||
</div>
|
||
</nav>
|
||
|
||
</div>
|
||
|
||
</header>
|
||
<main class="page-content" aria-label="Content">
|
||
<div class="wrapper">
|
||
<article class="post">
|
||
|
||
<header class="post-header">
|
||
<h1 class="post-title">Induction: Proof by Induction</h1>
|
||
</header>
|
||
|
||
<p style="text-align:center;">
|
||
|
||
<a alt="Previous chapter" href="/20.07/Naturals/">Prev</a>
|
||
|
||
|
||
•
|
||
|
||
|
||
<a alt="Source code" href="https://github.com/plfa/plfa.github.io/blob/dev-20.07/src/plfa/part1/Induction.lagda.md">Source</a>
|
||
|
||
|
||
•
|
||
|
||
|
||
<a alt="Next chapter" href="/20.07/Relations/">Next</a>
|
||
|
||
</p>
|
||
|
||
|
||
<div class="post-content">
|
||
<pre class="Agda"><a id="146" class="Keyword">module</a> <a id="153" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html" class="Module">plfa.part1.Induction</a> <a id="174" class="Keyword">where</a>
|
||
</pre>
|
||
<blockquote>
|
||
<p>Induction makes you feel guilty for getting something out of nothing
|
||
… but it is one of the greatest ideas of civilization.
|
||
– Herbert Wilf</p>
|
||
</blockquote>
|
||
|
||
<p>Now that we’ve defined the naturals and operations upon them, our next
|
||
step is to learn how to prove properties that they satisfy. As hinted
|
||
by their name, properties of <em>inductive datatypes</em> are proved by
|
||
<em>induction</em>.</p>
|
||
|
||
<h2 id="imports">Imports</h2>
|
||
|
||
<p>We require equality as in the previous chapter, plus the naturals
|
||
and some operations upon them. We also import a couple of new operations,
|
||
<code class="language-plaintext highlighter-rouge">cong</code>, <code class="language-plaintext highlighter-rouge">sym</code>, and <code class="language-plaintext highlighter-rouge">_≡⟨_⟩_</code>, which are explained below:</p>
|
||
<pre class="Agda"><a id="769" class="Keyword">import</a> <a id="776" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.html" class="Module">Relation.Binary.PropositionalEquality</a> <a id="814" class="Symbol">as</a> <a id="817" class="Module">Eq</a>
|
||
<a id="820" class="Keyword">open</a> <a id="825" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.html" class="Module">Eq</a> <a id="828" class="Keyword">using</a> <a id="834" class="Symbol">(</a><a id="835" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">_≡_</a><a id="838" class="Symbol">;</a> <a id="840" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a><a id="844" class="Symbol">;</a> <a id="846" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#1090" class="Function">cong</a><a id="850" class="Symbol">;</a> <a id="852" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#939" class="Function">sym</a><a id="855" class="Symbol">)</a>
|
||
<a id="857" class="Keyword">open</a> <a id="862" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2499" class="Module">Eq.≡-Reasoning</a> <a id="877" class="Keyword">using</a> <a id="883" class="Symbol">(</a><a id="884" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2597" class="Function Operator">begin_</a><a id="890" class="Symbol">;</a> <a id="892" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">_≡⟨⟩_</a><a id="897" class="Symbol">;</a> <a id="899" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">_≡⟨_⟩_</a><a id="905" class="Symbol">;</a> <a id="907" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2892" class="Function Operator">_∎</a><a id="909" class="Symbol">)</a>
|
||
<a id="911" class="Keyword">open</a> <a id="916" class="Keyword">import</a> <a id="923" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.html" class="Module">Data.Nat</a> <a id="932" class="Keyword">using</a> <a id="938" class="Symbol">(</a><a id="939" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="940" class="Symbol">;</a> <a id="942" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">zero</a><a id="946" class="Symbol">;</a> <a id="948" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a><a id="951" class="Symbol">;</a> <a id="953" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">_+_</a><a id="956" class="Symbol">;</a> <a id="958" href="Agda.Builtin.Nat.html#501" class="Primitive Operator">_*_</a><a id="961" class="Symbol">;</a> <a id="963" href="Agda.Builtin.Nat.html#388" class="Primitive Operator">_∸_</a><a id="966" class="Symbol">)</a>
|
||
</pre>
|
||
|
||
<h2 id="properties-of-operators">Properties of operators</h2>
|
||
|
||
<p>Operators pop up all the time, and mathematicians have agreed
|
||
on names for some of the most common properties.</p>
|
||
|
||
<ul>
|
||
<li>
|
||
<p><em>Identity</em>. Operator <code class="language-plaintext highlighter-rouge">+</code> has left identity <code class="language-plaintext highlighter-rouge">0</code> if <code class="language-plaintext highlighter-rouge">0 + n ≡ n</code>, and
|
||
right identity <code class="language-plaintext highlighter-rouge">0</code> if <code class="language-plaintext highlighter-rouge">n + 0 ≡ n</code>, for all <code class="language-plaintext highlighter-rouge">n</code>. A value that is both
|
||
a left and right identity is just called an identity. Identity is also
|
||
sometimes called <em>unit</em>.</p>
|
||
</li>
|
||
<li>
|
||
<p><em>Associativity</em>. Operator <code class="language-plaintext highlighter-rouge">+</code> is associative if the location
|
||
of parentheses does not matter: <code class="language-plaintext highlighter-rouge">(m + n) + p ≡ m + (n + p)</code>,
|
||
for all <code class="language-plaintext highlighter-rouge">m</code>, <code class="language-plaintext highlighter-rouge">n</code>, and <code class="language-plaintext highlighter-rouge">p</code>.</p>
|
||
</li>
|
||
<li>
|
||
<p><em>Commutativity</em>. Operator <code class="language-plaintext highlighter-rouge">+</code> is commutative if order of
|
||
arguments does not matter: <code class="language-plaintext highlighter-rouge">m + n ≡ n + m</code>, for all <code class="language-plaintext highlighter-rouge">m</code> and <code class="language-plaintext highlighter-rouge">n</code>.</p>
|
||
</li>
|
||
<li>
|
||
<p><em>Distributivity</em>. Operator <code class="language-plaintext highlighter-rouge">*</code> distributes over operator <code class="language-plaintext highlighter-rouge">+</code> from the
|
||
left if <code class="language-plaintext highlighter-rouge">(m + n) * p ≡ (m * p) + (n * p)</code>, for all <code class="language-plaintext highlighter-rouge">m</code>, <code class="language-plaintext highlighter-rouge">n</code>, and <code class="language-plaintext highlighter-rouge">p</code>,
|
||
and from the right if <code class="language-plaintext highlighter-rouge">m * (p + q) ≡ (m * p) + (m * q)</code>, for all <code class="language-plaintext highlighter-rouge">m</code>,
|
||
<code class="language-plaintext highlighter-rouge">p</code>, and <code class="language-plaintext highlighter-rouge">q</code>.</p>
|
||
</li>
|
||
</ul>
|
||
|
||
<p>Addition has identity <code class="language-plaintext highlighter-rouge">0</code> and multiplication has identity <code class="language-plaintext highlighter-rouge">1</code>;
|
||
addition and multiplication are both associative and commutative;
|
||
and multiplication distributes over addition.</p>
|
||
|
||
<p>If you ever bump into an operator at a party, you now know how
|
||
to make small talk, by asking whether it has a unit and is
|
||
associative or commutative. If you bump into two operators, you
|
||
might ask them if one distributes over the other.</p>
|
||
|
||
<p>Less frivolously, if you ever bump into an operator while reading a
|
||
technical paper, this gives you a way to orient yourself, by checking
|
||
whether or not it has an identity, is associative or commutative, or
|
||
distributes over another operator. A careful author will often call
|
||
out these properties—or their lack—for instance by pointing out
|
||
that a newly introduced operator is associative but not commutative.</p>
|
||
|
||
<h4 id="operators">Exercise <code class="language-plaintext highlighter-rouge">operators</code> (practice)</h4>
|
||
|
||
<p>Give another example of a pair of operators that have an identity
|
||
and are associative, commutative, and distribute over one another.
|
||
(You do not have to prove these properties.)</p>
|
||
|
||
<p>Give an example of an operator that has an identity and is
|
||
associative but is not commutative.
|
||
(You do not have to prove these properties.)</p>
|
||
|
||
<h2 id="associativity">Associativity</h2>
|
||
|
||
<p>One property of addition is that it is <em>associative</em>, that is, that the
|
||
location of the parentheses does not matter:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>(m + n) + p ≡ m + (n + p)
|
||
</code></pre></div></div>
|
||
|
||
<p>Here <code class="language-plaintext highlighter-rouge">m</code>, <code class="language-plaintext highlighter-rouge">n</code>, and <code class="language-plaintext highlighter-rouge">p</code> are variables that range over all natural numbers.</p>
|
||
|
||
<p>We can test the proposition by choosing specific numbers for the three
|
||
variables:</p>
|
||
<pre class="Agda"><a id="3407" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#3407" class="Function">_</a> <a id="3409" class="Symbol">:</a> <a id="3411" class="Symbol">(</a><a id="3412" class="Number">3</a> <a id="3414" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="3416" class="Number">4</a><a id="3417" class="Symbol">)</a> <a id="3419" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="3421" class="Number">5</a> <a id="3423" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="3425" class="Number">3</a> <a id="3427" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="3429" class="Symbol">(</a><a id="3430" class="Number">4</a> <a id="3432" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="3434" class="Number">5</a><a id="3435" class="Symbol">)</a>
|
||
<a id="3437" class="Symbol">_</a> <a id="3439" class="Symbol">=</a>
|
||
<a id="3443" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2597" class="Function Operator">begin</a>
|
||
<a id="3453" class="Symbol">(</a><a id="3454" class="Number">3</a> <a id="3456" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="3458" class="Number">4</a><a id="3459" class="Symbol">)</a> <a id="3461" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="3463" class="Number">5</a>
|
||
<a id="3467" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
|
||
<a id="3475" class="Number">7</a> <a id="3477" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="3479" class="Number">5</a>
|
||
<a id="3483" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
|
||
<a id="3491" class="Number">12</a>
|
||
<a id="3496" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
|
||
<a id="3504" class="Number">3</a> <a id="3506" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="3508" class="Number">9</a>
|
||
<a id="3512" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
|
||
<a id="3520" class="Number">3</a> <a id="3522" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="3524" class="Symbol">(</a><a id="3525" class="Number">4</a> <a id="3527" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="3529" class="Number">5</a><a id="3530" class="Symbol">)</a>
|
||
<a id="3534" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2892" class="Function Operator">∎</a>
|
||
</pre>
|
||
<p>Here we have displayed the computation as a chain of equations,
|
||
one term to a line. It is often easiest to read such chains from the top down
|
||
until one reaches the simplest term (in this case, <code class="language-plaintext highlighter-rouge">12</code>), and
|
||
then from the bottom up until one reaches the same term.</p>
|
||
|
||
<p>The test reveals that associativity is perhaps not as obvious as first
|
||
it appears. Why should <code class="language-plaintext highlighter-rouge">7 + 5</code> be the same as <code class="language-plaintext highlighter-rouge">3 + 9</code>? We might want
|
||
to gather more evidence, testing the proposition by choosing other
|
||
numbers. But—since there are an infinite number of
|
||
naturals—testing can never be complete. Is there any way we can be
|
||
sure that associativity holds for <em>all</em> the natural numbers?</p>
|
||
|
||
<p>The answer is yes! We can prove a property holds for all naturals using
|
||
<em>proof by induction</em>.</p>
|
||
|
||
<h2 id="proof-by-induction">Proof by induction</h2>
|
||
|
||
<p>Recall the definition of natural numbers consists of a <em>base case</em>
|
||
which tells us that <code class="language-plaintext highlighter-rouge">zero</code> is a natural, and an <em>inductive case</em>
|
||
which tells us that if <code class="language-plaintext highlighter-rouge">m</code> is a natural then <code class="language-plaintext highlighter-rouge">suc m</code> is also a natural.</p>
|
||
|
||
<p>Proof by induction follows the structure of this definition. To prove
|
||
a property of natural numbers by induction, we need to prove two cases.
|
||
First is the <em>base case</em>, where we show the property holds for <code class="language-plaintext highlighter-rouge">zero</code>.
|
||
Second is the <em>inductive case</em>, where we assume the property holds for
|
||
an arbitrary natural <code class="language-plaintext highlighter-rouge">m</code> (we call this the <em>inductive hypothesis</em>), and
|
||
then show that the property must also hold for <code class="language-plaintext highlighter-rouge">suc m</code>.</p>
|
||
|
||
<p>If we write <code class="language-plaintext highlighter-rouge">P m</code> for a property of <code class="language-plaintext highlighter-rouge">m</code>, then what we need to
|
||
demonstrate are the following two inference rules:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>------
|
||
P zero
|
||
|
||
P m
|
||
---------
|
||
P (suc m)
|
||
</code></pre></div></div>
|
||
|
||
<p>Let’s unpack these rules. The first rule is the base case, and
|
||
requires we show that property <code class="language-plaintext highlighter-rouge">P</code> holds for <code class="language-plaintext highlighter-rouge">zero</code>. The second rule
|
||
is the inductive case, and requires we show that if we assume the
|
||
inductive hypothesis—namely that <code class="language-plaintext highlighter-rouge">P</code> holds for <code class="language-plaintext highlighter-rouge">m</code>—then it follows that
|
||
<code class="language-plaintext highlighter-rouge">P</code> also holds for <code class="language-plaintext highlighter-rouge">suc m</code>.</p>
|
||
|
||
<p>Why does this work? Again, it can be explained by a creation story.
|
||
To start with, we know no properties:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>-- In the beginning, no properties are known.
|
||
</code></pre></div></div>
|
||
|
||
<p>Now, we apply the two rules to all the properties we know about. The
|
||
base case tells us that <code class="language-plaintext highlighter-rouge">P zero</code> holds, so we add it to the set of
|
||
known properties. The inductive case tells us that if <code class="language-plaintext highlighter-rouge">P m</code> holds (on
|
||
the day before today) then <code class="language-plaintext highlighter-rouge">P (suc m)</code> also holds (today). We didn’t
|
||
know about any properties before today, so the inductive case doesn’t
|
||
apply:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>-- On the first day, one property is known.
|
||
P zero
|
||
</code></pre></div></div>
|
||
|
||
<p>Then we repeat the process, so on the next day we know about all the
|
||
properties from the day before, plus any properties added by the rules.
|
||
The base case tells us that <code class="language-plaintext highlighter-rouge">P zero</code> holds, but we already
|
||
knew that. But now the inductive case tells us that since <code class="language-plaintext highlighter-rouge">P zero</code>
|
||
held yesterday, then <code class="language-plaintext highlighter-rouge">P (suc zero)</code> holds today:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>-- On the second day, two properties are known.
|
||
P zero
|
||
P (suc zero)
|
||
</code></pre></div></div>
|
||
|
||
<p>And we repeat the process again. Now the inductive case
|
||
tells us that since <code class="language-plaintext highlighter-rouge">P zero</code> and <code class="language-plaintext highlighter-rouge">P (suc zero)</code> both hold, then
|
||
<code class="language-plaintext highlighter-rouge">P (suc zero)</code> and <code class="language-plaintext highlighter-rouge">P (suc (suc zero))</code> also hold. We already knew about
|
||
the first of these, but the second is new:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>-- On the third day, three properties are known.
|
||
P zero
|
||
P (suc zero)
|
||
P (suc (suc zero))
|
||
</code></pre></div></div>
|
||
|
||
<p>You’ve got the hang of it by now:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>-- On the fourth day, four properties are known.
|
||
P zero
|
||
P (suc zero)
|
||
P (suc (suc zero))
|
||
P (suc (suc (suc zero)))
|
||
</code></pre></div></div>
|
||
|
||
<p>The process continues. On the <em>n</em>‘th day there will be <em>n</em> distinct
|
||
properties that hold. The property of every natural number will appear
|
||
on some given day. In particular, the property <code class="language-plaintext highlighter-rouge">P n</code> first appears on
|
||
day <em>n+1</em>.</p>
|
||
|
||
<h2 id="our-first-proof-associativity">Our first proof: associativity</h2>
|
||
|
||
<p>To prove associativity, we take <code class="language-plaintext highlighter-rouge">P m</code> to be the property:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>(m + n) + p ≡ m + (n + p)
|
||
</code></pre></div></div>
|
||
|
||
<p>Here <code class="language-plaintext highlighter-rouge">n</code> and <code class="language-plaintext highlighter-rouge">p</code> are arbitrary natural numbers, so if we can show the
|
||
equation holds for all <code class="language-plaintext highlighter-rouge">m</code> it will also hold for all <code class="language-plaintext highlighter-rouge">n</code> and <code class="language-plaintext highlighter-rouge">p</code>.
|
||
The appropriate instances of the inference rules are:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>-------------------------------
|
||
(zero + n) + p ≡ zero + (n + p)
|
||
|
||
(m + n) + p ≡ m + (n + p)
|
||
---------------------------------
|
||
(suc m + n) + p ≡ suc m + (n + p)
|
||
</code></pre></div></div>
|
||
|
||
<p>If we can demonstrate both of these, then associativity of addition
|
||
follows by induction.</p>
|
||
|
||
<p>Here is the proposition’s statement and proof:</p>
|
||
<pre class="Agda"><a id="+-assoc"></a><a id="7762" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#7762" class="Function">+-assoc</a> <a id="7770" class="Symbol">:</a> <a id="7772" class="Symbol">∀</a> <a id="7774" class="Symbol">(</a><a id="7775" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#7775" class="Bound">m</a> <a id="7777" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#7777" class="Bound">n</a> <a id="7779" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#7779" class="Bound">p</a> <a id="7781" class="Symbol">:</a> <a id="7783" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="7784" class="Symbol">)</a> <a id="7786" class="Symbol">→</a> <a id="7788" class="Symbol">(</a><a id="7789" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#7775" class="Bound">m</a> <a id="7791" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="7793" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#7777" class="Bound">n</a><a id="7794" class="Symbol">)</a> <a id="7796" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="7798" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#7779" class="Bound">p</a> <a id="7800" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="7802" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#7775" class="Bound">m</a> <a id="7804" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="7806" class="Symbol">(</a><a id="7807" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#7777" class="Bound">n</a> <a id="7809" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="7811" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#7779" class="Bound">p</a><a id="7812" class="Symbol">)</a>
|
||
<a id="7814" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#7762" class="Function">+-assoc</a> <a id="7822" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">zero</a> <a id="7827" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#7827" class="Bound">n</a> <a id="7829" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#7829" class="Bound">p</a> <a id="7831" class="Symbol">=</a>
|
||
<a id="7835" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2597" class="Function Operator">begin</a>
|
||
<a id="7845" class="Symbol">(</a><a id="7846" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">zero</a> <a id="7851" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="7853" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#7827" class="Bound">n</a><a id="7854" class="Symbol">)</a> <a id="7856" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="7858" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#7829" class="Bound">p</a>
|
||
<a id="7862" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
|
||
<a id="7870" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#7827" class="Bound">n</a> <a id="7872" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="7874" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#7829" class="Bound">p</a>
|
||
<a id="7878" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
|
||
<a id="7886" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">zero</a> <a id="7891" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="7893" class="Symbol">(</a><a id="7894" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#7827" class="Bound">n</a> <a id="7896" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="7898" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#7829" class="Bound">p</a><a id="7899" class="Symbol">)</a>
|
||
<a id="7903" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2892" class="Function Operator">∎</a>
|
||
<a id="7905" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#7762" class="Function">+-assoc</a> <a id="7913" class="Symbol">(</a><a id="7914" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="7918" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#7918" class="Bound">m</a><a id="7919" class="Symbol">)</a> <a id="7921" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#7921" class="Bound">n</a> <a id="7923" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#7923" class="Bound">p</a> <a id="7925" class="Symbol">=</a>
|
||
<a id="7929" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2597" class="Function Operator">begin</a>
|
||
<a id="7939" class="Symbol">(</a><a id="7940" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="7944" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#7918" class="Bound">m</a> <a id="7946" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="7948" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#7921" class="Bound">n</a><a id="7949" class="Symbol">)</a> <a id="7951" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="7953" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#7923" class="Bound">p</a>
|
||
<a id="7957" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
|
||
<a id="7965" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="7969" class="Symbol">(</a><a id="7970" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#7918" class="Bound">m</a> <a id="7972" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="7974" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#7921" class="Bound">n</a><a id="7975" class="Symbol">)</a> <a id="7977" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="7979" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#7923" class="Bound">p</a>
|
||
<a id="7983" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
|
||
<a id="7991" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="7995" class="Symbol">((</a><a id="7997" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#7918" class="Bound">m</a> <a id="7999" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="8001" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#7921" class="Bound">n</a><a id="8002" class="Symbol">)</a> <a id="8004" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="8006" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#7923" class="Bound">p</a><a id="8007" class="Symbol">)</a>
|
||
<a id="8011" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">≡⟨</a> <a id="8014" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#1090" class="Function">cong</a> <a id="8019" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="8023" class="Symbol">(</a><a id="8024" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#7762" class="Function">+-assoc</a> <a id="8032" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#7918" class="Bound">m</a> <a id="8034" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#7921" class="Bound">n</a> <a id="8036" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#7923" class="Bound">p</a><a id="8037" class="Symbol">)</a> <a id="8039" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">⟩</a>
|
||
<a id="8045" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="8049" class="Symbol">(</a><a id="8050" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#7918" class="Bound">m</a> <a id="8052" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="8054" class="Symbol">(</a><a id="8055" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#7921" class="Bound">n</a> <a id="8057" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="8059" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#7923" class="Bound">p</a><a id="8060" class="Symbol">))</a>
|
||
<a id="8065" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
|
||
<a id="8073" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="8077" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#7918" class="Bound">m</a> <a id="8079" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="8081" class="Symbol">(</a><a id="8082" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#7921" class="Bound">n</a> <a id="8084" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="8086" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#7923" class="Bound">p</a><a id="8087" class="Symbol">)</a>
|
||
<a id="8091" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2892" class="Function Operator">∎</a>
|
||
</pre>
|
||
<p>We have named the proof <code class="language-plaintext highlighter-rouge">+-assoc</code>. In Agda, identifiers can consist of
|
||
any sequence of characters not including spaces or the characters <code class="language-plaintext highlighter-rouge">@.(){};_</code>.</p>
|
||
|
||
<p>Let’s unpack this code. The signature states that we are
|
||
defining the identifier <code class="language-plaintext highlighter-rouge">+-assoc</code> which provides evidence for the
|
||
proposition:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
|
||
</code></pre></div></div>
|
||
|
||
<p>The upside down A is pronounced “for all”, and the proposition
|
||
asserts that for all natural numbers <code class="language-plaintext highlighter-rouge">m</code>, <code class="language-plaintext highlighter-rouge">n</code>, and <code class="language-plaintext highlighter-rouge">p</code>
|
||
the equation <code class="language-plaintext highlighter-rouge">(m + n) + p ≡ m + (n + p)</code> holds. Evidence for the proposition
|
||
is a function that accepts three natural numbers, binds them to <code class="language-plaintext highlighter-rouge">m</code>, <code class="language-plaintext highlighter-rouge">n</code>, and <code class="language-plaintext highlighter-rouge">p</code>,
|
||
and returns evidence for the corresponding instance of the equation.</p>
|
||
|
||
<p>For the base case, we must show:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>(zero + n) + p ≡ zero + (n + p)
|
||
</code></pre></div></div>
|
||
|
||
<p>Simplifying both sides with the base case of addition yields the equation:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>n + p ≡ n + p
|
||
</code></pre></div></div>
|
||
|
||
<p>This holds trivially. Reading the chain of equations in the base case of the proof,
|
||
the top and bottom of the chain match the two sides of the equation to
|
||
be shown, and reading down from the top and up from the bottom takes us to
|
||
<code class="language-plaintext highlighter-rouge">n + p</code> in the middle. No justification other than simplification is required.</p>
|
||
|
||
<p>For the inductive case, we must show:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>(suc m + n) + p ≡ suc m + (n + p)
|
||
</code></pre></div></div>
|
||
|
||
<p>Simplifying both sides with the inductive case of addition yields the equation:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>suc ((m + n) + p) ≡ suc (m + (n + p))
|
||
</code></pre></div></div>
|
||
|
||
<p>This in turn follows by prefacing <code class="language-plaintext highlighter-rouge">suc</code> to both sides of the induction
|
||
hypothesis:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>(m + n) + p ≡ m + (n + p)
|
||
</code></pre></div></div>
|
||
|
||
<p>Reading the chain of equations in the inductive case of the proof, the
|
||
top and bottom of the chain match the two sides of the equation to be
|
||
shown, and reading down from the top and up from the bottom takes us
|
||
to the simplified equation above. The remaining equation, does not follow
|
||
from simplification alone, so we use an additional operator for chain
|
||
reasoning, <code class="language-plaintext highlighter-rouge">_≡⟨_⟩_</code>, where a justification for the equation appears
|
||
within angle brackets. The justification given is:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>⟨ cong suc (+-assoc m n p) ⟩
|
||
</code></pre></div></div>
|
||
|
||
<p>Here, the recursive invocation <code class="language-plaintext highlighter-rouge">+-assoc m n p</code> has as its type the
|
||
induction hypothesis, and <code class="language-plaintext highlighter-rouge">cong suc</code> prefaces <code class="language-plaintext highlighter-rouge">suc</code> to each side to
|
||
yield the needed equation.</p>
|
||
|
||
<p>A relation is said to be a <em>congruence</em> for a given function if it is
|
||
preserved by applying that function. If <code class="language-plaintext highlighter-rouge">e</code> is evidence that <code class="language-plaintext highlighter-rouge">x ≡ y</code>,
|
||
then <code class="language-plaintext highlighter-rouge">cong f e</code> is evidence that <code class="language-plaintext highlighter-rouge">f x ≡ f y</code>, for any function <code class="language-plaintext highlighter-rouge">f</code>.</p>
|
||
|
||
<p>Here the inductive hypothesis is not assumed, but instead proved by a
|
||
recursive invocation of the function we are defining, <code class="language-plaintext highlighter-rouge">+-assoc m n p</code>.
|
||
As with addition, this is well founded because associativity of
|
||
larger numbers is proved in terms of associativity of smaller numbers.
|
||
In this case, <code class="language-plaintext highlighter-rouge">assoc (suc m) n p</code> is proved using <code class="language-plaintext highlighter-rouge">assoc m n p</code>.
|
||
The correspondence between proof by induction and definition by
|
||
recursion is one of the most appealing aspects of Agda.</p>
|
||
|
||
<h2 id="induction-as-recursion">Induction as recursion</h2>
|
||
|
||
<p>As a concrete example of how induction corresponds to recursion, here
|
||
is the computation that occurs when instantiating <code class="language-plaintext highlighter-rouge">m</code> to <code class="language-plaintext highlighter-rouge">2</code> in the
|
||
proof of associativity.</p>
|
||
|
||
<pre class="Agda"><a id="+-assoc-2"></a><a id="11115" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11115" class="Function">+-assoc-2</a> <a id="11125" class="Symbol">:</a> <a id="11127" class="Symbol">∀</a> <a id="11129" class="Symbol">(</a><a id="11130" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11130" class="Bound">n</a> <a id="11132" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11132" class="Bound">p</a> <a id="11134" class="Symbol">:</a> <a id="11136" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="11137" class="Symbol">)</a> <a id="11139" class="Symbol">→</a> <a id="11141" class="Symbol">(</a><a id="11142" class="Number">2</a> <a id="11144" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="11146" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11130" class="Bound">n</a><a id="11147" class="Symbol">)</a> <a id="11149" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="11151" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11132" class="Bound">p</a> <a id="11153" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="11155" class="Number">2</a> <a id="11157" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="11159" class="Symbol">(</a><a id="11160" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11130" class="Bound">n</a> <a id="11162" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="11164" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11132" class="Bound">p</a><a id="11165" class="Symbol">)</a>
|
||
<a id="11167" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11115" class="Function">+-assoc-2</a> <a id="11177" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11177" class="Bound">n</a> <a id="11179" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11179" class="Bound">p</a> <a id="11181" class="Symbol">=</a>
|
||
<a id="11185" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2597" class="Function Operator">begin</a>
|
||
<a id="11195" class="Symbol">(</a><a id="11196" class="Number">2</a> <a id="11198" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="11200" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11177" class="Bound">n</a><a id="11201" class="Symbol">)</a> <a id="11203" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="11205" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11179" class="Bound">p</a>
|
||
<a id="11209" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
|
||
<a id="11217" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="11221" class="Symbol">(</a><a id="11222" class="Number">1</a> <a id="11224" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="11226" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11177" class="Bound">n</a><a id="11227" class="Symbol">)</a> <a id="11229" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="11231" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11179" class="Bound">p</a>
|
||
<a id="11235" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
|
||
<a id="11243" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="11247" class="Symbol">((</a><a id="11249" class="Number">1</a> <a id="11251" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="11253" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11177" class="Bound">n</a><a id="11254" class="Symbol">)</a> <a id="11256" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="11258" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11179" class="Bound">p</a><a id="11259" class="Symbol">)</a>
|
||
<a id="11263" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">≡⟨</a> <a id="11266" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#1090" class="Function">cong</a> <a id="11271" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="11275" class="Symbol">(</a><a id="11276" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11351" class="Function">+-assoc-1</a> <a id="11286" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11177" class="Bound">n</a> <a id="11288" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11179" class="Bound">p</a><a id="11289" class="Symbol">)</a> <a id="11291" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">⟩</a>
|
||
<a id="11297" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="11301" class="Symbol">(</a><a id="11302" class="Number">1</a> <a id="11304" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="11306" class="Symbol">(</a><a id="11307" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11177" class="Bound">n</a> <a id="11309" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="11311" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11179" class="Bound">p</a><a id="11312" class="Symbol">))</a>
|
||
<a id="11317" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
|
||
<a id="11325" class="Number">2</a> <a id="11327" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="11329" class="Symbol">(</a><a id="11330" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11177" class="Bound">n</a> <a id="11332" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="11334" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11179" class="Bound">p</a><a id="11335" class="Symbol">)</a>
|
||
<a id="11339" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2892" class="Function Operator">∎</a>
|
||
<a id="11343" class="Keyword">where</a>
|
||
<a id="11351" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11351" class="Function">+-assoc-1</a> <a id="11361" class="Symbol">:</a> <a id="11363" class="Symbol">∀</a> <a id="11365" class="Symbol">(</a><a id="11366" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11366" class="Bound">n</a> <a id="11368" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11368" class="Bound">p</a> <a id="11370" class="Symbol">:</a> <a id="11372" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="11373" class="Symbol">)</a> <a id="11375" class="Symbol">→</a> <a id="11377" class="Symbol">(</a><a id="11378" class="Number">1</a> <a id="11380" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="11382" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11366" class="Bound">n</a><a id="11383" class="Symbol">)</a> <a id="11385" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="11387" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11368" class="Bound">p</a> <a id="11389" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="11391" class="Number">1</a> <a id="11393" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="11395" class="Symbol">(</a><a id="11396" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11366" class="Bound">n</a> <a id="11398" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="11400" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11368" class="Bound">p</a><a id="11401" class="Symbol">)</a>
|
||
<a id="11405" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11351" class="Function">+-assoc-1</a> <a id="11415" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11415" class="Bound">n</a> <a id="11417" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11417" class="Bound">p</a> <a id="11419" class="Symbol">=</a>
|
||
<a id="11425" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2597" class="Function Operator">begin</a>
|
||
<a id="11437" class="Symbol">(</a><a id="11438" class="Number">1</a> <a id="11440" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="11442" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11415" class="Bound">n</a><a id="11443" class="Symbol">)</a> <a id="11445" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="11447" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11417" class="Bound">p</a>
|
||
<a id="11453" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
|
||
<a id="11463" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="11467" class="Symbol">(</a><a id="11468" class="Number">0</a> <a id="11470" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="11472" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11415" class="Bound">n</a><a id="11473" class="Symbol">)</a> <a id="11475" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="11477" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11417" class="Bound">p</a>
|
||
<a id="11483" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
|
||
<a id="11493" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="11497" class="Symbol">((</a><a id="11499" class="Number">0</a> <a id="11501" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="11503" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11415" class="Bound">n</a><a id="11504" class="Symbol">)</a> <a id="11506" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="11508" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11417" class="Bound">p</a><a id="11509" class="Symbol">)</a>
|
||
<a id="11515" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">≡⟨</a> <a id="11518" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#1090" class="Function">cong</a> <a id="11523" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="11527" class="Symbol">(</a><a id="11528" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11615" class="Function">+-assoc-0</a> <a id="11538" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11415" class="Bound">n</a> <a id="11540" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11417" class="Bound">p</a><a id="11541" class="Symbol">)</a> <a id="11543" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">⟩</a>
|
||
<a id="11551" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="11555" class="Symbol">(</a><a id="11556" class="Number">0</a> <a id="11558" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="11560" class="Symbol">(</a><a id="11561" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11415" class="Bound">n</a> <a id="11563" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="11565" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11417" class="Bound">p</a><a id="11566" class="Symbol">))</a>
|
||
<a id="11573" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
|
||
<a id="11583" class="Number">1</a> <a id="11585" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="11587" class="Symbol">(</a><a id="11588" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11415" class="Bound">n</a> <a id="11590" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="11592" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11417" class="Bound">p</a><a id="11593" class="Symbol">)</a>
|
||
<a id="11599" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2892" class="Function Operator">∎</a>
|
||
<a id="11605" class="Keyword">where</a>
|
||
<a id="11615" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11615" class="Function">+-assoc-0</a> <a id="11625" class="Symbol">:</a> <a id="11627" class="Symbol">∀</a> <a id="11629" class="Symbol">(</a><a id="11630" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11630" class="Bound">n</a> <a id="11632" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11632" class="Bound">p</a> <a id="11634" class="Symbol">:</a> <a id="11636" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="11637" class="Symbol">)</a> <a id="11639" class="Symbol">→</a> <a id="11641" class="Symbol">(</a><a id="11642" class="Number">0</a> <a id="11644" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="11646" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11630" class="Bound">n</a><a id="11647" class="Symbol">)</a> <a id="11649" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="11651" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11632" class="Bound">p</a> <a id="11653" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="11655" class="Number">0</a> <a id="11657" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="11659" class="Symbol">(</a><a id="11660" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11630" class="Bound">n</a> <a id="11662" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="11664" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11632" class="Bound">p</a><a id="11665" class="Symbol">)</a>
|
||
<a id="11671" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11615" class="Function">+-assoc-0</a> <a id="11681" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11681" class="Bound">n</a> <a id="11683" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11683" class="Bound">p</a> <a id="11685" class="Symbol">=</a>
|
||
<a id="11693" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2597" class="Function Operator">begin</a>
|
||
<a id="11707" class="Symbol">(</a><a id="11708" class="Number">0</a> <a id="11710" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="11712" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11681" class="Bound">n</a><a id="11713" class="Symbol">)</a> <a id="11715" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="11717" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11683" class="Bound">p</a>
|
||
<a id="11725" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
|
||
<a id="11737" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11681" class="Bound">n</a> <a id="11739" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="11741" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11683" class="Bound">p</a>
|
||
<a id="11749" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
|
||
<a id="11761" class="Number">0</a> <a id="11763" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="11765" class="Symbol">(</a><a id="11766" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11681" class="Bound">n</a> <a id="11768" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="11770" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#11683" class="Bound">p</a><a id="11771" class="Symbol">)</a>
|
||
<a id="11779" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2892" class="Function Operator">∎</a>
|
||
</pre>
|
||
|
||
<h2 id="terminology-and-notation">Terminology and notation</h2>
|
||
|
||
<p>The symbol <code class="language-plaintext highlighter-rouge">∀</code> appears in the statement of associativity to indicate that
|
||
it holds for all numbers <code class="language-plaintext highlighter-rouge">m</code>, <code class="language-plaintext highlighter-rouge">n</code>, and <code class="language-plaintext highlighter-rouge">p</code>. We refer to <code class="language-plaintext highlighter-rouge">∀</code> as the <em>universal
|
||
quantifier</em>, and it is discussed further in Chapter <a href="/20.07/Quantifiers/">Quantifiers</a>.</p>
|
||
|
||
<p>Evidence for a universal quantifier is a function. The notations</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>+-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
|
||
</code></pre></div></div>
|
||
|
||
<p>and</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>+-assoc : ∀ (m : ℕ) → ∀ (n : ℕ) → ∀ (p : ℕ) → (m + n) + p ≡ m + (n + p)
|
||
</code></pre></div></div>
|
||
|
||
<p>are equivalent. They differ from a function type such as <code class="language-plaintext highlighter-rouge">ℕ → ℕ → ℕ</code>
|
||
in that variables are associated with each argument type, and the
|
||
result type may mention (or depend upon) these variables; hence they
|
||
are called <em>dependent functions</em>.</p>
|
||
|
||
<h2 id="our-second-proof-commutativity">Our second proof: commutativity</h2>
|
||
|
||
<p>Another important property of addition is that it is <em>commutative</em>, that is,
|
||
that the order of the operands does not matter:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>m + n ≡ n + m
|
||
</code></pre></div></div>
|
||
|
||
<p>The proof requires that we first demonstrate two lemmas.</p>
|
||
|
||
<h3 id="the-first-lemma">The first lemma</h3>
|
||
|
||
<p>The base case of the definition of addition states that zero
|
||
is a left-identity:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>zero + n ≡ n
|
||
</code></pre></div></div>
|
||
|
||
<p>Our first lemma states that zero is also a right-identity:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>m + zero ≡ m
|
||
</code></pre></div></div>
|
||
|
||
<p>Here is the lemma’s statement and proof:</p>
|
||
<pre class="Agda"><a id="+-identityʳ"></a><a id="12999" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#12999" class="Function">+-identityʳ</a> <a id="13011" class="Symbol">:</a> <a id="13013" class="Symbol">∀</a> <a id="13015" class="Symbol">(</a><a id="13016" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#13016" class="Bound">m</a> <a id="13018" class="Symbol">:</a> <a id="13020" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="13021" class="Symbol">)</a> <a id="13023" class="Symbol">→</a> <a id="13025" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#13016" class="Bound">m</a> <a id="13027" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="13029" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">zero</a> <a id="13034" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="13036" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#13016" class="Bound">m</a>
|
||
<a id="13038" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#12999" class="Function">+-identityʳ</a> <a id="13050" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">zero</a> <a id="13055" class="Symbol">=</a>
|
||
<a id="13059" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2597" class="Function Operator">begin</a>
|
||
<a id="13069" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">zero</a> <a id="13074" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="13076" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">zero</a>
|
||
<a id="13083" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
|
||
<a id="13091" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">zero</a>
|
||
<a id="13098" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2892" class="Function Operator">∎</a>
|
||
<a id="13100" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#12999" class="Function">+-identityʳ</a> <a id="13112" class="Symbol">(</a><a id="13113" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="13117" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#13117" class="Bound">m</a><a id="13118" class="Symbol">)</a> <a id="13120" class="Symbol">=</a>
|
||
<a id="13124" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2597" class="Function Operator">begin</a>
|
||
<a id="13134" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="13138" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#13117" class="Bound">m</a> <a id="13140" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="13142" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">zero</a>
|
||
<a id="13149" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
|
||
<a id="13157" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="13161" class="Symbol">(</a><a id="13162" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#13117" class="Bound">m</a> <a id="13164" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="13166" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">zero</a><a id="13170" class="Symbol">)</a>
|
||
<a id="13174" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">≡⟨</a> <a id="13177" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#1090" class="Function">cong</a> <a id="13182" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="13186" class="Symbol">(</a><a id="13187" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#12999" class="Function">+-identityʳ</a> <a id="13199" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#13117" class="Bound">m</a><a id="13200" class="Symbol">)</a> <a id="13202" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">⟩</a>
|
||
<a id="13208" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="13212" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#13117" class="Bound">m</a>
|
||
<a id="13216" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2892" class="Function Operator">∎</a>
|
||
</pre>
|
||
<p>The signature states that we are defining the identifier <code class="language-plaintext highlighter-rouge">+-identityʳ</code> which
|
||
provides evidence for the proposition:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>∀ (m : ℕ) → m + zero ≡ m
|
||
</code></pre></div></div>
|
||
|
||
<p>Evidence for the proposition is a function that accepts a natural
|
||
number, binds it to <code class="language-plaintext highlighter-rouge">m</code>, and returns evidence for the corresponding
|
||
instance of the equation. The proof is by induction on <code class="language-plaintext highlighter-rouge">m</code>.</p>
|
||
|
||
<p>For the base case, we must show:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>zero + zero ≡ zero
|
||
</code></pre></div></div>
|
||
|
||
<p>Simplifying with the base case of addition, this is straightforward.</p>
|
||
|
||
<p>For the inductive case, we must show:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>(suc m) + zero = suc m
|
||
</code></pre></div></div>
|
||
|
||
<p>Simplifying both sides with the inductive case of addition yields the equation:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>suc (m + zero) = suc m
|
||
</code></pre></div></div>
|
||
|
||
<p>This in turn follows by prefacing <code class="language-plaintext highlighter-rouge">suc</code> to both sides of the induction
|
||
hypothesis:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>m + zero ≡ m
|
||
</code></pre></div></div>
|
||
|
||
<p>Reading the chain of equations down from the top and up from the bottom
|
||
takes us to the simplified equation above. The remaining
|
||
equation has the justification:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>⟨ cong suc (+-identityʳ m) ⟩
|
||
</code></pre></div></div>
|
||
|
||
<p>Here, the recursive invocation <code class="language-plaintext highlighter-rouge">+-identityʳ m</code> has as its type the
|
||
induction hypothesis, and <code class="language-plaintext highlighter-rouge">cong suc</code> prefaces <code class="language-plaintext highlighter-rouge">suc</code> to each side to
|
||
yield the needed equation. This completes the first lemma.</p>
|
||
|
||
<h3 id="the-second-lemma">The second lemma</h3>
|
||
|
||
<p>The inductive case of the definition of addition pushes <code class="language-plaintext highlighter-rouge">suc</code> on the
|
||
first argument to the outside:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>suc m + n ≡ suc (m + n)
|
||
</code></pre></div></div>
|
||
|
||
<p>Our second lemma does the same for <code class="language-plaintext highlighter-rouge">suc</code> on the second argument:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>m + suc n ≡ suc (m + n)
|
||
</code></pre></div></div>
|
||
|
||
<p>Here is the lemma’s statement and proof:</p>
|
||
<pre class="Agda"><a id="+-suc"></a><a id="14656" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#14656" class="Function">+-suc</a> <a id="14662" class="Symbol">:</a> <a id="14664" class="Symbol">∀</a> <a id="14666" class="Symbol">(</a><a id="14667" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#14667" class="Bound">m</a> <a id="14669" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#14669" class="Bound">n</a> <a id="14671" class="Symbol">:</a> <a id="14673" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="14674" class="Symbol">)</a> <a id="14676" class="Symbol">→</a> <a id="14678" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#14667" class="Bound">m</a> <a id="14680" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="14682" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="14686" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#14669" class="Bound">n</a> <a id="14688" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="14690" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="14694" class="Symbol">(</a><a id="14695" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#14667" class="Bound">m</a> <a id="14697" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="14699" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#14669" class="Bound">n</a><a id="14700" class="Symbol">)</a>
|
||
<a id="14702" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#14656" class="Function">+-suc</a> <a id="14708" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">zero</a> <a id="14713" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#14713" class="Bound">n</a> <a id="14715" class="Symbol">=</a>
|
||
<a id="14719" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2597" class="Function Operator">begin</a>
|
||
<a id="14729" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">zero</a> <a id="14734" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="14736" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="14740" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#14713" class="Bound">n</a>
|
||
<a id="14744" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
|
||
<a id="14752" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="14756" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#14713" class="Bound">n</a>
|
||
<a id="14760" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
|
||
<a id="14768" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="14772" class="Symbol">(</a><a id="14773" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">zero</a> <a id="14778" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="14780" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#14713" class="Bound">n</a><a id="14781" class="Symbol">)</a>
|
||
<a id="14785" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2892" class="Function Operator">∎</a>
|
||
<a id="14787" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#14656" class="Function">+-suc</a> <a id="14793" class="Symbol">(</a><a id="14794" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="14798" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#14798" class="Bound">m</a><a id="14799" class="Symbol">)</a> <a id="14801" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#14801" class="Bound">n</a> <a id="14803" class="Symbol">=</a>
|
||
<a id="14807" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2597" class="Function Operator">begin</a>
|
||
<a id="14817" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="14821" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#14798" class="Bound">m</a> <a id="14823" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="14825" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="14829" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#14801" class="Bound">n</a>
|
||
<a id="14833" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
|
||
<a id="14841" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="14845" class="Symbol">(</a><a id="14846" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#14798" class="Bound">m</a> <a id="14848" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="14850" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="14854" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#14801" class="Bound">n</a><a id="14855" class="Symbol">)</a>
|
||
<a id="14859" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">≡⟨</a> <a id="14862" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#1090" class="Function">cong</a> <a id="14867" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="14871" class="Symbol">(</a><a id="14872" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#14656" class="Function">+-suc</a> <a id="14878" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#14798" class="Bound">m</a> <a id="14880" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#14801" class="Bound">n</a><a id="14881" class="Symbol">)</a> <a id="14883" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">⟩</a>
|
||
<a id="14889" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="14893" class="Symbol">(</a><a id="14894" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="14898" class="Symbol">(</a><a id="14899" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#14798" class="Bound">m</a> <a id="14901" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="14903" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#14801" class="Bound">n</a><a id="14904" class="Symbol">))</a>
|
||
<a id="14909" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
|
||
<a id="14917" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="14921" class="Symbol">(</a><a id="14922" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="14926" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#14798" class="Bound">m</a> <a id="14928" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="14930" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#14801" class="Bound">n</a><a id="14931" class="Symbol">)</a>
|
||
<a id="14935" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2892" class="Function Operator">∎</a>
|
||
</pre>
|
||
<p>The signature states that we are defining the identifier <code class="language-plaintext highlighter-rouge">+-suc</code> which provides
|
||
evidence for the proposition:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>∀ (m n : ℕ) → m + suc n ≡ suc (m + n)
|
||
</code></pre></div></div>
|
||
|
||
<p>Evidence for the proposition is a function that accepts two natural numbers,
|
||
binds them to <code class="language-plaintext highlighter-rouge">m</code> and <code class="language-plaintext highlighter-rouge">n</code>, and returns evidence for the corresponding instance
|
||
of the equation. The proof is by induction on <code class="language-plaintext highlighter-rouge">m</code>.</p>
|
||
|
||
<p>For the base case, we must show:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>zero + suc n ≡ suc (zero + n)
|
||
</code></pre></div></div>
|
||
|
||
<p>Simplifying with the base case of addition, this is straightforward.</p>
|
||
|
||
<p>For the inductive case, we must show:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>suc m + suc n ≡ suc (suc m + n)
|
||
</code></pre></div></div>
|
||
|
||
<p>Simplifying both sides with the inductive case of addition yields the equation:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>suc (m + suc n) ≡ suc (suc (m + n))
|
||
</code></pre></div></div>
|
||
|
||
<p>This in turn follows by prefacing <code class="language-plaintext highlighter-rouge">suc</code> to both sides of the induction
|
||
hypothesis:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>m + suc n ≡ suc (m + n)
|
||
</code></pre></div></div>
|
||
|
||
<p>Reading the chain of equations down from the top and up from the bottom
|
||
takes us to the simplified equation in the middle. The remaining
|
||
equation has the justification:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>⟨ cong suc (+-suc m n) ⟩
|
||
</code></pre></div></div>
|
||
|
||
<p>Here, the recursive invocation <code class="language-plaintext highlighter-rouge">+-suc m n</code> has as its type the
|
||
induction hypothesis, and <code class="language-plaintext highlighter-rouge">cong suc</code> prefaces <code class="language-plaintext highlighter-rouge">suc</code> to each side to
|
||
yield the needed equation. This completes the second lemma.</p>
|
||
|
||
<h3 id="the-proposition">The proposition</h3>
|
||
|
||
<p>Finally, here is our proposition’s statement and proof:</p>
|
||
<pre class="Agda"><a id="+-comm"></a><a id="16229" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#16229" class="Function">+-comm</a> <a id="16236" class="Symbol">:</a> <a id="16238" class="Symbol">∀</a> <a id="16240" class="Symbol">(</a><a id="16241" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#16241" class="Bound">m</a> <a id="16243" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#16243" class="Bound">n</a> <a id="16245" class="Symbol">:</a> <a id="16247" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="16248" class="Symbol">)</a> <a id="16250" class="Symbol">→</a> <a id="16252" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#16241" class="Bound">m</a> <a id="16254" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="16256" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#16243" class="Bound">n</a> <a id="16258" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="16260" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#16243" class="Bound">n</a> <a id="16262" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="16264" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#16241" class="Bound">m</a>
|
||
<a id="16266" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#16229" class="Function">+-comm</a> <a id="16273" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#16273" class="Bound">m</a> <a id="16275" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">zero</a> <a id="16280" class="Symbol">=</a>
|
||
<a id="16284" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2597" class="Function Operator">begin</a>
|
||
<a id="16294" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#16273" class="Bound">m</a> <a id="16296" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="16298" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">zero</a>
|
||
<a id="16305" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">≡⟨</a> <a id="16308" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#12999" class="Function">+-identityʳ</a> <a id="16320" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#16273" class="Bound">m</a> <a id="16322" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">⟩</a>
|
||
<a id="16328" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#16273" class="Bound">m</a>
|
||
<a id="16332" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
|
||
<a id="16340" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">zero</a> <a id="16345" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="16347" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#16273" class="Bound">m</a>
|
||
<a id="16351" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2892" class="Function Operator">∎</a>
|
||
<a id="16353" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#16229" class="Function">+-comm</a> <a id="16360" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#16360" class="Bound">m</a> <a id="16362" class="Symbol">(</a><a id="16363" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="16367" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#16367" class="Bound">n</a><a id="16368" class="Symbol">)</a> <a id="16370" class="Symbol">=</a>
|
||
<a id="16374" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2597" class="Function Operator">begin</a>
|
||
<a id="16384" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#16360" class="Bound">m</a> <a id="16386" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="16388" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="16392" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#16367" class="Bound">n</a>
|
||
<a id="16396" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">≡⟨</a> <a id="16399" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#14656" class="Function">+-suc</a> <a id="16405" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#16360" class="Bound">m</a> <a id="16407" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#16367" class="Bound">n</a> <a id="16409" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">⟩</a>
|
||
<a id="16415" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="16419" class="Symbol">(</a><a id="16420" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#16360" class="Bound">m</a> <a id="16422" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="16424" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#16367" class="Bound">n</a><a id="16425" class="Symbol">)</a>
|
||
<a id="16429" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">≡⟨</a> <a id="16432" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#1090" class="Function">cong</a> <a id="16437" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="16441" class="Symbol">(</a><a id="16442" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#16229" class="Function">+-comm</a> <a id="16449" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#16360" class="Bound">m</a> <a id="16451" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#16367" class="Bound">n</a><a id="16452" class="Symbol">)</a> <a id="16454" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">⟩</a>
|
||
<a id="16460" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="16464" class="Symbol">(</a><a id="16465" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#16367" class="Bound">n</a> <a id="16467" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="16469" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#16360" class="Bound">m</a><a id="16470" class="Symbol">)</a>
|
||
<a id="16474" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
|
||
<a id="16482" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="16486" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#16367" class="Bound">n</a> <a id="16488" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="16490" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#16360" class="Bound">m</a>
|
||
<a id="16494" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2892" class="Function Operator">∎</a>
|
||
</pre>
|
||
<p>The first line states that we are defining the identifier
|
||
<code class="language-plaintext highlighter-rouge">+-comm</code> which provides evidence for the proposition:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>∀ (m n : ℕ) → m + n ≡ n + m
|
||
</code></pre></div></div>
|
||
|
||
<p>Evidence for the proposition is a function that accepts two
|
||
natural numbers, binds them to <code class="language-plaintext highlighter-rouge">m</code> and <code class="language-plaintext highlighter-rouge">n</code>, and returns evidence for the
|
||
corresponding instance of the equation. The proof is by
|
||
induction on <code class="language-plaintext highlighter-rouge">n</code>. (Not on <code class="language-plaintext highlighter-rouge">m</code> this time!)</p>
|
||
|
||
<p>For the base case, we must show:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>m + zero ≡ zero + m
|
||
</code></pre></div></div>
|
||
|
||
<p>Simplifying both sides with the base case of addition yields the equation:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>m + zero ≡ m
|
||
</code></pre></div></div>
|
||
|
||
<p>The remaining equation has the justification <code class="language-plaintext highlighter-rouge">⟨ +-identityʳ m ⟩</code>,
|
||
which invokes the first lemma.</p>
|
||
|
||
<p>For the inductive case, we must show:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>m + suc n ≡ suc n + m
|
||
</code></pre></div></div>
|
||
|
||
<p>Simplifying both sides with the inductive case of addition yields the equation:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>m + suc n ≡ suc (n + m)
|
||
</code></pre></div></div>
|
||
|
||
<p>We show this in two steps. First, we have:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>m + suc n ≡ suc (m + n)
|
||
</code></pre></div></div>
|
||
|
||
<p>which is justified by the second lemma, <code class="language-plaintext highlighter-rouge">⟨ +-suc m n ⟩</code>. Then we
|
||
have</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>suc (m + n) ≡ suc (n + m)
|
||
</code></pre></div></div>
|
||
|
||
<p>which is justified by congruence and the induction hypothesis,
|
||
<code class="language-plaintext highlighter-rouge">⟨ cong suc (+-comm m n) ⟩</code>. This completes the proof.</p>
|
||
|
||
<p>Agda requires that identifiers are defined before they are used,
|
||
so we must present the lemmas before the main proposition, as we
|
||
have done above. In practice, one will often attempt to prove
|
||
the main proposition first, and the equations required to do so
|
||
will suggest what lemmas to prove.</p>
|
||
|
||
<h2 id="sections">Our first corollary: rearranging</h2>
|
||
|
||
<p>We can apply associativity to rearrange parentheses however we like.
|
||
Here is an example:</p>
|
||
<pre class="Agda"><a id="+-rearrange"></a><a id="18040" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#18040" class="Function">+-rearrange</a> <a id="18052" class="Symbol">:</a> <a id="18054" class="Symbol">∀</a> <a id="18056" class="Symbol">(</a><a id="18057" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#18057" class="Bound">m</a> <a id="18059" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#18059" class="Bound">n</a> <a id="18061" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#18061" class="Bound">p</a> <a id="18063" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#18063" class="Bound">q</a> <a id="18065" class="Symbol">:</a> <a id="18067" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="18068" class="Symbol">)</a> <a id="18070" class="Symbol">→</a> <a id="18072" class="Symbol">(</a><a id="18073" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#18057" class="Bound">m</a> <a id="18075" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="18077" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#18059" class="Bound">n</a><a id="18078" class="Symbol">)</a> <a id="18080" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="18082" class="Symbol">(</a><a id="18083" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#18061" class="Bound">p</a> <a id="18085" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="18087" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#18063" class="Bound">q</a><a id="18088" class="Symbol">)</a> <a id="18090" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="18092" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#18057" class="Bound">m</a> <a id="18094" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="18096" class="Symbol">(</a><a id="18097" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#18059" class="Bound">n</a> <a id="18099" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="18101" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#18061" class="Bound">p</a><a id="18102" class="Symbol">)</a> <a id="18104" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="18106" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#18063" class="Bound">q</a>
|
||
<a id="18108" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#18040" class="Function">+-rearrange</a> <a id="18120" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#18120" class="Bound">m</a> <a id="18122" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#18122" class="Bound">n</a> <a id="18124" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#18124" class="Bound">p</a> <a id="18126" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#18126" class="Bound">q</a> <a id="18128" class="Symbol">=</a>
|
||
<a id="18132" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2597" class="Function Operator">begin</a>
|
||
<a id="18142" class="Symbol">(</a><a id="18143" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#18120" class="Bound">m</a> <a id="18145" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="18147" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#18122" class="Bound">n</a><a id="18148" class="Symbol">)</a> <a id="18150" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="18152" class="Symbol">(</a><a id="18153" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#18124" class="Bound">p</a> <a id="18155" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="18157" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#18126" class="Bound">q</a><a id="18158" class="Symbol">)</a>
|
||
<a id="18162" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">≡⟨</a> <a id="18165" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#7762" class="Function">+-assoc</a> <a id="18173" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#18120" class="Bound">m</a> <a id="18175" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#18122" class="Bound">n</a> <a id="18177" class="Symbol">(</a><a id="18178" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#18124" class="Bound">p</a> <a id="18180" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="18182" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#18126" class="Bound">q</a><a id="18183" class="Symbol">)</a> <a id="18185" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">⟩</a>
|
||
<a id="18191" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#18120" class="Bound">m</a> <a id="18193" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="18195" class="Symbol">(</a><a id="18196" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#18122" class="Bound">n</a> <a id="18198" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="18200" class="Symbol">(</a><a id="18201" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#18124" class="Bound">p</a> <a id="18203" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="18205" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#18126" class="Bound">q</a><a id="18206" class="Symbol">))</a>
|
||
<a id="18211" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">≡⟨</a> <a id="18214" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#1090" class="Function">cong</a> <a id="18219" class="Symbol">(</a><a id="18220" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#18120" class="Bound">m</a> <a id="18222" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+_</a><a id="18224" class="Symbol">)</a> <a id="18226" class="Symbol">(</a><a id="18227" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#939" class="Function">sym</a> <a id="18231" class="Symbol">(</a><a id="18232" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#7762" class="Function">+-assoc</a> <a id="18240" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#18122" class="Bound">n</a> <a id="18242" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#18124" class="Bound">p</a> <a id="18244" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#18126" class="Bound">q</a><a id="18245" class="Symbol">))</a> <a id="18248" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">⟩</a>
|
||
<a id="18254" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#18120" class="Bound">m</a> <a id="18256" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="18258" class="Symbol">((</a><a id="18260" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#18122" class="Bound">n</a> <a id="18262" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="18264" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#18124" class="Bound">p</a><a id="18265" class="Symbol">)</a> <a id="18267" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="18269" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#18126" class="Bound">q</a><a id="18270" class="Symbol">)</a>
|
||
<a id="18274" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">≡⟨</a> <a id="18277" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#939" class="Function">sym</a> <a id="18281" class="Symbol">(</a><a id="18282" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#7762" class="Function">+-assoc</a> <a id="18290" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#18120" class="Bound">m</a> <a id="18292" class="Symbol">(</a><a id="18293" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#18122" class="Bound">n</a> <a id="18295" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="18297" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#18124" class="Bound">p</a><a id="18298" class="Symbol">)</a> <a id="18300" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#18126" class="Bound">q</a><a id="18301" class="Symbol">)</a> <a id="18303" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">⟩</a>
|
||
<a id="18309" class="Symbol">(</a><a id="18310" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#18120" class="Bound">m</a> <a id="18312" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="18314" class="Symbol">(</a><a id="18315" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#18122" class="Bound">n</a> <a id="18317" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="18319" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#18124" class="Bound">p</a><a id="18320" class="Symbol">))</a> <a id="18323" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="18325" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#18126" class="Bound">q</a>
|
||
<a id="18329" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2892" class="Function Operator">∎</a>
|
||
</pre>
|
||
<p>No induction is required, we simply apply associativity twice.
|
||
A few points are worthy of note.</p>
|
||
|
||
<p>First, addition associates to the left, so <code class="language-plaintext highlighter-rouge">m + (n + p) + q</code>
|
||
stands for <code class="language-plaintext highlighter-rouge">(m + (n + p)) + q</code>.</p>
|
||
|
||
<p>Second, we use <code class="language-plaintext highlighter-rouge">sym</code> to interchange the sides of an equation.
|
||
Proposition <code class="language-plaintext highlighter-rouge">+-assoc n p q</code> shifts parentheses from right to left:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>(n + p) + q ≡ n + (p + q)
|
||
</code></pre></div></div>
|
||
|
||
<p>To shift them the other way, we use <code class="language-plaintext highlighter-rouge">sym (+-assoc n p q)</code>:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>n + (p + q) ≡ (n + p) + q
|
||
</code></pre></div></div>
|
||
|
||
<p>In general, if <code class="language-plaintext highlighter-rouge">e</code> provides evidence for <code class="language-plaintext highlighter-rouge">x ≡ y</code> then <code class="language-plaintext highlighter-rouge">sym e</code> provides
|
||
evidence for <code class="language-plaintext highlighter-rouge">y ≡ x</code>.</p>
|
||
|
||
<p>Third, Agda supports a variant of the <em>section</em> notation introduced by
|
||
Richard Bird. We write <code class="language-plaintext highlighter-rouge">(x +_)</code> for the function that applied to <code class="language-plaintext highlighter-rouge">y</code>
|
||
returns <code class="language-plaintext highlighter-rouge">x + y</code>. Thus, applying the congruence <code class="language-plaintext highlighter-rouge">cong (m +_)</code> takes
|
||
the above equation into:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>m + (n + (p + q)) ≡ m + ((n + p) + q)
|
||
</code></pre></div></div>
|
||
|
||
<p>Similarly, we write <code class="language-plaintext highlighter-rouge">(_+ x)</code> for the function that applied to <code class="language-plaintext highlighter-rouge">y</code>
|
||
returns <code class="language-plaintext highlighter-rouge">y + x</code>; the same works for any infix operator.</p>
|
||
|
||
<h2 id="creation-one-last-time">Creation, one last time</h2>
|
||
|
||
<p>Returning to the proof of associativity, it may be helpful to view the inductive
|
||
proof (or, equivalently, the recursive definition) as a creation story. This
|
||
time we are concerned with judgments asserting associativity:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code> -- In the beginning, we know nothing about associativity.
|
||
</code></pre></div></div>
|
||
|
||
<p>Now, we apply the rules to all the judgments we know about. The base
|
||
case tells us that <code class="language-plaintext highlighter-rouge">(zero + n) + p ≡ zero + (n + p)</code> for every natural
|
||
<code class="language-plaintext highlighter-rouge">n</code> and <code class="language-plaintext highlighter-rouge">p</code>. The inductive case tells us that if
|
||
<code class="language-plaintext highlighter-rouge">(m + n) + p ≡ m + (n + p)</code> (on the day before today) then
|
||
<code class="language-plaintext highlighter-rouge">(suc m + n) + p ≡ suc m + (n + p)</code> (today).
|
||
We didn’t know any judgments about associativity before today, so that
|
||
rule doesn’t give us any new judgments:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>-- On the first day, we know about associativity of 0.
|
||
(0 + 0) + 0 ≡ 0 + (0 + 0) ... (0 + 4) + 5 ≡ 0 + (4 + 5) ...
|
||
</code></pre></div></div>
|
||
|
||
<p>Then we repeat the process, so on the next day we know about all the
|
||
judgments from the day before, plus any judgments added by the rules.
|
||
The base case tells us nothing new, but now the inductive case adds
|
||
more judgments:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>-- On the second day, we know about associativity of 0 and 1.
|
||
(0 + 0) + 0 ≡ 0 + (0 + 0) ... (0 + 4) + 5 ≡ 0 + (4 + 5) ...
|
||
(1 + 0) + 0 ≡ 1 + (0 + 0) ... (1 + 4) + 5 ≡ 1 + (4 + 5) ...
|
||
</code></pre></div></div>
|
||
|
||
<p>And we repeat the process again:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>-- On the third day, we know about associativity of 0, 1, and 2.
|
||
(0 + 0) + 0 ≡ 0 + (0 + 0) ... (0 + 4) + 5 ≡ 0 + (4 + 5) ...
|
||
(1 + 0) + 0 ≡ 1 + (0 + 0) ... (1 + 4) + 5 ≡ 1 + (4 + 5) ...
|
||
(2 + 0) + 0 ≡ 2 + (0 + 0) ... (2 + 4) + 5 ≡ 2 + (4 + 5) ...
|
||
</code></pre></div></div>
|
||
|
||
<p>You’ve got the hang of it by now:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>-- On the fourth day, we know about associativity of 0, 1, 2, and 3.
|
||
(0 + 0) + 0 ≡ 0 + (0 + 0) ... (0 + 4) + 5 ≡ 0 + (4 + 5) ...
|
||
(1 + 0) + 0 ≡ 1 + (0 + 0) ... (1 + 4) + 5 ≡ 1 + (4 + 5) ...
|
||
(2 + 0) + 0 ≡ 2 + (0 + 0) ... (2 + 4) + 5 ≡ 2 + (4 + 5) ...
|
||
(3 + 0) + 0 ≡ 3 + (0 + 0) ... (3 + 4) + 5 ≡ 3 + (4 + 5) ...
|
||
</code></pre></div></div>
|
||
|
||
<p>The process continues. On the <em>m</em>‘th day we will know all the
|
||
judgments where the first number is less than <em>m</em>.</p>
|
||
|
||
<p>There is also a completely finite approach to generating the same equations,
|
||
which is left as an exercise for the reader.</p>
|
||
|
||
<h4 id="finite-plus-assoc">Exercise <code class="language-plaintext highlighter-rouge">finite-+-assoc</code> (stretch)</h4>
|
||
|
||
<p>Write out what is known about associativity of addition on each of the
|
||
first four days using a finite story of creation, as
|
||
<a href="/20.07/Naturals/#finite-creation">earlier</a>.</p>
|
||
|
||
<pre class="Agda"><a id="21748" class="Comment">-- Your code goes here</a>
|
||
</pre>
|
||
<h2 id="associativity-with-rewrite">Associativity with rewrite</h2>
|
||
|
||
<p>There is more than one way to skin a cat. Here is a second proof of
|
||
associativity of addition in Agda, using <code class="language-plaintext highlighter-rouge">rewrite</code> rather than chains of
|
||
equations:</p>
|
||
<pre class="Agda"><a id="+-assoc′"></a><a id="21964" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#21964" class="Function">+-assoc′</a> <a id="21973" class="Symbol">:</a> <a id="21975" class="Symbol">∀</a> <a id="21977" class="Symbol">(</a><a id="21978" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#21978" class="Bound">m</a> <a id="21980" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#21980" class="Bound">n</a> <a id="21982" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#21982" class="Bound">p</a> <a id="21984" class="Symbol">:</a> <a id="21986" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="21987" class="Symbol">)</a> <a id="21989" class="Symbol">→</a> <a id="21991" class="Symbol">(</a><a id="21992" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#21978" class="Bound">m</a> <a id="21994" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="21996" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#21980" class="Bound">n</a><a id="21997" class="Symbol">)</a> <a id="21999" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="22001" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#21982" class="Bound">p</a> <a id="22003" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="22005" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#21978" class="Bound">m</a> <a id="22007" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="22009" class="Symbol">(</a><a id="22010" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#21980" class="Bound">n</a> <a id="22012" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="22014" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#21982" class="Bound">p</a><a id="22015" class="Symbol">)</a>
|
||
<a id="22017" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#21964" class="Function">+-assoc′</a> <a id="22026" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">zero</a> <a id="22034" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#22034" class="Bound">n</a> <a id="22036" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#22036" class="Bound">p</a> <a id="22063" class="Symbol">=</a> <a id="22066" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a>
|
||
<a id="22071" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#21964" class="Function">+-assoc′</a> <a id="22080" class="Symbol">(</a><a id="22081" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="22085" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#22085" class="Bound">m</a><a id="22086" class="Symbol">)</a> <a id="22088" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#22088" class="Bound">n</a> <a id="22090" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#22090" class="Bound">p</a> <a id="22093" class="Keyword">rewrite</a> <a id="22101" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#21964" class="Function">+-assoc′</a> <a id="22110" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#22085" class="Bound">m</a> <a id="22112" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#22088" class="Bound">n</a> <a id="22114" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#22090" class="Bound">p</a> <a id="22117" class="Symbol">=</a> <a id="22120" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a>
|
||
</pre>
|
||
<p>For the base case, we must show:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>(zero + n) + p ≡ zero + (n + p)
|
||
</code></pre></div></div>
|
||
|
||
<p>Simplifying both sides with the base case of addition yields the equation:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>n + p ≡ n + p
|
||
</code></pre></div></div>
|
||
|
||
<p>This holds trivially. The proof that a term is equal to itself is written <code class="language-plaintext highlighter-rouge">refl</code>.</p>
|
||
|
||
<p>For the inductive case, we must show:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>(suc m + n) + p ≡ suc m + (n + p)
|
||
</code></pre></div></div>
|
||
|
||
<p>Simplifying both sides with the inductive case of addition yields the equation:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>suc ((m + n) + p) ≡ suc (m + (n + p))
|
||
</code></pre></div></div>
|
||
|
||
<p>After rewriting with the inductive hypothesis these two terms are equal, and the
|
||
proof is again given by <code class="language-plaintext highlighter-rouge">refl</code>. Rewriting by a given equation is indicated by
|
||
the keyword <code class="language-plaintext highlighter-rouge">rewrite</code> followed by a proof of that equation. Rewriting avoids
|
||
not only chains of equations but also the need to invoke <code class="language-plaintext highlighter-rouge">cong</code>.</p>
|
||
|
||
<h2 id="commutativity-with-rewrite">Commutativity with rewrite</h2>
|
||
|
||
<p>Here is a second proof of commutativity of addition, using <code class="language-plaintext highlighter-rouge">rewrite</code> rather than
|
||
chains of equations:</p>
|
||
<pre class="Agda"><a id="+-identity′"></a><a id="23023" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#23023" class="Function">+-identity′</a> <a id="23035" class="Symbol">:</a> <a id="23037" class="Symbol">∀</a> <a id="23039" class="Symbol">(</a><a id="23040" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#23040" class="Bound">n</a> <a id="23042" class="Symbol">:</a> <a id="23044" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="23045" class="Symbol">)</a> <a id="23047" class="Symbol">→</a> <a id="23049" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#23040" class="Bound">n</a> <a id="23051" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="23053" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">zero</a> <a id="23058" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="23060" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#23040" class="Bound">n</a>
|
||
<a id="23062" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#23023" class="Function">+-identity′</a> <a id="23074" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">zero</a> <a id="23079" class="Symbol">=</a> <a id="23081" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a>
|
||
<a id="23086" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#23023" class="Function">+-identity′</a> <a id="23098" class="Symbol">(</a><a id="23099" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="23103" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#23103" class="Bound">n</a><a id="23104" class="Symbol">)</a> <a id="23106" class="Keyword">rewrite</a> <a id="23114" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#23023" class="Function">+-identity′</a> <a id="23126" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#23103" class="Bound">n</a> <a id="23128" class="Symbol">=</a> <a id="23130" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a>
|
||
|
||
<a id="+-suc′"></a><a id="23136" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#23136" class="Function">+-suc′</a> <a id="23143" class="Symbol">:</a> <a id="23145" class="Symbol">∀</a> <a id="23147" class="Symbol">(</a><a id="23148" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#23148" class="Bound">m</a> <a id="23150" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#23150" class="Bound">n</a> <a id="23152" class="Symbol">:</a> <a id="23154" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="23155" class="Symbol">)</a> <a id="23157" class="Symbol">→</a> <a id="23159" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#23148" class="Bound">m</a> <a id="23161" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="23163" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="23167" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#23150" class="Bound">n</a> <a id="23169" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="23171" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="23175" class="Symbol">(</a><a id="23176" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#23148" class="Bound">m</a> <a id="23178" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="23180" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#23150" class="Bound">n</a><a id="23181" class="Symbol">)</a>
|
||
<a id="23183" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#23136" class="Function">+-suc′</a> <a id="23190" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">zero</a> <a id="23195" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#23195" class="Bound">n</a> <a id="23197" class="Symbol">=</a> <a id="23199" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a>
|
||
<a id="23204" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#23136" class="Function">+-suc′</a> <a id="23211" class="Symbol">(</a><a id="23212" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="23216" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#23216" class="Bound">m</a><a id="23217" class="Symbol">)</a> <a id="23219" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#23219" class="Bound">n</a> <a id="23221" class="Keyword">rewrite</a> <a id="23229" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#23136" class="Function">+-suc′</a> <a id="23236" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#23216" class="Bound">m</a> <a id="23238" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#23219" class="Bound">n</a> <a id="23240" class="Symbol">=</a> <a id="23242" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a>
|
||
|
||
<a id="+-comm′"></a><a id="23248" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#23248" class="Function">+-comm′</a> <a id="23256" class="Symbol">:</a> <a id="23258" class="Symbol">∀</a> <a id="23260" class="Symbol">(</a><a id="23261" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#23261" class="Bound">m</a> <a id="23263" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#23263" class="Bound">n</a> <a id="23265" class="Symbol">:</a> <a id="23267" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="23268" class="Symbol">)</a> <a id="23270" class="Symbol">→</a> <a id="23272" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#23261" class="Bound">m</a> <a id="23274" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="23276" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#23263" class="Bound">n</a> <a id="23278" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="23280" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#23263" class="Bound">n</a> <a id="23282" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="23284" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#23261" class="Bound">m</a>
|
||
<a id="23286" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#23248" class="Function">+-comm′</a> <a id="23294" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#23294" class="Bound">m</a> <a id="23296" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">zero</a> <a id="23301" class="Keyword">rewrite</a> <a id="23309" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#23023" class="Function">+-identity′</a> <a id="23321" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#23294" class="Bound">m</a> <a id="23323" class="Symbol">=</a> <a id="23325" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a>
|
||
<a id="23330" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#23248" class="Function">+-comm′</a> <a id="23338" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#23338" class="Bound">m</a> <a id="23340" class="Symbol">(</a><a id="23341" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="23345" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#23345" class="Bound">n</a><a id="23346" class="Symbol">)</a> <a id="23348" class="Keyword">rewrite</a> <a id="23356" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#23136" class="Function">+-suc′</a> <a id="23363" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#23338" class="Bound">m</a> <a id="23365" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#23345" class="Bound">n</a> <a id="23367" class="Symbol">|</a> <a id="23369" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#23248" class="Function">+-comm′</a> <a id="23377" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#23338" class="Bound">m</a> <a id="23379" href="plfa.part1.https://agda.github.io/agda-stdlib/v1.1/Induction.html#23345" class="Bound">n</a> <a id="23381" class="Symbol">=</a> <a id="23383" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a>
|
||
</pre>
|
||
<p>In the final line, rewriting with two equations is
|
||
indicated by separating the two proofs of the relevant equations by a
|
||
vertical bar; the rewrite on the left is performed before that on the
|
||
right.</p>
|
||
|
||
<h2 id="building-proofs-interactively">Building proofs interactively</h2>
|
||
|
||
<p>It is instructive to see how to build the alternative proof of
|
||
associativity using the interactive features of Agda in Emacs.
|
||
Begin by typing:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>+-assoc′ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
|
||
+-assoc′ m n p = ?
|
||
</code></pre></div></div>
|
||
|
||
<p>The question mark indicates that you would like Agda to help with
|
||
filling in that part of the code. If you type <code class="language-plaintext highlighter-rouge">C-c C-l</code> (control-c
|
||
followed by control-l), the question mark will be replaced:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>+-assoc′ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
|
||
+-assoc′ m n p = { }0
|
||
</code></pre></div></div>
|
||
|
||
<p>The empty braces are called a <em>hole</em>, and 0 is a number used for
|
||
referring to the hole. The hole may display highlighted in green.
|
||
Emacs will also create a new window at the bottom of the screen
|
||
displaying the text:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>?0 : ((m + n) + p) ≡ (m + (n + p))
|
||
</code></pre></div></div>
|
||
|
||
<p>This indicates that hole 0 is to be filled in with a proof of
|
||
the stated judgment.</p>
|
||
|
||
<p>We wish to prove the proposition by induction on <code class="language-plaintext highlighter-rouge">m</code>. Move
|
||
the cursor into the hole and type <code class="language-plaintext highlighter-rouge">C-c C-c</code>. You will be given
|
||
the prompt:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>pattern variables to case (empty for split on result):
|
||
</code></pre></div></div>
|
||
|
||
<p>Typing <code class="language-plaintext highlighter-rouge">m</code> will cause a split on that variable, resulting
|
||
in an update to the code:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>+-assoc′ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
|
||
+-assoc′ zero n p = { }0
|
||
+-assoc′ (suc m) n p = { }1
|
||
</code></pre></div></div>
|
||
|
||
<p>There are now two holes, and the window at the bottom tells you what
|
||
each is required to prove:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>?0 : ((zero + n) + p) ≡ (zero + (n + p))
|
||
?1 : ((suc m + n) + p) ≡ (suc m + (n + p))
|
||
</code></pre></div></div>
|
||
|
||
<p>Going into hole 0 and typing <code class="language-plaintext highlighter-rouge">C-c C-,</code> will display the text:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>Goal: (n + p) ≡ (n + p)
|
||
————————————————————————————————————————————————————————————
|
||
p : ℕ
|
||
n : ℕ
|
||
</code></pre></div></div>
|
||
|
||
<p>This indicates that after simplification the goal for hole 0 is as
|
||
stated, and that variables <code class="language-plaintext highlighter-rouge">p</code> and <code class="language-plaintext highlighter-rouge">n</code> of the stated types are
|
||
available to use in the proof. The proof of the given goal is
|
||
trivial, and going into the goal and typing <code class="language-plaintext highlighter-rouge">C-c C-r</code> will fill it in.
|
||
Typing <code class="language-plaintext highlighter-rouge">C-c C-l</code> renumbers the remaining hole to 0:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>+-assoc′ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
|
||
+-assoc′ zero n p = refl
|
||
+-assoc′ (suc m) n p = { }0
|
||
</code></pre></div></div>
|
||
|
||
<p>Going into the new hole 0 and typing <code class="language-plaintext highlighter-rouge">C-c C-,</code> will display the text:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>Goal: suc ((m + n) + p) ≡ suc (m + (n + p))
|
||
————————————————————————————————————————————————————————————
|
||
p : ℕ
|
||
n : ℕ
|
||
m : ℕ
|
||
</code></pre></div></div>
|
||
|
||
<p>Again, this gives the simplified goal and the available variables.
|
||
In this case, we need to rewrite by the induction
|
||
hypothesis, so let’s edit the text accordingly:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>+-assoc′ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
|
||
+-assoc′ zero n p = refl
|
||
+-assoc′ (suc m) n p rewrite +-assoc′ m n p = { }0
|
||
</code></pre></div></div>
|
||
|
||
<p>Going into the remaining hole and typing <code class="language-plaintext highlighter-rouge">C-c C-,</code> will display the text:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>Goal: suc (m + (n + p)) ≡ suc (m + (n + p))
|
||
————————————————————————————————————————————————————————————
|
||
p : ℕ
|
||
n : ℕ
|
||
m : ℕ
|
||
</code></pre></div></div>
|
||
|
||
<p>The proof of the given goal is trivial, and going into the goal and
|
||
typing <code class="language-plaintext highlighter-rouge">C-c C-r</code> will fill it in, completing the proof:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>+-assoc′ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
|
||
+-assoc′ zero n p = refl
|
||
+-assoc′ (suc m) n p rewrite +-assoc′ m n p = refl
|
||
</code></pre></div></div>
|
||
|
||
<h4 id="plus-swap">Exercise <code class="language-plaintext highlighter-rouge">+-swap</code> (recommended)</h4>
|
||
|
||
<p>Show</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>m + (n + p) ≡ n + (m + p)
|
||
</code></pre></div></div>
|
||
|
||
<p>for all naturals <code class="language-plaintext highlighter-rouge">m</code>, <code class="language-plaintext highlighter-rouge">n</code>, and <code class="language-plaintext highlighter-rouge">p</code>. No induction is needed,
|
||
just apply the previous results which show addition
|
||
is associative and commutative.</p>
|
||
|
||
<pre class="Agda"><a id="26923" class="Comment">-- Your code goes here</a>
|
||
</pre>
|
||
|
||
<h4 id="times-distrib-plus">Exercise <code class="language-plaintext highlighter-rouge">*-distrib-+</code> (recommended)</h4>
|
||
|
||
<p>Show multiplication distributes over addition, that is,</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>(m + n) * p ≡ m * p + n * p
|
||
</code></pre></div></div>
|
||
|
||
<p>for all naturals <code class="language-plaintext highlighter-rouge">m</code>, <code class="language-plaintext highlighter-rouge">n</code>, and <code class="language-plaintext highlighter-rouge">p</code>.</p>
|
||
|
||
<pre class="Agda"><a id="27148" class="Comment">-- Your code goes here</a>
|
||
</pre>
|
||
|
||
<h4 id="times-assoc">Exercise <code class="language-plaintext highlighter-rouge">*-assoc</code> (recommended)</h4>
|
||
|
||
<p>Show multiplication is associative, that is,</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>(m * n) * p ≡ m * (n * p)
|
||
</code></pre></div></div>
|
||
|
||
<p>for all naturals <code class="language-plaintext highlighter-rouge">m</code>, <code class="language-plaintext highlighter-rouge">n</code>, and <code class="language-plaintext highlighter-rouge">p</code>.</p>
|
||
|
||
<pre class="Agda"><a id="27349" class="Comment">-- Your code goes here</a>
|
||
</pre>
|
||
|
||
<h4 id="times-comm">Exercise <code class="language-plaintext highlighter-rouge">*-comm</code> (practice)</h4>
|
||
|
||
<p>Show multiplication is commutative, that is,</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>m * n ≡ n * m
|
||
</code></pre></div></div>
|
||
|
||
<p>for all naturals <code class="language-plaintext highlighter-rouge">m</code> and <code class="language-plaintext highlighter-rouge">n</code>. As with commutativity of addition,
|
||
you will need to formulate and prove suitable lemmas.</p>
|
||
|
||
<pre class="Agda"><a id="27617" class="Comment">-- Your code goes here</a>
|
||
</pre>
|
||
|
||
<h4 id="zero-monus">Exercise <code class="language-plaintext highlighter-rouge">0∸n≡0</code> (practice)</h4>
|
||
|
||
<p>Show</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>zero ∸ n ≡ zero
|
||
</code></pre></div></div>
|
||
|
||
<p>for all naturals <code class="language-plaintext highlighter-rouge">n</code>. Did your proof require induction?</p>
|
||
|
||
<pre class="Agda"><a id="27782" class="Comment">-- Your code goes here</a>
|
||
</pre>
|
||
|
||
<h4 id="monus-plus-assoc">Exercise <code class="language-plaintext highlighter-rouge">∸-+-assoc</code> (practice)</h4>
|
||
|
||
<p>Show that monus associates with addition, that is,</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>m ∸ n ∸ p ≡ m ∸ (n + p)
|
||
</code></pre></div></div>
|
||
|
||
<p>for all naturals <code class="language-plaintext highlighter-rouge">m</code>, <code class="language-plaintext highlighter-rouge">n</code>, and <code class="language-plaintext highlighter-rouge">p</code>.</p>
|
||
|
||
<pre class="Agda"><a id="27991" class="Comment">-- Your code goes here</a>
|
||
</pre>
|
||
|
||
<h4 id="exercise--stretch">Exercise <code class="language-plaintext highlighter-rouge">+*^</code> (stretch)</h4>
|
||
|
||
<p>Show the following three laws</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code> m ^ (n + p) ≡ (m ^ n) * (m ^ p) (^-distribˡ-+-*)
|
||
(m * n) ^ p ≡ (m ^ p) * (n ^ p) (^-distribʳ-*)
|
||
(m ^ n) ^ p ≡ m ^ (n * p) (^-*-assoc)
|
||
</code></pre></div></div>
|
||
|
||
<p>for all <code class="language-plaintext highlighter-rouge">m</code>, <code class="language-plaintext highlighter-rouge">n</code>, and <code class="language-plaintext highlighter-rouge">p</code>.</p>
|
||
|
||
<h4 id="Bin-laws">Exercise <code class="language-plaintext highlighter-rouge">Bin-laws</code> (stretch)</h4>
|
||
|
||
<p>Recall that
|
||
Exercise <a href="/20.07/Naturals/#Bin">Bin</a>
|
||
defines a datatype <code class="language-plaintext highlighter-rouge">Bin</code> of bitstrings representing natural numbers,
|
||
and asks you to define functions</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>inc : Bin → Bin
|
||
to : ℕ → Bin
|
||
from : Bin → ℕ
|
||
</code></pre></div></div>
|
||
|
||
<p>Consider the following laws, where <code class="language-plaintext highlighter-rouge">n</code> ranges over naturals and <code class="language-plaintext highlighter-rouge">b</code>
|
||
over bitstrings:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>from (inc b) ≡ suc (from b)
|
||
to (from b) ≡ b
|
||
from (to n) ≡ n
|
||
</code></pre></div></div>
|
||
|
||
<p>For each law: if it holds, prove; if not, give a counterexample.</p>
|
||
|
||
<pre class="Agda"><a id="28774" class="Comment">-- Your code goes here</a>
|
||
</pre>
|
||
|
||
<h2 id="standard-library">Standard library</h2>
|
||
|
||
<p>Definitions similar to those in this chapter can be found in the standard library:</p>
|
||
<pre class="Agda"><a id="28911" class="Keyword">import</a> <a id="28918" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html" class="Module">Data.Nat.Properties</a> <a id="28938" class="Keyword">using</a> <a id="28944" class="Symbol">(</a><a id="28945" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#11578" class="Function">+-assoc</a><a id="28952" class="Symbol">;</a> <a id="28954" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#11734" class="Function">+-identityʳ</a><a id="28965" class="Symbol">;</a> <a id="28967" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#11370" class="Function">+-suc</a><a id="28972" class="Symbol">;</a> <a id="28974" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#11911" class="Function">+-comm</a><a id="28980" class="Symbol">)</a>
|
||
</pre>
|
||
<h2 id="unicode">Unicode</h2>
|
||
|
||
<p>This chapter uses the following unicode:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>∀ U+2200 FOR ALL (\forall, \all)
|
||
ʳ U+02B3 MODIFIER LETTER SMALL R (\^r)
|
||
′ U+2032 PRIME (\')
|
||
″ U+2033 DOUBLE PRIME (\')
|
||
‴ U+2034 TRIPLE PRIME (\')
|
||
⁗ U+2057 QUADRUPLE PRIME (\')
|
||
</code></pre></div></div>
|
||
|
||
<p>Similar to <code class="language-plaintext highlighter-rouge">\r</code>, the command <code class="language-plaintext highlighter-rouge">\^r</code> gives access to a variety of
|
||
superscript rightward arrows, and also a superscript letter <code class="language-plaintext highlighter-rouge">r</code>.
|
||
The command <code class="language-plaintext highlighter-rouge">\'</code> gives access to a range of primes (<code class="language-plaintext highlighter-rouge">′ ″ ‴ ⁗</code>).</p>
|
||
|
||
</div>
|
||
|
||
<p style="text-align:center;">
|
||
|
||
<a alt="Previous chapter" href="/20.07/Naturals/">Prev</a>
|
||
|
||
|
||
•
|
||
|
||
|
||
<a alt="Source code" href="https://github.com/plfa/plfa.github.io/blob/dev-20.07/src/plfa/part1/Induction.lagda.md">Source</a>
|
||
|
||
|
||
•
|
||
|
||
|
||
<a alt="Next chapter" href="/20.07/Relations/">Next</a>
|
||
|
||
</p>
|
||
|
||
|
||
</article>
|
||
|
||
</div>
|
||
</main><footer class="site-footer h-card">
|
||
<data class="u-url" href="/20.07/"></data>
|
||
|
||
<div class="wrapper">
|
||
|
||
<h2 class="footer-heading">Programming Language Foundations in Agda
|
||
</h2><div class="footer-col-wrapper">
|
||
<div class="footer-col footer-col-1">
|
||
<ul class="contact-list">
|
||
<li class="p-name">Philip Wadler</li>
|
||
<li><a class="u-email" href="mailto:wadler@inf.ed.ac.uk">wadler@inf.ed.ac.uk</a></li>
|
||
</ul>
|
||
</div>
|
||
|
||
<div class="footer-col footer-col-2"><ul class="social-media-list"><li><a href="https://github.com/wadler"><svg class="svg-icon"><use xlink:href="/20.07/assets/minima-social-icons.svg#github"></use></svg> <span class="username">wadler</span></a></li></ul>
|
||
</div>
|
||
|
||
<div class="footer-col footer-col-3"></div>
|
||
</div><div class="footer-col-wrapper">
|
||
<div class="footer-col footer-col-1">
|
||
<ul class="contact-list">
|
||
<li class="p-name">Wen Kokke</li>
|
||
<li><a class="u-email" href="mailto:wen.kokke@ed.ac.uk">wen.kokke@ed.ac.uk</a></li>
|
||
</ul>
|
||
</div>
|
||
|
||
<div class="footer-col footer-col-2"><ul class="social-media-list"><li><a href="https://github.com/wenkokke"><svg class="svg-icon"><use xlink:href="/20.07/assets/minima-social-icons.svg#github"></use></svg> <span class="username">wenkokke</span></a></li><li><a href="https://www.twitter.com/wenkokke"><svg class="svg-icon"><use xlink:href="/20.07/assets/minima-social-icons.svg#twitter"></use></svg> <span class="username">wenkokke</span></a></li></ul>
|
||
</div>
|
||
|
||
<div class="footer-col footer-col-3"></div>
|
||
</div><div class="footer-col-wrapper">
|
||
<div class="footer-col footer-col-1">
|
||
<ul class="contact-list">
|
||
<li class="p-name">Jeremy G. Siek</li>
|
||
<li><a class="u-email" href="mailto:jsiek@indiana.edu">jsiek@indiana.edu</a></li>
|
||
</ul>
|
||
</div>
|
||
|
||
<div class="footer-col footer-col-2"><ul class="social-media-list"><li><a href="https://github.com/jsiek"><svg class="svg-icon"><use xlink:href="/20.07/assets/minima-social-icons.svg#github"></use></svg> <span class="username">jsiek</span></a></li><li><a href="https://www.twitter.com/jeremysiek"><svg class="svg-icon"><use xlink:href="/20.07/assets/minima-social-icons.svg#twitter"></use></svg> <span class="username">jeremysiek</span></a></li></ul>
|
||
</div>
|
||
|
||
<div class="footer-col footer-col-3"></div>
|
||
</div>This work is licensed under a <a rel="license" href="https://creativecommons.org/licenses/by/4.0/">Creative Commons Attribution 4.0 International License</a>
|
||
</div>
|
||
</footer>
|
||
<!-- Import jQuery -->
|
||
<script type="text/javascript" src="/20.07/assets/jquery.js"></script>
|
||
|
||
<script src="https://cdnjs.cloudflare.com/ajax/libs/anchor-js/4.2.2/anchor.min.js" integrity="sha256-E4RlfxwyJVmkkk0szw7LYJxuPlp6evtPSBDlWHsYYL8=" crossorigin="anonymous"></script>
|
||
<script type="text/javascript">
|
||
anchors.add();
|
||
</script>
|
||
|
||
<script type="text/javascript">
|
||
|
||
// Makes sandwhich menu works
|
||
$('.menu-icon').click(function(){
|
||
$('.trigger').toggle();
|
||
});
|
||
|
||
// Script which allows for foldable code blocks
|
||
$('div.foldable pre').each(function(){
|
||
var autoHeight = $(this).height();
|
||
var lineHeight = parseFloat($(this).css('line-height'));
|
||
|
||
var plus = $("<div></div>");
|
||
var horLine = $("<div></div>");
|
||
var verLine = $("<div></div>");
|
||
$(this).prepend(plus);
|
||
plus.css({
|
||
'position' : 'relative',
|
||
'float' : 'right',
|
||
'right' : '-' + (0.5 * lineHeight - 1.5) + 'px',
|
||
'width' : lineHeight,
|
||
'height' : lineHeight});
|
||
verLine.css({
|
||
'position' : 'relative',
|
||
'height' : lineHeight,
|
||
'width' : '3px',
|
||
'background-color' : '#C1E0FF'});
|
||
horLine.css({
|
||
'position' : 'relative',
|
||
'top' : '-' + (0.5 * lineHeight + 1.5) + 'px',
|
||
'left' : '-' + (0.5 * lineHeight - 1.5) + 'px',
|
||
'height' : '3px',
|
||
'width' : lineHeight,
|
||
'background-color' : '#C1E0FF'});
|
||
plus.append(verLine);
|
||
plus.append(horLine);
|
||
|
||
$(this).height(2.0 * lineHeight);
|
||
$(this).css('overflow','hidden');
|
||
|
||
$(this).click(function(){
|
||
if ($(this).height() == autoHeight) {
|
||
$(this).height(2.0 * lineHeight);
|
||
plus.show();
|
||
}
|
||
else {
|
||
$(this).height('auto');
|
||
plus.hide();
|
||
}
|
||
});
|
||
});
|
||
</script>
|
||
|
||
<!-- Import KaTeX -->
|
||
<script type="text/javascript" src="/20.07/assets/katex.js"></script>
|
||
|
||
<!-- Script which renders TeX using KaTeX -->
|
||
<script type="text/javascript">
|
||
$("script[type='math/tex']").replaceWith(
|
||
function(){
|
||
var tex = $(this).text();
|
||
return "<span class=\"inline-equation\">" +
|
||
katex.renderToString(tex) +
|
||
"</span>";
|
||
});
|
||
$("script[type='math/tex; mode=display']").replaceWith(
|
||
function(){
|
||
var tex = $(this).text().replace(/%.*?(\n|$)/g,"");
|
||
return "<div class=\"equation\">" +
|
||
katex.renderToString("\\displaystyle "+tex) +
|
||
"</div>";
|
||
});
|
||
</script>
|
||
</body>
|
||
|
||
</html>
|