1034 lines
109 KiB
HTML
1034 lines
109 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>Relations: Inductive definition of relations | 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="Relations: Inductive definition of relations" />
|
||
<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/Relations/" />
|
||
<meta property="og:url" content="https://plfa.github.io/20.07/Relations/" />
|
||
<meta property="og:site_name" content="Programming Language Foundations in Agda" />
|
||
<script type="application/ld+json">
|
||
{"url":"https://plfa.github.io/20.07/Relations/","headline":"Relations: Inductive definition of relations","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">Relations: Inductive definition of relations</h1>
|
||
</header>
|
||
|
||
<p style="text-align:center;">
|
||
|
||
<a alt="Previous chapter" href="/20.07/Induction/">Prev</a>
|
||
|
||
|
||
•
|
||
|
||
|
||
<a alt="Source code" href="https://github.com/plfa/plfa.github.io/blob/dev-20.07/src/plfa/part1/Relations.lagda.md">Source</a>
|
||
|
||
|
||
•
|
||
|
||
|
||
<a alt="Next chapter" href="/20.07/Equality/">Next</a>
|
||
|
||
</p>
|
||
|
||
|
||
<div class="post-content">
|
||
<pre class="Agda"><a id="161" class="Keyword">module</a> <a id="168" href="/20.07/Relations/" class="Module">plfa.part1.Relations</a> <a id="189" class="Keyword">where</a>
|
||
</pre>
|
||
<p>After having defined operations such as addition and multiplication,
|
||
the next step is to define relations, such as <em>less than or equal</em>.</p>
|
||
|
||
<h2 id="imports">Imports</h2>
|
||
|
||
<pre class="Agda"><a id="354" class="Keyword">import</a> <a id="361" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.html" class="Module">Relation.Binary.PropositionalEquality</a> <a id="399" class="Symbol">as</a> <a id="402" class="Module">Eq</a>
|
||
<a id="405" class="Keyword">open</a> <a id="410" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.html" class="Module">Eq</a> <a id="413" class="Keyword">using</a> <a id="419" class="Symbol">(</a><a id="420" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">_≡_</a><a id="423" class="Symbol">;</a> <a id="425" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a><a id="429" class="Symbol">;</a> <a id="431" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#1090" class="Function">cong</a><a id="435" class="Symbol">)</a>
|
||
<a id="437" class="Keyword">open</a> <a id="442" class="Keyword">import</a> <a id="449" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.html" class="Module">Data.Nat</a> <a id="458" class="Keyword">using</a> <a id="464" class="Symbol">(</a><a id="465" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="466" class="Symbol">;</a> <a id="468" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">zero</a><a id="472" class="Symbol">;</a> <a id="474" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a><a id="477" class="Symbol">;</a> <a id="479" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">_+_</a><a id="482" class="Symbol">)</a>
|
||
<a id="484" class="Keyword">open</a> <a id="489" class="Keyword">import</a> <a id="496" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html" class="Module">Data.Nat.Properties</a> <a id="516" class="Keyword">using</a> <a id="522" class="Symbol">(</a><a id="523" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#11911" class="Function">+-comm</a><a id="529" class="Symbol">;</a> <a id="531" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#11734" class="Function">+-identityʳ</a><a id="542" class="Symbol">)</a>
|
||
</pre>
|
||
|
||
<h2 id="defining-relations">Defining relations</h2>
|
||
|
||
<p>The relation <em>less than or equal</em> has an infinite number of
|
||
instances. Here are a few of them:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>0 ≤ 0 0 ≤ 1 0 ≤ 2 0 ≤ 3 ...
|
||
1 ≤ 1 1 ≤ 2 1 ≤ 3 ...
|
||
2 ≤ 2 2 ≤ 3 ...
|
||
3 ≤ 3 ...
|
||
...
|
||
</code></pre></div></div>
|
||
|
||
<p>And yet, we can write a finite definition that encompasses
|
||
all of these instances in just a few lines. Here is the
|
||
definition as a pair of inference rules:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>z≤n --------
|
||
zero ≤ n
|
||
|
||
m ≤ n
|
||
s≤s -------------
|
||
suc m ≤ suc n
|
||
</code></pre></div></div>
|
||
|
||
<p>And here is the definition in Agda:</p>
|
||
<pre class="Agda"><a id="1203" class="Keyword">data</a> <a id="_≤_"></a><a id="1208" href="/20.07/Relations/#1208" class="Datatype Operator">_≤_</a> <a id="1212" class="Symbol">:</a> <a id="1214" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a> <a id="1216" class="Symbol">→</a> <a id="1218" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a> <a id="1220" class="Symbol">→</a> <a id="1222" class="PrimitiveType">Set</a> <a id="1226" class="Keyword">where</a>
|
||
|
||
<a id="_≤_.z≤n"></a><a id="1235" href="/20.07/Relations/#1235" class="InductiveConstructor">z≤n</a> <a id="1239" class="Symbol">:</a> <a id="1241" class="Symbol">∀</a> <a id="1243" class="Symbol">{</a><a id="1244" href="/20.07/Relations/#1244" class="Bound">n</a> <a id="1246" class="Symbol">:</a> <a id="1248" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="1249" class="Symbol">}</a>
|
||
<a id="1257" class="Comment">--------</a>
|
||
<a id="1270" class="Symbol">→</a> <a id="1272" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">zero</a> <a id="1277" href="/20.07/Relations/#1208" class="Datatype Operator">≤</a> <a id="1279" href="/20.07/Relations/#1244" class="Bound">n</a>
|
||
|
||
<a id="_≤_.s≤s"></a><a id="1284" href="/20.07/Relations/#1284" class="InductiveConstructor">s≤s</a> <a id="1288" class="Symbol">:</a> <a id="1290" class="Symbol">∀</a> <a id="1292" class="Symbol">{</a><a id="1293" href="/20.07/Relations/#1293" class="Bound">m</a> <a id="1295" href="/20.07/Relations/#1295" class="Bound">n</a> <a id="1297" class="Symbol">:</a> <a id="1299" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="1300" class="Symbol">}</a>
|
||
<a id="1306" class="Symbol">→</a> <a id="1308" href="/20.07/Relations/#1293" class="Bound">m</a> <a id="1310" href="/20.07/Relations/#1208" class="Datatype Operator">≤</a> <a id="1312" href="/20.07/Relations/#1295" class="Bound">n</a>
|
||
<a id="1320" class="Comment">-------------</a>
|
||
<a id="1338" class="Symbol">→</a> <a id="1340" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="1344" href="/20.07/Relations/#1293" class="Bound">m</a> <a id="1346" href="/20.07/Relations/#1208" class="Datatype Operator">≤</a> <a id="1348" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="1352" href="/20.07/Relations/#1295" class="Bound">n</a>
|
||
</pre>
|
||
<p>Here <code class="language-plaintext highlighter-rouge">z≤n</code> and <code class="language-plaintext highlighter-rouge">s≤s</code> (with no spaces) are constructor names, while
|
||
<code class="language-plaintext highlighter-rouge">zero ≤ n</code>, and <code class="language-plaintext highlighter-rouge">m ≤ n</code> and <code class="language-plaintext highlighter-rouge">suc m ≤ suc n</code> (with spaces) are types.
|
||
This is our first use of an <em>indexed</em> datatype, where the type <code class="language-plaintext highlighter-rouge">m ≤ n</code>
|
||
is indexed by two naturals, <code class="language-plaintext highlighter-rouge">m</code> and <code class="language-plaintext highlighter-rouge">n</code>. In Agda any line beginning
|
||
with two or more dashes is a comment, and here we have exploited that
|
||
convention to write our Agda code in a form that resembles the
|
||
corresponding inference rules, a trick we will use often from now on.</p>
|
||
|
||
<p>Both definitions above tell us the same two things:</p>
|
||
|
||
<ul>
|
||
<li><em>Base case</em>: for all naturals <code class="language-plaintext highlighter-rouge">n</code>, the proposition <code class="language-plaintext highlighter-rouge">zero ≤ n</code> holds.</li>
|
||
<li><em>Inductive case</em>: for all naturals <code class="language-plaintext highlighter-rouge">m</code> and <code class="language-plaintext highlighter-rouge">n</code>, if the proposition
|
||
<code class="language-plaintext highlighter-rouge">m ≤ n</code> holds, then the proposition <code class="language-plaintext highlighter-rouge">suc m ≤ suc n</code> holds.</li>
|
||
</ul>
|
||
|
||
<p>In fact, they each give us a bit more detail:</p>
|
||
|
||
<ul>
|
||
<li><em>Base case</em>: for all naturals <code class="language-plaintext highlighter-rouge">n</code>, the constructor <code class="language-plaintext highlighter-rouge">z≤n</code>
|
||
produces evidence that <code class="language-plaintext highlighter-rouge">zero ≤ n</code> holds.</li>
|
||
<li><em>Inductive case</em>: for all naturals <code class="language-plaintext highlighter-rouge">m</code> and <code class="language-plaintext highlighter-rouge">n</code>, the constructor
|
||
<code class="language-plaintext highlighter-rouge">s≤s</code> takes evidence that <code class="language-plaintext highlighter-rouge">m ≤ n</code> holds into evidence that
|
||
<code class="language-plaintext highlighter-rouge">suc m ≤ suc n</code> holds.</li>
|
||
</ul>
|
||
|
||
<p>For example, here in inference rule notation is the proof that
|
||
<code class="language-plaintext highlighter-rouge">2 ≤ 4</code>:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code> z≤n -----
|
||
0 ≤ 2
|
||
s≤s -------
|
||
1 ≤ 3
|
||
s≤s ---------
|
||
2 ≤ 4
|
||
</code></pre></div></div>
|
||
|
||
<p>And here is the corresponding Agda proof:</p>
|
||
<pre class="Agda"><a id="2614" href="/20.07/Relations/#2614" class="Function">_</a> <a id="2616" class="Symbol">:</a> <a id="2618" class="Number">2</a> <a id="2620" href="/20.07/Relations/#1208" class="Datatype Operator">≤</a> <a id="2622" class="Number">4</a>
|
||
<a id="2624" class="Symbol">_</a> <a id="2626" class="Symbol">=</a> <a id="2628" href="/20.07/Relations/#1284" class="InductiveConstructor">s≤s</a> <a id="2632" class="Symbol">(</a><a id="2633" href="/20.07/Relations/#1284" class="InductiveConstructor">s≤s</a> <a id="2637" href="/20.07/Relations/#1235" class="InductiveConstructor">z≤n</a><a id="2640" class="Symbol">)</a>
|
||
</pre>
|
||
|
||
<h2 id="implicit-arguments">Implicit arguments</h2>
|
||
|
||
<p>This is our first use of implicit arguments. In the definition of
|
||
inequality, the two lines defining the constructors use <code class="language-plaintext highlighter-rouge">∀</code>, very
|
||
similar to our use of <code class="language-plaintext highlighter-rouge">∀</code> in propositions such as:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>+-comm : ∀ (m n : ℕ) → m + n ≡ n + m
|
||
</code></pre></div></div>
|
||
|
||
<p>However, here the declarations are surrounded by curly braces <code class="language-plaintext highlighter-rouge">{ }</code>
|
||
rather than parentheses <code class="language-plaintext highlighter-rouge">( )</code>. This means that the arguments are
|
||
<em>implicit</em> and need not be written explicitly; instead, they are
|
||
<em>inferred</em> by Agda’s typechecker. Thus, we write <code class="language-plaintext highlighter-rouge">+-comm m n</code> for the
|
||
proof that <code class="language-plaintext highlighter-rouge">m + n ≡ n + m</code>, but <code class="language-plaintext highlighter-rouge">z≤n</code> for the proof that <code class="language-plaintext highlighter-rouge">zero ≤ n</code>,
|
||
leaving <code class="language-plaintext highlighter-rouge">n</code> implicit. Similarly, if <code class="language-plaintext highlighter-rouge">m≤n</code> is evidence that <code class="language-plaintext highlighter-rouge">m ≤ n</code>,
|
||
we write <code class="language-plaintext highlighter-rouge">s≤s m≤n</code> for evidence that <code class="language-plaintext highlighter-rouge">suc m ≤ suc n</code>, leaving both <code class="language-plaintext highlighter-rouge">m</code>
|
||
and <code class="language-plaintext highlighter-rouge">n</code> implicit.</p>
|
||
|
||
<p>If we wish, it is possible to provide implicit arguments explicitly by
|
||
writing the arguments inside curly braces. For instance, here is the
|
||
Agda proof that <code class="language-plaintext highlighter-rouge">2 ≤ 4</code> repeated, with the implicit arguments made
|
||
explicit:</p>
|
||
<pre class="Agda"><a id="3619" href="/20.07/Relations/#3619" class="Function">_</a> <a id="3621" class="Symbol">:</a> <a id="3623" class="Number">2</a> <a id="3625" href="/20.07/Relations/#1208" class="Datatype Operator">≤</a> <a id="3627" class="Number">4</a>
|
||
<a id="3629" class="Symbol">_</a> <a id="3631" class="Symbol">=</a> <a id="3633" href="/20.07/Relations/#1284" class="InductiveConstructor">s≤s</a> <a id="3637" class="Symbol">{</a><a id="3638" class="Number">1</a><a id="3639" class="Symbol">}</a> <a id="3641" class="Symbol">{</a><a id="3642" class="Number">3</a><a id="3643" class="Symbol">}</a> <a id="3645" class="Symbol">(</a><a id="3646" href="/20.07/Relations/#1284" class="InductiveConstructor">s≤s</a> <a id="3650" class="Symbol">{</a><a id="3651" class="Number">0</a><a id="3652" class="Symbol">}</a> <a id="3654" class="Symbol">{</a><a id="3655" class="Number">2</a><a id="3656" class="Symbol">}</a> <a id="3658" class="Symbol">(</a><a id="3659" href="/20.07/Relations/#1235" class="InductiveConstructor">z≤n</a> <a id="3663" class="Symbol">{</a><a id="3664" class="Number">2</a><a id="3665" class="Symbol">}))</a>
|
||
</pre>
|
||
<p>One may also identify implicit arguments by name:</p>
|
||
<pre class="Agda"><a id="3727" href="/20.07/Relations/#3727" class="Function">_</a> <a id="3729" class="Symbol">:</a> <a id="3731" class="Number">2</a> <a id="3733" href="/20.07/Relations/#1208" class="Datatype Operator">≤</a> <a id="3735" class="Number">4</a>
|
||
<a id="3737" class="Symbol">_</a> <a id="3739" class="Symbol">=</a> <a id="3741" href="/20.07/Relations/#1284" class="InductiveConstructor">s≤s</a> <a id="3745" class="Symbol">{</a><a id="3746" class="Argument">m</a> <a id="3748" class="Symbol">=</a> <a id="3750" class="Number">1</a><a id="3751" class="Symbol">}</a> <a id="3753" class="Symbol">{</a><a id="3754" class="Argument">n</a> <a id="3756" class="Symbol">=</a> <a id="3758" class="Number">3</a><a id="3759" class="Symbol">}</a> <a id="3761" class="Symbol">(</a><a id="3762" href="/20.07/Relations/#1284" class="InductiveConstructor">s≤s</a> <a id="3766" class="Symbol">{</a><a id="3767" class="Argument">m</a> <a id="3769" class="Symbol">=</a> <a id="3771" class="Number">0</a><a id="3772" class="Symbol">}</a> <a id="3774" class="Symbol">{</a><a id="3775" class="Argument">n</a> <a id="3777" class="Symbol">=</a> <a id="3779" class="Number">2</a><a id="3780" class="Symbol">}</a> <a id="3782" class="Symbol">(</a><a id="3783" href="/20.07/Relations/#1235" class="InductiveConstructor">z≤n</a> <a id="3787" class="Symbol">{</a><a id="3788" class="Argument">n</a> <a id="3790" class="Symbol">=</a> <a id="3792" class="Number">2</a><a id="3793" class="Symbol">}))</a>
|
||
</pre>
|
||
<p>In the latter format, you can choose to only supply some implicit arguments:</p>
|
||
<pre class="Agda"><a id="3882" href="/20.07/Relations/#3882" class="Function">_</a> <a id="3884" class="Symbol">:</a> <a id="3886" class="Number">2</a> <a id="3888" href="/20.07/Relations/#1208" class="Datatype Operator">≤</a> <a id="3890" class="Number">4</a>
|
||
<a id="3892" class="Symbol">_</a> <a id="3894" class="Symbol">=</a> <a id="3896" href="/20.07/Relations/#1284" class="InductiveConstructor">s≤s</a> <a id="3900" class="Symbol">{</a><a id="3901" class="Argument">n</a> <a id="3903" class="Symbol">=</a> <a id="3905" class="Number">3</a><a id="3906" class="Symbol">}</a> <a id="3908" class="Symbol">(</a><a id="3909" href="/20.07/Relations/#1284" class="InductiveConstructor">s≤s</a> <a id="3913" class="Symbol">{</a><a id="3914" class="Argument">n</a> <a id="3916" class="Symbol">=</a> <a id="3918" class="Number">2</a><a id="3919" class="Symbol">}</a> <a id="3921" href="/20.07/Relations/#1235" class="InductiveConstructor">z≤n</a><a id="3924" class="Symbol">)</a>
|
||
</pre>
|
||
<p>It is not permitted to swap implicit arguments, even when named.</p>
|
||
|
||
<p>We can ask Agda to use the same inference to try and infer an <em>explicit</em> term,
|
||
by writing <code class="language-plaintext highlighter-rouge">_</code>. For instance, we can define a variant of the proposition
|
||
<code class="language-plaintext highlighter-rouge">+-identityʳ</code> with implicit arguments:</p>
|
||
<pre class="Agda"><a id="+-identityʳ′"></a><a id="4191" href="/20.07/Relations/#4191" class="Function">+-identityʳ′</a> <a id="4204" class="Symbol">:</a> <a id="4206" class="Symbol">∀</a> <a id="4208" class="Symbol">{</a><a id="4209" href="/20.07/Relations/#4209" class="Bound">m</a> <a id="4211" class="Symbol">:</a> <a id="4213" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="4214" class="Symbol">}</a> <a id="4216" class="Symbol">→</a> <a id="4218" href="/20.07/Relations/#4209" class="Bound">m</a> <a id="4220" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="4222" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">zero</a> <a id="4227" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="4229" href="/20.07/Relations/#4209" class="Bound">m</a>
|
||
<a id="4231" href="/20.07/Relations/#4191" class="Function">+-identityʳ′</a> <a id="4244" class="Symbol">=</a> <a id="4246" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#11734" class="Function">+-identityʳ</a> <a id="4258" class="Symbol">_</a>
|
||
</pre>
|
||
<p>We use <code class="language-plaintext highlighter-rouge">_</code> to ask Agda to infer the value of the <em>explicit</em> argument from
|
||
context. There is only one value which gives us the correct proof, <code class="language-plaintext highlighter-rouge">m</code>, so Agda
|
||
happily fills it in.
|
||
If Agda fails to infer the value, it reports an error.</p>
|
||
|
||
<h2 id="precedence">Precedence</h2>
|
||
|
||
<p>We declare the precedence for comparison as follows:</p>
|
||
<pre class="Agda"><a id="4568" class="Keyword">infix</a> <a id="4574" class="Number">4</a> <a id="4576" href="/20.07/Relations/#1208" class="Datatype Operator">_≤_</a>
|
||
</pre>
|
||
<p>We set the precedence of <code class="language-plaintext highlighter-rouge">_≤_</code> at level 4, so it binds less tightly
|
||
than <code class="language-plaintext highlighter-rouge">_+_</code> at level 6 and hence <code class="language-plaintext highlighter-rouge">1 + 2 ≤ 3</code> parses as <code class="language-plaintext highlighter-rouge">(1 + 2) ≤ 3</code>.
|
||
We write <code class="language-plaintext highlighter-rouge">infix</code> to indicate that the operator does not associate to
|
||
either the left or right, as it makes no sense to parse <code class="language-plaintext highlighter-rouge">1 ≤ 2 ≤ 3</code> as
|
||
either <code class="language-plaintext highlighter-rouge">(1 ≤ 2) ≤ 3</code> or <code class="language-plaintext highlighter-rouge">1 ≤ (2 ≤ 3)</code>.</p>
|
||
|
||
<h2 id="decidability">Decidability</h2>
|
||
|
||
<p>Given two numbers, it is straightforward to compute whether or not the
|
||
first is less than or equal to the second. We don’t give the code for
|
||
doing so here, but will return to this point in
|
||
Chapter <a href="/20.07/Decidable/">Decidable</a>.</p>
|
||
|
||
<h2 id="inversion">Inversion</h2>
|
||
|
||
<p>In our definitions, we go from smaller things to larger things.
|
||
For instance, from <code class="language-plaintext highlighter-rouge">m ≤ n</code> we can conclude <code class="language-plaintext highlighter-rouge">suc m ≤ suc n</code>,
|
||
where <code class="language-plaintext highlighter-rouge">suc m</code> is bigger than <code class="language-plaintext highlighter-rouge">m</code> (that is, the former contains
|
||
the latter), and <code class="language-plaintext highlighter-rouge">suc n</code> is bigger than <code class="language-plaintext highlighter-rouge">n</code>. But sometimes we
|
||
want to go from bigger things to smaller things.</p>
|
||
|
||
<p>There is only one way to prove that <code class="language-plaintext highlighter-rouge">suc m ≤ suc n</code>, for any <code class="language-plaintext highlighter-rouge">m</code>
|
||
and <code class="language-plaintext highlighter-rouge">n</code>. This lets us invert our previous rule.</p>
|
||
<pre class="Agda"><a id="inv-s≤s"></a><a id="5594" href="/20.07/Relations/#5594" class="Function">inv-s≤s</a> <a id="5602" class="Symbol">:</a> <a id="5604" class="Symbol">∀</a> <a id="5606" class="Symbol">{</a><a id="5607" href="/20.07/Relations/#5607" class="Bound">m</a> <a id="5609" href="/20.07/Relations/#5609" class="Bound">n</a> <a id="5611" class="Symbol">:</a> <a id="5613" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="5614" class="Symbol">}</a>
|
||
<a id="5618" class="Symbol">→</a> <a id="5620" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="5624" href="/20.07/Relations/#5607" class="Bound">m</a> <a id="5626" href="/20.07/Relations/#1208" class="Datatype Operator">≤</a> <a id="5628" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="5632" href="/20.07/Relations/#5609" class="Bound">n</a>
|
||
<a id="5638" class="Comment">-------------</a>
|
||
<a id="5654" class="Symbol">→</a> <a id="5656" href="/20.07/Relations/#5607" class="Bound">m</a> <a id="5658" href="/20.07/Relations/#1208" class="Datatype Operator">≤</a> <a id="5660" href="/20.07/Relations/#5609" class="Bound">n</a>
|
||
<a id="5662" href="/20.07/Relations/#5594" class="Function">inv-s≤s</a> <a id="5670" class="Symbol">(</a><a id="5671" href="/20.07/Relations/#1284" class="InductiveConstructor">s≤s</a> <a id="5675" href="/20.07/Relations/#5675" class="Bound">m≤n</a><a id="5678" class="Symbol">)</a> <a id="5680" class="Symbol">=</a> <a id="5682" href="/20.07/Relations/#5675" class="Bound">m≤n</a>
|
||
</pre>
|
||
<p>Here <code class="language-plaintext highlighter-rouge">m≤n</code> (with no spaces) is a variable name while
|
||
<code class="language-plaintext highlighter-rouge">m ≤ n</code> (with spaces) is a type, and the latter
|
||
is the type of the former. It is a common convention
|
||
in Agda to derive a variable name by removing
|
||
spaces from its type.</p>
|
||
|
||
<p>Not every rule is invertible; indeed, the rule for <code class="language-plaintext highlighter-rouge">z≤n</code> has
|
||
no non-implicit hypotheses, so there is nothing to invert.
|
||
But often inversions of this kind hold.</p>
|
||
|
||
<p>Another example of inversion is showing that there is
|
||
only one way a number can be less than or equal to zero.</p>
|
||
<pre class="Agda"><a id="inv-z≤n"></a><a id="6190" href="/20.07/Relations/#6190" class="Function">inv-z≤n</a> <a id="6198" class="Symbol">:</a> <a id="6200" class="Symbol">∀</a> <a id="6202" class="Symbol">{</a><a id="6203" href="/20.07/Relations/#6203" class="Bound">m</a> <a id="6205" class="Symbol">:</a> <a id="6207" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="6208" class="Symbol">}</a>
|
||
<a id="6212" class="Symbol">→</a> <a id="6214" href="/20.07/Relations/#6203" class="Bound">m</a> <a id="6216" href="/20.07/Relations/#1208" class="Datatype Operator">≤</a> <a id="6218" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">zero</a>
|
||
<a id="6227" class="Comment">--------</a>
|
||
<a id="6238" class="Symbol">→</a> <a id="6240" href="/20.07/Relations/#6203" class="Bound">m</a> <a id="6242" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="6244" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">zero</a>
|
||
<a id="6249" href="/20.07/Relations/#6190" class="Function">inv-z≤n</a> <a id="6257" href="/20.07/Relations/#1235" class="InductiveConstructor">z≤n</a> <a id="6261" class="Symbol">=</a> <a id="6263" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a>
|
||
</pre>
|
||
<h2 id="properties-of-ordering-relations">Properties of ordering relations</h2>
|
||
|
||
<p>Relations pop up all the time, and mathematicians have agreed
|
||
on names for some of the most common properties.</p>
|
||
|
||
<ul>
|
||
<li><em>Reflexive</em>. For all <code class="language-plaintext highlighter-rouge">n</code>, the relation <code class="language-plaintext highlighter-rouge">n ≤ n</code> holds.</li>
|
||
<li><em>Transitive</em>. 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>, if <code class="language-plaintext highlighter-rouge">m ≤ n</code> and
|
||
<code class="language-plaintext highlighter-rouge">n ≤ p</code> hold, then <code class="language-plaintext highlighter-rouge">m ≤ p</code> holds.</li>
|
||
<li><em>Anti-symmetric</em>. For all <code class="language-plaintext highlighter-rouge">m</code> and <code class="language-plaintext highlighter-rouge">n</code>, if both <code class="language-plaintext highlighter-rouge">m ≤ n</code> and
|
||
<code class="language-plaintext highlighter-rouge">n ≤ m</code> hold, then <code class="language-plaintext highlighter-rouge">m ≡ n</code> holds.</li>
|
||
<li><em>Total</em>. For all <code class="language-plaintext highlighter-rouge">m</code> and <code class="language-plaintext highlighter-rouge">n</code>, either <code class="language-plaintext highlighter-rouge">m ≤ n</code> or <code class="language-plaintext highlighter-rouge">n ≤ m</code>
|
||
holds.</li>
|
||
</ul>
|
||
|
||
<p>The relation <code class="language-plaintext highlighter-rouge">_≤_</code> satisfies all four of these properties.</p>
|
||
|
||
<p>There are also names for some combinations of these properties.</p>
|
||
|
||
<ul>
|
||
<li><em>Preorder</em>. Any relation that is reflexive and transitive.</li>
|
||
<li><em>Partial order</em>. Any preorder that is also anti-symmetric.</li>
|
||
<li><em>Total order</em>. Any partial order that is also total.</li>
|
||
</ul>
|
||
|
||
<p>If you ever bump into a relation at a party, you now know how
|
||
to make small talk, by asking it whether it is reflexive, transitive,
|
||
anti-symmetric, and total. Or instead you might ask whether it is a
|
||
preorder, partial order, or total order.</p>
|
||
|
||
<p>Less frivolously, if you ever bump into a relation while reading a
|
||
technical paper, this gives you a way to orient yourself, by checking
|
||
whether or not it is a preorder, partial order, or total order. A
|
||
careful author will often call out these properties—or their
|
||
lack—for instance by saying that a newly introduced relation is a
|
||
partial order but not a total order.</p>
|
||
|
||
<h4 id="orderings">Exercise <code class="language-plaintext highlighter-rouge">orderings</code> (practice)</h4>
|
||
|
||
<p>Give an example of a preorder that is not a partial order.</p>
|
||
|
||
<pre class="Agda"><a id="7765" class="Comment">-- Your code goes here</a>
|
||
</pre>
|
||
<p>Give an example of a partial order that is not a total order.</p>
|
||
|
||
<pre class="Agda"><a id="7860" class="Comment">-- Your code goes here</a>
|
||
</pre>
|
||
<h2 id="reflexivity">Reflexivity</h2>
|
||
|
||
<p>The first property to prove about comparison is that it is reflexive:
|
||
for any natural <code class="language-plaintext highlighter-rouge">n</code>, the relation <code class="language-plaintext highlighter-rouge">n ≤ n</code> holds. We follow the
|
||
convention in the standard library and make the argument implicit,
|
||
as that will make it easier to invoke reflexivity:</p>
|
||
<pre class="Agda"><a id="≤-refl"></a><a id="8160" href="/20.07/Relations/#8160" class="Function">≤-refl</a> <a id="8167" class="Symbol">:</a> <a id="8169" class="Symbol">∀</a> <a id="8171" class="Symbol">{</a><a id="8172" href="/20.07/Relations/#8172" class="Bound">n</a> <a id="8174" class="Symbol">:</a> <a id="8176" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="8177" class="Symbol">}</a>
|
||
<a id="8183" class="Comment">-----</a>
|
||
<a id="8191" class="Symbol">→</a> <a id="8193" href="/20.07/Relations/#8172" class="Bound">n</a> <a id="8195" href="/20.07/Relations/#1208" class="Datatype Operator">≤</a> <a id="8197" href="/20.07/Relations/#8172" class="Bound">n</a>
|
||
<a id="8199" href="/20.07/Relations/#8160" class="Function">≤-refl</a> <a id="8206" class="Symbol">{</a><a id="8207" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">zero</a><a id="8211" class="Symbol">}</a> <a id="8213" class="Symbol">=</a> <a id="8215" href="/20.07/Relations/#1235" class="InductiveConstructor">z≤n</a>
|
||
<a id="8219" href="/20.07/Relations/#8160" class="Function">≤-refl</a> <a id="8226" class="Symbol">{</a><a id="8227" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="8231" href="/20.07/Relations/#8231" class="Bound">n</a><a id="8232" class="Symbol">}</a> <a id="8234" class="Symbol">=</a> <a id="8236" href="/20.07/Relations/#1284" class="InductiveConstructor">s≤s</a> <a id="8240" href="/20.07/Relations/#8160" class="Function">≤-refl</a>
|
||
</pre>
|
||
<p>The proof is a straightforward induction on the implicit argument <code class="language-plaintext highlighter-rouge">n</code>.
|
||
In the base case, <code class="language-plaintext highlighter-rouge">zero ≤ zero</code> holds by <code class="language-plaintext highlighter-rouge">z≤n</code>. In the inductive
|
||
case, the inductive hypothesis <code class="language-plaintext highlighter-rouge">≤-refl {n}</code> gives us a proof of <code class="language-plaintext highlighter-rouge">n ≤
|
||
n</code>, and applying <code class="language-plaintext highlighter-rouge">s≤s</code> to that yields a proof of <code class="language-plaintext highlighter-rouge">suc n ≤ suc n</code>.</p>
|
||
|
||
<p>It is a good exercise to prove reflexivity interactively in Emacs,
|
||
using holes and the <code class="language-plaintext highlighter-rouge">C-c C-c</code>, <code class="language-plaintext highlighter-rouge">C-c C-,</code>, and <code class="language-plaintext highlighter-rouge">C-c C-r</code> commands.</p>
|
||
|
||
<h2 id="transitivity">Transitivity</h2>
|
||
|
||
<p>The second property to prove about comparison is that it is
|
||
transitive: for any 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>, if <code class="language-plaintext highlighter-rouge">m ≤ n</code> and <code class="language-plaintext highlighter-rouge">n ≤ p</code>
|
||
hold, then <code class="language-plaintext highlighter-rouge">m ≤ p</code> holds. Again, <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 implicit:</p>
|
||
<pre class="Agda"><a id="≤-trans"></a><a id="8877" href="/20.07/Relations/#8877" class="Function">≤-trans</a> <a id="8885" class="Symbol">:</a> <a id="8887" class="Symbol">∀</a> <a id="8889" class="Symbol">{</a><a id="8890" href="/20.07/Relations/#8890" class="Bound">m</a> <a id="8892" href="/20.07/Relations/#8892" class="Bound">n</a> <a id="8894" href="/20.07/Relations/#8894" class="Bound">p</a> <a id="8896" class="Symbol">:</a> <a id="8898" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="8899" class="Symbol">}</a>
|
||
<a id="8903" class="Symbol">→</a> <a id="8905" href="/20.07/Relations/#8890" class="Bound">m</a> <a id="8907" href="/20.07/Relations/#1208" class="Datatype Operator">≤</a> <a id="8909" href="/20.07/Relations/#8892" class="Bound">n</a>
|
||
<a id="8913" class="Symbol">→</a> <a id="8915" href="/20.07/Relations/#8892" class="Bound">n</a> <a id="8917" href="/20.07/Relations/#1208" class="Datatype Operator">≤</a> <a id="8919" href="/20.07/Relations/#8894" class="Bound">p</a>
|
||
<a id="8925" class="Comment">-----</a>
|
||
<a id="8933" class="Symbol">→</a> <a id="8935" href="/20.07/Relations/#8890" class="Bound">m</a> <a id="8937" href="/20.07/Relations/#1208" class="Datatype Operator">≤</a> <a id="8939" href="/20.07/Relations/#8894" class="Bound">p</a>
|
||
<a id="8941" href="/20.07/Relations/#8877" class="Function">≤-trans</a> <a id="8949" href="/20.07/Relations/#1235" class="InductiveConstructor">z≤n</a> <a id="8959" class="Symbol">_</a> <a id="8970" class="Symbol">=</a> <a id="8973" href="/20.07/Relations/#1235" class="InductiveConstructor">z≤n</a>
|
||
<a id="8977" href="/20.07/Relations/#8877" class="Function">≤-trans</a> <a id="8985" class="Symbol">(</a><a id="8986" href="/20.07/Relations/#1284" class="InductiveConstructor">s≤s</a> <a id="8990" href="/20.07/Relations/#8990" class="Bound">m≤n</a><a id="8993" class="Symbol">)</a> <a id="8995" class="Symbol">(</a><a id="8996" href="/20.07/Relations/#1284" class="InductiveConstructor">s≤s</a> <a id="9000" href="/20.07/Relations/#9000" class="Bound">n≤p</a><a id="9003" class="Symbol">)</a> <a id="9006" class="Symbol">=</a> <a id="9009" href="/20.07/Relations/#1284" class="InductiveConstructor">s≤s</a> <a id="9013" class="Symbol">(</a><a id="9014" href="/20.07/Relations/#8877" class="Function">≤-trans</a> <a id="9022" href="/20.07/Relations/#8990" class="Bound">m≤n</a> <a id="9026" href="/20.07/Relations/#9000" class="Bound">n≤p</a><a id="9029" class="Symbol">)</a>
|
||
</pre>
|
||
<p>Here the proof is by induction on the <em>evidence</em> that <code class="language-plaintext highlighter-rouge">m ≤ n</code>. In the
|
||
base case, the first inequality holds by <code class="language-plaintext highlighter-rouge">z≤n</code> and must show <code class="language-plaintext highlighter-rouge">zero ≤ p</code>,
|
||
which follows immediately by <code class="language-plaintext highlighter-rouge">z≤n</code>. In this case, the fact that
|
||
<code class="language-plaintext highlighter-rouge">n ≤ p</code> is irrelevant, and we write <code class="language-plaintext highlighter-rouge">_</code> as the pattern to indicate
|
||
that the corresponding evidence is unused.</p>
|
||
|
||
<p>In the inductive case, the first inequality holds by <code class="language-plaintext highlighter-rouge">s≤s m≤n</code>
|
||
and the second inequality by <code class="language-plaintext highlighter-rouge">s≤s n≤p</code>, and so we are given
|
||
<code class="language-plaintext highlighter-rouge">suc m ≤ suc n</code> and <code class="language-plaintext highlighter-rouge">suc n ≤ suc p</code>, and must show <code class="language-plaintext highlighter-rouge">suc m ≤ suc p</code>.
|
||
The inductive hypothesis <code class="language-plaintext highlighter-rouge">≤-trans m≤n n≤p</code> establishes
|
||
that <code class="language-plaintext highlighter-rouge">m ≤ p</code>, and our goal follows by applying <code class="language-plaintext highlighter-rouge">s≤s</code>.</p>
|
||
|
||
<p>The case <code class="language-plaintext highlighter-rouge">≤-trans (s≤s m≤n) z≤n</code> cannot arise, since the first
|
||
inequality implies the middle value is <code class="language-plaintext highlighter-rouge">suc n</code> while the second
|
||
inequality implies that it is <code class="language-plaintext highlighter-rouge">zero</code>. Agda can determine that such a
|
||
case cannot arise, and does not require (or permit) it to be listed.</p>
|
||
|
||
<p>Alternatively, we could make the implicit parameters explicit:</p>
|
||
<pre class="Agda"><a id="≤-trans′"></a><a id="9990" href="/20.07/Relations/#9990" class="Function">≤-trans′</a> <a id="9999" class="Symbol">:</a> <a id="10001" class="Symbol">∀</a> <a id="10003" class="Symbol">(</a><a id="10004" href="/20.07/Relations/#10004" class="Bound">m</a> <a id="10006" href="/20.07/Relations/#10006" class="Bound">n</a> <a id="10008" href="/20.07/Relations/#10008" class="Bound">p</a> <a id="10010" class="Symbol">:</a> <a id="10012" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="10013" class="Symbol">)</a>
|
||
<a id="10017" class="Symbol">→</a> <a id="10019" href="/20.07/Relations/#10004" class="Bound">m</a> <a id="10021" href="/20.07/Relations/#1208" class="Datatype Operator">≤</a> <a id="10023" href="/20.07/Relations/#10006" class="Bound">n</a>
|
||
<a id="10027" class="Symbol">→</a> <a id="10029" href="/20.07/Relations/#10006" class="Bound">n</a> <a id="10031" href="/20.07/Relations/#1208" class="Datatype Operator">≤</a> <a id="10033" href="/20.07/Relations/#10008" class="Bound">p</a>
|
||
<a id="10039" class="Comment">-----</a>
|
||
<a id="10047" class="Symbol">→</a> <a id="10049" href="/20.07/Relations/#10004" class="Bound">m</a> <a id="10051" href="/20.07/Relations/#1208" class="Datatype Operator">≤</a> <a id="10053" href="/20.07/Relations/#10008" class="Bound">p</a>
|
||
<a id="10055" href="/20.07/Relations/#9990" class="Function">≤-trans′</a> <a id="10064" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">zero</a> <a id="10072" class="Symbol">_</a> <a id="10080" class="Symbol">_</a> <a id="10088" href="/20.07/Relations/#1235" class="InductiveConstructor">z≤n</a> <a id="10098" class="Symbol">_</a> <a id="10109" class="Symbol">=</a> <a id="10112" href="/20.07/Relations/#1235" class="InductiveConstructor">z≤n</a>
|
||
<a id="10116" href="/20.07/Relations/#9990" class="Function">≤-trans′</a> <a id="10125" class="Symbol">(</a><a id="10126" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="10130" href="/20.07/Relations/#10130" class="Bound">m</a><a id="10131" class="Symbol">)</a> <a id="10133" class="Symbol">(</a><a id="10134" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="10138" href="/20.07/Relations/#10138" class="Bound">n</a><a id="10139" class="Symbol">)</a> <a id="10141" class="Symbol">(</a><a id="10142" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="10146" href="/20.07/Relations/#10146" class="Bound">p</a><a id="10147" class="Symbol">)</a> <a id="10149" class="Symbol">(</a><a id="10150" href="/20.07/Relations/#1284" class="InductiveConstructor">s≤s</a> <a id="10154" href="/20.07/Relations/#10154" class="Bound">m≤n</a><a id="10157" class="Symbol">)</a> <a id="10159" class="Symbol">(</a><a id="10160" href="/20.07/Relations/#1284" class="InductiveConstructor">s≤s</a> <a id="10164" href="/20.07/Relations/#10164" class="Bound">n≤p</a><a id="10167" class="Symbol">)</a> <a id="10170" class="Symbol">=</a> <a id="10173" href="/20.07/Relations/#1284" class="InductiveConstructor">s≤s</a> <a id="10177" class="Symbol">(</a><a id="10178" href="/20.07/Relations/#9990" class="Function">≤-trans′</a> <a id="10187" href="/20.07/Relations/#10130" class="Bound">m</a> <a id="10189" href="/20.07/Relations/#10138" class="Bound">n</a> <a id="10191" href="/20.07/Relations/#10146" class="Bound">p</a> <a id="10193" href="/20.07/Relations/#10154" class="Bound">m≤n</a> <a id="10197" href="/20.07/Relations/#10164" class="Bound">n≤p</a><a id="10200" class="Symbol">)</a>
|
||
</pre>
|
||
<p>One might argue that this is clearer or one might argue that the extra
|
||
length obscures the essence of the proof. We will usually opt for
|
||
shorter proofs.</p>
|
||
|
||
<p>The technique of induction on evidence that a property holds (e.g.,
|
||
inducting on evidence that <code class="language-plaintext highlighter-rouge">m ≤ n</code>)—rather than induction on
|
||
values of which the property holds (e.g., inducting on <code class="language-plaintext highlighter-rouge">m</code>)—will turn
|
||
out to be immensely valuable, and one that we use often.</p>
|
||
|
||
<p>Again, it is a good exercise to prove transitivity interactively in Emacs,
|
||
using holes and the <code class="language-plaintext highlighter-rouge">C-c C-c</code>, <code class="language-plaintext highlighter-rouge">C-c C-,</code>, and <code class="language-plaintext highlighter-rouge">C-c C-r</code> commands.</p>
|
||
|
||
<h2 id="anti-symmetry">Anti-symmetry</h2>
|
||
|
||
<p>The third property to prove about comparison is that it is
|
||
antisymmetric: for all naturals <code class="language-plaintext highlighter-rouge">m</code> and <code class="language-plaintext highlighter-rouge">n</code>, if both <code class="language-plaintext highlighter-rouge">m ≤ n</code> and <code class="language-plaintext highlighter-rouge">n ≤
|
||
m</code> hold, then <code class="language-plaintext highlighter-rouge">m ≡ n</code> holds:</p>
|
||
<pre class="Agda"><a id="≤-antisym"></a><a id="10945" href="/20.07/Relations/#10945" class="Function">≤-antisym</a> <a id="10955" class="Symbol">:</a> <a id="10957" class="Symbol">∀</a> <a id="10959" class="Symbol">{</a><a id="10960" href="/20.07/Relations/#10960" class="Bound">m</a> <a id="10962" href="/20.07/Relations/#10962" class="Bound">n</a> <a id="10964" class="Symbol">:</a> <a id="10966" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="10967" class="Symbol">}</a>
|
||
<a id="10971" class="Symbol">→</a> <a id="10973" href="/20.07/Relations/#10960" class="Bound">m</a> <a id="10975" href="/20.07/Relations/#1208" class="Datatype Operator">≤</a> <a id="10977" href="/20.07/Relations/#10962" class="Bound">n</a>
|
||
<a id="10981" class="Symbol">→</a> <a id="10983" href="/20.07/Relations/#10962" class="Bound">n</a> <a id="10985" href="/20.07/Relations/#1208" class="Datatype Operator">≤</a> <a id="10987" href="/20.07/Relations/#10960" class="Bound">m</a>
|
||
<a id="10993" class="Comment">-----</a>
|
||
<a id="11001" class="Symbol">→</a> <a id="11003" href="/20.07/Relations/#10960" class="Bound">m</a> <a id="11005" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="11007" href="/20.07/Relations/#10962" class="Bound">n</a>
|
||
<a id="11009" href="/20.07/Relations/#10945" class="Function">≤-antisym</a> <a id="11019" href="/20.07/Relations/#1235" class="InductiveConstructor">z≤n</a> <a id="11029" href="/20.07/Relations/#1235" class="InductiveConstructor">z≤n</a> <a id="11040" class="Symbol">=</a> <a id="11043" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a>
|
||
<a id="11048" href="/20.07/Relations/#10945" class="Function">≤-antisym</a> <a id="11058" class="Symbol">(</a><a id="11059" href="/20.07/Relations/#1284" class="InductiveConstructor">s≤s</a> <a id="11063" href="/20.07/Relations/#11063" class="Bound">m≤n</a><a id="11066" class="Symbol">)</a> <a id="11068" class="Symbol">(</a><a id="11069" href="/20.07/Relations/#1284" class="InductiveConstructor">s≤s</a> <a id="11073" href="/20.07/Relations/#11073" class="Bound">n≤m</a><a id="11076" class="Symbol">)</a> <a id="11079" class="Symbol">=</a> <a id="11082" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#1090" class="Function">cong</a> <a id="11087" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="11091" class="Symbol">(</a><a id="11092" href="/20.07/Relations/#10945" class="Function">≤-antisym</a> <a id="11102" href="/20.07/Relations/#11063" class="Bound">m≤n</a> <a id="11106" href="/20.07/Relations/#11073" class="Bound">n≤m</a><a id="11109" class="Symbol">)</a>
|
||
</pre>
|
||
<p>Again, the proof is by induction over the evidence that <code class="language-plaintext highlighter-rouge">m ≤ n</code>
|
||
and <code class="language-plaintext highlighter-rouge">n ≤ m</code> hold.</p>
|
||
|
||
<p>In the base case, both inequalities hold by <code class="language-plaintext highlighter-rouge">z≤n</code>, and so we are given
|
||
<code class="language-plaintext highlighter-rouge">zero ≤ zero</code> and <code class="language-plaintext highlighter-rouge">zero ≤ zero</code> and must show <code class="language-plaintext highlighter-rouge">zero ≡ zero</code>, which
|
||
follows by reflexivity. (Reflexivity of equality, that is, not
|
||
reflexivity of inequality.)</p>
|
||
|
||
<p>In the inductive case, the first inequality holds by <code class="language-plaintext highlighter-rouge">s≤s m≤n</code> and the
|
||
second inequality holds by <code class="language-plaintext highlighter-rouge">s≤s n≤m</code>, and so we are given <code class="language-plaintext highlighter-rouge">suc m ≤ suc n</code>
|
||
and <code class="language-plaintext highlighter-rouge">suc n ≤ suc m</code> and must show <code class="language-plaintext highlighter-rouge">suc m ≡ suc n</code>. The inductive
|
||
hypothesis <code class="language-plaintext highlighter-rouge">≤-antisym m≤n n≤m</code> establishes that <code class="language-plaintext highlighter-rouge">m ≡ n</code>, and our goal
|
||
follows by congruence.</p>
|
||
|
||
<h4 id="leq-antisym-cases">Exercise <code class="language-plaintext highlighter-rouge">≤-antisym-cases</code> (practice)</h4>
|
||
|
||
<p>The above proof omits cases where one argument is <code class="language-plaintext highlighter-rouge">z≤n</code> and one
|
||
argument is <code class="language-plaintext highlighter-rouge">s≤s</code>. Why is it ok to omit them?</p>
|
||
|
||
<pre class="Agda"><a id="11915" class="Comment">-- Your code goes here</a>
|
||
</pre>
|
||
|
||
<h2 id="total">Total</h2>
|
||
|
||
<p>The fourth property to prove about comparison is that it is total:
|
||
for any naturals <code class="language-plaintext highlighter-rouge">m</code> and <code class="language-plaintext highlighter-rouge">n</code> either <code class="language-plaintext highlighter-rouge">m ≤ n</code> or <code class="language-plaintext highlighter-rouge">n ≤ m</code>, or both if
|
||
<code class="language-plaintext highlighter-rouge">m</code> and <code class="language-plaintext highlighter-rouge">n</code> are equal.</p>
|
||
|
||
<p>We specify what it means for inequality to be total:</p>
|
||
<pre class="Agda"><a id="12169" class="Keyword">data</a> <a id="Total"></a><a id="12174" href="/20.07/Relations/#12174" class="Datatype">Total</a> <a id="12180" class="Symbol">(</a><a id="12181" href="/20.07/Relations/#12181" class="Bound">m</a> <a id="12183" href="/20.07/Relations/#12183" class="Bound">n</a> <a id="12185" class="Symbol">:</a> <a id="12187" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="12188" class="Symbol">)</a> <a id="12190" class="Symbol">:</a> <a id="12192" class="PrimitiveType">Set</a> <a id="12196" class="Keyword">where</a>
|
||
|
||
<a id="Total.forward"></a><a id="12205" href="/20.07/Relations/#12205" class="InductiveConstructor">forward</a> <a id="12213" class="Symbol">:</a>
|
||
<a id="12221" href="/20.07/Relations/#12181" class="Bound">m</a> <a id="12223" href="/20.07/Relations/#1208" class="Datatype Operator">≤</a> <a id="12225" href="/20.07/Relations/#12183" class="Bound">n</a>
|
||
<a id="12233" class="Comment">---------</a>
|
||
<a id="12247" class="Symbol">→</a> <a id="12249" href="/20.07/Relations/#12174" class="Datatype">Total</a> <a id="12255" href="/20.07/Relations/#12181" class="Bound">m</a> <a id="12257" href="/20.07/Relations/#12183" class="Bound">n</a>
|
||
|
||
<a id="Total.flipped"></a><a id="12262" href="/20.07/Relations/#12262" class="InductiveConstructor">flipped</a> <a id="12270" class="Symbol">:</a>
|
||
<a id="12278" href="/20.07/Relations/#12183" class="Bound">n</a> <a id="12280" href="/20.07/Relations/#1208" class="Datatype Operator">≤</a> <a id="12282" href="/20.07/Relations/#12181" class="Bound">m</a>
|
||
<a id="12290" class="Comment">---------</a>
|
||
<a id="12304" class="Symbol">→</a> <a id="12306" href="/20.07/Relations/#12174" class="Datatype">Total</a> <a id="12312" href="/20.07/Relations/#12181" class="Bound">m</a> <a id="12314" href="/20.07/Relations/#12183" class="Bound">n</a>
|
||
</pre>
|
||
<p>Evidence that <code class="language-plaintext highlighter-rouge">Total m n</code> holds is either of the form
|
||
<code class="language-plaintext highlighter-rouge">forward m≤n</code> or <code class="language-plaintext highlighter-rouge">flipped n≤m</code>, where <code class="language-plaintext highlighter-rouge">m≤n</code> and <code class="language-plaintext highlighter-rouge">n≤m</code> are
|
||
evidence of <code class="language-plaintext highlighter-rouge">m ≤ n</code> and <code class="language-plaintext highlighter-rouge">n ≤ m</code> respectively.</p>
|
||
|
||
<p>(For those familiar with logic, the above definition
|
||
could also be written as a disjunction. Disjunctions will
|
||
be introduced in Chapter <a href="/20.07/Connectives/">Connectives</a>.)</p>
|
||
|
||
<p>This is our first use of a datatype with <em>parameters</em>,
|
||
in this case <code class="language-plaintext highlighter-rouge">m</code> and <code class="language-plaintext highlighter-rouge">n</code>. It is equivalent to the following
|
||
indexed datatype:</p>
|
||
<pre class="Agda"><a id="12803" class="Keyword">data</a> <a id="Total′"></a><a id="12808" href="/20.07/Relations/#12808" class="Datatype">Total′</a> <a id="12815" class="Symbol">:</a> <a id="12817" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a> <a id="12819" class="Symbol">→</a> <a id="12821" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a> <a id="12823" class="Symbol">→</a> <a id="12825" class="PrimitiveType">Set</a> <a id="12829" class="Keyword">where</a>
|
||
|
||
<a id="Total′.forward′"></a><a id="12838" href="/20.07/Relations/#12838" class="InductiveConstructor">forward′</a> <a id="12847" class="Symbol">:</a> <a id="12849" class="Symbol">∀</a> <a id="12851" class="Symbol">{</a><a id="12852" href="/20.07/Relations/#12852" class="Bound">m</a> <a id="12854" href="/20.07/Relations/#12854" class="Bound">n</a> <a id="12856" class="Symbol">:</a> <a id="12858" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="12859" class="Symbol">}</a>
|
||
<a id="12865" class="Symbol">→</a> <a id="12867" href="/20.07/Relations/#12852" class="Bound">m</a> <a id="12869" href="/20.07/Relations/#1208" class="Datatype Operator">≤</a> <a id="12871" href="/20.07/Relations/#12854" class="Bound">n</a>
|
||
<a id="12879" class="Comment">----------</a>
|
||
<a id="12894" class="Symbol">→</a> <a id="12896" href="/20.07/Relations/#12808" class="Datatype">Total′</a> <a id="12903" href="/20.07/Relations/#12852" class="Bound">m</a> <a id="12905" href="/20.07/Relations/#12854" class="Bound">n</a>
|
||
|
||
<a id="Total′.flipped′"></a><a id="12910" href="/20.07/Relations/#12910" class="InductiveConstructor">flipped′</a> <a id="12919" class="Symbol">:</a> <a id="12921" class="Symbol">∀</a> <a id="12923" class="Symbol">{</a><a id="12924" href="/20.07/Relations/#12924" class="Bound">m</a> <a id="12926" href="/20.07/Relations/#12926" class="Bound">n</a> <a id="12928" class="Symbol">:</a> <a id="12930" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="12931" class="Symbol">}</a>
|
||
<a id="12937" class="Symbol">→</a> <a id="12939" href="/20.07/Relations/#12926" class="Bound">n</a> <a id="12941" href="/20.07/Relations/#1208" class="Datatype Operator">≤</a> <a id="12943" href="/20.07/Relations/#12924" class="Bound">m</a>
|
||
<a id="12951" class="Comment">----------</a>
|
||
<a id="12966" class="Symbol">→</a> <a id="12968" href="/20.07/Relations/#12808" class="Datatype">Total′</a> <a id="12975" href="/20.07/Relations/#12924" class="Bound">m</a> <a id="12977" href="/20.07/Relations/#12926" class="Bound">n</a>
|
||
</pre>
|
||
<p>Each parameter of the type translates as an implicit parameter of each
|
||
constructor. Unlike an indexed datatype, where the indexes can vary
|
||
(as in <code class="language-plaintext highlighter-rouge">zero ≤ n</code> and <code class="language-plaintext highlighter-rouge">suc m ≤ suc n</code>), in a parameterised datatype
|
||
the parameters must always be the same (as in <code class="language-plaintext highlighter-rouge">Total m n</code>).
|
||
Parameterised declarations are shorter, easier to read, and
|
||
occasionally aid Agda’s termination checker, so we will use them in
|
||
preference to indexed types when possible.</p>
|
||
|
||
<p>With that preliminary out of the way, we specify and prove totality:</p>
|
||
<pre class="Agda"><a id="≤-total"></a><a id="13496" href="/20.07/Relations/#13496" class="Function">≤-total</a> <a id="13504" class="Symbol">:</a> <a id="13506" class="Symbol">∀</a> <a id="13508" class="Symbol">(</a><a id="13509" href="/20.07/Relations/#13509" class="Bound">m</a> <a id="13511" href="/20.07/Relations/#13511" class="Bound">n</a> <a id="13513" class="Symbol">:</a> <a id="13515" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="13516" class="Symbol">)</a> <a id="13518" class="Symbol">→</a> <a id="13520" href="/20.07/Relations/#12174" class="Datatype">Total</a> <a id="13526" href="/20.07/Relations/#13509" class="Bound">m</a> <a id="13528" href="/20.07/Relations/#13511" class="Bound">n</a>
|
||
<a id="13530" href="/20.07/Relations/#13496" class="Function">≤-total</a> <a id="13538" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">zero</a> <a id="13546" href="/20.07/Relations/#13546" class="Bound">n</a> <a id="13572" class="Symbol">=</a> <a id="13575" href="/20.07/Relations/#12205" class="InductiveConstructor">forward</a> <a id="13583" href="/20.07/Relations/#1235" class="InductiveConstructor">z≤n</a>
|
||
<a id="13587" href="/20.07/Relations/#13496" class="Function">≤-total</a> <a id="13595" class="Symbol">(</a><a id="13596" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="13600" href="/20.07/Relations/#13600" class="Bound">m</a><a id="13601" class="Symbol">)</a> <a id="13603" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">zero</a> <a id="13629" class="Symbol">=</a> <a id="13632" href="/20.07/Relations/#12262" class="InductiveConstructor">flipped</a> <a id="13640" href="/20.07/Relations/#1235" class="InductiveConstructor">z≤n</a>
|
||
<a id="13644" href="/20.07/Relations/#13496" class="Function">≤-total</a> <a id="13652" class="Symbol">(</a><a id="13653" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="13657" href="/20.07/Relations/#13657" class="Bound">m</a><a id="13658" class="Symbol">)</a> <a id="13660" class="Symbol">(</a><a id="13661" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="13665" href="/20.07/Relations/#13665" class="Bound">n</a><a id="13666" class="Symbol">)</a> <a id="13668" class="Keyword">with</a> <a id="13673" href="/20.07/Relations/#13496" class="Function">≤-total</a> <a id="13681" href="/20.07/Relations/#13657" class="Bound">m</a> <a id="13683" href="/20.07/Relations/#13665" class="Bound">n</a>
|
||
<a id="13685" class="Symbol">...</a> <a id="13712" class="Symbol">|</a> <a id="13714" href="/20.07/Relations/#12205" class="InductiveConstructor">forward</a> <a id="13722" href="/20.07/Relations/#13722" class="Bound">m≤n</a> <a id="13727" class="Symbol">=</a> <a id="13730" href="/20.07/Relations/#12205" class="InductiveConstructor">forward</a> <a id="13738" class="Symbol">(</a><a id="13739" href="/20.07/Relations/#1284" class="InductiveConstructor">s≤s</a> <a id="13743" href="/20.07/Relations/#13722" class="Bound">m≤n</a><a id="13746" class="Symbol">)</a>
|
||
<a id="13748" class="Symbol">...</a> <a id="13775" class="Symbol">|</a> <a id="13777" href="/20.07/Relations/#12262" class="InductiveConstructor">flipped</a> <a id="13785" href="/20.07/Relations/#13785" class="Bound">n≤m</a> <a id="13790" class="Symbol">=</a> <a id="13793" href="/20.07/Relations/#12262" class="InductiveConstructor">flipped</a> <a id="13801" class="Symbol">(</a><a id="13802" href="/20.07/Relations/#1284" class="InductiveConstructor">s≤s</a> <a id="13806" href="/20.07/Relations/#13785" class="Bound">n≤m</a><a id="13809" class="Symbol">)</a>
|
||
</pre>
|
||
<p>In this case the proof is by induction over both the first
|
||
and second arguments. We perform a case analysis:</p>
|
||
|
||
<ul>
|
||
<li>
|
||
<p><em>First base case</em>: If the first argument is <code class="language-plaintext highlighter-rouge">zero</code> and the
|
||
second argument is <code class="language-plaintext highlighter-rouge">n</code> then the forward case holds,
|
||
with <code class="language-plaintext highlighter-rouge">z≤n</code> as evidence that <code class="language-plaintext highlighter-rouge">zero ≤ n</code>.</p>
|
||
</li>
|
||
<li>
|
||
<p><em>Second base case</em>: If the first argument is <code class="language-plaintext highlighter-rouge">suc m</code> and the
|
||
second argument is <code class="language-plaintext highlighter-rouge">zero</code> then the flipped case holds, with
|
||
<code class="language-plaintext highlighter-rouge">z≤n</code> as evidence that <code class="language-plaintext highlighter-rouge">zero ≤ suc m</code>.</p>
|
||
</li>
|
||
<li>
|
||
<p><em>Inductive case</em>: If the first argument is <code class="language-plaintext highlighter-rouge">suc m</code> and the
|
||
second argument is <code class="language-plaintext highlighter-rouge">suc n</code>, then the inductive hypothesis
|
||
<code class="language-plaintext highlighter-rouge">≤-total m n</code> establishes one of the following:</p>
|
||
|
||
<ul>
|
||
<li>
|
||
<p>The forward case of the inductive hypothesis holds with <code class="language-plaintext highlighter-rouge">m≤n</code> as
|
||
evidence that <code class="language-plaintext highlighter-rouge">m ≤ n</code>, from which it follows that the forward case of the
|
||
proposition holds with <code class="language-plaintext highlighter-rouge">s≤s m≤n</code> as evidence that <code class="language-plaintext highlighter-rouge">suc m ≤ suc n</code>.</p>
|
||
</li>
|
||
<li>
|
||
<p>The flipped case of the inductive hypothesis holds with <code class="language-plaintext highlighter-rouge">n≤m</code> as
|
||
evidence that <code class="language-plaintext highlighter-rouge">n ≤ m</code>, from which it follows that the flipped case of the
|
||
proposition holds with <code class="language-plaintext highlighter-rouge">s≤s n≤m</code> as evidence that <code class="language-plaintext highlighter-rouge">suc n ≤ suc m</code>.</p>
|
||
</li>
|
||
</ul>
|
||
</li>
|
||
</ul>
|
||
|
||
<p>This is our first use of the <code class="language-plaintext highlighter-rouge">with</code> clause in Agda. The keyword
|
||
<code class="language-plaintext highlighter-rouge">with</code> is followed by an expression and one or more subsequent lines.
|
||
Each line begins with an ellipsis (<code class="language-plaintext highlighter-rouge">...</code>) and a vertical bar (<code class="language-plaintext highlighter-rouge">|</code>),
|
||
followed by a pattern to be matched against the expression
|
||
and the right-hand side of the equation.</p>
|
||
|
||
<p>Every use of <code class="language-plaintext highlighter-rouge">with</code> is equivalent to defining a helper function. For
|
||
example, the definition above is equivalent to the following:</p>
|
||
<pre class="Agda"><a id="≤-total′"></a><a id="15301" href="/20.07/Relations/#15301" class="Function">≤-total′</a> <a id="15310" class="Symbol">:</a> <a id="15312" class="Symbol">∀</a> <a id="15314" class="Symbol">(</a><a id="15315" href="/20.07/Relations/#15315" class="Bound">m</a> <a id="15317" href="/20.07/Relations/#15317" class="Bound">n</a> <a id="15319" class="Symbol">:</a> <a id="15321" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="15322" class="Symbol">)</a> <a id="15324" class="Symbol">→</a> <a id="15326" href="/20.07/Relations/#12174" class="Datatype">Total</a> <a id="15332" href="/20.07/Relations/#15315" class="Bound">m</a> <a id="15334" href="/20.07/Relations/#15317" class="Bound">n</a>
|
||
<a id="15336" href="/20.07/Relations/#15301" class="Function">≤-total′</a> <a id="15345" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">zero</a> <a id="15353" href="/20.07/Relations/#15353" class="Bound">n</a> <a id="15362" class="Symbol">=</a> <a id="15365" href="/20.07/Relations/#12205" class="InductiveConstructor">forward</a> <a id="15373" href="/20.07/Relations/#1235" class="InductiveConstructor">z≤n</a>
|
||
<a id="15377" href="/20.07/Relations/#15301" class="Function">≤-total′</a> <a id="15386" class="Symbol">(</a><a id="15387" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="15391" href="/20.07/Relations/#15391" class="Bound">m</a><a id="15392" class="Symbol">)</a> <a id="15394" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">zero</a> <a id="15403" class="Symbol">=</a> <a id="15406" href="/20.07/Relations/#12262" class="InductiveConstructor">flipped</a> <a id="15414" href="/20.07/Relations/#1235" class="InductiveConstructor">z≤n</a>
|
||
<a id="15418" href="/20.07/Relations/#15301" class="Function">≤-total′</a> <a id="15427" class="Symbol">(</a><a id="15428" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="15432" href="/20.07/Relations/#15432" class="Bound">m</a><a id="15433" class="Symbol">)</a> <a id="15435" class="Symbol">(</a><a id="15436" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="15440" href="/20.07/Relations/#15440" class="Bound">n</a><a id="15441" class="Symbol">)</a> <a id="15444" class="Symbol">=</a> <a id="15447" href="/20.07/Relations/#15479" class="Function">helper</a> <a id="15454" class="Symbol">(</a><a id="15455" href="/20.07/Relations/#15301" class="Function">≤-total′</a> <a id="15464" href="/20.07/Relations/#15432" class="Bound">m</a> <a id="15466" href="/20.07/Relations/#15440" class="Bound">n</a><a id="15467" class="Symbol">)</a>
|
||
<a id="15471" class="Keyword">where</a>
|
||
<a id="15479" href="/20.07/Relations/#15479" class="Function">helper</a> <a id="15486" class="Symbol">:</a> <a id="15488" href="/20.07/Relations/#12174" class="Datatype">Total</a> <a id="15494" href="/20.07/Relations/#15432" class="Bound">m</a> <a id="15496" href="/20.07/Relations/#15440" class="Bound">n</a> <a id="15498" class="Symbol">→</a> <a id="15500" href="/20.07/Relations/#12174" class="Datatype">Total</a> <a id="15506" class="Symbol">(</a><a id="15507" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="15511" href="/20.07/Relations/#15432" class="Bound">m</a><a id="15512" class="Symbol">)</a> <a id="15514" class="Symbol">(</a><a id="15515" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="15519" href="/20.07/Relations/#15440" class="Bound">n</a><a id="15520" class="Symbol">)</a>
|
||
<a id="15524" href="/20.07/Relations/#15479" class="Function">helper</a> <a id="15531" class="Symbol">(</a><a id="15532" href="/20.07/Relations/#12205" class="InductiveConstructor">forward</a> <a id="15540" href="/20.07/Relations/#15540" class="Bound">m≤n</a><a id="15543" class="Symbol">)</a> <a id="15546" class="Symbol">=</a> <a id="15549" href="/20.07/Relations/#12205" class="InductiveConstructor">forward</a> <a id="15557" class="Symbol">(</a><a id="15558" href="/20.07/Relations/#1284" class="InductiveConstructor">s≤s</a> <a id="15562" href="/20.07/Relations/#15540" class="Bound">m≤n</a><a id="15565" class="Symbol">)</a>
|
||
<a id="15569" href="/20.07/Relations/#15479" class="Function">helper</a> <a id="15576" class="Symbol">(</a><a id="15577" href="/20.07/Relations/#12262" class="InductiveConstructor">flipped</a> <a id="15585" href="/20.07/Relations/#15585" class="Bound">n≤m</a><a id="15588" class="Symbol">)</a> <a id="15591" class="Symbol">=</a> <a id="15594" href="/20.07/Relations/#12262" class="InductiveConstructor">flipped</a> <a id="15602" class="Symbol">(</a><a id="15603" href="/20.07/Relations/#1284" class="InductiveConstructor">s≤s</a> <a id="15607" href="/20.07/Relations/#15585" class="Bound">n≤m</a><a id="15610" class="Symbol">)</a>
|
||
</pre>
|
||
<p>This is also our first use of a <code class="language-plaintext highlighter-rouge">where</code> clause in Agda. The keyword <code class="language-plaintext highlighter-rouge">where</code> is
|
||
followed by one or more definitions, which must be indented. Any variables
|
||
bound on the left-hand side of the preceding equation (in this case, <code class="language-plaintext highlighter-rouge">m</code> and
|
||
<code class="language-plaintext highlighter-rouge">n</code>) are in scope within the nested definition, and any identifiers bound in the
|
||
nested definition (in this case, <code class="language-plaintext highlighter-rouge">helper</code>) are in scope in the right-hand side
|
||
of the preceding equation.</p>
|
||
|
||
<p>If both arguments are equal, then both cases hold and we could return evidence
|
||
of either. In the code above we return the forward case, but there is a
|
||
variant that returns the flipped case:</p>
|
||
<pre class="Agda"><a id="≤-total″"></a><a id="16232" href="/20.07/Relations/#16232" class="Function">≤-total″</a> <a id="16241" class="Symbol">:</a> <a id="16243" class="Symbol">∀</a> <a id="16245" class="Symbol">(</a><a id="16246" href="/20.07/Relations/#16246" class="Bound">m</a> <a id="16248" href="/20.07/Relations/#16248" class="Bound">n</a> <a id="16250" class="Symbol">:</a> <a id="16252" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="16253" class="Symbol">)</a> <a id="16255" class="Symbol">→</a> <a id="16257" href="/20.07/Relations/#12174" class="Datatype">Total</a> <a id="16263" href="/20.07/Relations/#16246" class="Bound">m</a> <a id="16265" href="/20.07/Relations/#16248" class="Bound">n</a>
|
||
<a id="16267" href="/20.07/Relations/#16232" class="Function">≤-total″</a> <a id="16276" href="/20.07/Relations/#16276" class="Bound">m</a> <a id="16284" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">zero</a> <a id="16310" class="Symbol">=</a> <a id="16313" href="/20.07/Relations/#12262" class="InductiveConstructor">flipped</a> <a id="16321" href="/20.07/Relations/#1235" class="InductiveConstructor">z≤n</a>
|
||
<a id="16325" href="/20.07/Relations/#16232" class="Function">≤-total″</a> <a id="16334" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">zero</a> <a id="16342" class="Symbol">(</a><a id="16343" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="16347" href="/20.07/Relations/#16347" class="Bound">n</a><a id="16348" class="Symbol">)</a> <a id="16368" class="Symbol">=</a> <a id="16371" href="/20.07/Relations/#12205" class="InductiveConstructor">forward</a> <a id="16379" href="/20.07/Relations/#1235" class="InductiveConstructor">z≤n</a>
|
||
<a id="16383" href="/20.07/Relations/#16232" class="Function">≤-total″</a> <a id="16392" class="Symbol">(</a><a id="16393" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="16397" href="/20.07/Relations/#16397" class="Bound">m</a><a id="16398" class="Symbol">)</a> <a id="16400" class="Symbol">(</a><a id="16401" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="16405" href="/20.07/Relations/#16405" class="Bound">n</a><a id="16406" class="Symbol">)</a> <a id="16408" class="Keyword">with</a> <a id="16413" href="/20.07/Relations/#16232" class="Function">≤-total″</a> <a id="16422" href="/20.07/Relations/#16397" class="Bound">m</a> <a id="16424" href="/20.07/Relations/#16405" class="Bound">n</a>
|
||
<a id="16426" class="Symbol">...</a> <a id="16453" class="Symbol">|</a> <a id="16455" href="/20.07/Relations/#12205" class="InductiveConstructor">forward</a> <a id="16463" href="/20.07/Relations/#16463" class="Bound">m≤n</a> <a id="16469" class="Symbol">=</a> <a id="16472" href="/20.07/Relations/#12205" class="InductiveConstructor">forward</a> <a id="16480" class="Symbol">(</a><a id="16481" href="/20.07/Relations/#1284" class="InductiveConstructor">s≤s</a> <a id="16485" href="/20.07/Relations/#16463" class="Bound">m≤n</a><a id="16488" class="Symbol">)</a>
|
||
<a id="16490" class="Symbol">...</a> <a id="16517" class="Symbol">|</a> <a id="16519" href="/20.07/Relations/#12262" class="InductiveConstructor">flipped</a> <a id="16527" href="/20.07/Relations/#16527" class="Bound">n≤m</a> <a id="16533" class="Symbol">=</a> <a id="16536" href="/20.07/Relations/#12262" class="InductiveConstructor">flipped</a> <a id="16544" class="Symbol">(</a><a id="16545" href="/20.07/Relations/#1284" class="InductiveConstructor">s≤s</a> <a id="16549" href="/20.07/Relations/#16527" class="Bound">n≤m</a><a id="16552" class="Symbol">)</a>
|
||
</pre>
|
||
<p>It differs from the original code in that it pattern
|
||
matches on the second argument before the first argument.</p>
|
||
|
||
<h2 id="monotonicity">Monotonicity</h2>
|
||
|
||
<p>If one bumps into both an operator and an ordering at a party, one may ask if
|
||
the operator is <em>monotonic</em> with regard to the ordering. For example, addition
|
||
is monotonic with regard to inequality, meaning:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>∀ {m n p q : ℕ} → m ≤ n → p ≤ q → m + p ≤ n + q
|
||
</code></pre></div></div>
|
||
|
||
<p>The proof is straightforward using the techniques we have learned, and is best
|
||
broken into three parts. First, we deal with the special case of showing
|
||
addition is monotonic on the right:</p>
|
||
<pre class="Agda"><a id="+-monoʳ-≤"></a><a id="17141" href="/20.07/Relations/#17141" class="Function">+-monoʳ-≤</a> <a id="17151" class="Symbol">:</a> <a id="17153" class="Symbol">∀</a> <a id="17155" class="Symbol">(</a><a id="17156" href="/20.07/Relations/#17156" class="Bound">n</a> <a id="17158" href="/20.07/Relations/#17158" class="Bound">p</a> <a id="17160" href="/20.07/Relations/#17160" class="Bound">q</a> <a id="17162" class="Symbol">:</a> <a id="17164" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="17165" class="Symbol">)</a>
|
||
<a id="17169" class="Symbol">→</a> <a id="17171" href="/20.07/Relations/#17158" class="Bound">p</a> <a id="17173" href="/20.07/Relations/#1208" class="Datatype Operator">≤</a> <a id="17175" href="/20.07/Relations/#17160" class="Bound">q</a>
|
||
<a id="17181" class="Comment">-------------</a>
|
||
<a id="17197" class="Symbol">→</a> <a id="17199" href="/20.07/Relations/#17156" class="Bound">n</a> <a id="17201" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="17203" href="/20.07/Relations/#17158" class="Bound">p</a> <a id="17205" href="/20.07/Relations/#1208" class="Datatype Operator">≤</a> <a id="17207" href="/20.07/Relations/#17156" class="Bound">n</a> <a id="17209" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="17211" href="/20.07/Relations/#17160" class="Bound">q</a>
|
||
<a id="17213" href="/20.07/Relations/#17141" class="Function">+-monoʳ-≤</a> <a id="17223" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">zero</a> <a id="17231" href="/20.07/Relations/#17231" class="Bound">p</a> <a id="17233" href="/20.07/Relations/#17233" class="Bound">q</a> <a id="17235" href="/20.07/Relations/#17235" class="Bound">p≤q</a> <a id="17240" class="Symbol">=</a> <a id="17243" href="/20.07/Relations/#17235" class="Bound">p≤q</a>
|
||
<a id="17247" href="/20.07/Relations/#17141" class="Function">+-monoʳ-≤</a> <a id="17257" class="Symbol">(</a><a id="17258" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="17262" href="/20.07/Relations/#17262" class="Bound">n</a><a id="17263" class="Symbol">)</a> <a id="17265" href="/20.07/Relations/#17265" class="Bound">p</a> <a id="17267" href="/20.07/Relations/#17267" class="Bound">q</a> <a id="17269" href="/20.07/Relations/#17269" class="Bound">p≤q</a> <a id="17274" class="Symbol">=</a> <a id="17277" href="/20.07/Relations/#1284" class="InductiveConstructor">s≤s</a> <a id="17281" class="Symbol">(</a><a id="17282" href="/20.07/Relations/#17141" class="Function">+-monoʳ-≤</a> <a id="17292" href="/20.07/Relations/#17262" class="Bound">n</a> <a id="17294" href="/20.07/Relations/#17265" class="Bound">p</a> <a id="17296" href="/20.07/Relations/#17267" class="Bound">q</a> <a id="17298" href="/20.07/Relations/#17269" class="Bound">p≤q</a><a id="17301" class="Symbol">)</a>
|
||
</pre>
|
||
<p>The proof is by induction on the first argument.</p>
|
||
|
||
<ul>
|
||
<li>
|
||
<p><em>Base case</em>: The first argument is <code class="language-plaintext highlighter-rouge">zero</code> in which case
|
||
<code class="language-plaintext highlighter-rouge">zero + p ≤ zero + q</code> simplifies to <code class="language-plaintext highlighter-rouge">p ≤ q</code>, the evidence
|
||
for which is given by the argument <code class="language-plaintext highlighter-rouge">p≤q</code>.</p>
|
||
</li>
|
||
<li>
|
||
<p><em>Inductive case</em>: The first argument is <code class="language-plaintext highlighter-rouge">suc n</code>, in which case
|
||
<code class="language-plaintext highlighter-rouge">suc n + p ≤ suc n + q</code> simplifies to <code class="language-plaintext highlighter-rouge">suc (n + p) ≤ suc (n + q)</code>.
|
||
The inductive hypothesis <code class="language-plaintext highlighter-rouge">+-monoʳ-≤ n p q p≤q</code> establishes that
|
||
<code class="language-plaintext highlighter-rouge">n + p ≤ n + q</code>, and our goal follows by applying <code class="language-plaintext highlighter-rouge">s≤s</code>.</p>
|
||
</li>
|
||
</ul>
|
||
|
||
<p>Second, we deal with the special case of showing addition is
|
||
monotonic on the left. This follows from the previous
|
||
result and the commutativity of addition:</p>
|
||
<pre class="Agda"><a id="+-monoˡ-≤"></a><a id="17941" href="/20.07/Relations/#17941" class="Function">+-monoˡ-≤</a> <a id="17951" class="Symbol">:</a> <a id="17953" class="Symbol">∀</a> <a id="17955" class="Symbol">(</a><a id="17956" href="/20.07/Relations/#17956" class="Bound">m</a> <a id="17958" href="/20.07/Relations/#17958" class="Bound">n</a> <a id="17960" href="/20.07/Relations/#17960" class="Bound">p</a> <a id="17962" class="Symbol">:</a> <a id="17964" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="17965" class="Symbol">)</a>
|
||
<a id="17969" class="Symbol">→</a> <a id="17971" href="/20.07/Relations/#17956" class="Bound">m</a> <a id="17973" href="/20.07/Relations/#1208" class="Datatype Operator">≤</a> <a id="17975" href="/20.07/Relations/#17958" class="Bound">n</a>
|
||
<a id="17981" class="Comment">-------------</a>
|
||
<a id="17997" class="Symbol">→</a> <a id="17999" href="/20.07/Relations/#17956" class="Bound">m</a> <a id="18001" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="18003" href="/20.07/Relations/#17960" class="Bound">p</a> <a id="18005" href="/20.07/Relations/#1208" class="Datatype Operator">≤</a> <a id="18007" href="/20.07/Relations/#17958" class="Bound">n</a> <a id="18009" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="18011" href="/20.07/Relations/#17960" class="Bound">p</a>
|
||
<a id="18013" href="/20.07/Relations/#17941" class="Function">+-monoˡ-≤</a> <a id="18023" href="/20.07/Relations/#18023" class="Bound">m</a> <a id="18025" href="/20.07/Relations/#18025" class="Bound">n</a> <a id="18027" href="/20.07/Relations/#18027" class="Bound">p</a> <a id="18029" href="/20.07/Relations/#18029" class="Bound">m≤n</a> <a id="18034" class="Keyword">rewrite</a> <a id="18042" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#11911" class="Function">+-comm</a> <a id="18049" href="/20.07/Relations/#18023" class="Bound">m</a> <a id="18051" href="/20.07/Relations/#18027" class="Bound">p</a> <a id="18053" class="Symbol">|</a> <a id="18055" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#11911" class="Function">+-comm</a> <a id="18062" href="/20.07/Relations/#18025" class="Bound">n</a> <a id="18064" href="/20.07/Relations/#18027" class="Bound">p</a> <a id="18067" class="Symbol">=</a> <a id="18069" href="/20.07/Relations/#17141" class="Function">+-monoʳ-≤</a> <a id="18079" href="/20.07/Relations/#18027" class="Bound">p</a> <a id="18081" href="/20.07/Relations/#18023" class="Bound">m</a> <a id="18083" href="/20.07/Relations/#18025" class="Bound">n</a> <a id="18085" href="/20.07/Relations/#18029" class="Bound">m≤n</a>
|
||
</pre>
|
||
<p>Rewriting by <code class="language-plaintext highlighter-rouge">+-comm m p</code> and <code class="language-plaintext highlighter-rouge">+-comm n p</code> converts <code class="language-plaintext highlighter-rouge">m + p ≤ n + p</code> into
|
||
<code class="language-plaintext highlighter-rouge">p + m ≤ p + n</code>, which is proved by invoking <code class="language-plaintext highlighter-rouge">+-monoʳ-≤ p m n m≤n</code>.</p>
|
||
|
||
<p>Third, we combine the two previous results:</p>
|
||
<pre class="Agda"><a id="+-mono-≤"></a><a id="18283" href="/20.07/Relations/#18283" class="Function">+-mono-≤</a> <a id="18292" class="Symbol">:</a> <a id="18294" class="Symbol">∀</a> <a id="18296" class="Symbol">(</a><a id="18297" href="/20.07/Relations/#18297" class="Bound">m</a> <a id="18299" href="/20.07/Relations/#18299" class="Bound">n</a> <a id="18301" href="/20.07/Relations/#18301" class="Bound">p</a> <a id="18303" href="/20.07/Relations/#18303" class="Bound">q</a> <a id="18305" class="Symbol">:</a> <a id="18307" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="18308" class="Symbol">)</a>
|
||
<a id="18312" class="Symbol">→</a> <a id="18314" href="/20.07/Relations/#18297" class="Bound">m</a> <a id="18316" href="/20.07/Relations/#1208" class="Datatype Operator">≤</a> <a id="18318" href="/20.07/Relations/#18299" class="Bound">n</a>
|
||
<a id="18322" class="Symbol">→</a> <a id="18324" href="/20.07/Relations/#18301" class="Bound">p</a> <a id="18326" href="/20.07/Relations/#1208" class="Datatype Operator">≤</a> <a id="18328" href="/20.07/Relations/#18303" class="Bound">q</a>
|
||
<a id="18334" class="Comment">-------------</a>
|
||
<a id="18350" class="Symbol">→</a> <a id="18352" href="/20.07/Relations/#18297" class="Bound">m</a> <a id="18354" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="18356" href="/20.07/Relations/#18301" class="Bound">p</a> <a id="18358" href="/20.07/Relations/#1208" class="Datatype Operator">≤</a> <a id="18360" href="/20.07/Relations/#18299" class="Bound">n</a> <a id="18362" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="18364" href="/20.07/Relations/#18303" class="Bound">q</a>
|
||
<a id="18366" href="/20.07/Relations/#18283" class="Function">+-mono-≤</a> <a id="18375" href="/20.07/Relations/#18375" class="Bound">m</a> <a id="18377" href="/20.07/Relations/#18377" class="Bound">n</a> <a id="18379" href="/20.07/Relations/#18379" class="Bound">p</a> <a id="18381" href="/20.07/Relations/#18381" class="Bound">q</a> <a id="18383" href="/20.07/Relations/#18383" class="Bound">m≤n</a> <a id="18387" href="/20.07/Relations/#18387" class="Bound">p≤q</a> <a id="18392" class="Symbol">=</a> <a id="18395" href="/20.07/Relations/#8877" class="Function">≤-trans</a> <a id="18403" class="Symbol">(</a><a id="18404" href="/20.07/Relations/#17941" class="Function">+-monoˡ-≤</a> <a id="18414" href="/20.07/Relations/#18375" class="Bound">m</a> <a id="18416" href="/20.07/Relations/#18377" class="Bound">n</a> <a id="18418" href="/20.07/Relations/#18379" class="Bound">p</a> <a id="18420" href="/20.07/Relations/#18383" class="Bound">m≤n</a><a id="18423" class="Symbol">)</a> <a id="18425" class="Symbol">(</a><a id="18426" href="/20.07/Relations/#17141" class="Function">+-monoʳ-≤</a> <a id="18436" href="/20.07/Relations/#18377" class="Bound">n</a> <a id="18438" href="/20.07/Relations/#18379" class="Bound">p</a> <a id="18440" href="/20.07/Relations/#18381" class="Bound">q</a> <a id="18442" href="/20.07/Relations/#18387" class="Bound">p≤q</a><a id="18445" class="Symbol">)</a>
|
||
</pre>
|
||
<p>Invoking <code class="language-plaintext highlighter-rouge">+-monoˡ-≤ m n p m≤n</code> proves <code class="language-plaintext highlighter-rouge">m + p ≤ n + p</code> and invoking
|
||
<code class="language-plaintext highlighter-rouge">+-monoʳ-≤ n p q p≤q</code> proves <code class="language-plaintext highlighter-rouge">n + p ≤ n + q</code>, and combining these with
|
||
transitivity proves <code class="language-plaintext highlighter-rouge">m + p ≤ n + q</code>, as was to be shown.</p>
|
||
|
||
<h4 id="exercise--mono--stretch">Exercise <code class="language-plaintext highlighter-rouge">*-mono-≤</code> (stretch)</h4>
|
||
|
||
<p>Show that multiplication is monotonic with regard to inequality.</p>
|
||
|
||
<pre class="Agda"><a id="18754" class="Comment">-- Your code goes here</a>
|
||
</pre>
|
||
|
||
<h2 id="strict-inequality">Strict inequality</h2>
|
||
|
||
<p>We can define strict inequality similarly to inequality:</p>
|
||
<pre class="Agda"><a id="18887" class="Keyword">infix</a> <a id="18893" class="Number">4</a> <a id="18895" href="/20.07/Relations/#18905" class="Datatype Operator">_<_</a>
|
||
|
||
<a id="18900" class="Keyword">data</a> <a id="_<_"></a><a id="18905" href="/20.07/Relations/#18905" class="Datatype Operator">_<_</a> <a id="18909" class="Symbol">:</a> <a id="18911" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a> <a id="18913" class="Symbol">→</a> <a id="18915" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a> <a id="18917" class="Symbol">→</a> <a id="18919" class="PrimitiveType">Set</a> <a id="18923" class="Keyword">where</a>
|
||
|
||
<a id="_<_.z<s"></a><a id="18932" href="/20.07/Relations/#18932" class="InductiveConstructor">z<s</a> <a id="18936" class="Symbol">:</a> <a id="18938" class="Symbol">∀</a> <a id="18940" class="Symbol">{</a><a id="18941" href="/20.07/Relations/#18941" class="Bound">n</a> <a id="18943" class="Symbol">:</a> <a id="18945" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="18946" class="Symbol">}</a>
|
||
<a id="18954" class="Comment">------------</a>
|
||
<a id="18971" class="Symbol">→</a> <a id="18973" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">zero</a> <a id="18978" href="/20.07/Relations/#18905" class="Datatype Operator"><</a> <a id="18980" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="18984" href="/20.07/Relations/#18941" class="Bound">n</a>
|
||
|
||
<a id="_<_.s<s"></a><a id="18989" href="/20.07/Relations/#18989" class="InductiveConstructor">s<s</a> <a id="18993" class="Symbol">:</a> <a id="18995" class="Symbol">∀</a> <a id="18997" class="Symbol">{</a><a id="18998" href="/20.07/Relations/#18998" class="Bound">m</a> <a id="19000" href="/20.07/Relations/#19000" class="Bound">n</a> <a id="19002" class="Symbol">:</a> <a id="19004" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="19005" class="Symbol">}</a>
|
||
<a id="19011" class="Symbol">→</a> <a id="19013" href="/20.07/Relations/#18998" class="Bound">m</a> <a id="19015" href="/20.07/Relations/#18905" class="Datatype Operator"><</a> <a id="19017" href="/20.07/Relations/#19000" class="Bound">n</a>
|
||
<a id="19025" class="Comment">-------------</a>
|
||
<a id="19043" class="Symbol">→</a> <a id="19045" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="19049" href="/20.07/Relations/#18998" class="Bound">m</a> <a id="19051" href="/20.07/Relations/#18905" class="Datatype Operator"><</a> <a id="19053" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="19057" href="/20.07/Relations/#19000" class="Bound">n</a>
|
||
</pre>
|
||
<p>The key difference is that zero is less than the successor of an
|
||
arbitrary number, but is not less than zero.</p>
|
||
|
||
<p>Clearly, strict inequality is not reflexive. However it is
|
||
<em>irreflexive</em> in that <code class="language-plaintext highlighter-rouge">n < n</code> never holds for any value of <code class="language-plaintext highlighter-rouge">n</code>.
|
||
Like inequality, strict inequality is transitive.
|
||
Strict inequality is not total, but satisfies the closely related property of
|
||
<em>trichotomy</em>: for any <code class="language-plaintext highlighter-rouge">m</code> and <code class="language-plaintext highlighter-rouge">n</code>, exactly one of <code class="language-plaintext highlighter-rouge">m < n</code>, <code class="language-plaintext highlighter-rouge">m ≡ n</code>, or <code class="language-plaintext highlighter-rouge">m > n</code>
|
||
holds (where we define <code class="language-plaintext highlighter-rouge">m > n</code> to hold exactly when <code class="language-plaintext highlighter-rouge">n < m</code>).
|
||
It is also monotonic with regards to addition and multiplication.</p>
|
||
|
||
<p>Most of the above are considered in exercises below. Irreflexivity
|
||
requires negation, as does the fact that the three cases in
|
||
trichotomy are mutually exclusive, so those points are deferred to
|
||
Chapter <a href="/20.07/Negation/">Negation</a>.</p>
|
||
|
||
<p>It is straightforward to show that <code class="language-plaintext highlighter-rouge">suc m ≤ n</code> implies <code class="language-plaintext highlighter-rouge">m < n</code>,
|
||
and conversely. One can then give an alternative derivation of the
|
||
properties of strict inequality, such as transitivity, by
|
||
exploiting the corresponding properties of inequality.</p>
|
||
|
||
<h4 id="less-trans">Exercise <code class="language-plaintext highlighter-rouge"><-trans</code> (recommended)</h4>
|
||
|
||
<p>Show that strict inequality is transitive.</p>
|
||
|
||
<pre class="Agda"><a id="20226" class="Comment">-- Your code goes here</a>
|
||
</pre>
|
||
<h4 id="trichotomy">Exercise <code class="language-plaintext highlighter-rouge">trichotomy</code> (practice)</h4>
|
||
|
||
<p>Show that strict inequality satisfies a weak version of trichotomy, in
|
||
the sense that for any <code class="language-plaintext highlighter-rouge">m</code> and <code class="language-plaintext highlighter-rouge">n</code> that one of the following holds:</p>
|
||
<ul>
|
||
<li><code class="language-plaintext highlighter-rouge">m < n</code>,</li>
|
||
<li><code class="language-plaintext highlighter-rouge">m ≡ n</code>, or</li>
|
||
<li><code class="language-plaintext highlighter-rouge">m > n</code>.</li>
|
||
</ul>
|
||
|
||
<p>Define <code class="language-plaintext highlighter-rouge">m > n</code> to be the same as <code class="language-plaintext highlighter-rouge">n < m</code>.
|
||
You will need a suitable data declaration,
|
||
similar to that used for totality.
|
||
(We will show that the three cases are exclusive after we introduce
|
||
<a href="/20.07/Negation/">negation</a>.)</p>
|
||
|
||
<pre class="Agda"><a id="20725" class="Comment">-- Your code goes here</a>
|
||
</pre>
|
||
<h4 id="plus-mono-less">Exercise <code class="language-plaintext highlighter-rouge">+-mono-<</code> (practice)</h4>
|
||
|
||
<p>Show that addition is monotonic with respect to strict inequality.
|
||
As with inequality, some additional definitions may be required.</p>
|
||
|
||
<pre class="Agda"><a id="20945" class="Comment">-- Your code goes here</a>
|
||
</pre>
|
||
<h4 id="leq-iff-less">Exercise <code class="language-plaintext highlighter-rouge">≤-iff-<</code> (recommended)</h4>
|
||
|
||
<p>Show that <code class="language-plaintext highlighter-rouge">suc m ≤ n</code> implies <code class="language-plaintext highlighter-rouge">m < n</code>, and conversely.</p>
|
||
|
||
<pre class="Agda"><a id="21088" class="Comment">-- Your code goes here</a>
|
||
</pre>
|
||
<h4 id="less-trans-revisited">Exercise <code class="language-plaintext highlighter-rouge"><-trans-revisited</code> (practice)</h4>
|
||
|
||
<p>Give an alternative proof that strict inequality is transitive,
|
||
using the relation between strict inequality and inequality and
|
||
the fact that inequality is transitive.</p>
|
||
|
||
<pre class="Agda"><a id="21359" class="Comment">-- Your code goes here</a>
|
||
</pre>
|
||
|
||
<h2 id="even-and-odd">Even and odd</h2>
|
||
|
||
<p>As a further example, let’s specify even and odd numbers. Inequality
|
||
and strict inequality are <em>binary relations</em>, while even and odd are
|
||
<em>unary relations</em>, sometimes called <em>predicates</em>:</p>
|
||
<pre class="Agda"><a id="21598" class="Keyword">data</a> <a id="even"></a><a id="21603" href="/20.07/Relations/#21603" class="Datatype">even</a> <a id="21608" class="Symbol">:</a> <a id="21610" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a> <a id="21612" class="Symbol">→</a> <a id="21614" class="PrimitiveType">Set</a>
|
||
<a id="21618" class="Keyword">data</a> <a id="odd"></a><a id="21623" href="/20.07/Relations/#21623" class="Datatype">odd</a> <a id="21628" class="Symbol">:</a> <a id="21630" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a> <a id="21632" class="Symbol">→</a> <a id="21634" class="PrimitiveType">Set</a>
|
||
|
||
<a id="21639" class="Keyword">data</a> <a id="21644" href="/20.07/Relations/#21603" class="Datatype">even</a> <a id="21649" class="Keyword">where</a>
|
||
|
||
<a id="even.zero"></a><a id="21658" href="/20.07/Relations/#21658" class="InductiveConstructor">zero</a> <a id="21663" class="Symbol">:</a>
|
||
<a id="21671" class="Comment">---------</a>
|
||
<a id="21687" href="/20.07/Relations/#21603" class="Datatype">even</a> <a id="21692" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">zero</a>
|
||
|
||
<a id="even.suc"></a><a id="21700" href="/20.07/Relations/#21700" class="InductiveConstructor">suc</a> <a id="21705" class="Symbol">:</a> <a id="21707" class="Symbol">∀</a> <a id="21709" class="Symbol">{</a><a id="21710" href="/20.07/Relations/#21710" class="Bound">n</a> <a id="21712" class="Symbol">:</a> <a id="21714" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="21715" class="Symbol">}</a>
|
||
<a id="21721" class="Symbol">→</a> <a id="21723" href="/20.07/Relations/#21623" class="Datatype">odd</a> <a id="21727" href="/20.07/Relations/#21710" class="Bound">n</a>
|
||
<a id="21735" class="Comment">------------</a>
|
||
<a id="21752" class="Symbol">→</a> <a id="21754" href="/20.07/Relations/#21603" class="Datatype">even</a> <a id="21759" class="Symbol">(</a><a id="21760" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="21764" href="/20.07/Relations/#21710" class="Bound">n</a><a id="21765" class="Symbol">)</a>
|
||
|
||
<a id="21768" class="Keyword">data</a> <a id="21773" href="/20.07/Relations/#21623" class="Datatype">odd</a> <a id="21777" class="Keyword">where</a>
|
||
|
||
<a id="odd.suc"></a><a id="21786" href="/20.07/Relations/#21786" class="InductiveConstructor">suc</a> <a id="21792" class="Symbol">:</a> <a id="21794" class="Symbol">∀</a> <a id="21796" class="Symbol">{</a><a id="21797" href="/20.07/Relations/#21797" class="Bound">n</a> <a id="21799" class="Symbol">:</a> <a id="21801" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="21802" class="Symbol">}</a>
|
||
<a id="21808" class="Symbol">→</a> <a id="21810" href="/20.07/Relations/#21603" class="Datatype">even</a> <a id="21815" href="/20.07/Relations/#21797" class="Bound">n</a>
|
||
<a id="21823" class="Comment">-----------</a>
|
||
<a id="21839" class="Symbol">→</a> <a id="21841" href="/20.07/Relations/#21623" class="Datatype">odd</a> <a id="21845" class="Symbol">(</a><a id="21846" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="21850" href="/20.07/Relations/#21797" class="Bound">n</a><a id="21851" class="Symbol">)</a>
|
||
</pre>
|
||
<p>A number is even if it is zero or the successor of an odd number,
|
||
and odd if it is the successor of an even number.</p>
|
||
|
||
<p>This is our first use of a mutually recursive datatype declaration.
|
||
Since each identifier must be defined before it is used, we first
|
||
declare the indexed types <code class="language-plaintext highlighter-rouge">even</code> and <code class="language-plaintext highlighter-rouge">odd</code> (omitting the <code class="language-plaintext highlighter-rouge">where</code>
|
||
keyword and the declarations of the constructors) and then
|
||
declare the constructors (omitting the signatures <code class="language-plaintext highlighter-rouge">ℕ → Set</code>
|
||
which were given earlier).</p>
|
||
|
||
<p>This is also our first use of <em>overloaded</em> constructors,
|
||
that is, using the same name for constructors of different types.
|
||
Here <code class="language-plaintext highlighter-rouge">suc</code> means one of three constructors:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>suc : ℕ → ℕ
|
||
|
||
suc : ∀ {n : ℕ}
|
||
→ odd n
|
||
------------
|
||
→ even (suc n)
|
||
|
||
suc : ∀ {n : ℕ}
|
||
→ even n
|
||
-----------
|
||
→ odd (suc n)
|
||
</code></pre></div></div>
|
||
|
||
<p>Similarly, <code class="language-plaintext highlighter-rouge">zero</code> refers to one of two constructors. Due to how it
|
||
does type inference, Agda does not allow overloading of defined names,
|
||
but does allow overloading of constructors. It is recommended that
|
||
one restrict overloading to related meanings, as we have done here,
|
||
but it is not required.</p>
|
||
|
||
<p>We show that the sum of two even numbers is even:</p>
|
||
<pre class="Agda"><a id="e+e≡e"></a><a id="23011" href="/20.07/Relations/#23011" class="Function">e+e≡e</a> <a id="23017" class="Symbol">:</a> <a id="23019" class="Symbol">∀</a> <a id="23021" class="Symbol">{</a><a id="23022" href="/20.07/Relations/#23022" class="Bound">m</a> <a id="23024" href="/20.07/Relations/#23024" class="Bound">n</a> <a id="23026" class="Symbol">:</a> <a id="23028" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="23029" class="Symbol">}</a>
|
||
<a id="23033" class="Symbol">→</a> <a id="23035" href="/20.07/Relations/#21603" class="Datatype">even</a> <a id="23040" href="/20.07/Relations/#23022" class="Bound">m</a>
|
||
<a id="23044" class="Symbol">→</a> <a id="23046" href="/20.07/Relations/#21603" class="Datatype">even</a> <a id="23051" href="/20.07/Relations/#23024" class="Bound">n</a>
|
||
<a id="23057" class="Comment">------------</a>
|
||
<a id="23072" class="Symbol">→</a> <a id="23074" href="/20.07/Relations/#21603" class="Datatype">even</a> <a id="23079" class="Symbol">(</a><a id="23080" href="/20.07/Relations/#23022" class="Bound">m</a> <a id="23082" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="23084" href="/20.07/Relations/#23024" class="Bound">n</a><a id="23085" class="Symbol">)</a>
|
||
|
||
<a id="o+e≡o"></a><a id="23088" href="/20.07/Relations/#23088" class="Function">o+e≡o</a> <a id="23094" class="Symbol">:</a> <a id="23096" class="Symbol">∀</a> <a id="23098" class="Symbol">{</a><a id="23099" href="/20.07/Relations/#23099" class="Bound">m</a> <a id="23101" href="/20.07/Relations/#23101" class="Bound">n</a> <a id="23103" class="Symbol">:</a> <a id="23105" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="23106" class="Symbol">}</a>
|
||
<a id="23110" class="Symbol">→</a> <a id="23112" href="/20.07/Relations/#21623" class="Datatype">odd</a> <a id="23116" href="/20.07/Relations/#23099" class="Bound">m</a>
|
||
<a id="23120" class="Symbol">→</a> <a id="23122" href="/20.07/Relations/#21603" class="Datatype">even</a> <a id="23127" href="/20.07/Relations/#23101" class="Bound">n</a>
|
||
<a id="23133" class="Comment">-----------</a>
|
||
<a id="23147" class="Symbol">→</a> <a id="23149" href="/20.07/Relations/#21623" class="Datatype">odd</a> <a id="23153" class="Symbol">(</a><a id="23154" href="/20.07/Relations/#23099" class="Bound">m</a> <a id="23156" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="23158" href="/20.07/Relations/#23101" class="Bound">n</a><a id="23159" class="Symbol">)</a>
|
||
|
||
<a id="23162" href="/20.07/Relations/#23011" class="Function">e+e≡e</a> <a id="23168" href="/20.07/Relations/#21658" class="InductiveConstructor">zero</a> <a id="23177" href="/20.07/Relations/#23177" class="Bound">en</a> <a id="23181" class="Symbol">=</a> <a id="23184" href="/20.07/Relations/#23177" class="Bound">en</a>
|
||
<a id="23187" href="/20.07/Relations/#23011" class="Function">e+e≡e</a> <a id="23193" class="Symbol">(</a><a id="23194" href="/20.07/Relations/#21700" class="InductiveConstructor">suc</a> <a id="23198" href="/20.07/Relations/#23198" class="Bound">om</a><a id="23200" class="Symbol">)</a> <a id="23202" href="/20.07/Relations/#23202" class="Bound">en</a> <a id="23206" class="Symbol">=</a> <a id="23209" href="/20.07/Relations/#21700" class="InductiveConstructor">suc</a> <a id="23213" class="Symbol">(</a><a id="23214" href="/20.07/Relations/#23088" class="Function">o+e≡o</a> <a id="23220" href="/20.07/Relations/#23198" class="Bound">om</a> <a id="23223" href="/20.07/Relations/#23202" class="Bound">en</a><a id="23225" class="Symbol">)</a>
|
||
|
||
<a id="23228" href="/20.07/Relations/#23088" class="Function">o+e≡o</a> <a id="23234" class="Symbol">(</a><a id="23235" href="/20.07/Relations/#21786" class="InductiveConstructor">suc</a> <a id="23239" href="/20.07/Relations/#23239" class="Bound">em</a><a id="23241" class="Symbol">)</a> <a id="23243" href="/20.07/Relations/#23243" class="Bound">en</a> <a id="23247" class="Symbol">=</a> <a id="23250" href="/20.07/Relations/#21786" class="InductiveConstructor">suc</a> <a id="23254" class="Symbol">(</a><a id="23255" href="/20.07/Relations/#23011" class="Function">e+e≡e</a> <a id="23261" href="/20.07/Relations/#23239" class="Bound">em</a> <a id="23264" href="/20.07/Relations/#23243" class="Bound">en</a><a id="23266" class="Symbol">)</a>
|
||
</pre>
|
||
<p>Corresponding to the mutually recursive types, we use two mutually recursive
|
||
functions, one to show that the sum of two even numbers is even, and the other
|
||
to show that the sum of an odd and an even number is odd.</p>
|
||
|
||
<p>This is our first use of mutually recursive functions. Since each identifier
|
||
must be defined before it is used, we first give the signatures for both
|
||
functions and then the equations that define them.</p>
|
||
|
||
<p>To show that the sum of two even numbers is even, consider the
|
||
evidence that the first number is even. If it is because it is zero,
|
||
then the sum is even because the second number is even. If it is
|
||
because it is the successor of an odd number, then the result is even
|
||
because it is the successor of the sum of an odd and an even number,
|
||
which is odd.</p>
|
||
|
||
<p>To show that the sum of an odd and even number is odd, consider the
|
||
evidence that the first number is odd. If it is because it is the
|
||
successor of an even number, then the result is odd because it is the
|
||
successor of the sum of two even numbers, which is even.</p>
|
||
|
||
<h4 id="odd-plus-odd">Exercise <code class="language-plaintext highlighter-rouge">o+o≡e</code> (stretch)</h4>
|
||
|
||
<p>Show that the sum of two odd numbers is even.</p>
|
||
|
||
<pre class="Agda"><a id="24404" class="Comment">-- Your code goes here</a>
|
||
</pre>
|
||
<h4 id="Bin-predicates">Exercise <code class="language-plaintext highlighter-rouge">Bin-predicates</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.
|
||
Representations are not unique due to leading zeros.
|
||
Hence, eleven may be represented by both of the following:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>⟨⟩ I O I I
|
||
⟨⟩ O O I O I I
|
||
</code></pre></div></div>
|
||
|
||
<p>Define a predicate</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>Can : Bin → Set
|
||
</code></pre></div></div>
|
||
|
||
<p>over all bitstrings that holds if the bitstring is canonical, meaning
|
||
it has no leading zeros; the first representation of eleven above is
|
||
canonical, and the second is not. To define it, you will need an
|
||
auxiliary predicate</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>One : Bin → Set
|
||
</code></pre></div></div>
|
||
|
||
<p>that holds only if the bistring has a leading one. A bitstring is
|
||
canonical if it has a leading one (representing a positive number) or
|
||
if it consists of a single zero (representing zero).</p>
|
||
|
||
<p>Show that increment preserves canonical bitstrings:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>Can b
|
||
------------
|
||
Can (inc b)
|
||
</code></pre></div></div>
|
||
|
||
<p>Show that converting a natural to a bitstring always yields a
|
||
canonical bitstring:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>----------
|
||
Can (to n)
|
||
</code></pre></div></div>
|
||
|
||
<p>Show that converting a canonical bitstring to a natural
|
||
and back is the identity:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>Can b
|
||
---------------
|
||
to (from b) ≡ b
|
||
</code></pre></div></div>
|
||
|
||
<p>(Hint: For each of these, you may first need to prove related
|
||
properties of <code class="language-plaintext highlighter-rouge">One</code>. Also, you may need to prove that
|
||
if <code class="language-plaintext highlighter-rouge">One b</code> then <code class="language-plaintext highlighter-rouge">1</code> is less or equal to the result of <code class="language-plaintext highlighter-rouge">from b</code>.)</p>
|
||
|
||
<pre class="Agda"><a id="25781" 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="25917" class="Keyword">import</a> <a id="25924" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.html" class="Module">Data.Nat</a> <a id="25933" class="Keyword">using</a> <a id="25939" class="Symbol">(</a><a id="25940" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Base.html#895" class="Datatype Operator">_≤_</a><a id="25943" class="Symbol">;</a> <a id="25945" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Base.html#918" class="InductiveConstructor">z≤n</a><a id="25948" class="Symbol">;</a> <a id="25950" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Base.html#960" class="InductiveConstructor">s≤s</a><a id="25953" class="Symbol">)</a>
|
||
<a id="25955" class="Keyword">import</a> <a id="25962" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html" class="Module">Data.Nat.Properties</a> <a id="25982" class="Keyword">using</a> <a id="25988" class="Symbol">(</a><a id="25989" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#3632" class="Function">≤-refl</a><a id="25995" class="Symbol">;</a> <a id="25997" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#3815" class="Function">≤-trans</a><a id="26004" class="Symbol">;</a> <a id="26006" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#3682" class="Function">≤-antisym</a><a id="26015" class="Symbol">;</a> <a id="26017" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#3927" class="Function">≤-total</a><a id="26024" class="Symbol">;</a>
|
||
<a id="26060" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#15619" class="Function">+-monoʳ-≤</a><a id="26069" class="Symbol">;</a> <a id="26071" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#15529" class="Function">+-monoˡ-≤</a><a id="26080" class="Symbol">;</a> <a id="26082" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#15373" class="Function">+-mono-≤</a><a id="26090" class="Symbol">)</a>
|
||
</pre>
|
||
<p>In the standard library, <code class="language-plaintext highlighter-rouge">≤-total</code> is formalised in terms of
|
||
disjunction (which we define in
|
||
Chapter <a href="/20.07/Connectives/">Connectives</a>),
|
||
and <code class="language-plaintext highlighter-rouge">+-monoʳ-≤</code>, <code class="language-plaintext highlighter-rouge">+-monoˡ-≤</code>, <code class="language-plaintext highlighter-rouge">+-mono-≤</code> are proved differently than here,
|
||
and more arguments are implicit.</p>
|
||
|
||
<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+2264 LESS-THAN OR EQUAL TO (\<=, \le)
|
||
≥ U+2265 GREATER-THAN OR EQUAL TO (\>=, \ge)
|
||
ˡ U+02E1 MODIFIER LETTER SMALL L (\^l)
|
||
ʳ U+02B3 MODIFIER LETTER SMALL R (\^r)
|
||
</code></pre></div></div>
|
||
|
||
<p>The commands <code class="language-plaintext highlighter-rouge">\^l</code> and <code class="language-plaintext highlighter-rouge">\^r</code> give access to a variety of superscript
|
||
leftward and rightward arrows in addition to superscript letters <code class="language-plaintext highlighter-rouge">l</code> and <code class="language-plaintext highlighter-rouge">r</code>.</p>
|
||
|
||
</div>
|
||
|
||
<p style="text-align:center;">
|
||
|
||
<a alt="Previous chapter" href="/20.07/Induction/">Prev</a>
|
||
|
||
|
||
•
|
||
|
||
|
||
<a alt="Source code" href="https://github.com/plfa/plfa.github.io/blob/dev-20.07/src/plfa/part1/Relations.lagda.md">Source</a>
|
||
|
||
|
||
•
|
||
|
||
|
||
<a alt="Next chapter" href="/20.07/Equality/">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>
|