michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
csci8980-f21/versions/20.07/Lists/index.html

1261 lines
243 KiB
HTML
Raw Permalink Blame History

This file contains invisible Unicode characters

This file contains invisible Unicode characters that are indistinguishable to humans but may be processed differently by a computer. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

<!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>Lists: Lists and higher-order functions | 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="Lists: Lists and higher-order functions" />
<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/Lists/" />
<meta property="og:url" content="https://plfa.github.io/20.07/Lists/" />
<meta property="og:site_name" content="Programming Language Foundations in Agda" />
<script type="application/ld+json">
{"url":"https://plfa.github.io/20.07/Lists/","headline":"Lists: Lists and higher-order functions","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">Lists: Lists and higher-order functions</h1>
</header>
<p style="text-align:center;">
<a alt="Previous chapter" href="/20.07/Decidable/">Prev</a>
&bullet;
<a alt="Source code" href="https://github.com/plfa/plfa.github.io/blob/dev-20.07/src/plfa/part1/Lists.lagda.md">Source</a>
&bullet;
<a alt="Next chapter" href="/20.07/Lambda/">Next</a>
</p>
<div class="post-content">
<pre class="Agda"><a id="150" class="Keyword">module</a> <a id="157" href="/20.07/Lists/" class="Module">plfa.part1.Lists</a> <a id="174" class="Keyword">where</a>
</pre>
<p>This chapter discusses the list data type. It gives further examples
of many of the techniques we have developed so far, and provides
examples of polymorphic types and higher-order functions.</p>
<h2 id="imports">Imports</h2>
<pre class="Agda"><a id="395" class="Keyword">import</a> <a id="402" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.html" class="Module">Relation.Binary.PropositionalEquality</a> <a id="440" class="Symbol">as</a> <a id="443" class="Module">Eq</a>
<a id="446" class="Keyword">open</a> <a id="451" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.html" class="Module">Eq</a> <a id="454" class="Keyword">using</a> <a id="460" class="Symbol">(</a><a id="461" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">_≡_</a><a id="464" class="Symbol">;</a> <a id="466" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a><a id="470" class="Symbol">;</a> <a id="472" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#939" class="Function">sym</a><a id="475" class="Symbol">;</a> <a id="477" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#984" class="Function">trans</a><a id="482" class="Symbol">;</a> <a id="484" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#1090" class="Function">cong</a><a id="488" class="Symbol">)</a>
<a id="490" class="Keyword">open</a> <a id="495" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2499" class="Module">Eq.≡-Reasoning</a>
<a id="510" class="Keyword">open</a> <a id="515" class="Keyword">import</a> <a id="522" href="https://agda.github.io/agda-stdlib/v1.1/Data.Bool.html" class="Module">Data.Bool</a> <a id="532" class="Keyword">using</a> <a id="538" class="Symbol">(</a><a id="539" href="Agda.Builtin.Bool.html#135" class="Datatype">Bool</a><a id="543" class="Symbol">;</a> <a id="545" href="Agda.Builtin.Bool.html#160" class="InductiveConstructor">true</a><a id="549" class="Symbol">;</a> <a id="551" href="Agda.Builtin.Bool.html#154" class="InductiveConstructor">false</a><a id="556" class="Symbol">;</a> <a id="558" href="https://agda.github.io/agda-stdlib/v1.1/Data.Bool.Base.html#1480" class="Function">T</a><a id="559" class="Symbol">;</a> <a id="561" href="https://agda.github.io/agda-stdlib/v1.1/Data.Bool.Base.html#1015" class="Function Operator">_∧_</a><a id="564" class="Symbol">;</a> <a id="566" href="https://agda.github.io/agda-stdlib/v1.1/Data.Bool.Base.html#1073" class="Function Operator">_∨_</a><a id="569" class="Symbol">;</a> <a id="571" href="https://agda.github.io/agda-stdlib/v1.1/Data.Bool.Base.html#961" class="Function">not</a><a id="574" class="Symbol">)</a>
<a id="576" class="Keyword">open</a> <a id="581" class="Keyword">import</a> <a id="588" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.html" class="Module">Data.Nat</a> <a id="597" class="Keyword">using</a> <a id="603" class="Symbol">(</a><a id="604" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="605" class="Symbol">;</a> <a id="607" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">zero</a><a id="611" class="Symbol">;</a> <a id="613" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a><a id="616" class="Symbol">;</a> <a id="618" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">_+_</a><a id="621" class="Symbol">;</a> <a id="623" href="Agda.Builtin.Nat.html#501" class="Primitive Operator">_*_</a><a id="626" class="Symbol">;</a> <a id="628" href="Agda.Builtin.Nat.html#388" class="Primitive Operator">_∸_</a><a id="631" class="Symbol">;</a> <a id="633" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Base.html#895" class="Datatype Operator">_≤_</a><a id="636" class="Symbol">;</a> <a id="638" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Base.html#960" class="InductiveConstructor">s≤s</a><a id="641" class="Symbol">;</a> <a id="643" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Base.html#918" class="InductiveConstructor">z≤n</a><a id="646" class="Symbol">)</a>
<a id="648" class="Keyword">open</a> <a id="653" class="Keyword">import</a> <a id="660" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html" class="Module">Data.Nat.Properties</a> <a id="680" class="Keyword">using</a>
<a id="688" class="Symbol">(</a><a id="689" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#11578" class="Function">+-assoc</a><a id="696" class="Symbol">;</a> <a id="698" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#11679" class="Function">+-identityˡ</a><a id="709" class="Symbol">;</a> <a id="711" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#11734" class="Function">+-identityʳ</a><a id="722" class="Symbol">;</a> <a id="724" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#18464" class="Function">*-assoc</a><a id="731" class="Symbol">;</a> <a id="733" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#17362" class="Function">*-identityˡ</a><a id="744" class="Symbol">;</a> <a id="746" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#17426" class="Function">*-identityʳ</a><a id="757" class="Symbol">)</a>
<a id="759" class="Keyword">open</a> <a id="764" class="Keyword">import</a> <a id="771" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html" class="Module">Relation.Nullary</a> <a id="788" class="Keyword">using</a> <a id="794" class="Symbol">(</a><a id="795" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#535" class="Function Operator">¬_</a><a id="797" class="Symbol">;</a> <a id="799" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#605" class="Datatype">Dec</a><a id="802" class="Symbol">;</a> <a id="804" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a><a id="807" class="Symbol">;</a> <a id="809" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a><a id="811" class="Symbol">)</a>
<a id="813" class="Keyword">open</a> <a id="818" class="Keyword">import</a> <a id="825" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html" class="Module">Data.Product</a> <a id="838" class="Keyword">using</a> <a id="844" class="Symbol">(</a><a id="845" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1162" class="Function Operator">_×_</a><a id="848" class="Symbol">;</a> <a id="850" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1364" class="Function">∃</a><a id="851" class="Symbol">;</a> <a id="853" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1783" class="Function">∃-syntax</a><a id="861" class="Symbol">)</a> <a id="863" class="Keyword">renaming</a> <a id="872" class="Symbol">(</a><a id="873" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">_,_</a> <a id="877" class="Symbol">to</a> <a id="880" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨_,_⟩</a><a id="885" class="Symbol">)</a>
<a id="887" class="Keyword">open</a> <a id="892" class="Keyword">import</a> <a id="899" href="https://agda.github.io/agda-stdlib/v1.1/Function.html" class="Module">Function</a> <a id="908" class="Keyword">using</a> <a id="914" class="Symbol">(</a><a id="915" href="https://agda.github.io/agda-stdlib/v1.1/Function.html#1099" class="Function Operator">_∘_</a><a id="918" class="Symbol">)</a>
<a id="920" class="Keyword">open</a> <a id="925" class="Keyword">import</a> <a id="932" href="https://agda.github.io/agda-stdlib/v1.1/Level.html" class="Module">Level</a> <a id="938" class="Keyword">using</a> <a id="944" class="Symbol">(</a><a id="945" href="Agda.Primitive.html#408" class="Postulate">Level</a><a id="950" class="Symbol">)</a>
<a id="952" class="Keyword">open</a> <a id="957" class="Keyword">import</a> <a id="964" href="/20.07/Isomorphism/" class="Module">plfa.part1.Isomorphism</a> <a id="987" class="Keyword">using</a> <a id="993" class="Symbol">(</a><a id="994" href="/20.07/Isomorphism/#4365" class="Record Operator">_≃_</a><a id="997" class="Symbol">;</a> <a id="999" href="/20.07/Isomorphism/#12042" class="Record Operator">_⇔_</a><a id="1002" class="Symbol">)</a>
</pre>
<h2 id="lists">Lists</h2>
<p>Lists are defined in Agda as follows:</p>
<pre class="Agda"><a id="1062" class="Keyword">data</a> <a id="List"></a><a id="1067" href="/20.07/Lists/#1067" class="Datatype">List</a> <a id="1072" class="Symbol">(</a><a id="1073" href="/20.07/Lists/#1073" class="Bound">A</a> <a id="1075" class="Symbol">:</a> <a id="1077" class="PrimitiveType">Set</a><a id="1080" class="Symbol">)</a> <a id="1082" class="Symbol">:</a> <a id="1084" class="PrimitiveType">Set</a> <a id="1088" class="Keyword">where</a>
<a id="List.[]"></a><a id="1096" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a> <a id="1100" class="Symbol">:</a> <a id="1102" href="/20.07/Lists/#1067" class="Datatype">List</a> <a id="1107" href="/20.07/Lists/#1073" class="Bound">A</a>
<a id="List._∷_"></a><a id="1111" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">_∷_</a> <a id="1115" class="Symbol">:</a> <a id="1117" href="/20.07/Lists/#1073" class="Bound">A</a> <a id="1119" class="Symbol">→</a> <a id="1121" href="/20.07/Lists/#1067" class="Datatype">List</a> <a id="1126" href="/20.07/Lists/#1073" class="Bound">A</a> <a id="1128" class="Symbol">→</a> <a id="1130" href="/20.07/Lists/#1067" class="Datatype">List</a> <a id="1135" href="/20.07/Lists/#1073" class="Bound">A</a>
<a id="1138" class="Keyword">infixr</a> <a id="1145" class="Number">5</a> <a id="1147" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">_∷_</a>
</pre>
<p>Let’s unpack this definition. If <code class="language-plaintext highlighter-rouge">A</code> is a set, then <code class="language-plaintext highlighter-rouge">List A</code> is a set.
The next two lines tell us that <code class="language-plaintext highlighter-rouge">[]</code> (pronounced <em>nil</em>) is a list of
type <code class="language-plaintext highlighter-rouge">A</code> (often called the <em>empty</em> list), and that <code class="language-plaintext highlighter-rouge">_∷_</code> (pronounced
<em>cons</em>, short for <em>constructor</em>) takes a value of type <code class="language-plaintext highlighter-rouge">A</code> and a value
of type <code class="language-plaintext highlighter-rouge">List A</code> and returns a value of type <code class="language-plaintext highlighter-rouge">List A</code>. Operator <code class="language-plaintext highlighter-rouge">_∷_</code>
has precedence level 5 and associates to the right.</p>
<p>For example,</p>
<pre class="Agda"><a id="1576" href="/20.07/Lists/#1576" class="Function">_</a> <a id="1578" class="Symbol">:</a> <a id="1580" href="/20.07/Lists/#1067" class="Datatype">List</a> <a id="1585" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a>
<a id="1587" class="Symbol">_</a> <a id="1589" class="Symbol">=</a> <a id="1591" class="Number">0</a> <a id="1593" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="1595" class="Number">1</a> <a id="1597" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="1599" class="Number">2</a> <a id="1601" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="1603" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a>
</pre>
<p>denotes the list of the first three natural numbers. Since <code class="language-plaintext highlighter-rouge">_∷_</code>
associates to the right, the term parses as <code class="language-plaintext highlighter-rouge">0 ∷ (1 ∷ (2 ∷ []))</code>.
Here <code class="language-plaintext highlighter-rouge">0</code> is the first element of the list, called the <em>head</em>,
and <code class="language-plaintext highlighter-rouge">1 ∷ (2 ∷ [])</code> is a list of the remaining elements, called the
<em>tail</em>. A list is a strange beast: it has a head and a tail,
nothing in between, and the tail is itself another list!</p>
<p>As we’ve seen, parameterised types can be translated to
indexed types. The definition above is equivalent to the following:</p>
<pre class="Agda"><a id="2118" class="Keyword">data</a> <a id="List′"></a><a id="2123" href="/20.07/Lists/#2123" class="Datatype">List′</a> <a id="2129" class="Symbol">:</a> <a id="2131" class="PrimitiveType">Set</a> <a id="2135" class="Symbol">→</a> <a id="2137" class="PrimitiveType">Set</a> <a id="2141" class="Keyword">where</a>
<a id="List′.[]′"></a><a id="2149" href="/20.07/Lists/#2149" class="InductiveConstructor">[]′</a> <a id="2154" class="Symbol">:</a> <a id="2156" class="Symbol">∀</a> <a id="2158" class="Symbol">{</a><a id="2159" href="/20.07/Lists/#2159" class="Bound">A</a> <a id="2161" class="Symbol">:</a> <a id="2163" class="PrimitiveType">Set</a><a id="2166" class="Symbol">}</a> <a id="2168" class="Symbol">→</a> <a id="2170" href="/20.07/Lists/#2123" class="Datatype">List′</a> <a id="2176" href="/20.07/Lists/#2159" class="Bound">A</a>
<a id="List′._∷′_"></a><a id="2180" href="/20.07/Lists/#2180" class="InductiveConstructor Operator">_∷′_</a> <a id="2185" class="Symbol">:</a> <a id="2187" class="Symbol">∀</a> <a id="2189" class="Symbol">{</a><a id="2190" href="/20.07/Lists/#2190" class="Bound">A</a> <a id="2192" class="Symbol">:</a> <a id="2194" class="PrimitiveType">Set</a><a id="2197" class="Symbol">}</a> <a id="2199" class="Symbol">→</a> <a id="2201" href="/20.07/Lists/#2190" class="Bound">A</a> <a id="2203" class="Symbol">→</a> <a id="2205" href="/20.07/Lists/#2123" class="Datatype">List′</a> <a id="2211" href="/20.07/Lists/#2190" class="Bound">A</a> <a id="2213" class="Symbol">→</a> <a id="2215" href="/20.07/Lists/#2123" class="Datatype">List′</a> <a id="2221" href="/20.07/Lists/#2190" class="Bound">A</a>
</pre>
<p>Each constructor takes the parameter as an implicit argument.
Thus, our example list could also be written:</p>
<pre class="Agda"><a id="2339" href="/20.07/Lists/#2339" class="Function">_</a> <a id="2341" class="Symbol">:</a> <a id="2343" href="/20.07/Lists/#1067" class="Datatype">List</a> <a id="2348" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a>
<a id="2350" class="Symbol">_</a> <a id="2352" class="Symbol">=</a> <a id="2354" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">_∷_</a> <a id="2358" class="Symbol">{</a><a id="2359" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="2360" class="Symbol">}</a> <a id="2362" class="Number">0</a> <a id="2364" class="Symbol">(</a><a id="2365" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">_∷_</a> <a id="2369" class="Symbol">{</a><a id="2370" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="2371" class="Symbol">}</a> <a id="2373" class="Number">1</a> <a id="2375" class="Symbol">(</a><a id="2376" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">_∷_</a> <a id="2380" class="Symbol">{</a><a id="2381" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="2382" class="Symbol">}</a> <a id="2384" class="Number">2</a> <a id="2386" class="Symbol">(</a><a id="2387" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a> <a id="2390" class="Symbol">{</a><a id="2391" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="2392" class="Symbol">})))</a>
</pre>
<p>where here we have provided the implicit parameters explicitly.</p>
<p>Including the pragma:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>{-# BUILTIN LIST List #-}
</code></pre></div></div>
<p>tells Agda that the type <code class="language-plaintext highlighter-rouge">List</code> corresponds to the Haskell type
list, and the constructors <code class="language-plaintext highlighter-rouge">[]</code> and <code class="language-plaintext highlighter-rouge">_∷_</code> correspond to nil and
cons respectively, allowing a more efficient representation of lists.</p>
<h2 id="list-syntax">List syntax</h2>
<p>We can write lists more conveniently by introducing the following definitions:</p>
<pre class="Agda"><a id="2819" class="Keyword">pattern</a> <a id="[_]"></a><a id="2827" href="/20.07/Lists/#2827" class="InductiveConstructor Operator">[_]</a> <a id="2831" href="/20.07/Lists/#2835" class="Bound">z</a> <a id="2833" class="Symbol">=</a> <a id="2835" href="/20.07/Lists/#2835" class="Bound">z</a> <a id="2837" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="2839" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a>
<a id="2842" class="Keyword">pattern</a> <a id="[_,_]"></a><a id="2850" href="/20.07/Lists/#2850" class="InductiveConstructor Operator">[_,_]</a> <a id="2856" href="/20.07/Lists/#2862" class="Bound">y</a> <a id="2858" href="/20.07/Lists/#2866" class="Bound">z</a> <a id="2860" class="Symbol">=</a> <a id="2862" href="/20.07/Lists/#2862" class="Bound">y</a> <a id="2864" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="2866" href="/20.07/Lists/#2866" class="Bound">z</a> <a id="2868" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="2870" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a>
<a id="2873" class="Keyword">pattern</a> <a id="[_,_,_]"></a><a id="2881" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">[_,_,_]</a> <a id="2889" href="/20.07/Lists/#2897" class="Bound">x</a> <a id="2891" href="/20.07/Lists/#2901" class="Bound">y</a> <a id="2893" href="/20.07/Lists/#2905" class="Bound">z</a> <a id="2895" class="Symbol">=</a> <a id="2897" href="/20.07/Lists/#2897" class="Bound">x</a> <a id="2899" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="2901" href="/20.07/Lists/#2901" class="Bound">y</a> <a id="2903" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="2905" href="/20.07/Lists/#2905" class="Bound">z</a> <a id="2907" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="2909" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a>
<a id="2912" class="Keyword">pattern</a> <a id="[_,_,_,_]"></a><a id="2920" href="/20.07/Lists/#2920" class="InductiveConstructor Operator">[_,_,_,_]</a> <a id="2930" href="/20.07/Lists/#2940" class="Bound">w</a> <a id="2932" href="/20.07/Lists/#2944" class="Bound">x</a> <a id="2934" href="/20.07/Lists/#2948" class="Bound">y</a> <a id="2936" href="/20.07/Lists/#2952" class="Bound">z</a> <a id="2938" class="Symbol">=</a> <a id="2940" href="/20.07/Lists/#2940" class="Bound">w</a> <a id="2942" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="2944" href="/20.07/Lists/#2944" class="Bound">x</a> <a id="2946" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="2948" href="/20.07/Lists/#2948" class="Bound">y</a> <a id="2950" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="2952" href="/20.07/Lists/#2952" class="Bound">z</a> <a id="2954" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="2956" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a>
<a id="2959" class="Keyword">pattern</a> <a id="[_,_,_,_,_]"></a><a id="2967" href="/20.07/Lists/#2967" class="InductiveConstructor Operator">[_,_,_,_,_]</a> <a id="2979" href="/20.07/Lists/#2991" class="Bound">v</a> <a id="2981" href="/20.07/Lists/#2995" class="Bound">w</a> <a id="2983" href="/20.07/Lists/#2999" class="Bound">x</a> <a id="2985" href="/20.07/Lists/#3003" class="Bound">y</a> <a id="2987" href="/20.07/Lists/#3007" class="Bound">z</a> <a id="2989" class="Symbol">=</a> <a id="2991" href="/20.07/Lists/#2991" class="Bound">v</a> <a id="2993" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="2995" href="/20.07/Lists/#2995" class="Bound">w</a> <a id="2997" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="2999" href="/20.07/Lists/#2999" class="Bound">x</a> <a id="3001" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="3003" href="/20.07/Lists/#3003" class="Bound">y</a> <a id="3005" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="3007" href="/20.07/Lists/#3007" class="Bound">z</a> <a id="3009" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="3011" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a>
<a id="3014" class="Keyword">pattern</a> <a id="[_,_,_,_,_,_]"></a><a id="3022" href="/20.07/Lists/#3022" class="InductiveConstructor Operator">[_,_,_,_,_,_]</a> <a id="3036" href="/20.07/Lists/#3050" class="Bound">u</a> <a id="3038" href="/20.07/Lists/#3054" class="Bound">v</a> <a id="3040" href="/20.07/Lists/#3058" class="Bound">w</a> <a id="3042" href="/20.07/Lists/#3062" class="Bound">x</a> <a id="3044" href="/20.07/Lists/#3066" class="Bound">y</a> <a id="3046" href="/20.07/Lists/#3070" class="Bound">z</a> <a id="3048" class="Symbol">=</a> <a id="3050" href="/20.07/Lists/#3050" class="Bound">u</a> <a id="3052" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="3054" href="/20.07/Lists/#3054" class="Bound">v</a> <a id="3056" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="3058" href="/20.07/Lists/#3058" class="Bound">w</a> <a id="3060" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="3062" href="/20.07/Lists/#3062" class="Bound">x</a> <a id="3064" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="3066" href="/20.07/Lists/#3066" class="Bound">y</a> <a id="3068" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="3070" href="/20.07/Lists/#3070" class="Bound">z</a> <a id="3072" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="3074" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a>
</pre>
<p>This is our first use of pattern declarations. For instance,
the third line tells us that <code class="language-plaintext highlighter-rouge">[ x , y , z ]</code> is equivalent to
<code class="language-plaintext highlighter-rouge">x ∷ y ∷ z ∷ []</code>, and permits the former to appear either in
a pattern on the left-hand side of an equation, or a term
on the right-hand side of an equation.</p>
<h2 id="append">Append</h2>
<p>Our first function on lists is written <code class="language-plaintext highlighter-rouge">_++_</code> and pronounced
<em>append</em>:</p>
<pre class="Agda"><a id="3452" class="Keyword">infixr</a> <a id="3459" class="Number">5</a> <a id="3461" href="/20.07/Lists/#3467" class="Function Operator">_++_</a>
<a id="_++_"></a><a id="3467" href="/20.07/Lists/#3467" class="Function Operator">_++_</a> <a id="3472" class="Symbol">:</a> <a id="3474" class="Symbol">∀</a> <a id="3476" class="Symbol">{</a><a id="3477" href="/20.07/Lists/#3477" class="Bound">A</a> <a id="3479" class="Symbol">:</a> <a id="3481" class="PrimitiveType">Set</a><a id="3484" class="Symbol">}</a> <a id="3486" class="Symbol">→</a> <a id="3488" href="/20.07/Lists/#1067" class="Datatype">List</a> <a id="3493" href="/20.07/Lists/#3477" class="Bound">A</a> <a id="3495" class="Symbol">→</a> <a id="3497" href="/20.07/Lists/#1067" class="Datatype">List</a> <a id="3502" href="/20.07/Lists/#3477" class="Bound">A</a> <a id="3504" class="Symbol">→</a> <a id="3506" href="/20.07/Lists/#1067" class="Datatype">List</a> <a id="3511" href="/20.07/Lists/#3477" class="Bound">A</a>
<a id="3513" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a> <a id="3522" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="3525" href="/20.07/Lists/#3525" class="Bound">ys</a> <a id="3529" class="Symbol">=</a> <a id="3532" href="/20.07/Lists/#3525" class="Bound">ys</a>
<a id="3535" class="Symbol">(</a><a id="3536" href="/20.07/Lists/#3536" class="Bound">x</a> <a id="3538" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="3540" href="/20.07/Lists/#3540" class="Bound">xs</a><a id="3542" class="Symbol">)</a> <a id="3544" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="3547" href="/20.07/Lists/#3547" class="Bound">ys</a> <a id="3551" class="Symbol">=</a> <a id="3554" href="/20.07/Lists/#3536" class="Bound">x</a> <a id="3556" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="3558" class="Symbol">(</a><a id="3559" href="/20.07/Lists/#3540" class="Bound">xs</a> <a id="3562" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="3565" href="/20.07/Lists/#3547" class="Bound">ys</a><a id="3567" class="Symbol">)</a>
</pre>
<p>The type <code class="language-plaintext highlighter-rouge">A</code> is an implicit argument to append, making it a <em>polymorphic</em>
function (one that can be used at many types). A list appended to the empty list
yields the list itself. A list appended to a non-empty list yields a list with
the head the same as the head of the non-empty list, and a tail the same as the
other list appended to tail of the non-empty list.</p>
<p>Here is an example, showing how to compute the result
of appending two lists:</p>
<pre class="Agda"><a id="4021" href="/20.07/Lists/#4021" class="Function">_</a> <a id="4023" class="Symbol">:</a> <a id="4025" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">[</a> <a id="4027" class="Number">0</a> <a id="4029" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">,</a> <a id="4031" class="Number">1</a> <a id="4033" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">,</a> <a id="4035" class="Number">2</a> <a id="4037" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">]</a> <a id="4039" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="4042" href="/20.07/Lists/#2850" class="InductiveConstructor Operator">[</a> <a id="4044" class="Number">3</a> <a id="4046" href="/20.07/Lists/#2850" class="InductiveConstructor Operator">,</a> <a id="4048" class="Number">4</a> <a id="4050" href="/20.07/Lists/#2850" class="InductiveConstructor Operator">]</a> <a id="4052" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="4054" href="/20.07/Lists/#2967" class="InductiveConstructor Operator">[</a> <a id="4056" class="Number">0</a> <a id="4058" href="/20.07/Lists/#2967" class="InductiveConstructor Operator">,</a> <a id="4060" class="Number">1</a> <a id="4062" href="/20.07/Lists/#2967" class="InductiveConstructor Operator">,</a> <a id="4064" class="Number">2</a> <a id="4066" href="/20.07/Lists/#2967" class="InductiveConstructor Operator">,</a> <a id="4068" class="Number">3</a> <a id="4070" href="/20.07/Lists/#2967" class="InductiveConstructor Operator">,</a> <a id="4072" class="Number">4</a> <a id="4074" href="/20.07/Lists/#2967" class="InductiveConstructor Operator">]</a>
<a id="4076" class="Symbol">_</a> <a id="4078" class="Symbol">=</a>
<a id="4082" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2597" class="Function Operator">begin</a>
<a id="4092" class="Number">0</a> <a id="4094" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="4096" class="Number">1</a> <a id="4098" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="4100" class="Number">2</a> <a id="4102" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="4104" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a> <a id="4107" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="4110" class="Number">3</a> <a id="4112" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="4114" class="Number">4</a> <a id="4116" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="4118" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a>
<a id="4123" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="4131" class="Number">0</a> <a id="4133" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="4135" class="Symbol">(</a><a id="4136" class="Number">1</a> <a id="4138" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="4140" class="Number">2</a> <a id="4142" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="4144" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a> <a id="4147" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="4150" class="Number">3</a> <a id="4152" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="4154" class="Number">4</a> <a id="4156" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="4158" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a><a id="4160" class="Symbol">)</a>
<a id="4164" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="4172" class="Number">0</a> <a id="4174" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="4176" class="Number">1</a> <a id="4178" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="4180" class="Symbol">(</a><a id="4181" class="Number">2</a> <a id="4183" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="4185" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a> <a id="4188" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="4191" class="Number">3</a> <a id="4193" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="4195" class="Number">4</a> <a id="4197" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="4199" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a><a id="4201" class="Symbol">)</a>
<a id="4205" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="4213" class="Number">0</a> <a id="4215" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="4217" class="Number">1</a> <a id="4219" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="4221" class="Number">2</a> <a id="4223" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="4225" class="Symbol">(</a><a id="4226" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a> <a id="4229" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="4232" class="Number">3</a> <a id="4234" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="4236" class="Number">4</a> <a id="4238" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="4240" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a><a id="4242" class="Symbol">)</a>
<a id="4246" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="4254" class="Number">0</a> <a id="4256" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="4258" class="Number">1</a> <a id="4260" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="4262" class="Number">2</a> <a id="4264" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="4266" class="Number">3</a> <a id="4268" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="4270" class="Number">4</a> <a id="4272" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="4274" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a>
<a id="4279" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2892" class="Function Operator">∎</a>
</pre>
<p>Appending two lists requires time linear in the
number of elements in the first list.</p>
<h2 id="reasoning-about-append">Reasoning about append</h2>
<p>We can reason about lists in much the same way that we reason
about numbers. Here is the proof that append is associative:</p>
<pre class="Agda"><a id="++-assoc"></a><a id="4528" href="/20.07/Lists/#4528" class="Function">++-assoc</a> <a id="4537" class="Symbol">:</a> <a id="4539" class="Symbol">∀</a> <a id="4541" class="Symbol">{</a><a id="4542" href="/20.07/Lists/#4542" class="Bound">A</a> <a id="4544" class="Symbol">:</a> <a id="4546" class="PrimitiveType">Set</a><a id="4549" class="Symbol">}</a> <a id="4551" class="Symbol">(</a><a id="4552" href="/20.07/Lists/#4552" class="Bound">xs</a> <a id="4555" href="/20.07/Lists/#4555" class="Bound">ys</a> <a id="4558" href="/20.07/Lists/#4558" class="Bound">zs</a> <a id="4561" class="Symbol">:</a> <a id="4563" href="/20.07/Lists/#1067" class="Datatype">List</a> <a id="4568" href="/20.07/Lists/#4542" class="Bound">A</a><a id="4569" class="Symbol">)</a>
<a id="4573" class="Symbol">→</a> <a id="4575" class="Symbol">(</a><a id="4576" href="/20.07/Lists/#4552" class="Bound">xs</a> <a id="4579" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="4582" href="/20.07/Lists/#4555" class="Bound">ys</a><a id="4584" class="Symbol">)</a> <a id="4586" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="4589" href="/20.07/Lists/#4558" class="Bound">zs</a> <a id="4592" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="4594" href="/20.07/Lists/#4552" class="Bound">xs</a> <a id="4597" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="4600" class="Symbol">(</a><a id="4601" href="/20.07/Lists/#4555" class="Bound">ys</a> <a id="4604" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="4607" href="/20.07/Lists/#4558" class="Bound">zs</a><a id="4609" class="Symbol">)</a>
<a id="4611" href="/20.07/Lists/#4528" class="Function">++-assoc</a> <a id="4620" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a> <a id="4623" href="/20.07/Lists/#4623" class="Bound">ys</a> <a id="4626" href="/20.07/Lists/#4626" class="Bound">zs</a> <a id="4629" class="Symbol">=</a>
<a id="4633" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2597" class="Function Operator">begin</a>
<a id="4643" class="Symbol">(</a><a id="4644" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a> <a id="4647" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="4650" href="/20.07/Lists/#4623" class="Bound">ys</a><a id="4652" class="Symbol">)</a> <a id="4654" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="4657" href="/20.07/Lists/#4626" class="Bound">zs</a>
<a id="4662" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="4670" href="/20.07/Lists/#4623" class="Bound">ys</a> <a id="4673" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="4676" href="/20.07/Lists/#4626" class="Bound">zs</a>
<a id="4681" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="4689" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a> <a id="4692" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="4695" class="Symbol">(</a><a id="4696" href="/20.07/Lists/#4623" class="Bound">ys</a> <a id="4699" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="4702" href="/20.07/Lists/#4626" class="Bound">zs</a><a id="4704" class="Symbol">)</a>
<a id="4708" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2892" class="Function Operator">∎</a>
<a id="4710" href="/20.07/Lists/#4528" class="Function">++-assoc</a> <a id="4719" class="Symbol">(</a><a id="4720" href="/20.07/Lists/#4720" class="Bound">x</a> <a id="4722" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="4724" href="/20.07/Lists/#4724" class="Bound">xs</a><a id="4726" class="Symbol">)</a> <a id="4728" href="/20.07/Lists/#4728" class="Bound">ys</a> <a id="4731" href="/20.07/Lists/#4731" class="Bound">zs</a> <a id="4734" class="Symbol">=</a>
<a id="4738" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2597" class="Function Operator">begin</a>
<a id="4748" class="Symbol">(</a><a id="4749" href="/20.07/Lists/#4720" class="Bound">x</a> <a id="4751" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="4753" href="/20.07/Lists/#4724" class="Bound">xs</a> <a id="4756" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="4759" href="/20.07/Lists/#4728" class="Bound">ys</a><a id="4761" class="Symbol">)</a> <a id="4763" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="4766" href="/20.07/Lists/#4731" class="Bound">zs</a>
<a id="4771" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="4779" href="/20.07/Lists/#4720" class="Bound">x</a> <a id="4781" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="4783" class="Symbol">(</a><a id="4784" href="/20.07/Lists/#4724" class="Bound">xs</a> <a id="4787" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="4790" href="/20.07/Lists/#4728" class="Bound">ys</a><a id="4792" class="Symbol">)</a> <a id="4794" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="4797" href="/20.07/Lists/#4731" class="Bound">zs</a>
<a id="4802" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="4810" href="/20.07/Lists/#4720" class="Bound">x</a> <a id="4812" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="4814" class="Symbol">((</a><a id="4816" href="/20.07/Lists/#4724" class="Bound">xs</a> <a id="4819" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="4822" href="/20.07/Lists/#4728" class="Bound">ys</a><a id="4824" class="Symbol">)</a> <a id="4826" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="4829" href="/20.07/Lists/#4731" class="Bound">zs</a><a id="4831" class="Symbol">)</a>
<a id="4835" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">≡⟨</a> <a id="4838" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#1090" class="Function">cong</a> <a id="4843" class="Symbol">(</a><a id="4844" href="/20.07/Lists/#4720" class="Bound">x</a> <a id="4846" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷_</a><a id="4848" class="Symbol">)</a> <a id="4850" class="Symbol">(</a><a id="4851" href="/20.07/Lists/#4528" class="Function">++-assoc</a> <a id="4860" href="/20.07/Lists/#4724" class="Bound">xs</a> <a id="4863" href="/20.07/Lists/#4728" class="Bound">ys</a> <a id="4866" href="/20.07/Lists/#4731" class="Bound">zs</a><a id="4868" class="Symbol">)</a> <a id="4870" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">⟩</a>
<a id="4876" href="/20.07/Lists/#4720" class="Bound">x</a> <a id="4878" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="4880" class="Symbol">(</a><a id="4881" href="/20.07/Lists/#4724" class="Bound">xs</a> <a id="4884" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="4887" class="Symbol">(</a><a id="4888" href="/20.07/Lists/#4728" class="Bound">ys</a> <a id="4891" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="4894" href="/20.07/Lists/#4731" class="Bound">zs</a><a id="4896" class="Symbol">))</a>
<a id="4901" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="4909" href="/20.07/Lists/#4720" class="Bound">x</a> <a id="4911" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="4913" href="/20.07/Lists/#4724" class="Bound">xs</a> <a id="4916" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="4919" class="Symbol">(</a><a id="4920" href="/20.07/Lists/#4728" class="Bound">ys</a> <a id="4923" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="4926" href="/20.07/Lists/#4731" class="Bound">zs</a><a id="4928" class="Symbol">)</a>
<a id="4932" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2892" class="Function Operator">∎</a>
</pre>
<p>The proof is by induction on the first argument. The base case instantiates
to <code class="language-plaintext highlighter-rouge">[]</code>, and follows by straightforward computation.
The inductive case instantiates to <code class="language-plaintext highlighter-rouge">x ∷ xs</code>,
and follows by straightforward computation combined with the
inductive hypothesis. As usual, the inductive hypothesis is indicated by a recursive
invocation of the proof, in this case <code class="language-plaintext highlighter-rouge">++-assoc xs ys zs</code>.</p>
<p>Recall that Agda supports <a href="/20.07/Induction/#sections">sections</a>.
Applying <code class="language-plaintext highlighter-rouge">cong (x ∷_)</code> promotes the inductive hypothesis:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>(xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
</code></pre></div></div>
<p>to the equality:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>x ∷ ((xs ++ ys) ++ zs) ≡ x ∷ (xs ++ (ys ++ zs))
</code></pre></div></div>
<p>which is needed in the proof.</p>
<p>It is also easy to show that <code class="language-plaintext highlighter-rouge">[]</code> is a left and right identity for <code class="language-plaintext highlighter-rouge">_++_</code>.
That it is a left identity is immediate from the definition:</p>
<pre class="Agda"><a id="++-identityˡ"></a><a id="5739" href="/20.07/Lists/#5739" class="Function">++-identityˡ</a> <a id="5752" class="Symbol">:</a> <a id="5754" class="Symbol">∀</a> <a id="5756" class="Symbol">{</a><a id="5757" href="/20.07/Lists/#5757" class="Bound">A</a> <a id="5759" class="Symbol">:</a> <a id="5761" class="PrimitiveType">Set</a><a id="5764" class="Symbol">}</a> <a id="5766" class="Symbol">(</a><a id="5767" href="/20.07/Lists/#5767" class="Bound">xs</a> <a id="5770" class="Symbol">:</a> <a id="5772" href="/20.07/Lists/#1067" class="Datatype">List</a> <a id="5777" href="/20.07/Lists/#5757" class="Bound">A</a><a id="5778" class="Symbol">)</a> <a id="5780" class="Symbol">→</a> <a id="5782" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a> <a id="5785" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="5788" href="/20.07/Lists/#5767" class="Bound">xs</a> <a id="5791" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="5793" href="/20.07/Lists/#5767" class="Bound">xs</a>
<a id="5796" href="/20.07/Lists/#5739" class="Function">++-identityˡ</a> <a id="5809" href="/20.07/Lists/#5809" class="Bound">xs</a> <a id="5812" class="Symbol">=</a>
<a id="5816" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2597" class="Function Operator">begin</a>
<a id="5826" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a> <a id="5829" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="5832" href="/20.07/Lists/#5809" class="Bound">xs</a>
<a id="5837" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="5845" href="/20.07/Lists/#5809" class="Bound">xs</a>
<a id="5850" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2892" class="Function Operator">∎</a>
</pre>
<p>That it is a right identity follows by simple induction:</p>
<pre class="Agda"><a id="++-identityʳ"></a><a id="5917" href="/20.07/Lists/#5917" class="Function">++-identityʳ</a> <a id="5930" class="Symbol">:</a> <a id="5932" class="Symbol">∀</a> <a id="5934" class="Symbol">{</a><a id="5935" href="/20.07/Lists/#5935" class="Bound">A</a> <a id="5937" class="Symbol">:</a> <a id="5939" class="PrimitiveType">Set</a><a id="5942" class="Symbol">}</a> <a id="5944" class="Symbol">(</a><a id="5945" href="/20.07/Lists/#5945" class="Bound">xs</a> <a id="5948" class="Symbol">:</a> <a id="5950" href="/20.07/Lists/#1067" class="Datatype">List</a> <a id="5955" href="/20.07/Lists/#5935" class="Bound">A</a><a id="5956" class="Symbol">)</a> <a id="5958" class="Symbol">→</a> <a id="5960" href="/20.07/Lists/#5945" class="Bound">xs</a> <a id="5963" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="5966" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a> <a id="5969" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="5971" href="/20.07/Lists/#5945" class="Bound">xs</a>
<a id="5974" href="/20.07/Lists/#5917" class="Function">++-identityʳ</a> <a id="5987" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a> <a id="5990" class="Symbol">=</a>
<a id="5994" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2597" class="Function Operator">begin</a>
<a id="6004" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a> <a id="6007" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="6010" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a>
<a id="6015" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="6023" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a>
<a id="6028" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2892" class="Function Operator">∎</a>
<a id="6030" href="/20.07/Lists/#5917" class="Function">++-identityʳ</a> <a id="6043" class="Symbol">(</a><a id="6044" href="/20.07/Lists/#6044" class="Bound">x</a> <a id="6046" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="6048" href="/20.07/Lists/#6048" class="Bound">xs</a><a id="6050" class="Symbol">)</a> <a id="6052" class="Symbol">=</a>
<a id="6056" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2597" class="Function Operator">begin</a>
<a id="6066" class="Symbol">(</a><a id="6067" href="/20.07/Lists/#6044" class="Bound">x</a> <a id="6069" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="6071" href="/20.07/Lists/#6048" class="Bound">xs</a><a id="6073" class="Symbol">)</a> <a id="6075" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="6078" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a>
<a id="6083" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="6091" href="/20.07/Lists/#6044" class="Bound">x</a> <a id="6093" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="6095" class="Symbol">(</a><a id="6096" href="/20.07/Lists/#6048" class="Bound">xs</a> <a id="6099" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="6102" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a><a id="6104" class="Symbol">)</a>
<a id="6108" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">≡⟨</a> <a id="6111" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#1090" class="Function">cong</a> <a id="6116" class="Symbol">(</a><a id="6117" href="/20.07/Lists/#6044" class="Bound">x</a> <a id="6119" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷_</a><a id="6121" class="Symbol">)</a> <a id="6123" class="Symbol">(</a><a id="6124" href="/20.07/Lists/#5917" class="Function">++-identityʳ</a> <a id="6137" href="/20.07/Lists/#6048" class="Bound">xs</a><a id="6139" class="Symbol">)</a> <a id="6141" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">⟩</a>
<a id="6147" href="/20.07/Lists/#6044" class="Bound">x</a> <a id="6149" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="6151" href="/20.07/Lists/#6048" class="Bound">xs</a>
<a id="6156" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2892" class="Function Operator">∎</a>
</pre>
<p>As we will see later,
these three properties establish that <code class="language-plaintext highlighter-rouge">_++_</code> and <code class="language-plaintext highlighter-rouge">[]</code> form
a <em>monoid</em> over lists.</p>
<h2 id="length">Length</h2>
<p>Our next function finds the length of a list:</p>
<pre class="Agda"><a id="length"></a><a id="6328" href="/20.07/Lists/#6328" class="Function">length</a> <a id="6335" class="Symbol">:</a> <a id="6337" class="Symbol">∀</a> <a id="6339" class="Symbol">{</a><a id="6340" href="/20.07/Lists/#6340" class="Bound">A</a> <a id="6342" class="Symbol">:</a> <a id="6344" class="PrimitiveType">Set</a><a id="6347" class="Symbol">}</a> <a id="6349" class="Symbol">→</a> <a id="6351" href="/20.07/Lists/#1067" class="Datatype">List</a> <a id="6356" href="/20.07/Lists/#6340" class="Bound">A</a> <a id="6358" class="Symbol">→</a> <a id="6360" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a>
<a id="6362" href="/20.07/Lists/#6328" class="Function">length</a> <a id="6369" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a> <a id="6379" class="Symbol">=</a> <a id="6382" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">zero</a>
<a id="6387" href="/20.07/Lists/#6328" class="Function">length</a> <a id="6394" class="Symbol">(</a><a id="6395" href="/20.07/Lists/#6395" class="Bound">x</a> <a id="6397" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="6399" href="/20.07/Lists/#6399" class="Bound">xs</a><a id="6401" class="Symbol">)</a> <a id="6404" class="Symbol">=</a> <a id="6407" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="6411" class="Symbol">(</a><a id="6412" href="/20.07/Lists/#6328" class="Function">length</a> <a id="6419" href="/20.07/Lists/#6399" class="Bound">xs</a><a id="6421" class="Symbol">)</a>
</pre>
<p>Again, it takes an implicit parameter <code class="language-plaintext highlighter-rouge">A</code>.
The length of the empty list is zero.
The length of a non-empty list
is one greater than the length of the tail of the list.</p>
<p>Here is an example showing how to compute the length of a list:</p>
<pre class="Agda"><a id="6664" href="/20.07/Lists/#6664" class="Function">_</a> <a id="6666" class="Symbol">:</a> <a id="6668" href="/20.07/Lists/#6328" class="Function">length</a> <a id="6675" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">[</a> <a id="6677" class="Number">0</a> <a id="6679" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">,</a> <a id="6681" class="Number">1</a> <a id="6683" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">,</a> <a id="6685" class="Number">2</a> <a id="6687" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">]</a> <a id="6689" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="6691" class="Number">3</a>
<a id="6693" class="Symbol">_</a> <a id="6695" class="Symbol">=</a>
<a id="6699" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2597" class="Function Operator">begin</a>
<a id="6709" href="/20.07/Lists/#6328" class="Function">length</a> <a id="6716" class="Symbol">(</a><a id="6717" class="Number">0</a> <a id="6719" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="6721" class="Number">1</a> <a id="6723" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="6725" class="Number">2</a> <a id="6727" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="6729" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a><a id="6731" class="Symbol">)</a>
<a id="6735" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="6743" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="6747" class="Symbol">(</a><a id="6748" href="/20.07/Lists/#6328" class="Function">length</a> <a id="6755" class="Symbol">(</a><a id="6756" class="Number">1</a> <a id="6758" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="6760" class="Number">2</a> <a id="6762" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="6764" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a><a id="6766" class="Symbol">))</a>
<a id="6771" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="6779" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="6783" class="Symbol">(</a><a id="6784" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="6788" class="Symbol">(</a><a id="6789" href="/20.07/Lists/#6328" class="Function">length</a> <a id="6796" class="Symbol">(</a><a id="6797" class="Number">2</a> <a id="6799" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="6801" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a><a id="6803" class="Symbol">)))</a>
<a id="6809" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="6817" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="6821" class="Symbol">(</a><a id="6822" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="6826" class="Symbol">(</a><a id="6827" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="6831" class="Symbol">(</a><a id="6832" href="/20.07/Lists/#6328" class="Function">length</a> <a id="6839" class="Symbol">{</a><a id="6840" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a><a id="6841" class="Symbol">}</a> <a id="6843" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a><a id="6845" class="Symbol">)))</a>
<a id="6851" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="6859" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="6863" class="Symbol">(</a><a id="6864" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="6868" class="Symbol">(</a><a id="6869" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="6873" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">zero</a><a id="6877" class="Symbol">))</a>
<a id="6882" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2892" class="Function Operator">∎</a>
</pre>
<p>Computing the length of a list requires time
linear in the number of elements in the list.</p>
<p>In the second-to-last line, we cannot write simply <code class="language-plaintext highlighter-rouge">length []</code> but
must instead write <code class="language-plaintext highlighter-rouge">length {ℕ} []</code>. Since <code class="language-plaintext highlighter-rouge">[]</code> has no elements, Agda
has insufficient information to infer the implicit parameter.</p>
<h2 id="reasoning-about-length">Reasoning about length</h2>
<p>The length of one list appended to another is the
sum of the lengths of the lists:</p>
<pre class="Agda"><a id="length-++"></a><a id="7295" href="/20.07/Lists/#7295" class="Function">length-++</a> <a id="7305" class="Symbol">:</a> <a id="7307" class="Symbol">∀</a> <a id="7309" class="Symbol">{</a><a id="7310" href="/20.07/Lists/#7310" class="Bound">A</a> <a id="7312" class="Symbol">:</a> <a id="7314" class="PrimitiveType">Set</a><a id="7317" class="Symbol">}</a> <a id="7319" class="Symbol">(</a><a id="7320" href="/20.07/Lists/#7320" class="Bound">xs</a> <a id="7323" href="/20.07/Lists/#7323" class="Bound">ys</a> <a id="7326" class="Symbol">:</a> <a id="7328" href="/20.07/Lists/#1067" class="Datatype">List</a> <a id="7333" href="/20.07/Lists/#7310" class="Bound">A</a><a id="7334" class="Symbol">)</a>
<a id="7338" class="Symbol">→</a> <a id="7340" href="/20.07/Lists/#6328" class="Function">length</a> <a id="7347" class="Symbol">(</a><a id="7348" href="/20.07/Lists/#7320" class="Bound">xs</a> <a id="7351" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="7354" href="/20.07/Lists/#7323" class="Bound">ys</a><a id="7356" class="Symbol">)</a> <a id="7358" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="7360" href="/20.07/Lists/#6328" class="Function">length</a> <a id="7367" href="/20.07/Lists/#7320" class="Bound">xs</a> <a id="7370" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="7372" href="/20.07/Lists/#6328" class="Function">length</a> <a id="7379" href="/20.07/Lists/#7323" class="Bound">ys</a>
<a id="7382" href="/20.07/Lists/#7295" class="Function">length-++</a> <a id="7392" class="Symbol">{</a><a id="7393" href="/20.07/Lists/#7393" class="Bound">A</a><a id="7394" class="Symbol">}</a> <a id="7396" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a> <a id="7399" href="/20.07/Lists/#7399" class="Bound">ys</a> <a id="7402" class="Symbol">=</a>
<a id="7406" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2597" class="Function Operator">begin</a>
<a id="7416" href="/20.07/Lists/#6328" class="Function">length</a> <a id="7423" class="Symbol">(</a><a id="7424" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a> <a id="7427" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="7430" href="/20.07/Lists/#7399" class="Bound">ys</a><a id="7432" class="Symbol">)</a>
<a id="7436" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="7444" href="/20.07/Lists/#6328" class="Function">length</a> <a id="7451" href="/20.07/Lists/#7399" class="Bound">ys</a>
<a id="7456" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="7464" href="/20.07/Lists/#6328" class="Function">length</a> <a id="7471" class="Symbol">{</a><a id="7472" href="/20.07/Lists/#7393" class="Bound">A</a><a id="7473" class="Symbol">}</a> <a id="7475" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a> <a id="7478" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="7480" href="/20.07/Lists/#6328" class="Function">length</a> <a id="7487" href="/20.07/Lists/#7399" class="Bound">ys</a>
<a id="7492" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2892" class="Function Operator">∎</a>
<a id="7494" href="/20.07/Lists/#7295" class="Function">length-++</a> <a id="7504" class="Symbol">(</a><a id="7505" href="/20.07/Lists/#7505" class="Bound">x</a> <a id="7507" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="7509" href="/20.07/Lists/#7509" class="Bound">xs</a><a id="7511" class="Symbol">)</a> <a id="7513" href="/20.07/Lists/#7513" class="Bound">ys</a> <a id="7516" class="Symbol">=</a>
<a id="7520" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2597" class="Function Operator">begin</a>
<a id="7530" href="/20.07/Lists/#6328" class="Function">length</a> <a id="7537" class="Symbol">((</a><a id="7539" href="/20.07/Lists/#7505" class="Bound">x</a> <a id="7541" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="7543" href="/20.07/Lists/#7509" class="Bound">xs</a><a id="7545" class="Symbol">)</a> <a id="7547" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="7550" href="/20.07/Lists/#7513" class="Bound">ys</a><a id="7552" class="Symbol">)</a>
<a id="7556" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="7564" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="7568" class="Symbol">(</a><a id="7569" href="/20.07/Lists/#6328" class="Function">length</a> <a id="7576" class="Symbol">(</a><a id="7577" href="/20.07/Lists/#7509" class="Bound">xs</a> <a id="7580" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="7583" href="/20.07/Lists/#7513" class="Bound">ys</a><a id="7585" class="Symbol">))</a>
<a id="7590" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">≡⟨</a> <a id="7593" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#1090" class="Function">cong</a> <a id="7598" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="7602" class="Symbol">(</a><a id="7603" href="/20.07/Lists/#7295" class="Function">length-++</a> <a id="7613" href="/20.07/Lists/#7509" class="Bound">xs</a> <a id="7616" href="/20.07/Lists/#7513" class="Bound">ys</a><a id="7618" class="Symbol">)</a> <a id="7620" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">⟩</a>
<a id="7626" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="7630" class="Symbol">(</a><a id="7631" href="/20.07/Lists/#6328" class="Function">length</a> <a id="7638" href="/20.07/Lists/#7509" class="Bound">xs</a> <a id="7641" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="7643" href="/20.07/Lists/#6328" class="Function">length</a> <a id="7650" href="/20.07/Lists/#7513" class="Bound">ys</a><a id="7652" class="Symbol">)</a>
<a id="7656" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="7664" href="/20.07/Lists/#6328" class="Function">length</a> <a id="7671" class="Symbol">(</a><a id="7672" href="/20.07/Lists/#7505" class="Bound">x</a> <a id="7674" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="7676" href="/20.07/Lists/#7509" class="Bound">xs</a><a id="7678" class="Symbol">)</a> <a id="7680" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="7682" href="/20.07/Lists/#6328" class="Function">length</a> <a id="7689" href="/20.07/Lists/#7513" class="Bound">ys</a>
<a id="7694" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2892" class="Function Operator">∎</a>
</pre>
<p>The proof is by induction on the first argument. The base case
instantiates to <code class="language-plaintext highlighter-rouge">[]</code>, and follows by straightforward computation. As
before, Agda cannot infer the implicit type parameter to <code class="language-plaintext highlighter-rouge">length</code>, and
it must be given explicitly. The inductive case instantiates to
<code class="language-plaintext highlighter-rouge">x ∷ xs</code>, and follows by straightforward computation combined with the
inductive hypothesis. As usual, the inductive hypothesis is indicated
by a recursive invocation of the proof, in this case <code class="language-plaintext highlighter-rouge">length-++ xs ys</code>,
and it is promoted by the congruence <code class="language-plaintext highlighter-rouge">cong suc</code>.</p>
<h2 id="reverse">Reverse</h2>
<p>Using append, it is easy to formulate a function to reverse a list:</p>
<pre class="Agda"><a id="reverse"></a><a id="8318" href="/20.07/Lists/#8318" class="Function">reverse</a> <a id="8326" class="Symbol">:</a> <a id="8328" class="Symbol">∀</a> <a id="8330" class="Symbol">{</a><a id="8331" href="/20.07/Lists/#8331" class="Bound">A</a> <a id="8333" class="Symbol">:</a> <a id="8335" class="PrimitiveType">Set</a><a id="8338" class="Symbol">}</a> <a id="8340" class="Symbol">→</a> <a id="8342" href="/20.07/Lists/#1067" class="Datatype">List</a> <a id="8347" href="/20.07/Lists/#8331" class="Bound">A</a> <a id="8349" class="Symbol">→</a> <a id="8351" href="/20.07/Lists/#1067" class="Datatype">List</a> <a id="8356" href="/20.07/Lists/#8331" class="Bound">A</a>
<a id="8358" href="/20.07/Lists/#8318" class="Function">reverse</a> <a id="8366" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a> <a id="8376" class="Symbol">=</a> <a id="8379" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a>
<a id="8382" href="/20.07/Lists/#8318" class="Function">reverse</a> <a id="8390" class="Symbol">(</a><a id="8391" href="/20.07/Lists/#8391" class="Bound">x</a> <a id="8393" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="8395" href="/20.07/Lists/#8395" class="Bound">xs</a><a id="8397" class="Symbol">)</a> <a id="8400" class="Symbol">=</a> <a id="8403" href="/20.07/Lists/#8318" class="Function">reverse</a> <a id="8411" href="/20.07/Lists/#8395" class="Bound">xs</a> <a id="8414" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="8417" href="/20.07/Lists/#2827" class="InductiveConstructor Operator">[</a> <a id="8419" href="/20.07/Lists/#8391" class="Bound">x</a> <a id="8421" href="/20.07/Lists/#2827" class="InductiveConstructor Operator">]</a>
</pre>
<p>The reverse of the empty list is the empty list.
The reverse of a non-empty list
is the reverse of its tail appended to a unit list
containing its head.</p>
<p>Here is an example showing how to reverse a list:</p>
<pre class="Agda"><a id="8635" href="/20.07/Lists/#8635" class="Function">_</a> <a id="8637" class="Symbol">:</a> <a id="8639" href="/20.07/Lists/#8318" class="Function">reverse</a> <a id="8647" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">[</a> <a id="8649" class="Number">0</a> <a id="8651" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">,</a> <a id="8653" class="Number">1</a> <a id="8655" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">,</a> <a id="8657" class="Number">2</a> <a id="8659" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">]</a> <a id="8661" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="8663" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">[</a> <a id="8665" class="Number">2</a> <a id="8667" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">,</a> <a id="8669" class="Number">1</a> <a id="8671" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">,</a> <a id="8673" class="Number">0</a> <a id="8675" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">]</a>
<a id="8677" class="Symbol">_</a> <a id="8679" class="Symbol">=</a>
<a id="8683" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2597" class="Function Operator">begin</a>
<a id="8693" href="/20.07/Lists/#8318" class="Function">reverse</a> <a id="8701" class="Symbol">(</a><a id="8702" class="Number">0</a> <a id="8704" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="8706" class="Number">1</a> <a id="8708" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="8710" class="Number">2</a> <a id="8712" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="8714" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a><a id="8716" class="Symbol">)</a>
<a id="8720" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="8728" href="/20.07/Lists/#8318" class="Function">reverse</a> <a id="8736" class="Symbol">(</a><a id="8737" class="Number">1</a> <a id="8739" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="8741" class="Number">2</a> <a id="8743" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="8745" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a><a id="8747" class="Symbol">)</a> <a id="8749" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="8752" href="/20.07/Lists/#2827" class="InductiveConstructor Operator">[</a> <a id="8754" class="Number">0</a> <a id="8756" href="/20.07/Lists/#2827" class="InductiveConstructor Operator">]</a>
<a id="8760" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="8768" class="Symbol">(</a><a id="8769" href="/20.07/Lists/#8318" class="Function">reverse</a> <a id="8777" class="Symbol">(</a><a id="8778" class="Number">2</a> <a id="8780" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="8782" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a><a id="8784" class="Symbol">)</a> <a id="8786" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="8789" href="/20.07/Lists/#2827" class="InductiveConstructor Operator">[</a> <a id="8791" class="Number">1</a> <a id="8793" href="/20.07/Lists/#2827" class="InductiveConstructor Operator">]</a><a id="8794" class="Symbol">)</a> <a id="8796" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="8799" href="/20.07/Lists/#2827" class="InductiveConstructor Operator">[</a> <a id="8801" class="Number">0</a> <a id="8803" href="/20.07/Lists/#2827" class="InductiveConstructor Operator">]</a>
<a id="8807" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="8815" class="Symbol">((</a><a id="8817" href="/20.07/Lists/#8318" class="Function">reverse</a> <a id="8825" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a> <a id="8828" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="8831" href="/20.07/Lists/#2827" class="InductiveConstructor Operator">[</a> <a id="8833" class="Number">2</a> <a id="8835" href="/20.07/Lists/#2827" class="InductiveConstructor Operator">]</a><a id="8836" class="Symbol">)</a> <a id="8838" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="8841" href="/20.07/Lists/#2827" class="InductiveConstructor Operator">[</a> <a id="8843" class="Number">1</a> <a id="8845" href="/20.07/Lists/#2827" class="InductiveConstructor Operator">]</a><a id="8846" class="Symbol">)</a> <a id="8848" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="8851" href="/20.07/Lists/#2827" class="InductiveConstructor Operator">[</a> <a id="8853" class="Number">0</a> <a id="8855" href="/20.07/Lists/#2827" class="InductiveConstructor Operator">]</a>
<a id="8859" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="8867" class="Symbol">((</a><a id="8869" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a> <a id="8872" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="8875" href="/20.07/Lists/#2827" class="InductiveConstructor Operator">[</a> <a id="8877" class="Number">2</a> <a id="8879" href="/20.07/Lists/#2827" class="InductiveConstructor Operator">]</a><a id="8880" class="Symbol">)</a> <a id="8882" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="8885" href="/20.07/Lists/#2827" class="InductiveConstructor Operator">[</a> <a id="8887" class="Number">1</a> <a id="8889" href="/20.07/Lists/#2827" class="InductiveConstructor Operator">]</a><a id="8890" class="Symbol">)</a> <a id="8892" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="8895" href="/20.07/Lists/#2827" class="InductiveConstructor Operator">[</a> <a id="8897" class="Number">0</a> <a id="8899" href="/20.07/Lists/#2827" class="InductiveConstructor Operator">]</a>
<a id="8903" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="8911" class="Symbol">((</a><a id="8913" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a> <a id="8916" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="8919" class="Number">2</a> <a id="8921" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="8923" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a><a id="8925" class="Symbol">)</a> <a id="8927" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="8930" class="Number">1</a> <a id="8932" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="8934" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a><a id="8936" class="Symbol">)</a> <a id="8938" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="8941" class="Number">0</a> <a id="8943" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="8945" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a>
<a id="8950" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="8958" class="Symbol">(</a><a id="8959" class="Number">2</a> <a id="8961" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="8963" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a> <a id="8966" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="8969" class="Number">1</a> <a id="8971" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="8973" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a><a id="8975" class="Symbol">)</a> <a id="8977" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="8980" class="Number">0</a> <a id="8982" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="8984" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a>
<a id="8989" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="8997" class="Number">2</a> <a id="8999" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="9001" class="Symbol">(</a><a id="9002" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a> <a id="9005" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="9008" class="Number">1</a> <a id="9010" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="9012" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a><a id="9014" class="Symbol">)</a> <a id="9016" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="9019" class="Number">0</a> <a id="9021" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="9023" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a>
<a id="9028" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="9036" class="Symbol">(</a><a id="9037" class="Number">2</a> <a id="9039" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="9041" class="Number">1</a> <a id="9043" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="9045" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a><a id="9047" class="Symbol">)</a> <a id="9049" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="9052" class="Number">0</a> <a id="9054" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="9056" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a>
<a id="9061" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="9069" class="Number">2</a> <a id="9071" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="9073" class="Symbol">(</a><a id="9074" class="Number">1</a> <a id="9076" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="9078" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a> <a id="9081" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="9084" class="Number">0</a> <a id="9086" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="9088" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a><a id="9090" class="Symbol">)</a>
<a id="9094" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="9102" class="Number">2</a> <a id="9104" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="9106" class="Number">1</a> <a id="9108" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="9110" class="Symbol">(</a><a id="9111" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a> <a id="9114" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="9117" class="Number">0</a> <a id="9119" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="9121" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a><a id="9123" class="Symbol">)</a>
<a id="9127" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="9135" class="Number">2</a> <a id="9137" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="9139" class="Number">1</a> <a id="9141" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="9143" class="Number">0</a> <a id="9145" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="9147" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a>
<a id="9152" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="9160" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">[</a> <a id="9162" class="Number">2</a> <a id="9164" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">,</a> <a id="9166" class="Number">1</a> <a id="9168" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">,</a> <a id="9170" class="Number">0</a> <a id="9172" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">]</a>
<a id="9176" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2892" class="Function Operator">∎</a>
</pre>
<p>Reversing a list in this way takes time <em>quadratic</em> in the length of
the list. This is because reverse ends up appending lists of lengths
<code class="language-plaintext highlighter-rouge">1</code>, <code class="language-plaintext highlighter-rouge">2</code>, up to <code class="language-plaintext highlighter-rouge">n - 1</code>, where <code class="language-plaintext highlighter-rouge">n</code> is the length of the list being
reversed, append takes time linear in the length of the first
list, and the sum of the numbers up to <code class="language-plaintext highlighter-rouge">n - 1</code> is <code class="language-plaintext highlighter-rouge">n * (n - 1) / 2</code>.
(We will validate that last fact in an exercise later in this chapter.)</p>
<h4 id="exercise-reverse--distrib-recommended">Exercise <code class="language-plaintext highlighter-rouge">reverse-++-distrib</code> (recommended)</h4>
<p>Show that the reverse of one list appended to another is the
reverse of the second appended to the reverse of the first:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
</code></pre></div></div>
<h4 id="exercise-reverse-involutive-recommended">Exercise <code class="language-plaintext highlighter-rouge">reverse-involutive</code> (recommended)</h4>
<p>A function is an <em>involution</em> if when applied twice it acts
as the identity function. Show that reverse is an involution:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>reverse (reverse xs) ≡ xs
</code></pre></div></div>
<h2 id="faster-reverse">Faster reverse</h2>
<p>The definition above, while easy to reason about, is less efficient than
one might expect since it takes time quadratic in the length of the list.
The idea is that we generalise reverse to take an additional argument:</p>
<pre class="Agda"><a id="shunt"></a><a id="10262" href="/20.07/Lists/#10262" class="Function">shunt</a> <a id="10268" class="Symbol">:</a> <a id="10270" class="Symbol">∀</a> <a id="10272" class="Symbol">{</a><a id="10273" href="/20.07/Lists/#10273" class="Bound">A</a> <a id="10275" class="Symbol">:</a> <a id="10277" class="PrimitiveType">Set</a><a id="10280" class="Symbol">}</a> <a id="10282" class="Symbol">→</a> <a id="10284" href="/20.07/Lists/#1067" class="Datatype">List</a> <a id="10289" href="/20.07/Lists/#10273" class="Bound">A</a> <a id="10291" class="Symbol">→</a> <a id="10293" href="/20.07/Lists/#1067" class="Datatype">List</a> <a id="10298" href="/20.07/Lists/#10273" class="Bound">A</a> <a id="10300" class="Symbol">→</a> <a id="10302" href="/20.07/Lists/#1067" class="Datatype">List</a> <a id="10307" href="/20.07/Lists/#10273" class="Bound">A</a>
<a id="10309" href="/20.07/Lists/#10262" class="Function">shunt</a> <a id="10315" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a> <a id="10324" href="/20.07/Lists/#10324" class="Bound">ys</a> <a id="10328" class="Symbol">=</a> <a id="10331" href="/20.07/Lists/#10324" class="Bound">ys</a>
<a id="10334" href="/20.07/Lists/#10262" class="Function">shunt</a> <a id="10340" class="Symbol">(</a><a id="10341" href="/20.07/Lists/#10341" class="Bound">x</a> <a id="10343" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="10345" href="/20.07/Lists/#10345" class="Bound">xs</a><a id="10347" class="Symbol">)</a> <a id="10349" href="/20.07/Lists/#10349" class="Bound">ys</a> <a id="10353" class="Symbol">=</a> <a id="10356" href="/20.07/Lists/#10262" class="Function">shunt</a> <a id="10362" href="/20.07/Lists/#10345" class="Bound">xs</a> <a id="10365" class="Symbol">(</a><a id="10366" href="/20.07/Lists/#10341" class="Bound">x</a> <a id="10368" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="10370" href="/20.07/Lists/#10349" class="Bound">ys</a><a id="10372" class="Symbol">)</a>
</pre>
<p>The definition is by recursion on the first argument. The second argument
actually becomes <em>larger</em>, but this is not a problem because the argument
on which we recurse becomes <em>smaller</em>.</p>
<p>Shunt is related to reverse as follows:</p>
<pre class="Agda"><a id="shunt-reverse"></a><a id="10610" href="/20.07/Lists/#10610" class="Function">shunt-reverse</a> <a id="10624" class="Symbol">:</a> <a id="10626" class="Symbol">∀</a> <a id="10628" class="Symbol">{</a><a id="10629" href="/20.07/Lists/#10629" class="Bound">A</a> <a id="10631" class="Symbol">:</a> <a id="10633" class="PrimitiveType">Set</a><a id="10636" class="Symbol">}</a> <a id="10638" class="Symbol">(</a><a id="10639" href="/20.07/Lists/#10639" class="Bound">xs</a> <a id="10642" href="/20.07/Lists/#10642" class="Bound">ys</a> <a id="10645" class="Symbol">:</a> <a id="10647" href="/20.07/Lists/#1067" class="Datatype">List</a> <a id="10652" href="/20.07/Lists/#10629" class="Bound">A</a><a id="10653" class="Symbol">)</a>
<a id="10657" class="Symbol">→</a> <a id="10659" href="/20.07/Lists/#10262" class="Function">shunt</a> <a id="10665" href="/20.07/Lists/#10639" class="Bound">xs</a> <a id="10668" href="/20.07/Lists/#10642" class="Bound">ys</a> <a id="10671" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="10673" href="/20.07/Lists/#8318" class="Function">reverse</a> <a id="10681" href="/20.07/Lists/#10639" class="Bound">xs</a> <a id="10684" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="10687" href="/20.07/Lists/#10642" class="Bound">ys</a>
<a id="10690" href="/20.07/Lists/#10610" class="Function">shunt-reverse</a> <a id="10704" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a> <a id="10707" href="/20.07/Lists/#10707" class="Bound">ys</a> <a id="10710" class="Symbol">=</a>
<a id="10714" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2597" class="Function Operator">begin</a>
<a id="10724" href="/20.07/Lists/#10262" class="Function">shunt</a> <a id="10730" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a> <a id="10733" href="/20.07/Lists/#10707" class="Bound">ys</a>
<a id="10738" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="10746" href="/20.07/Lists/#10707" class="Bound">ys</a>
<a id="10751" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="10759" href="/20.07/Lists/#8318" class="Function">reverse</a> <a id="10767" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a> <a id="10770" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="10773" href="/20.07/Lists/#10707" class="Bound">ys</a>
<a id="10778" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2892" class="Function Operator">∎</a>
<a id="10780" href="/20.07/Lists/#10610" class="Function">shunt-reverse</a> <a id="10794" class="Symbol">(</a><a id="10795" href="/20.07/Lists/#10795" class="Bound">x</a> <a id="10797" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="10799" href="/20.07/Lists/#10799" class="Bound">xs</a><a id="10801" class="Symbol">)</a> <a id="10803" href="/20.07/Lists/#10803" class="Bound">ys</a> <a id="10806" class="Symbol">=</a>
<a id="10810" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2597" class="Function Operator">begin</a>
<a id="10820" href="/20.07/Lists/#10262" class="Function">shunt</a> <a id="10826" class="Symbol">(</a><a id="10827" href="/20.07/Lists/#10795" class="Bound">x</a> <a id="10829" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="10831" href="/20.07/Lists/#10799" class="Bound">xs</a><a id="10833" class="Symbol">)</a> <a id="10835" href="/20.07/Lists/#10803" class="Bound">ys</a>
<a id="10840" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="10848" href="/20.07/Lists/#10262" class="Function">shunt</a> <a id="10854" href="/20.07/Lists/#10799" class="Bound">xs</a> <a id="10857" class="Symbol">(</a><a id="10858" href="/20.07/Lists/#10795" class="Bound">x</a> <a id="10860" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="10862" href="/20.07/Lists/#10803" class="Bound">ys</a><a id="10864" class="Symbol">)</a>
<a id="10868" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">≡⟨</a> <a id="10871" href="/20.07/Lists/#10610" class="Function">shunt-reverse</a> <a id="10885" href="/20.07/Lists/#10799" class="Bound">xs</a> <a id="10888" class="Symbol">(</a><a id="10889" href="/20.07/Lists/#10795" class="Bound">x</a> <a id="10891" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="10893" href="/20.07/Lists/#10803" class="Bound">ys</a><a id="10895" class="Symbol">)</a> <a id="10897" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">⟩</a>
<a id="10903" href="/20.07/Lists/#8318" class="Function">reverse</a> <a id="10911" href="/20.07/Lists/#10799" class="Bound">xs</a> <a id="10914" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="10917" class="Symbol">(</a><a id="10918" href="/20.07/Lists/#10795" class="Bound">x</a> <a id="10920" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="10922" href="/20.07/Lists/#10803" class="Bound">ys</a><a id="10924" class="Symbol">)</a>
<a id="10928" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="10936" href="/20.07/Lists/#8318" class="Function">reverse</a> <a id="10944" href="/20.07/Lists/#10799" class="Bound">xs</a> <a id="10947" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="10950" class="Symbol">(</a><a id="10951" href="/20.07/Lists/#2827" class="InductiveConstructor Operator">[</a> <a id="10953" href="/20.07/Lists/#10795" class="Bound">x</a> <a id="10955" href="/20.07/Lists/#2827" class="InductiveConstructor Operator">]</a> <a id="10957" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="10960" href="/20.07/Lists/#10803" class="Bound">ys</a><a id="10962" class="Symbol">)</a>
<a id="10966" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">≡⟨</a> <a id="10969" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#939" class="Function">sym</a> <a id="10973" class="Symbol">(</a><a id="10974" href="/20.07/Lists/#4528" class="Function">++-assoc</a> <a id="10983" class="Symbol">(</a><a id="10984" href="/20.07/Lists/#8318" class="Function">reverse</a> <a id="10992" href="/20.07/Lists/#10799" class="Bound">xs</a><a id="10994" class="Symbol">)</a> <a id="10996" href="/20.07/Lists/#2827" class="InductiveConstructor Operator">[</a> <a id="10998" href="/20.07/Lists/#10795" class="Bound">x</a> <a id="11000" href="/20.07/Lists/#2827" class="InductiveConstructor Operator">]</a> <a id="11002" href="/20.07/Lists/#10803" class="Bound">ys</a><a id="11004" class="Symbol">)</a> <a id="11006" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">⟩</a>
<a id="11012" class="Symbol">(</a><a id="11013" href="/20.07/Lists/#8318" class="Function">reverse</a> <a id="11021" href="/20.07/Lists/#10799" class="Bound">xs</a> <a id="11024" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="11027" href="/20.07/Lists/#2827" class="InductiveConstructor Operator">[</a> <a id="11029" href="/20.07/Lists/#10795" class="Bound">x</a> <a id="11031" href="/20.07/Lists/#2827" class="InductiveConstructor Operator">]</a><a id="11032" class="Symbol">)</a> <a id="11034" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="11037" href="/20.07/Lists/#10803" class="Bound">ys</a>
<a id="11042" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="11050" href="/20.07/Lists/#8318" class="Function">reverse</a> <a id="11058" class="Symbol">(</a><a id="11059" href="/20.07/Lists/#10795" class="Bound">x</a> <a id="11061" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="11063" href="/20.07/Lists/#10799" class="Bound">xs</a><a id="11065" class="Symbol">)</a> <a id="11067" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="11070" href="/20.07/Lists/#10803" class="Bound">ys</a>
<a id="11075" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2892" class="Function Operator">∎</a>
</pre>
<p>The proof is by induction on the first argument.
The base case instantiates to <code class="language-plaintext highlighter-rouge">[]</code>, and follows by straightforward computation.
The inductive case instantiates to <code class="language-plaintext highlighter-rouge">x ∷ xs</code> and follows by the inductive
hypothesis and associativity of append. When we invoke the inductive hypothesis,
the second argument actually becomes <em>larger</em>, but this is not a problem because
the argument on which we induct becomes <em>smaller</em>.</p>
<p>Generalising on an auxiliary argument, which becomes larger as the argument on
which we recurse or induct becomes smaller, is a common trick. It belongs in
your quiver of arrows, ready to slay the right problem.</p>
<p>Having defined shunt be generalisation, it is now easy to respecialise to
give a more efficient definition of reverse:</p>
<pre class="Agda"><a id="reverse′"></a><a id="11834" href="/20.07/Lists/#11834" class="Function">reverse′</a> <a id="11843" class="Symbol">:</a> <a id="11845" class="Symbol">∀</a> <a id="11847" class="Symbol">{</a><a id="11848" href="/20.07/Lists/#11848" class="Bound">A</a> <a id="11850" class="Symbol">:</a> <a id="11852" class="PrimitiveType">Set</a><a id="11855" class="Symbol">}</a> <a id="11857" class="Symbol">→</a> <a id="11859" href="/20.07/Lists/#1067" class="Datatype">List</a> <a id="11864" href="/20.07/Lists/#11848" class="Bound">A</a> <a id="11866" class="Symbol">→</a> <a id="11868" href="/20.07/Lists/#1067" class="Datatype">List</a> <a id="11873" href="/20.07/Lists/#11848" class="Bound">A</a>
<a id="11875" href="/20.07/Lists/#11834" class="Function">reverse′</a> <a id="11884" href="/20.07/Lists/#11884" class="Bound">xs</a> <a id="11887" class="Symbol">=</a> <a id="11889" href="/20.07/Lists/#10262" class="Function">shunt</a> <a id="11895" href="/20.07/Lists/#11884" class="Bound">xs</a> <a id="11898" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a>
</pre>
<p>Given our previous lemma, it is straightforward to show
the two definitions equivalent:</p>
<pre class="Agda"><a id="reverses"></a><a id="11998" href="/20.07/Lists/#11998" class="Function">reverses</a> <a id="12007" class="Symbol">:</a> <a id="12009" class="Symbol">∀</a> <a id="12011" class="Symbol">{</a><a id="12012" href="/20.07/Lists/#12012" class="Bound">A</a> <a id="12014" class="Symbol">:</a> <a id="12016" class="PrimitiveType">Set</a><a id="12019" class="Symbol">}</a> <a id="12021" class="Symbol">(</a><a id="12022" href="/20.07/Lists/#12022" class="Bound">xs</a> <a id="12025" class="Symbol">:</a> <a id="12027" href="/20.07/Lists/#1067" class="Datatype">List</a> <a id="12032" href="/20.07/Lists/#12012" class="Bound">A</a><a id="12033" class="Symbol">)</a>
<a id="12037" class="Symbol">→</a> <a id="12039" href="/20.07/Lists/#11834" class="Function">reverse′</a> <a id="12048" href="/20.07/Lists/#12022" class="Bound">xs</a> <a id="12051" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="12053" href="/20.07/Lists/#8318" class="Function">reverse</a> <a id="12061" href="/20.07/Lists/#12022" class="Bound">xs</a>
<a id="12064" href="/20.07/Lists/#11998" class="Function">reverses</a> <a id="12073" href="/20.07/Lists/#12073" class="Bound">xs</a> <a id="12076" class="Symbol">=</a>
<a id="12080" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2597" class="Function Operator">begin</a>
<a id="12090" href="/20.07/Lists/#11834" class="Function">reverse′</a> <a id="12099" href="/20.07/Lists/#12073" class="Bound">xs</a>
<a id="12104" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="12112" href="/20.07/Lists/#10262" class="Function">shunt</a> <a id="12118" href="/20.07/Lists/#12073" class="Bound">xs</a> <a id="12121" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a>
<a id="12126" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">≡⟨</a> <a id="12129" href="/20.07/Lists/#10610" class="Function">shunt-reverse</a> <a id="12143" href="/20.07/Lists/#12073" class="Bound">xs</a> <a id="12146" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a> <a id="12149" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">⟩</a>
<a id="12155" href="/20.07/Lists/#8318" class="Function">reverse</a> <a id="12163" href="/20.07/Lists/#12073" class="Bound">xs</a> <a id="12166" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="12169" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a>
<a id="12174" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">≡⟨</a> <a id="12177" href="/20.07/Lists/#5917" class="Function">++-identityʳ</a> <a id="12190" class="Symbol">(</a><a id="12191" href="/20.07/Lists/#8318" class="Function">reverse</a> <a id="12199" href="/20.07/Lists/#12073" class="Bound">xs</a><a id="12201" class="Symbol">)</a> <a id="12203" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">⟩</a>
<a id="12209" href="/20.07/Lists/#8318" class="Function">reverse</a> <a id="12217" href="/20.07/Lists/#12073" class="Bound">xs</a>
<a id="12222" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2892" class="Function Operator">∎</a>
</pre>
<p>Here is an example showing fast reverse of the list <code class="language-plaintext highlighter-rouge">[ 0 , 1 , 2 ]</code>:</p>
<pre class="Agda"><a id="12302" href="/20.07/Lists/#12302" class="Function">_</a> <a id="12304" class="Symbol">:</a> <a id="12306" href="/20.07/Lists/#11834" class="Function">reverse′</a> <a id="12315" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">[</a> <a id="12317" class="Number">0</a> <a id="12319" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">,</a> <a id="12321" class="Number">1</a> <a id="12323" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">,</a> <a id="12325" class="Number">2</a> <a id="12327" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">]</a> <a id="12329" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="12331" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">[</a> <a id="12333" class="Number">2</a> <a id="12335" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">,</a> <a id="12337" class="Number">1</a> <a id="12339" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">,</a> <a id="12341" class="Number">0</a> <a id="12343" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">]</a>
<a id="12345" class="Symbol">_</a> <a id="12347" class="Symbol">=</a>
<a id="12351" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2597" class="Function Operator">begin</a>
<a id="12361" href="/20.07/Lists/#11834" class="Function">reverse′</a> <a id="12370" class="Symbol">(</a><a id="12371" class="Number">0</a> <a id="12373" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="12375" class="Number">1</a> <a id="12377" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="12379" class="Number">2</a> <a id="12381" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="12383" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a><a id="12385" class="Symbol">)</a>
<a id="12389" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="12397" href="/20.07/Lists/#10262" class="Function">shunt</a> <a id="12403" class="Symbol">(</a><a id="12404" class="Number">0</a> <a id="12406" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="12408" class="Number">1</a> <a id="12410" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="12412" class="Number">2</a> <a id="12414" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="12416" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a><a id="12418" class="Symbol">)</a> <a id="12420" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a>
<a id="12425" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="12433" href="/20.07/Lists/#10262" class="Function">shunt</a> <a id="12439" class="Symbol">(</a><a id="12440" class="Number">1</a> <a id="12442" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="12444" class="Number">2</a> <a id="12446" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="12448" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a><a id="12450" class="Symbol">)</a> <a id="12452" class="Symbol">(</a><a id="12453" class="Number">0</a> <a id="12455" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="12457" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a><a id="12459" class="Symbol">)</a>
<a id="12463" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="12471" href="/20.07/Lists/#10262" class="Function">shunt</a> <a id="12477" class="Symbol">(</a><a id="12478" class="Number">2</a> <a id="12480" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="12482" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a><a id="12484" class="Symbol">)</a> <a id="12486" class="Symbol">(</a><a id="12487" class="Number">1</a> <a id="12489" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="12491" class="Number">0</a> <a id="12493" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="12495" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a><a id="12497" class="Symbol">)</a>
<a id="12501" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="12509" href="/20.07/Lists/#10262" class="Function">shunt</a> <a id="12515" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a> <a id="12518" class="Symbol">(</a><a id="12519" class="Number">2</a> <a id="12521" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="12523" class="Number">1</a> <a id="12525" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="12527" class="Number">0</a> <a id="12529" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="12531" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a><a id="12533" class="Symbol">)</a>
<a id="12537" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="12545" class="Number">2</a> <a id="12547" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="12549" class="Number">1</a> <a id="12551" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="12553" class="Number">0</a> <a id="12555" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="12557" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a>
<a id="12562" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2892" class="Function Operator">∎</a>
</pre>
<p>Now the time to reverse a list is linear in the length of the list.</p>
<h2 id="Map">Map</h2>
<p>Map applies a function to every element of a list to generate a corresponding list.
Map is an example of a <em>higher-order function</em>, one which takes a function as an
argument or returns a function as a result:</p>
<pre class="Agda"><a id="map"></a><a id="12865" href="/20.07/Lists/#12865" class="Function">map</a> <a id="12869" class="Symbol">:</a> <a id="12871" class="Symbol">∀</a> <a id="12873" class="Symbol">{</a><a id="12874" href="/20.07/Lists/#12874" class="Bound">A</a> <a id="12876" href="/20.07/Lists/#12876" class="Bound">B</a> <a id="12878" class="Symbol">:</a> <a id="12880" class="PrimitiveType">Set</a><a id="12883" class="Symbol">}</a> <a id="12885" class="Symbol">→</a> <a id="12887" class="Symbol">(</a><a id="12888" href="/20.07/Lists/#12874" class="Bound">A</a> <a id="12890" class="Symbol">→</a> <a id="12892" href="/20.07/Lists/#12876" class="Bound">B</a><a id="12893" class="Symbol">)</a> <a id="12895" class="Symbol">→</a> <a id="12897" href="/20.07/Lists/#1067" class="Datatype">List</a> <a id="12902" href="/20.07/Lists/#12874" class="Bound">A</a> <a id="12904" class="Symbol">→</a> <a id="12906" href="/20.07/Lists/#1067" class="Datatype">List</a> <a id="12911" href="/20.07/Lists/#12876" class="Bound">B</a>
<a id="12913" href="/20.07/Lists/#12865" class="Function">map</a> <a id="12917" href="/20.07/Lists/#12917" class="Bound">f</a> <a id="12919" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a> <a id="12929" class="Symbol">=</a> <a id="12932" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a>
<a id="12935" href="/20.07/Lists/#12865" class="Function">map</a> <a id="12939" href="/20.07/Lists/#12939" class="Bound">f</a> <a id="12941" class="Symbol">(</a><a id="12942" href="/20.07/Lists/#12942" class="Bound">x</a> <a id="12944" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="12946" href="/20.07/Lists/#12946" class="Bound">xs</a><a id="12948" class="Symbol">)</a> <a id="12951" class="Symbol">=</a> <a id="12954" href="/20.07/Lists/#12939" class="Bound">f</a> <a id="12956" href="/20.07/Lists/#12942" class="Bound">x</a> <a id="12958" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="12960" href="/20.07/Lists/#12865" class="Function">map</a> <a id="12964" href="/20.07/Lists/#12939" class="Bound">f</a> <a id="12966" href="/20.07/Lists/#12946" class="Bound">xs</a>
</pre>
<p>Map of the empty list is the empty list.
Map of a non-empty list yields a list
with head the same as the function applied to the head of the given list,
and tail the same as map of the function applied to the tail of the given list.</p>
<p>Here is an example showing how to use map to increment every element of a list:</p>
<pre class="Agda"><a id="13291" href="/20.07/Lists/#13291" class="Function">_</a> <a id="13293" class="Symbol">:</a> <a id="13295" href="/20.07/Lists/#12865" class="Function">map</a> <a id="13299" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="13303" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">[</a> <a id="13305" class="Number">0</a> <a id="13307" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">,</a> <a id="13309" class="Number">1</a> <a id="13311" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">,</a> <a id="13313" class="Number">2</a> <a id="13315" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">]</a> <a id="13317" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="13319" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">[</a> <a id="13321" class="Number">1</a> <a id="13323" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">,</a> <a id="13325" class="Number">2</a> <a id="13327" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">,</a> <a id="13329" class="Number">3</a> <a id="13331" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">]</a>
<a id="13333" class="Symbol">_</a> <a id="13335" class="Symbol">=</a>
<a id="13339" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2597" class="Function Operator">begin</a>
<a id="13349" href="/20.07/Lists/#12865" class="Function">map</a> <a id="13353" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="13357" class="Symbol">(</a><a id="13358" class="Number">0</a> <a id="13360" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="13362" class="Number">1</a> <a id="13364" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="13366" class="Number">2</a> <a id="13368" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="13370" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a><a id="13372" class="Symbol">)</a>
<a id="13376" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="13384" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="13388" class="Number">0</a> <a id="13390" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="13392" href="/20.07/Lists/#12865" class="Function">map</a> <a id="13396" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="13400" class="Symbol">(</a><a id="13401" class="Number">1</a> <a id="13403" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="13405" class="Number">2</a> <a id="13407" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="13409" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a><a id="13411" class="Symbol">)</a>
<a id="13415" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="13423" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="13427" class="Number">0</a> <a id="13429" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="13431" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="13435" class="Number">1</a> <a id="13437" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="13439" href="/20.07/Lists/#12865" class="Function">map</a> <a id="13443" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="13447" class="Symbol">(</a><a id="13448" class="Number">2</a> <a id="13450" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="13452" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a><a id="13454" class="Symbol">)</a>
<a id="13458" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="13466" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="13470" class="Number">0</a> <a id="13472" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="13474" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="13478" class="Number">1</a> <a id="13480" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="13482" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="13486" class="Number">2</a> <a id="13488" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="13490" href="/20.07/Lists/#12865" class="Function">map</a> <a id="13494" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="13498" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a>
<a id="13503" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="13511" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="13515" class="Number">0</a> <a id="13517" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="13519" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="13523" class="Number">1</a> <a id="13525" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="13527" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="13531" class="Number">2</a> <a id="13533" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="13535" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a>
<a id="13540" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="13548" class="Number">1</a> <a id="13550" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="13552" class="Number">2</a> <a id="13554" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="13556" class="Number">3</a> <a id="13558" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="13560" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a>
<a id="13565" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2892" class="Function Operator">∎</a>
</pre>
<p>Map requires time linear in the length of the list.</p>
<p>It is often convenient to exploit currying by applying
map to a function to yield a new function, and at a later
point applying the resulting function:</p>
<pre class="Agda"><a id="sucs"></a><a id="13780" href="/20.07/Lists/#13780" class="Function">sucs</a> <a id="13785" class="Symbol">:</a> <a id="13787" href="/20.07/Lists/#1067" class="Datatype">List</a> <a id="13792" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a> <a id="13794" class="Symbol">→</a> <a id="13796" href="/20.07/Lists/#1067" class="Datatype">List</a> <a id="13801" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a>
<a id="13803" href="/20.07/Lists/#13780" class="Function">sucs</a> <a id="13808" class="Symbol">=</a> <a id="13810" href="/20.07/Lists/#12865" class="Function">map</a> <a id="13814" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a>
<a id="13819" href="/20.07/Lists/#13819" class="Function">_</a> <a id="13821" class="Symbol">:</a> <a id="13823" href="/20.07/Lists/#13780" class="Function">sucs</a> <a id="13828" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">[</a> <a id="13830" class="Number">0</a> <a id="13832" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">,</a> <a id="13834" class="Number">1</a> <a id="13836" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">,</a> <a id="13838" class="Number">2</a> <a id="13840" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">]</a> <a id="13842" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="13844" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">[</a> <a id="13846" class="Number">1</a> <a id="13848" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">,</a> <a id="13850" class="Number">2</a> <a id="13852" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">,</a> <a id="13854" class="Number">3</a> <a id="13856" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">]</a>
<a id="13858" class="Symbol">_</a> <a id="13860" class="Symbol">=</a>
<a id="13864" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2597" class="Function Operator">begin</a>
<a id="13874" href="/20.07/Lists/#13780" class="Function">sucs</a> <a id="13879" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">[</a> <a id="13881" class="Number">0</a> <a id="13883" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">,</a> <a id="13885" class="Number">1</a> <a id="13887" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">,</a> <a id="13889" class="Number">2</a> <a id="13891" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">]</a>
<a id="13895" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="13903" href="/20.07/Lists/#12865" class="Function">map</a> <a id="13907" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="13911" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">[</a> <a id="13913" class="Number">0</a> <a id="13915" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">,</a> <a id="13917" class="Number">1</a> <a id="13919" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">,</a> <a id="13921" class="Number">2</a> <a id="13923" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">]</a>
<a id="13927" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="13935" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">[</a> <a id="13937" class="Number">1</a> <a id="13939" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">,</a> <a id="13941" class="Number">2</a> <a id="13943" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">,</a> <a id="13945" class="Number">3</a> <a id="13947" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">]</a>
<a id="13951" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2892" class="Function Operator">∎</a>
</pre>
<p>Any type that is parameterised on another type, such as lists, has a
corresponding map, which accepts a function and returns a function
from the type parameterised on the domain of the function to the type
parameterised on the range of the function. Further, a type that is
parameterised on <em>n</em> types will have a map that is parameterised on
<em>n</em> functions.</p>
<h4 id="exercise-map-compose-practice">Exercise <code class="language-plaintext highlighter-rouge">map-compose</code> (practice)</h4>
<p>Prove that the map of a composition is equal to the composition of two maps:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>map (g ∘ f) ≡ map g ∘ map f
</code></pre></div></div>
<p>The last step of the proof requires extensionality.</p>
<pre class="Agda"><a id="14525" class="Comment">-- Your code goes here</a>
</pre>
<h4 id="exercise-map--distribute-practice">Exercise <code class="language-plaintext highlighter-rouge">map-++-distribute</code> (practice)</h4>
<p>Prove the following relationship between map and append:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>map f (xs ++ ys) ≡ map f xs ++ map f ys
</code></pre></div></div>
<pre class="Agda"><a id="14706" class="Comment">-- Your code goes here</a>
</pre>
<h4 id="exercise-map-tree-practice">Exercise <code class="language-plaintext highlighter-rouge">map-Tree</code> (practice)</h4>
<p>Define a type of trees with leaves of type <code class="language-plaintext highlighter-rouge">A</code> and internal
nodes of type <code class="language-plaintext highlighter-rouge">B</code>:</p>
<pre class="Agda"><a id="14854" class="Keyword">data</a> <a id="Tree"></a><a id="14859" href="/20.07/Lists/#14859" class="Datatype">Tree</a> <a id="14864" class="Symbol">(</a><a id="14865" href="/20.07/Lists/#14865" class="Bound">A</a> <a id="14867" href="/20.07/Lists/#14867" class="Bound">B</a> <a id="14869" class="Symbol">:</a> <a id="14871" class="PrimitiveType">Set</a><a id="14874" class="Symbol">)</a> <a id="14876" class="Symbol">:</a> <a id="14878" class="PrimitiveType">Set</a> <a id="14882" class="Keyword">where</a>
<a id="Tree.leaf"></a><a id="14890" href="/20.07/Lists/#14890" class="InductiveConstructor">leaf</a> <a id="14895" class="Symbol">:</a> <a id="14897" href="/20.07/Lists/#14865" class="Bound">A</a> <a id="14899" class="Symbol">→</a> <a id="14901" href="/20.07/Lists/#14859" class="Datatype">Tree</a> <a id="14906" href="/20.07/Lists/#14865" class="Bound">A</a> <a id="14908" href="/20.07/Lists/#14867" class="Bound">B</a>
<a id="Tree.node"></a><a id="14912" href="/20.07/Lists/#14912" class="InductiveConstructor">node</a> <a id="14917" class="Symbol">:</a> <a id="14919" href="/20.07/Lists/#14859" class="Datatype">Tree</a> <a id="14924" href="/20.07/Lists/#14865" class="Bound">A</a> <a id="14926" href="/20.07/Lists/#14867" class="Bound">B</a> <a id="14928" class="Symbol">→</a> <a id="14930" href="/20.07/Lists/#14867" class="Bound">B</a> <a id="14932" class="Symbol">→</a> <a id="14934" href="/20.07/Lists/#14859" class="Datatype">Tree</a> <a id="14939" href="/20.07/Lists/#14865" class="Bound">A</a> <a id="14941" href="/20.07/Lists/#14867" class="Bound">B</a> <a id="14943" class="Symbol">→</a> <a id="14945" href="/20.07/Lists/#14859" class="Datatype">Tree</a> <a id="14950" href="/20.07/Lists/#14865" class="Bound">A</a> <a id="14952" href="/20.07/Lists/#14867" class="Bound">B</a>
</pre>
<p>Define a suitable map operator over trees:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>map-Tree : ∀ {A B C D : Set} → (A → C) → (B → D) → Tree A B → Tree C D
</code></pre></div></div>
<pre class="Agda"><a id="15082" class="Comment">-- Your code goes here</a>
</pre>
<h2 id="Fold">Fold</h2>
<p>Fold takes an operator and a value, and uses the operator to combine
each of the elements of the list, taking the given value as the result
for the empty list:</p>
<pre class="Agda"><a id="foldr"></a><a id="15291" href="/20.07/Lists/#15291" class="Function">foldr</a> <a id="15297" class="Symbol">:</a> <a id="15299" class="Symbol">∀</a> <a id="15301" class="Symbol">{</a><a id="15302" href="/20.07/Lists/#15302" class="Bound">A</a> <a id="15304" href="/20.07/Lists/#15304" class="Bound">B</a> <a id="15306" class="Symbol">:</a> <a id="15308" class="PrimitiveType">Set</a><a id="15311" class="Symbol">}</a> <a id="15313" class="Symbol">→</a> <a id="15315" class="Symbol">(</a><a id="15316" href="/20.07/Lists/#15302" class="Bound">A</a> <a id="15318" class="Symbol">→</a> <a id="15320" href="/20.07/Lists/#15304" class="Bound">B</a> <a id="15322" class="Symbol">→</a> <a id="15324" href="/20.07/Lists/#15304" class="Bound">B</a><a id="15325" class="Symbol">)</a> <a id="15327" class="Symbol">→</a> <a id="15329" href="/20.07/Lists/#15304" class="Bound">B</a> <a id="15331" class="Symbol">→</a> <a id="15333" href="/20.07/Lists/#1067" class="Datatype">List</a> <a id="15338" href="/20.07/Lists/#15302" class="Bound">A</a> <a id="15340" class="Symbol">→</a> <a id="15342" href="/20.07/Lists/#15304" class="Bound">B</a>
<a id="15344" href="/20.07/Lists/#15291" class="Function">foldr</a> <a id="15350" href="/20.07/Lists/#15350" class="Bound Operator">_⊗_</a> <a id="15354" href="/20.07/Lists/#15354" class="Bound">e</a> <a id="15356" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a> <a id="15366" class="Symbol">=</a> <a id="15369" href="/20.07/Lists/#15354" class="Bound">e</a>
<a id="15371" href="/20.07/Lists/#15291" class="Function">foldr</a> <a id="15377" href="/20.07/Lists/#15377" class="Bound Operator">_⊗_</a> <a id="15381" href="/20.07/Lists/#15381" class="Bound">e</a> <a id="15383" class="Symbol">(</a><a id="15384" href="/20.07/Lists/#15384" class="Bound">x</a> <a id="15386" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="15388" href="/20.07/Lists/#15388" class="Bound">xs</a><a id="15390" class="Symbol">)</a> <a id="15393" class="Symbol">=</a> <a id="15396" href="/20.07/Lists/#15384" class="Bound">x</a> <a id="15398" href="/20.07/Lists/#15377" class="Bound Operator">⊗</a> <a id="15400" href="/20.07/Lists/#15291" class="Function">foldr</a> <a id="15406" href="/20.07/Lists/#15377" class="Bound Operator">_⊗_</a> <a id="15410" href="/20.07/Lists/#15381" class="Bound">e</a> <a id="15412" href="/20.07/Lists/#15388" class="Bound">xs</a>
</pre>
<p>Fold of the empty list is the given value.
Fold of a non-empty list uses the operator to combine
the head of the list and the fold of the tail of the list.</p>
<p>Here is an example showing how to use fold to find the sum of a list:</p>
<pre class="Agda"><a id="15650" href="/20.07/Lists/#15650" class="Function">_</a> <a id="15652" class="Symbol">:</a> <a id="15654" href="/20.07/Lists/#15291" class="Function">foldr</a> <a id="15660" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">_+_</a> <a id="15664" class="Number">0</a> <a id="15666" href="/20.07/Lists/#2920" class="InductiveConstructor Operator">[</a> <a id="15668" class="Number">1</a> <a id="15670" href="/20.07/Lists/#2920" class="InductiveConstructor Operator">,</a> <a id="15672" class="Number">2</a> <a id="15674" href="/20.07/Lists/#2920" class="InductiveConstructor Operator">,</a> <a id="15676" class="Number">3</a> <a id="15678" href="/20.07/Lists/#2920" class="InductiveConstructor Operator">,</a> <a id="15680" class="Number">4</a> <a id="15682" href="/20.07/Lists/#2920" class="InductiveConstructor Operator">]</a> <a id="15684" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="15686" class="Number">10</a>
<a id="15689" class="Symbol">_</a> <a id="15691" class="Symbol">=</a>
<a id="15695" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2597" class="Function Operator">begin</a>
<a id="15705" href="/20.07/Lists/#15291" class="Function">foldr</a> <a id="15711" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">_+_</a> <a id="15715" class="Number">0</a> <a id="15717" class="Symbol">(</a><a id="15718" class="Number">1</a> <a id="15720" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="15722" class="Number">2</a> <a id="15724" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="15726" class="Number">3</a> <a id="15728" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="15730" class="Number">4</a> <a id="15732" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="15734" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a><a id="15736" class="Symbol">)</a>
<a id="15740" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="15748" class="Number">1</a> <a id="15750" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="15752" href="/20.07/Lists/#15291" class="Function">foldr</a> <a id="15758" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">_+_</a> <a id="15762" class="Number">0</a> <a id="15764" class="Symbol">(</a><a id="15765" class="Number">2</a> <a id="15767" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="15769" class="Number">3</a> <a id="15771" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="15773" class="Number">4</a> <a id="15775" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="15777" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a><a id="15779" class="Symbol">)</a>
<a id="15783" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="15791" class="Number">1</a> <a id="15793" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="15795" class="Symbol">(</a><a id="15796" class="Number">2</a> <a id="15798" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="15800" href="/20.07/Lists/#15291" class="Function">foldr</a> <a id="15806" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">_+_</a> <a id="15810" class="Number">0</a> <a id="15812" class="Symbol">(</a><a id="15813" class="Number">3</a> <a id="15815" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="15817" class="Number">4</a> <a id="15819" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="15821" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a><a id="15823" class="Symbol">))</a>
<a id="15828" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="15836" class="Number">1</a> <a id="15838" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="15840" class="Symbol">(</a><a id="15841" class="Number">2</a> <a id="15843" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="15845" class="Symbol">(</a><a id="15846" class="Number">3</a> <a id="15848" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="15850" href="/20.07/Lists/#15291" class="Function">foldr</a> <a id="15856" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">_+_</a> <a id="15860" class="Number">0</a> <a id="15862" class="Symbol">(</a><a id="15863" class="Number">4</a> <a id="15865" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="15867" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a><a id="15869" class="Symbol">)))</a>
<a id="15875" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="15883" class="Number">1</a> <a id="15885" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="15887" class="Symbol">(</a><a id="15888" class="Number">2</a> <a id="15890" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="15892" class="Symbol">(</a><a id="15893" class="Number">3</a> <a id="15895" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="15897" class="Symbol">(</a><a id="15898" class="Number">4</a> <a id="15900" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="15902" href="/20.07/Lists/#15291" class="Function">foldr</a> <a id="15908" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">_+_</a> <a id="15912" class="Number">0</a> <a id="15914" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a><a id="15916" class="Symbol">)))</a>
<a id="15922" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="15930" class="Number">1</a> <a id="15932" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="15934" class="Symbol">(</a><a id="15935" class="Number">2</a> <a id="15937" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="15939" class="Symbol">(</a><a id="15940" class="Number">3</a> <a id="15942" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="15944" class="Symbol">(</a><a id="15945" class="Number">4</a> <a id="15947" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">+</a> <a id="15949" class="Number">0</a><a id="15950" class="Symbol">)))</a>
<a id="15956" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2892" class="Function Operator">∎</a>
</pre>
<p>Here we have an instance of <code class="language-plaintext highlighter-rouge">foldr</code> where <code class="language-plaintext highlighter-rouge">A</code> and <code class="language-plaintext highlighter-rouge">B</code> are both <code class="language-plaintext highlighter-rouge">ℕ</code>.
Fold requires time linear in the length of the list.</p>
<p>It is often convenient to exploit currying by applying
fold to an operator and a value to yield a new function,
and at a later point applying the resulting function:</p>
<pre class="Agda"><a id="sum"></a><a id="16254" href="/20.07/Lists/#16254" class="Function">sum</a> <a id="16258" class="Symbol">:</a> <a id="16260" href="/20.07/Lists/#1067" class="Datatype">List</a> <a id="16265" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a> <a id="16267" class="Symbol">→</a> <a id="16269" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a>
<a id="16271" href="/20.07/Lists/#16254" class="Function">sum</a> <a id="16275" class="Symbol">=</a> <a id="16277" href="/20.07/Lists/#15291" class="Function">foldr</a> <a id="16283" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">_+_</a> <a id="16287" class="Number">0</a>
<a id="16290" href="/20.07/Lists/#16290" class="Function">_</a> <a id="16292" class="Symbol">:</a> <a id="16294" href="/20.07/Lists/#16254" class="Function">sum</a> <a id="16298" href="/20.07/Lists/#2920" class="InductiveConstructor Operator">[</a> <a id="16300" class="Number">1</a> <a id="16302" href="/20.07/Lists/#2920" class="InductiveConstructor Operator">,</a> <a id="16304" class="Number">2</a> <a id="16306" href="/20.07/Lists/#2920" class="InductiveConstructor Operator">,</a> <a id="16308" class="Number">3</a> <a id="16310" href="/20.07/Lists/#2920" class="InductiveConstructor Operator">,</a> <a id="16312" class="Number">4</a> <a id="16314" href="/20.07/Lists/#2920" class="InductiveConstructor Operator">]</a> <a id="16316" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="16318" class="Number">10</a>
<a id="16321" class="Symbol">_</a> <a id="16323" class="Symbol">=</a>
<a id="16327" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2597" class="Function Operator">begin</a>
<a id="16337" href="/20.07/Lists/#16254" class="Function">sum</a> <a id="16341" href="/20.07/Lists/#2920" class="InductiveConstructor Operator">[</a> <a id="16343" class="Number">1</a> <a id="16345" href="/20.07/Lists/#2920" class="InductiveConstructor Operator">,</a> <a id="16347" class="Number">2</a> <a id="16349" href="/20.07/Lists/#2920" class="InductiveConstructor Operator">,</a> <a id="16351" class="Number">3</a> <a id="16353" href="/20.07/Lists/#2920" class="InductiveConstructor Operator">,</a> <a id="16355" class="Number">4</a> <a id="16357" href="/20.07/Lists/#2920" class="InductiveConstructor Operator">]</a>
<a id="16361" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="16369" href="/20.07/Lists/#15291" class="Function">foldr</a> <a id="16375" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">_+_</a> <a id="16379" class="Number">0</a> <a id="16381" href="/20.07/Lists/#2920" class="InductiveConstructor Operator">[</a> <a id="16383" class="Number">1</a> <a id="16385" href="/20.07/Lists/#2920" class="InductiveConstructor Operator">,</a> <a id="16387" class="Number">2</a> <a id="16389" href="/20.07/Lists/#2920" class="InductiveConstructor Operator">,</a> <a id="16391" class="Number">3</a> <a id="16393" href="/20.07/Lists/#2920" class="InductiveConstructor Operator">,</a> <a id="16395" class="Number">4</a> <a id="16397" href="/20.07/Lists/#2920" class="InductiveConstructor Operator">]</a>
<a id="16401" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="16409" class="Number">10</a>
<a id="16414" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2892" class="Function Operator">∎</a>
</pre>
<p>Just as the list type has two constructors, <code class="language-plaintext highlighter-rouge">[]</code> and <code class="language-plaintext highlighter-rouge">_∷_</code>,
so the fold function takes two arguments, <code class="language-plaintext highlighter-rouge">e</code> and <code class="language-plaintext highlighter-rouge">_⊗_</code>
(in addition to the list argument).
In general, a data type with <em>n</em> constructors will have
a corresponding fold function that takes <em>n</em> arguments.</p>
<p>As another example, observe that</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>foldr _∷_ [] xs ≡ xs
</code></pre></div></div>
<p>Here, if <code class="language-plaintext highlighter-rouge">xs</code> is of type <code class="language-plaintext highlighter-rouge">List A</code>, then we see we have an instance of
<code class="language-plaintext highlighter-rouge">foldr</code> where <code class="language-plaintext highlighter-rouge">A</code> is <code class="language-plaintext highlighter-rouge">A</code> and <code class="language-plaintext highlighter-rouge">B</code> is <code class="language-plaintext highlighter-rouge">List A</code>. It follows that</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>xs ++ ys ≡ foldr _∷_ ys xs
</code></pre></div></div>
<p>Demonstrating both these equations is left as an exercise.</p>
<h4 id="exercise-product-recommended">Exercise <code class="language-plaintext highlighter-rouge">product</code> (recommended)</h4>
<p>Use fold to define a function to find the product of a list of numbers.
For example:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>product [ 1 , 2 , 3 , 4 ] ≡ 24
</code></pre></div></div>
<pre class="Agda"><a id="17138" class="Comment">-- Your code goes here</a>
</pre>
<h4 id="exercise-foldr--recommended">Exercise <code class="language-plaintext highlighter-rouge">foldr-++</code> (recommended)</h4>
<p>Show that fold and append are related as follows:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>foldr _⊗_ e (xs ++ ys) ≡ foldr _⊗_ (foldr _⊗_ e ys) xs
</code></pre></div></div>
<pre class="Agda"><a id="17321" class="Comment">-- Your code goes here</a>
</pre>
<h4 id="exercise-foldr--practice">Exercise <code class="language-plaintext highlighter-rouge">foldr-∷</code> (practice)</h4>
<p>Show</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>foldr _∷_ [] xs ≡ xs
</code></pre></div></div>
<p>Show as a consequence of <code class="language-plaintext highlighter-rouge">foldr-++</code> above that</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>xs ++ ys ≡ foldr _∷_ ys xs
</code></pre></div></div>
<pre class="Agda"><a id="17502" class="Comment">-- Your code goes here</a>
</pre>
<h4 id="exercise-map-is-foldr-practice">Exercise <code class="language-plaintext highlighter-rouge">map-is-foldr</code> (practice)</h4>
<p>Show that map can be defined using fold:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>map f ≡ foldr (λ x xs → f x ∷ xs) []
</code></pre></div></div>
<p>The proof requires extensionality.</p>
<pre class="Agda"><a id="17695" class="Comment">-- Your code goes here</a>
</pre>
<h4 id="exercise-fold-tree-practice">Exercise <code class="language-plaintext highlighter-rouge">fold-Tree</code> (practice)</h4>
<p>Define a suitable fold function for the type of trees given earlier:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>fold-Tree : ∀ {A B C : Set} → (A → C) → (C → B → C → C) → Tree A B → C
</code></pre></div></div>
<pre class="Agda"><a id="17912" class="Comment">-- Your code goes here</a>
</pre>
<h4 id="exercise-map-is-fold-tree-practice">Exercise <code class="language-plaintext highlighter-rouge">map-is-fold-Tree</code> (practice)</h4>
<p>Demonstrate an analogue of <code class="language-plaintext highlighter-rouge">map-is-foldr</code> for the type of trees.</p>
<pre class="Agda"><a id="18055" class="Comment">-- Your code goes here</a>
</pre>
<h4 id="exercise-sum-downfrom-stretch">Exercise <code class="language-plaintext highlighter-rouge">sum-downFrom</code> (stretch)</h4>
<p>Define a function that counts down as follows:</p>
<pre class="Agda"><a id="downFrom"></a><a id="18174" href="/20.07/Lists/#18174" class="Function">downFrom</a> <a id="18183" class="Symbol">:</a> <a id="18185" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a> <a id="18187" class="Symbol">→</a> <a id="18189" href="/20.07/Lists/#1067" class="Datatype">List</a> <a id="18194" href="Agda.Builtin.Nat.html#165" class="Datatype">ℕ</a>
<a id="18196" href="/20.07/Lists/#18174" class="Function">downFrom</a> <a id="18205" href="Agda.Builtin.Nat.html#183" class="InductiveConstructor">zero</a> <a id="18214" class="Symbol">=</a> <a id="18217" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a>
<a id="18220" href="/20.07/Lists/#18174" class="Function">downFrom</a> <a id="18229" class="Symbol">(</a><a id="18230" href="Agda.Builtin.Nat.html#196" class="InductiveConstructor">suc</a> <a id="18234" href="/20.07/Lists/#18234" class="Bound">n</a><a id="18235" class="Symbol">)</a> <a id="18238" class="Symbol">=</a> <a id="18241" href="/20.07/Lists/#18234" class="Bound">n</a> <a id="18243" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="18245" href="/20.07/Lists/#18174" class="Function">downFrom</a> <a id="18254" href="/20.07/Lists/#18234" class="Bound">n</a>
</pre>
<p>For example:</p>
<pre class="Agda"><a id="18277" href="/20.07/Lists/#18277" class="Function">_</a> <a id="18279" class="Symbol">:</a> <a id="18281" href="/20.07/Lists/#18174" class="Function">downFrom</a> <a id="18290" class="Number">3</a> <a id="18292" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="18294" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">[</a> <a id="18296" class="Number">2</a> <a id="18298" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">,</a> <a id="18300" class="Number">1</a> <a id="18302" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">,</a> <a id="18304" class="Number">0</a> <a id="18306" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">]</a>
<a id="18308" class="Symbol">_</a> <a id="18310" class="Symbol">=</a> <a id="18312" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a>
</pre>
<p>Prove that the sum of the numbers <code class="language-plaintext highlighter-rouge">(n - 1) + ⋯ + 0</code> is
equal to <code class="language-plaintext highlighter-rouge">n * (n ∸ 1) / 2</code>:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>sum (downFrom n) * 2 ≡ n * (n ∸ 1)
</code></pre></div></div>
<h2 id="monoids">Monoids</h2>
<p>Typically when we use a fold the operator is associative and the
value is a left and right identity for the operator, meaning that the
operator and the value form a <em>monoid</em>.</p>
<p>We can define a monoid as a suitable record type:</p>
<pre class="Agda"><a id="18688" class="Keyword">record</a> <a id="IsMonoid"></a><a id="18695" href="/20.07/Lists/#18695" class="Record">IsMonoid</a> <a id="18704" class="Symbol">{</a><a id="18705" href="/20.07/Lists/#18705" class="Bound">A</a> <a id="18707" class="Symbol">:</a> <a id="18709" class="PrimitiveType">Set</a><a id="18712" class="Symbol">}</a> <a id="18714" class="Symbol">(</a><a id="18715" href="/20.07/Lists/#18715" class="Bound Operator">_⊗_</a> <a id="18719" class="Symbol">:</a> <a id="18721" href="/20.07/Lists/#18705" class="Bound">A</a> <a id="18723" class="Symbol">→</a> <a id="18725" href="/20.07/Lists/#18705" class="Bound">A</a> <a id="18727" class="Symbol">→</a> <a id="18729" href="/20.07/Lists/#18705" class="Bound">A</a><a id="18730" class="Symbol">)</a> <a id="18732" class="Symbol">(</a><a id="18733" href="/20.07/Lists/#18733" class="Bound">e</a> <a id="18735" class="Symbol">:</a> <a id="18737" href="/20.07/Lists/#18705" class="Bound">A</a><a id="18738" class="Symbol">)</a> <a id="18740" class="Symbol">:</a> <a id="18742" class="PrimitiveType">Set</a> <a id="18746" class="Keyword">where</a>
<a id="18754" class="Keyword">field</a>
<a id="IsMonoid.assoc"></a><a id="18764" href="/20.07/Lists/#18764" class="Field">assoc</a> <a id="18770" class="Symbol">:</a> <a id="18772" class="Symbol">∀</a> <a id="18774" class="Symbol">(</a><a id="18775" href="/20.07/Lists/#18775" class="Bound">x</a> <a id="18777" href="/20.07/Lists/#18777" class="Bound">y</a> <a id="18779" href="/20.07/Lists/#18779" class="Bound">z</a> <a id="18781" class="Symbol">:</a> <a id="18783" href="/20.07/Lists/#18705" class="Bound">A</a><a id="18784" class="Symbol">)</a> <a id="18786" class="Symbol">→</a> <a id="18788" class="Symbol">(</a><a id="18789" href="/20.07/Lists/#18775" class="Bound">x</a> <a id="18791" href="/20.07/Lists/#18715" class="Bound Operator">⊗</a> <a id="18793" href="/20.07/Lists/#18777" class="Bound">y</a><a id="18794" class="Symbol">)</a> <a id="18796" href="/20.07/Lists/#18715" class="Bound Operator">⊗</a> <a id="18798" href="/20.07/Lists/#18779" class="Bound">z</a> <a id="18800" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="18802" href="/20.07/Lists/#18775" class="Bound">x</a> <a id="18804" href="/20.07/Lists/#18715" class="Bound Operator">⊗</a> <a id="18806" class="Symbol">(</a><a id="18807" href="/20.07/Lists/#18777" class="Bound">y</a> <a id="18809" href="/20.07/Lists/#18715" class="Bound Operator">⊗</a> <a id="18811" href="/20.07/Lists/#18779" class="Bound">z</a><a id="18812" class="Symbol">)</a>
<a id="IsMonoid.identityˡ"></a><a id="18818" href="/20.07/Lists/#18818" class="Field">identityˡ</a> <a id="18828" class="Symbol">:</a> <a id="18830" class="Symbol">∀</a> <a id="18832" class="Symbol">(</a><a id="18833" href="/20.07/Lists/#18833" class="Bound">x</a> <a id="18835" class="Symbol">:</a> <a id="18837" href="/20.07/Lists/#18705" class="Bound">A</a><a id="18838" class="Symbol">)</a> <a id="18840" class="Symbol">→</a> <a id="18842" href="/20.07/Lists/#18733" class="Bound">e</a> <a id="18844" href="/20.07/Lists/#18715" class="Bound Operator">⊗</a> <a id="18846" href="/20.07/Lists/#18833" class="Bound">x</a> <a id="18848" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="18850" href="/20.07/Lists/#18833" class="Bound">x</a>
<a id="IsMonoid.identityʳ"></a><a id="18856" href="/20.07/Lists/#18856" class="Field">identityʳ</a> <a id="18866" class="Symbol">:</a> <a id="18868" class="Symbol">∀</a> <a id="18870" class="Symbol">(</a><a id="18871" href="/20.07/Lists/#18871" class="Bound">x</a> <a id="18873" class="Symbol">:</a> <a id="18875" href="/20.07/Lists/#18705" class="Bound">A</a><a id="18876" class="Symbol">)</a> <a id="18878" class="Symbol">→</a> <a id="18880" href="/20.07/Lists/#18871" class="Bound">x</a> <a id="18882" href="/20.07/Lists/#18715" class="Bound Operator">⊗</a> <a id="18884" href="/20.07/Lists/#18733" class="Bound">e</a> <a id="18886" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="18888" href="/20.07/Lists/#18871" class="Bound">x</a>
<a id="18891" class="Keyword">open</a> <a id="18896" href="/20.07/Lists/#18695" class="Module">IsMonoid</a>
</pre>
<p>As examples, sum and zero, multiplication and one, and append and the empty
list, are all examples of monoids:</p>
<pre class="Agda"><a id="+-monoid"></a><a id="19025" href="/20.07/Lists/#19025" class="Function">+-monoid</a> <a id="19034" class="Symbol">:</a> <a id="19036" href="/20.07/Lists/#18695" class="Record">IsMonoid</a> <a id="19045" href="Agda.Builtin.Nat.html#298" class="Primitive Operator">_+_</a> <a id="19049" class="Number">0</a>
<a id="19051" href="/20.07/Lists/#19025" class="Function">+-monoid</a> <a id="19060" class="Symbol">=</a>
<a id="19064" class="Keyword">record</a>
<a id="19075" class="Symbol">{</a> <a id="19077" href="/20.07/Lists/#18764" class="Field">assoc</a> <a id="19083" class="Symbol">=</a> <a id="19085" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#11578" class="Function">+-assoc</a>
<a id="19097" class="Symbol">;</a> <a id="19099" href="/20.07/Lists/#18818" class="Field">identityˡ</a> <a id="19109" class="Symbol">=</a> <a id="19111" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#11679" class="Function">+-identityˡ</a>
<a id="19127" class="Symbol">;</a> <a id="19129" href="/20.07/Lists/#18856" class="Field">identityʳ</a> <a id="19139" class="Symbol">=</a> <a id="19141" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#11734" class="Function">+-identityʳ</a>
<a id="19157" class="Symbol">}</a>
<a id="*-monoid"></a><a id="19160" href="/20.07/Lists/#19160" class="Function">*-monoid</a> <a id="19169" class="Symbol">:</a> <a id="19171" href="/20.07/Lists/#18695" class="Record">IsMonoid</a> <a id="19180" href="Agda.Builtin.Nat.html#501" class="Primitive Operator">_*_</a> <a id="19184" class="Number">1</a>
<a id="19186" href="/20.07/Lists/#19160" class="Function">*-monoid</a> <a id="19195" class="Symbol">=</a>
<a id="19199" class="Keyword">record</a>
<a id="19210" class="Symbol">{</a> <a id="19212" href="/20.07/Lists/#18764" class="Field">assoc</a> <a id="19218" class="Symbol">=</a> <a id="19220" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#18464" class="Function">*-assoc</a>
<a id="19232" class="Symbol">;</a> <a id="19234" href="/20.07/Lists/#18818" class="Field">identityˡ</a> <a id="19244" class="Symbol">=</a> <a id="19246" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#17362" class="Function">*-identityˡ</a>
<a id="19262" class="Symbol">;</a> <a id="19264" href="/20.07/Lists/#18856" class="Field">identityʳ</a> <a id="19274" class="Symbol">=</a> <a id="19276" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Properties.html#17426" class="Function">*-identityʳ</a>
<a id="19292" class="Symbol">}</a>
<a id="++-monoid"></a><a id="19295" href="/20.07/Lists/#19295" class="Function">++-monoid</a> <a id="19305" class="Symbol">:</a> <a id="19307" class="Symbol">∀</a> <a id="19309" class="Symbol">{</a><a id="19310" href="/20.07/Lists/#19310" class="Bound">A</a> <a id="19312" class="Symbol">:</a> <a id="19314" class="PrimitiveType">Set</a><a id="19317" class="Symbol">}</a> <a id="19319" class="Symbol">→</a> <a id="19321" href="/20.07/Lists/#18695" class="Record">IsMonoid</a> <a id="19330" class="Symbol">{</a><a id="19331" href="/20.07/Lists/#1067" class="Datatype">List</a> <a id="19336" href="/20.07/Lists/#19310" class="Bound">A</a><a id="19337" class="Symbol">}</a> <a id="19339" href="/20.07/Lists/#3467" class="Function Operator">_++_</a> <a id="19344" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a>
<a id="19347" href="/20.07/Lists/#19295" class="Function">++-monoid</a> <a id="19357" class="Symbol">=</a>
<a id="19361" class="Keyword">record</a>
<a id="19372" class="Symbol">{</a> <a id="19374" href="/20.07/Lists/#18764" class="Field">assoc</a> <a id="19380" class="Symbol">=</a> <a id="19382" href="/20.07/Lists/#4528" class="Function">++-assoc</a>
<a id="19395" class="Symbol">;</a> <a id="19397" href="/20.07/Lists/#18818" class="Field">identityˡ</a> <a id="19407" class="Symbol">=</a> <a id="19409" href="/20.07/Lists/#5739" class="Function">++-identityˡ</a>
<a id="19426" class="Symbol">;</a> <a id="19428" href="/20.07/Lists/#18856" class="Field">identityʳ</a> <a id="19438" class="Symbol">=</a> <a id="19440" href="/20.07/Lists/#5917" class="Function">++-identityʳ</a>
<a id="19457" class="Symbol">}</a>
</pre>
<p>If <code class="language-plaintext highlighter-rouge">_⊗_</code> and <code class="language-plaintext highlighter-rouge">e</code> form a monoid, then we can re-express fold on the
same operator and an arbitrary value:</p>
<pre class="Agda"><a id="foldr-monoid"></a><a id="19573" href="/20.07/Lists/#19573" class="Function">foldr-monoid</a> <a id="19586" class="Symbol">:</a> <a id="19588" class="Symbol">∀</a> <a id="19590" class="Symbol">{</a><a id="19591" href="/20.07/Lists/#19591" class="Bound">A</a> <a id="19593" class="Symbol">:</a> <a id="19595" class="PrimitiveType">Set</a><a id="19598" class="Symbol">}</a> <a id="19600" class="Symbol">(</a><a id="19601" href="/20.07/Lists/#19601" class="Bound Operator">_⊗_</a> <a id="19605" class="Symbol">:</a> <a id="19607" href="/20.07/Lists/#19591" class="Bound">A</a> <a id="19609" class="Symbol">→</a> <a id="19611" href="/20.07/Lists/#19591" class="Bound">A</a> <a id="19613" class="Symbol">→</a> <a id="19615" href="/20.07/Lists/#19591" class="Bound">A</a><a id="19616" class="Symbol">)</a> <a id="19618" class="Symbol">(</a><a id="19619" href="/20.07/Lists/#19619" class="Bound">e</a> <a id="19621" class="Symbol">:</a> <a id="19623" href="/20.07/Lists/#19591" class="Bound">A</a><a id="19624" class="Symbol">)</a> <a id="19626" class="Symbol">→</a> <a id="19628" href="/20.07/Lists/#18695" class="Record">IsMonoid</a> <a id="19637" href="/20.07/Lists/#19601" class="Bound Operator">_⊗_</a> <a id="19641" href="/20.07/Lists/#19619" class="Bound">e</a> <a id="19643" class="Symbol">→</a>
<a id="19647" class="Symbol">∀</a> <a id="19649" class="Symbol">(</a><a id="19650" href="/20.07/Lists/#19650" class="Bound">xs</a> <a id="19653" class="Symbol">:</a> <a id="19655" href="/20.07/Lists/#1067" class="Datatype">List</a> <a id="19660" href="/20.07/Lists/#19591" class="Bound">A</a><a id="19661" class="Symbol">)</a> <a id="19663" class="Symbol">(</a><a id="19664" href="/20.07/Lists/#19664" class="Bound">y</a> <a id="19666" class="Symbol">:</a> <a id="19668" href="/20.07/Lists/#19591" class="Bound">A</a><a id="19669" class="Symbol">)</a> <a id="19671" class="Symbol">→</a> <a id="19673" href="/20.07/Lists/#15291" class="Function">foldr</a> <a id="19679" href="/20.07/Lists/#19601" class="Bound Operator">_⊗_</a> <a id="19683" href="/20.07/Lists/#19664" class="Bound">y</a> <a id="19685" href="/20.07/Lists/#19650" class="Bound">xs</a> <a id="19688" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="19690" href="/20.07/Lists/#15291" class="Function">foldr</a> <a id="19696" href="/20.07/Lists/#19601" class="Bound Operator">_⊗_</a> <a id="19700" href="/20.07/Lists/#19619" class="Bound">e</a> <a id="19702" href="/20.07/Lists/#19650" class="Bound">xs</a> <a id="19705" href="/20.07/Lists/#19601" class="Bound Operator">⊗</a> <a id="19707" href="/20.07/Lists/#19664" class="Bound">y</a>
<a id="19709" href="/20.07/Lists/#19573" class="Function">foldr-monoid</a> <a id="19722" href="/20.07/Lists/#19722" class="Bound Operator">_⊗_</a> <a id="19726" href="/20.07/Lists/#19726" class="Bound">e</a> <a id="19728" href="/20.07/Lists/#19728" class="Bound">⊗-monoid</a> <a id="19737" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a> <a id="19740" href="/20.07/Lists/#19740" class="Bound">y</a> <a id="19742" class="Symbol">=</a>
<a id="19746" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2597" class="Function Operator">begin</a>
<a id="19756" href="/20.07/Lists/#15291" class="Function">foldr</a> <a id="19762" href="/20.07/Lists/#19722" class="Bound Operator">_⊗_</a> <a id="19766" href="/20.07/Lists/#19740" class="Bound">y</a> <a id="19768" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a>
<a id="19773" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="19781" href="/20.07/Lists/#19740" class="Bound">y</a>
<a id="19785" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">≡⟨</a> <a id="19788" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#939" class="Function">sym</a> <a id="19792" class="Symbol">(</a><a id="19793" href="/20.07/Lists/#18818" class="Field">identityˡ</a> <a id="19803" href="/20.07/Lists/#19728" class="Bound">⊗-monoid</a> <a id="19812" href="/20.07/Lists/#19740" class="Bound">y</a><a id="19813" class="Symbol">)</a> <a id="19815" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">⟩</a>
<a id="19821" class="Symbol">(</a><a id="19822" href="/20.07/Lists/#19726" class="Bound">e</a> <a id="19824" href="/20.07/Lists/#19722" class="Bound Operator">⊗</a> <a id="19826" href="/20.07/Lists/#19740" class="Bound">y</a><a id="19827" class="Symbol">)</a>
<a id="19831" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="19839" href="/20.07/Lists/#15291" class="Function">foldr</a> <a id="19845" href="/20.07/Lists/#19722" class="Bound Operator">_⊗_</a> <a id="19849" href="/20.07/Lists/#19726" class="Bound">e</a> <a id="19851" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a> <a id="19854" href="/20.07/Lists/#19722" class="Bound Operator">⊗</a> <a id="19856" href="/20.07/Lists/#19740" class="Bound">y</a>
<a id="19860" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2892" class="Function Operator">∎</a>
<a id="19862" href="/20.07/Lists/#19573" class="Function">foldr-monoid</a> <a id="19875" href="/20.07/Lists/#19875" class="Bound Operator">_⊗_</a> <a id="19879" href="/20.07/Lists/#19879" class="Bound">e</a> <a id="19881" href="/20.07/Lists/#19881" class="Bound">⊗-monoid</a> <a id="19890" class="Symbol">(</a><a id="19891" href="/20.07/Lists/#19891" class="Bound">x</a> <a id="19893" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="19895" href="/20.07/Lists/#19895" class="Bound">xs</a><a id="19897" class="Symbol">)</a> <a id="19899" href="/20.07/Lists/#19899" class="Bound">y</a> <a id="19901" class="Symbol">=</a>
<a id="19905" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2597" class="Function Operator">begin</a>
<a id="19915" href="/20.07/Lists/#15291" class="Function">foldr</a> <a id="19921" href="/20.07/Lists/#19875" class="Bound Operator">_⊗_</a> <a id="19925" href="/20.07/Lists/#19899" class="Bound">y</a> <a id="19927" class="Symbol">(</a><a id="19928" href="/20.07/Lists/#19891" class="Bound">x</a> <a id="19930" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="19932" href="/20.07/Lists/#19895" class="Bound">xs</a><a id="19934" class="Symbol">)</a>
<a id="19938" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="19946" href="/20.07/Lists/#19891" class="Bound">x</a> <a id="19948" href="/20.07/Lists/#19875" class="Bound Operator">⊗</a> <a id="19950" class="Symbol">(</a><a id="19951" href="/20.07/Lists/#15291" class="Function">foldr</a> <a id="19957" href="/20.07/Lists/#19875" class="Bound Operator">_⊗_</a> <a id="19961" href="/20.07/Lists/#19899" class="Bound">y</a> <a id="19963" href="/20.07/Lists/#19895" class="Bound">xs</a><a id="19965" class="Symbol">)</a>
<a id="19969" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">≡⟨</a> <a id="19972" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#1090" class="Function">cong</a> <a id="19977" class="Symbol">(</a><a id="19978" href="/20.07/Lists/#19891" class="Bound">x</a> <a id="19980" href="/20.07/Lists/#19875" class="Bound Operator">⊗_</a><a id="19982" class="Symbol">)</a> <a id="19984" class="Symbol">(</a><a id="19985" href="/20.07/Lists/#19573" class="Function">foldr-monoid</a> <a id="19998" href="/20.07/Lists/#19875" class="Bound Operator">_⊗_</a> <a id="20002" href="/20.07/Lists/#19879" class="Bound">e</a> <a id="20004" href="/20.07/Lists/#19881" class="Bound">⊗-monoid</a> <a id="20013" href="/20.07/Lists/#19895" class="Bound">xs</a> <a id="20016" href="/20.07/Lists/#19899" class="Bound">y</a><a id="20017" class="Symbol">)</a> <a id="20019" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">⟩</a>
<a id="20025" href="/20.07/Lists/#19891" class="Bound">x</a> <a id="20027" href="/20.07/Lists/#19875" class="Bound Operator">⊗</a> <a id="20029" class="Symbol">(</a><a id="20030" href="/20.07/Lists/#15291" class="Function">foldr</a> <a id="20036" href="/20.07/Lists/#19875" class="Bound Operator">_⊗_</a> <a id="20040" href="/20.07/Lists/#19879" class="Bound">e</a> <a id="20042" href="/20.07/Lists/#19895" class="Bound">xs</a> <a id="20045" href="/20.07/Lists/#19875" class="Bound Operator">⊗</a> <a id="20047" href="/20.07/Lists/#19899" class="Bound">y</a><a id="20048" class="Symbol">)</a>
<a id="20052" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">≡⟨</a> <a id="20055" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#939" class="Function">sym</a> <a id="20059" class="Symbol">(</a><a id="20060" href="/20.07/Lists/#18764" class="Field">assoc</a> <a id="20066" href="/20.07/Lists/#19881" class="Bound">⊗-monoid</a> <a id="20075" href="/20.07/Lists/#19891" class="Bound">x</a> <a id="20077" class="Symbol">(</a><a id="20078" href="/20.07/Lists/#15291" class="Function">foldr</a> <a id="20084" href="/20.07/Lists/#19875" class="Bound Operator">_⊗_</a> <a id="20088" href="/20.07/Lists/#19879" class="Bound">e</a> <a id="20090" href="/20.07/Lists/#19895" class="Bound">xs</a><a id="20092" class="Symbol">)</a> <a id="20094" href="/20.07/Lists/#19899" class="Bound">y</a><a id="20095" class="Symbol">)</a> <a id="20097" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">⟩</a>
<a id="20103" class="Symbol">(</a><a id="20104" href="/20.07/Lists/#19891" class="Bound">x</a> <a id="20106" href="/20.07/Lists/#19875" class="Bound Operator">⊗</a> <a id="20108" href="/20.07/Lists/#15291" class="Function">foldr</a> <a id="20114" href="/20.07/Lists/#19875" class="Bound Operator">_⊗_</a> <a id="20118" href="/20.07/Lists/#19879" class="Bound">e</a> <a id="20120" href="/20.07/Lists/#19895" class="Bound">xs</a><a id="20122" class="Symbol">)</a> <a id="20124" href="/20.07/Lists/#19875" class="Bound Operator">⊗</a> <a id="20126" href="/20.07/Lists/#19899" class="Bound">y</a>
<a id="20130" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2655" class="Function Operator">≡⟨⟩</a>
<a id="20138" href="/20.07/Lists/#15291" class="Function">foldr</a> <a id="20144" href="/20.07/Lists/#19875" class="Bound Operator">_⊗_</a> <a id="20148" href="/20.07/Lists/#19879" class="Bound">e</a> <a id="20150" class="Symbol">(</a><a id="20151" href="/20.07/Lists/#19891" class="Bound">x</a> <a id="20153" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="20155" href="/20.07/Lists/#19895" class="Bound">xs</a><a id="20157" class="Symbol">)</a> <a id="20159" href="/20.07/Lists/#19875" class="Bound Operator">⊗</a> <a id="20161" href="/20.07/Lists/#19899" class="Bound">y</a>
<a id="20165" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2892" class="Function Operator">∎</a>
</pre>
<p>In a previous exercise we showed the following.</p>
<pre class="Agda"><a id="20224" class="Keyword">postulate</a>
<a id="foldr-++"></a><a id="20236" href="/20.07/Lists/#20236" class="Postulate">foldr-++</a> <a id="20245" class="Symbol">:</a> <a id="20247" class="Symbol">∀</a> <a id="20249" class="Symbol">{</a><a id="20250" href="/20.07/Lists/#20250" class="Bound">A</a> <a id="20252" class="Symbol">:</a> <a id="20254" class="PrimitiveType">Set</a><a id="20257" class="Symbol">}</a> <a id="20259" class="Symbol">(</a><a id="20260" href="/20.07/Lists/#20260" class="Bound Operator">_⊗_</a> <a id="20264" class="Symbol">:</a> <a id="20266" href="/20.07/Lists/#20250" class="Bound">A</a> <a id="20268" class="Symbol">→</a> <a id="20270" href="/20.07/Lists/#20250" class="Bound">A</a> <a id="20272" class="Symbol">→</a> <a id="20274" href="/20.07/Lists/#20250" class="Bound">A</a><a id="20275" class="Symbol">)</a> <a id="20277" class="Symbol">(</a><a id="20278" href="/20.07/Lists/#20278" class="Bound">e</a> <a id="20280" class="Symbol">:</a> <a id="20282" href="/20.07/Lists/#20250" class="Bound">A</a><a id="20283" class="Symbol">)</a> <a id="20285" class="Symbol">(</a><a id="20286" href="/20.07/Lists/#20286" class="Bound">xs</a> <a id="20289" href="/20.07/Lists/#20289" class="Bound">ys</a> <a id="20292" class="Symbol">:</a> <a id="20294" href="/20.07/Lists/#1067" class="Datatype">List</a> <a id="20299" href="/20.07/Lists/#20250" class="Bound">A</a><a id="20300" class="Symbol">)</a> <a id="20302" class="Symbol">→</a>
<a id="20308" href="/20.07/Lists/#15291" class="Function">foldr</a> <a id="20314" href="/20.07/Lists/#20260" class="Bound Operator">_⊗_</a> <a id="20318" href="/20.07/Lists/#20278" class="Bound">e</a> <a id="20320" class="Symbol">(</a><a id="20321" href="/20.07/Lists/#20286" class="Bound">xs</a> <a id="20324" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="20327" href="/20.07/Lists/#20289" class="Bound">ys</a><a id="20329" class="Symbol">)</a> <a id="20331" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="20333" href="/20.07/Lists/#15291" class="Function">foldr</a> <a id="20339" href="/20.07/Lists/#20260" class="Bound Operator">_⊗_</a> <a id="20343" class="Symbol">(</a><a id="20344" href="/20.07/Lists/#15291" class="Function">foldr</a> <a id="20350" href="/20.07/Lists/#20260" class="Bound Operator">_⊗_</a> <a id="20354" href="/20.07/Lists/#20278" class="Bound">e</a> <a id="20356" href="/20.07/Lists/#20289" class="Bound">ys</a><a id="20358" class="Symbol">)</a> <a id="20360" href="/20.07/Lists/#20286" class="Bound">xs</a>
</pre>
<p>As a consequence, using a previous exercise, we have the following:</p>
<pre class="Agda"><a id="foldr-monoid-++"></a><a id="20440" href="/20.07/Lists/#20440" class="Function">foldr-monoid-++</a> <a id="20456" class="Symbol">:</a> <a id="20458" class="Symbol">∀</a> <a id="20460" class="Symbol">{</a><a id="20461" href="/20.07/Lists/#20461" class="Bound">A</a> <a id="20463" class="Symbol">:</a> <a id="20465" class="PrimitiveType">Set</a><a id="20468" class="Symbol">}</a> <a id="20470" class="Symbol">(</a><a id="20471" href="/20.07/Lists/#20471" class="Bound Operator">_⊗_</a> <a id="20475" class="Symbol">:</a> <a id="20477" href="/20.07/Lists/#20461" class="Bound">A</a> <a id="20479" class="Symbol">→</a> <a id="20481" href="/20.07/Lists/#20461" class="Bound">A</a> <a id="20483" class="Symbol">→</a> <a id="20485" href="/20.07/Lists/#20461" class="Bound">A</a><a id="20486" class="Symbol">)</a> <a id="20488" class="Symbol">(</a><a id="20489" href="/20.07/Lists/#20489" class="Bound">e</a> <a id="20491" class="Symbol">:</a> <a id="20493" href="/20.07/Lists/#20461" class="Bound">A</a><a id="20494" class="Symbol">)</a> <a id="20496" class="Symbol">→</a> <a id="20498" href="/20.07/Lists/#18695" class="Record">IsMonoid</a> <a id="20507" href="/20.07/Lists/#20471" class="Bound Operator">_⊗_</a> <a id="20511" href="/20.07/Lists/#20489" class="Bound">e</a> <a id="20513" class="Symbol">→</a>
<a id="20517" class="Symbol">∀</a> <a id="20519" class="Symbol">(</a><a id="20520" href="/20.07/Lists/#20520" class="Bound">xs</a> <a id="20523" href="/20.07/Lists/#20523" class="Bound">ys</a> <a id="20526" class="Symbol">:</a> <a id="20528" href="/20.07/Lists/#1067" class="Datatype">List</a> <a id="20533" href="/20.07/Lists/#20461" class="Bound">A</a><a id="20534" class="Symbol">)</a> <a id="20536" class="Symbol">→</a> <a id="20538" href="/20.07/Lists/#15291" class="Function">foldr</a> <a id="20544" href="/20.07/Lists/#20471" class="Bound Operator">_⊗_</a> <a id="20548" href="/20.07/Lists/#20489" class="Bound">e</a> <a id="20550" class="Symbol">(</a><a id="20551" href="/20.07/Lists/#20520" class="Bound">xs</a> <a id="20554" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="20557" href="/20.07/Lists/#20523" class="Bound">ys</a><a id="20559" class="Symbol">)</a> <a id="20561" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="20563" href="/20.07/Lists/#15291" class="Function">foldr</a> <a id="20569" href="/20.07/Lists/#20471" class="Bound Operator">_⊗_</a> <a id="20573" href="/20.07/Lists/#20489" class="Bound">e</a> <a id="20575" href="/20.07/Lists/#20520" class="Bound">xs</a> <a id="20578" href="/20.07/Lists/#20471" class="Bound Operator">⊗</a> <a id="20580" href="/20.07/Lists/#15291" class="Function">foldr</a> <a id="20586" href="/20.07/Lists/#20471" class="Bound Operator">_⊗_</a> <a id="20590" href="/20.07/Lists/#20489" class="Bound">e</a> <a id="20592" href="/20.07/Lists/#20523" class="Bound">ys</a>
<a id="20595" href="/20.07/Lists/#20440" class="Function">foldr-monoid-++</a> <a id="20611" href="/20.07/Lists/#20611" class="Bound Operator">_⊗_</a> <a id="20615" href="/20.07/Lists/#20615" class="Bound">e</a> <a id="20617" href="/20.07/Lists/#20617" class="Bound">monoid-⊗</a> <a id="20626" href="/20.07/Lists/#20626" class="Bound">xs</a> <a id="20629" href="/20.07/Lists/#20629" class="Bound">ys</a> <a id="20632" class="Symbol">=</a>
<a id="20636" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2597" class="Function Operator">begin</a>
<a id="20646" href="/20.07/Lists/#15291" class="Function">foldr</a> <a id="20652" href="/20.07/Lists/#20611" class="Bound Operator">_⊗_</a> <a id="20656" href="/20.07/Lists/#20615" class="Bound">e</a> <a id="20658" class="Symbol">(</a><a id="20659" href="/20.07/Lists/#20626" class="Bound">xs</a> <a id="20662" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="20665" href="/20.07/Lists/#20629" class="Bound">ys</a><a id="20667" class="Symbol">)</a>
<a id="20671" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">≡⟨</a> <a id="20674" href="/20.07/Lists/#20236" class="Postulate">foldr-++</a> <a id="20683" href="/20.07/Lists/#20611" class="Bound Operator">_⊗_</a> <a id="20687" href="/20.07/Lists/#20615" class="Bound">e</a> <a id="20689" href="/20.07/Lists/#20626" class="Bound">xs</a> <a id="20692" href="/20.07/Lists/#20629" class="Bound">ys</a> <a id="20695" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">⟩</a>
<a id="20701" href="/20.07/Lists/#15291" class="Function">foldr</a> <a id="20707" href="/20.07/Lists/#20611" class="Bound Operator">_⊗_</a> <a id="20711" class="Symbol">(</a><a id="20712" href="/20.07/Lists/#15291" class="Function">foldr</a> <a id="20718" href="/20.07/Lists/#20611" class="Bound Operator">_⊗_</a> <a id="20722" href="/20.07/Lists/#20615" class="Bound">e</a> <a id="20724" href="/20.07/Lists/#20629" class="Bound">ys</a><a id="20726" class="Symbol">)</a> <a id="20728" href="/20.07/Lists/#20626" class="Bound">xs</a>
<a id="20733" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">≡⟨</a> <a id="20736" href="/20.07/Lists/#19573" class="Function">foldr-monoid</a> <a id="20749" href="/20.07/Lists/#20611" class="Bound Operator">_⊗_</a> <a id="20753" href="/20.07/Lists/#20615" class="Bound">e</a> <a id="20755" href="/20.07/Lists/#20617" class="Bound">monoid-⊗</a> <a id="20764" href="/20.07/Lists/#20626" class="Bound">xs</a> <a id="20767" class="Symbol">(</a><a id="20768" href="/20.07/Lists/#15291" class="Function">foldr</a> <a id="20774" href="/20.07/Lists/#20611" class="Bound Operator">_⊗_</a> <a id="20778" href="/20.07/Lists/#20615" class="Bound">e</a> <a id="20780" href="/20.07/Lists/#20629" class="Bound">ys</a><a id="20782" class="Symbol">)</a> <a id="20784" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2714" class="Function Operator">⟩</a>
<a id="20790" href="/20.07/Lists/#15291" class="Function">foldr</a> <a id="20796" href="/20.07/Lists/#20611" class="Bound Operator">_⊗_</a> <a id="20800" href="/20.07/Lists/#20615" class="Bound">e</a> <a id="20802" href="/20.07/Lists/#20626" class="Bound">xs</a> <a id="20805" href="/20.07/Lists/#20611" class="Bound Operator">⊗</a> <a id="20807" href="/20.07/Lists/#15291" class="Function">foldr</a> <a id="20813" href="/20.07/Lists/#20611" class="Bound Operator">_⊗_</a> <a id="20817" href="/20.07/Lists/#20615" class="Bound">e</a> <a id="20819" href="/20.07/Lists/#20629" class="Bound">ys</a>
<a id="20824" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#2892" class="Function Operator">∎</a>
</pre>
<h4 id="exercise-foldl-practice">Exercise <code class="language-plaintext highlighter-rouge">foldl</code> (practice)</h4>
<p>Define a function <code class="language-plaintext highlighter-rouge">foldl</code> which is analogous to <code class="language-plaintext highlighter-rouge">foldr</code>, but where
operations associate to the left rather than the right. For example:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>foldr _⊗_ e [ x , y , z ] = x ⊗ (y ⊗ (z ⊗ e))
foldl _⊗_ e [ x , y , z ] = ((e ⊗ x) ⊗ y) ⊗ z
</code></pre></div></div>
<pre class="Agda"><a id="21112" class="Comment">-- Your code goes here</a>
</pre>
<h4 id="exercise-foldr-monoid-foldl-practice">Exercise <code class="language-plaintext highlighter-rouge">foldr-monoid-foldl</code> (practice)</h4>
<p>Show that if <code class="language-plaintext highlighter-rouge">_⊗_</code> and <code class="language-plaintext highlighter-rouge">e</code> form a monoid, then <code class="language-plaintext highlighter-rouge">foldr _⊗_ e</code> and
<code class="language-plaintext highlighter-rouge">foldl _⊗_ e</code> always compute the same result.</p>
<pre class="Agda"><a id="21304" class="Comment">-- Your code goes here</a>
</pre>
<h2 id="All">All</h2>
<p>We can also define predicates over lists. Two of the most important
are <code class="language-plaintext highlighter-rouge">All</code> and <code class="language-plaintext highlighter-rouge">Any</code>.</p>
<p>Predicate <code class="language-plaintext highlighter-rouge">All P</code> holds if predicate <code class="language-plaintext highlighter-rouge">P</code> is satisfied by every element of a list:</p>
<pre class="Agda"><a id="21524" class="Keyword">data</a> <a id="All"></a><a id="21529" href="/20.07/Lists/#21529" class="Datatype">All</a> <a id="21533" class="Symbol">{</a><a id="21534" href="/20.07/Lists/#21534" class="Bound">A</a> <a id="21536" class="Symbol">:</a> <a id="21538" class="PrimitiveType">Set</a><a id="21541" class="Symbol">}</a> <a id="21543" class="Symbol">(</a><a id="21544" href="/20.07/Lists/#21544" class="Bound">P</a> <a id="21546" class="Symbol">:</a> <a id="21548" href="/20.07/Lists/#21534" class="Bound">A</a> <a id="21550" class="Symbol">→</a> <a id="21552" class="PrimitiveType">Set</a><a id="21555" class="Symbol">)</a> <a id="21557" class="Symbol">:</a> <a id="21559" href="/20.07/Lists/#1067" class="Datatype">List</a> <a id="21564" href="/20.07/Lists/#21534" class="Bound">A</a> <a id="21566" class="Symbol">→</a> <a id="21568" class="PrimitiveType">Set</a> <a id="21572" class="Keyword">where</a>
<a id="All.[]"></a><a id="21580" href="/20.07/Lists/#21580" class="InductiveConstructor">[]</a> <a id="21584" class="Symbol">:</a> <a id="21586" href="/20.07/Lists/#21529" class="Datatype">All</a> <a id="21590" href="/20.07/Lists/#21544" class="Bound">P</a> <a id="21592" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a>
<a id="All._∷_"></a><a id="21597" href="/20.07/Lists/#21597" class="InductiveConstructor Operator">_∷_</a> <a id="21601" class="Symbol">:</a> <a id="21603" class="Symbol">∀</a> <a id="21605" class="Symbol">{</a><a id="21606" href="/20.07/Lists/#21606" class="Bound">x</a> <a id="21608" class="Symbol">:</a> <a id="21610" href="/20.07/Lists/#21534" class="Bound">A</a><a id="21611" class="Symbol">}</a> <a id="21613" class="Symbol">{</a><a id="21614" href="/20.07/Lists/#21614" class="Bound">xs</a> <a id="21617" class="Symbol">:</a> <a id="21619" href="/20.07/Lists/#1067" class="Datatype">List</a> <a id="21624" href="/20.07/Lists/#21534" class="Bound">A</a><a id="21625" class="Symbol">}</a> <a id="21627" class="Symbol">→</a> <a id="21629" href="/20.07/Lists/#21544" class="Bound">P</a> <a id="21631" href="/20.07/Lists/#21606" class="Bound">x</a> <a id="21633" class="Symbol">→</a> <a id="21635" href="/20.07/Lists/#21529" class="Datatype">All</a> <a id="21639" href="/20.07/Lists/#21544" class="Bound">P</a> <a id="21641" href="/20.07/Lists/#21614" class="Bound">xs</a> <a id="21644" class="Symbol">→</a> <a id="21646" href="/20.07/Lists/#21529" class="Datatype">All</a> <a id="21650" href="/20.07/Lists/#21544" class="Bound">P</a> <a id="21652" class="Symbol">(</a><a id="21653" href="/20.07/Lists/#21606" class="Bound">x</a> <a id="21655" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="21657" href="/20.07/Lists/#21614" class="Bound">xs</a><a id="21659" class="Symbol">)</a>
</pre>
<p>The type has two constructors, reusing the names of the same constructors for lists.
The first asserts that <code class="language-plaintext highlighter-rouge">P</code> holds for every element of the empty list.
The second asserts that if <code class="language-plaintext highlighter-rouge">P</code> holds of the head of a list and for every
element of the tail of a list, then <code class="language-plaintext highlighter-rouge">P</code> holds for every element of the list.
Agda uses types to disambiguate whether the constructor is building
a list or evidence that <code class="language-plaintext highlighter-rouge">All P</code> holds.</p>
<p>For example, <code class="language-plaintext highlighter-rouge">All (_≤ 2)</code> holds of a list where every element is less
than or equal to two. Recall that <code class="language-plaintext highlighter-rouge">z≤n</code> proves <code class="language-plaintext highlighter-rouge">zero ≤ n</code> for any
<code class="language-plaintext highlighter-rouge">n</code>, and that if <code class="language-plaintext highlighter-rouge">m≤n</code> proves <code class="language-plaintext highlighter-rouge">m ≤ n</code> then <code class="language-plaintext highlighter-rouge">s≤s m≤n</code> proves <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>:</p>
<pre class="Agda"><a id="22317" href="/20.07/Lists/#22317" class="Function">_</a> <a id="22319" class="Symbol">:</a> <a id="22321" href="/20.07/Lists/#21529" class="Datatype">All</a> <a id="22325" class="Symbol">(</a><a id="22326" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Base.html#895" class="Datatype Operator">_≤</a> <a id="22329" class="Number">2</a><a id="22330" class="Symbol">)</a> <a id="22332" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">[</a> <a id="22334" class="Number">0</a> <a id="22336" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">,</a> <a id="22338" class="Number">1</a> <a id="22340" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">,</a> <a id="22342" class="Number">2</a> <a id="22344" href="/20.07/Lists/#2881" class="InductiveConstructor Operator">]</a>
<a id="22346" class="Symbol">_</a> <a id="22348" class="Symbol">=</a> <a id="22350" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Base.html#918" class="InductiveConstructor">z≤n</a> <a id="22354" href="/20.07/Lists/#21597" class="InductiveConstructor Operator">∷</a> <a id="22356" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Base.html#960" class="InductiveConstructor">s≤s</a> <a id="22360" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Base.html#918" class="InductiveConstructor">z≤n</a> <a id="22364" href="/20.07/Lists/#21597" class="InductiveConstructor Operator">∷</a> <a id="22366" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Base.html#960" class="InductiveConstructor">s≤s</a> <a id="22370" class="Symbol">(</a><a id="22371" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Base.html#960" class="InductiveConstructor">s≤s</a> <a id="22375" href="https://agda.github.io/agda-stdlib/v1.1/Data.Nat.Base.html#918" class="InductiveConstructor">z≤n</a><a id="22378" class="Symbol">)</a> <a id="22380" href="/20.07/Lists/#21597" class="InductiveConstructor Operator">∷</a> <a id="22382" href="/20.07/Lists/#21580" class="InductiveConstructor">[]</a>
</pre>
<p>Here <code class="language-plaintext highlighter-rouge">_∷_</code> and <code class="language-plaintext highlighter-rouge">[]</code> are the constructors of <code class="language-plaintext highlighter-rouge">All P</code> rather than of <code class="language-plaintext highlighter-rouge">List A</code>.
The three items are proofs of <code class="language-plaintext highlighter-rouge">0 ≤ 2</code>, <code class="language-plaintext highlighter-rouge">1 ≤ 2</code>, and <code class="language-plaintext highlighter-rouge">2 ≤ 2</code>, respectively.</p>
<p>(One might wonder whether a pattern such as <code class="language-plaintext highlighter-rouge">[_,_,_]</code> can be used to
construct values of type <code class="language-plaintext highlighter-rouge">All</code> as well as type <code class="language-plaintext highlighter-rouge">List</code>, since both use
the same constructors. Indeed it can, so long as both types are in
scope when the pattern is declared. That’s not the case here, since
<code class="language-plaintext highlighter-rouge">List</code> is defined before <code class="language-plaintext highlighter-rouge">[_,_,_]</code>, but <code class="language-plaintext highlighter-rouge">All</code> is defined later.)</p>
<h2 id="any">Any</h2>
<p>Predicate <code class="language-plaintext highlighter-rouge">Any P</code> holds if predicate <code class="language-plaintext highlighter-rouge">P</code> is satisfied by some element of a list:</p>
<pre class="Agda"><a id="22977" class="Keyword">data</a> <a id="Any"></a><a id="22982" href="/20.07/Lists/#22982" class="Datatype">Any</a> <a id="22986" class="Symbol">{</a><a id="22987" href="/20.07/Lists/#22987" class="Bound">A</a> <a id="22989" class="Symbol">:</a> <a id="22991" class="PrimitiveType">Set</a><a id="22994" class="Symbol">}</a> <a id="22996" class="Symbol">(</a><a id="22997" href="/20.07/Lists/#22997" class="Bound">P</a> <a id="22999" class="Symbol">:</a> <a id="23001" href="/20.07/Lists/#22987" class="Bound">A</a> <a id="23003" class="Symbol">→</a> <a id="23005" class="PrimitiveType">Set</a><a id="23008" class="Symbol">)</a> <a id="23010" class="Symbol">:</a> <a id="23012" href="/20.07/Lists/#1067" class="Datatype">List</a> <a id="23017" href="/20.07/Lists/#22987" class="Bound">A</a> <a id="23019" class="Symbol">→</a> <a id="23021" class="PrimitiveType">Set</a> <a id="23025" class="Keyword">where</a>
<a id="Any.here"></a><a id="23033" href="/20.07/Lists/#23033" class="InductiveConstructor">here</a> <a id="23039" class="Symbol">:</a> <a id="23041" class="Symbol">∀</a> <a id="23043" class="Symbol">{</a><a id="23044" href="/20.07/Lists/#23044" class="Bound">x</a> <a id="23046" class="Symbol">:</a> <a id="23048" href="/20.07/Lists/#22987" class="Bound">A</a><a id="23049" class="Symbol">}</a> <a id="23051" class="Symbol">{</a><a id="23052" href="/20.07/Lists/#23052" class="Bound">xs</a> <a id="23055" class="Symbol">:</a> <a id="23057" href="/20.07/Lists/#1067" class="Datatype">List</a> <a id="23062" href="/20.07/Lists/#22987" class="Bound">A</a><a id="23063" class="Symbol">}</a> <a id="23065" class="Symbol">→</a> <a id="23067" href="/20.07/Lists/#22997" class="Bound">P</a> <a id="23069" href="/20.07/Lists/#23044" class="Bound">x</a> <a id="23071" class="Symbol">→</a> <a id="23073" href="/20.07/Lists/#22982" class="Datatype">Any</a> <a id="23077" href="/20.07/Lists/#22997" class="Bound">P</a> <a id="23079" class="Symbol">(</a><a id="23080" href="/20.07/Lists/#23044" class="Bound">x</a> <a id="23082" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="23084" href="/20.07/Lists/#23052" class="Bound">xs</a><a id="23086" class="Symbol">)</a>
<a id="Any.there"></a><a id="23090" href="/20.07/Lists/#23090" class="InductiveConstructor">there</a> <a id="23096" class="Symbol">:</a> <a id="23098" class="Symbol">∀</a> <a id="23100" class="Symbol">{</a><a id="23101" href="/20.07/Lists/#23101" class="Bound">x</a> <a id="23103" class="Symbol">:</a> <a id="23105" href="/20.07/Lists/#22987" class="Bound">A</a><a id="23106" class="Symbol">}</a> <a id="23108" class="Symbol">{</a><a id="23109" href="/20.07/Lists/#23109" class="Bound">xs</a> <a id="23112" class="Symbol">:</a> <a id="23114" href="/20.07/Lists/#1067" class="Datatype">List</a> <a id="23119" href="/20.07/Lists/#22987" class="Bound">A</a><a id="23120" class="Symbol">}</a> <a id="23122" class="Symbol">→</a> <a id="23124" href="/20.07/Lists/#22982" class="Datatype">Any</a> <a id="23128" href="/20.07/Lists/#22997" class="Bound">P</a> <a id="23130" href="/20.07/Lists/#23109" class="Bound">xs</a> <a id="23133" class="Symbol">→</a> <a id="23135" href="/20.07/Lists/#22982" class="Datatype">Any</a> <a id="23139" href="/20.07/Lists/#22997" class="Bound">P</a> <a id="23141" class="Symbol">(</a><a id="23142" href="/20.07/Lists/#23101" class="Bound">x</a> <a id="23144" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="23146" href="/20.07/Lists/#23109" class="Bound">xs</a><a id="23148" class="Symbol">)</a>
</pre>
<p>The first constructor provides evidence that the head of the list
satisfies <code class="language-plaintext highlighter-rouge">P</code>, while the second provides evidence that some element of
the tail of the list satisfies <code class="language-plaintext highlighter-rouge">P</code>. For example, we can define list
membership as follows:</p>
<pre class="Agda"><a id="23387" class="Keyword">infix</a> <a id="23393" class="Number">4</a> <a id="23395" href="/20.07/Lists/#23404" class="Function Operator">_∈_</a> <a id="23399" href="/20.07/Lists/#23474" class="Function Operator">_∉_</a>
<a id="_∈_"></a><a id="23404" href="/20.07/Lists/#23404" class="Function Operator">_∈_</a> <a id="23408" class="Symbol">:</a> <a id="23410" class="Symbol">∀</a> <a id="23412" class="Symbol">{</a><a id="23413" href="/20.07/Lists/#23413" class="Bound">A</a> <a id="23415" class="Symbol">:</a> <a id="23417" class="PrimitiveType">Set</a><a id="23420" class="Symbol">}</a> <a id="23422" class="Symbol">(</a><a id="23423" href="/20.07/Lists/#23423" class="Bound">x</a> <a id="23425" class="Symbol">:</a> <a id="23427" href="/20.07/Lists/#23413" class="Bound">A</a><a id="23428" class="Symbol">)</a> <a id="23430" class="Symbol">(</a><a id="23431" href="/20.07/Lists/#23431" class="Bound">xs</a> <a id="23434" class="Symbol">:</a> <a id="23436" href="/20.07/Lists/#1067" class="Datatype">List</a> <a id="23441" href="/20.07/Lists/#23413" class="Bound">A</a><a id="23442" class="Symbol">)</a> <a id="23444" class="Symbol">→</a> <a id="23446" class="PrimitiveType">Set</a>
<a id="23450" href="/20.07/Lists/#23450" class="Bound">x</a> <a id="23452" href="/20.07/Lists/#23404" class="Function Operator">∈</a> <a id="23454" href="/20.07/Lists/#23454" class="Bound">xs</a> <a id="23457" class="Symbol">=</a> <a id="23459" href="/20.07/Lists/#22982" class="Datatype">Any</a> <a id="23463" class="Symbol">(</a><a id="23464" href="/20.07/Lists/#23450" class="Bound">x</a> <a id="23466" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡_</a><a id="23468" class="Symbol">)</a> <a id="23470" href="/20.07/Lists/#23454" class="Bound">xs</a>
<a id="_∉_"></a><a id="23474" href="/20.07/Lists/#23474" class="Function Operator">_∉_</a> <a id="23478" class="Symbol">:</a> <a id="23480" class="Symbol">∀</a> <a id="23482" class="Symbol">{</a><a id="23483" href="/20.07/Lists/#23483" class="Bound">A</a> <a id="23485" class="Symbol">:</a> <a id="23487" class="PrimitiveType">Set</a><a id="23490" class="Symbol">}</a> <a id="23492" class="Symbol">(</a><a id="23493" href="/20.07/Lists/#23493" class="Bound">x</a> <a id="23495" class="Symbol">:</a> <a id="23497" href="/20.07/Lists/#23483" class="Bound">A</a><a id="23498" class="Symbol">)</a> <a id="23500" class="Symbol">(</a><a id="23501" href="/20.07/Lists/#23501" class="Bound">xs</a> <a id="23504" class="Symbol">:</a> <a id="23506" href="/20.07/Lists/#1067" class="Datatype">List</a> <a id="23511" href="/20.07/Lists/#23483" class="Bound">A</a><a id="23512" class="Symbol">)</a> <a id="23514" class="Symbol">→</a> <a id="23516" class="PrimitiveType">Set</a>
<a id="23520" href="/20.07/Lists/#23520" class="Bound">x</a> <a id="23522" href="/20.07/Lists/#23474" class="Function Operator">∉</a> <a id="23524" href="/20.07/Lists/#23524" class="Bound">xs</a> <a id="23527" class="Symbol">=</a> <a id="23529" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#535" class="Function Operator">¬</a> <a id="23531" class="Symbol">(</a><a id="23532" href="/20.07/Lists/#23520" class="Bound">x</a> <a id="23534" href="/20.07/Lists/#23404" class="Function Operator">∈</a> <a id="23536" href="/20.07/Lists/#23524" class="Bound">xs</a><a id="23538" class="Symbol">)</a>
</pre>
<p>For example, zero is an element of the list <code class="language-plaintext highlighter-rouge">[ 0 , 1 , 0 , 2 ]</code>. Indeed, we can demonstrate
this fact in two different ways, corresponding to the two different
occurrences of zero in the list, as the first element and as the third element:</p>
<pre class="Agda"><a id="23789" href="/20.07/Lists/#23789" class="Function">_</a> <a id="23791" class="Symbol">:</a> <a id="23793" class="Number">0</a> <a id="23795" href="/20.07/Lists/#23404" class="Function Operator">∈</a> <a id="23797" href="/20.07/Lists/#2920" class="InductiveConstructor Operator">[</a> <a id="23799" class="Number">0</a> <a id="23801" href="/20.07/Lists/#2920" class="InductiveConstructor Operator">,</a> <a id="23803" class="Number">1</a> <a id="23805" href="/20.07/Lists/#2920" class="InductiveConstructor Operator">,</a> <a id="23807" class="Number">0</a> <a id="23809" href="/20.07/Lists/#2920" class="InductiveConstructor Operator">,</a> <a id="23811" class="Number">2</a> <a id="23813" href="/20.07/Lists/#2920" class="InductiveConstructor Operator">]</a>
<a id="23815" class="Symbol">_</a> <a id="23817" class="Symbol">=</a> <a id="23819" href="/20.07/Lists/#23033" class="InductiveConstructor">here</a> <a id="23824" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a>
<a id="23830" href="/20.07/Lists/#23830" class="Function">_</a> <a id="23832" class="Symbol">:</a> <a id="23834" class="Number">0</a> <a id="23836" href="/20.07/Lists/#23404" class="Function Operator">∈</a> <a id="23838" href="/20.07/Lists/#2920" class="InductiveConstructor Operator">[</a> <a id="23840" class="Number">0</a> <a id="23842" href="/20.07/Lists/#2920" class="InductiveConstructor Operator">,</a> <a id="23844" class="Number">1</a> <a id="23846" href="/20.07/Lists/#2920" class="InductiveConstructor Operator">,</a> <a id="23848" class="Number">0</a> <a id="23850" href="/20.07/Lists/#2920" class="InductiveConstructor Operator">,</a> <a id="23852" class="Number">2</a> <a id="23854" href="/20.07/Lists/#2920" class="InductiveConstructor Operator">]</a>
<a id="23856" class="Symbol">_</a> <a id="23858" class="Symbol">=</a> <a id="23860" href="/20.07/Lists/#23090" class="InductiveConstructor">there</a> <a id="23866" class="Symbol">(</a><a id="23867" href="/20.07/Lists/#23090" class="InductiveConstructor">there</a> <a id="23873" class="Symbol">(</a><a id="23874" href="/20.07/Lists/#23033" class="InductiveConstructor">here</a> <a id="23879" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a><a id="23883" class="Symbol">))</a>
</pre>
<p>Further, we can demonstrate that three is not in the list, because
any possible proof that it is in the list leads to contradiction:</p>
<pre class="Agda"><a id="not-in"></a><a id="24027" href="/20.07/Lists/#24027" class="Function">not-in</a> <a id="24034" class="Symbol">:</a> <a id="24036" class="Number">3</a> <a id="24038" href="/20.07/Lists/#23474" class="Function Operator">∉</a> <a id="24040" href="/20.07/Lists/#2920" class="InductiveConstructor Operator">[</a> <a id="24042" class="Number">0</a> <a id="24044" href="/20.07/Lists/#2920" class="InductiveConstructor Operator">,</a> <a id="24046" class="Number">1</a> <a id="24048" href="/20.07/Lists/#2920" class="InductiveConstructor Operator">,</a> <a id="24050" class="Number">0</a> <a id="24052" href="/20.07/Lists/#2920" class="InductiveConstructor Operator">,</a> <a id="24054" class="Number">2</a> <a id="24056" href="/20.07/Lists/#2920" class="InductiveConstructor Operator">]</a>
<a id="24058" href="/20.07/Lists/#24027" class="Function">not-in</a> <a id="24065" class="Symbol">(</a><a id="24066" href="/20.07/Lists/#23033" class="InductiveConstructor">here</a> <a id="24071" class="Symbol">())</a>
<a id="24075" href="/20.07/Lists/#24027" class="Function">not-in</a> <a id="24082" class="Symbol">(</a><a id="24083" href="/20.07/Lists/#23090" class="InductiveConstructor">there</a> <a id="24089" class="Symbol">(</a><a id="24090" href="/20.07/Lists/#23033" class="InductiveConstructor">here</a> <a id="24095" class="Symbol">()))</a>
<a id="24100" href="/20.07/Lists/#24027" class="Function">not-in</a> <a id="24107" class="Symbol">(</a><a id="24108" href="/20.07/Lists/#23090" class="InductiveConstructor">there</a> <a id="24114" class="Symbol">(</a><a id="24115" href="/20.07/Lists/#23090" class="InductiveConstructor">there</a> <a id="24121" class="Symbol">(</a><a id="24122" href="/20.07/Lists/#23033" class="InductiveConstructor">here</a> <a id="24127" class="Symbol">())))</a>
<a id="24133" href="/20.07/Lists/#24027" class="Function">not-in</a> <a id="24140" class="Symbol">(</a><a id="24141" href="/20.07/Lists/#23090" class="InductiveConstructor">there</a> <a id="24147" class="Symbol">(</a><a id="24148" href="/20.07/Lists/#23090" class="InductiveConstructor">there</a> <a id="24154" class="Symbol">(</a><a id="24155" href="/20.07/Lists/#23090" class="InductiveConstructor">there</a> <a id="24161" class="Symbol">(</a><a id="24162" href="/20.07/Lists/#23033" class="InductiveConstructor">here</a> <a id="24167" class="Symbol">()))))</a>
<a id="24174" href="/20.07/Lists/#24027" class="Function">not-in</a> <a id="24181" class="Symbol">(</a><a id="24182" href="/20.07/Lists/#23090" class="InductiveConstructor">there</a> <a id="24188" class="Symbol">(</a><a id="24189" href="/20.07/Lists/#23090" class="InductiveConstructor">there</a> <a id="24195" class="Symbol">(</a><a id="24196" href="/20.07/Lists/#23090" class="InductiveConstructor">there</a> <a id="24202" class="Symbol">(</a><a id="24203" href="/20.07/Lists/#23090" class="InductiveConstructor">there</a> <a id="24209" class="Symbol">()))))</a>
</pre>
<p>The five occurrences of <code class="language-plaintext highlighter-rouge">()</code> attest to the fact that there is no
possible evidence for <code class="language-plaintext highlighter-rouge">3 ≡ 0</code>, <code class="language-plaintext highlighter-rouge">3 ≡ 1</code>, <code class="language-plaintext highlighter-rouge">3 ≡ 0</code>, <code class="language-plaintext highlighter-rouge">3 ≡ 2</code>, and
<code class="language-plaintext highlighter-rouge">3 ∈ []</code>, respectively.</p>
<h2 id="all-and-append">All and append</h2>
<p>A predicate holds for every element of one list appended to another if and
only if it holds for every element of both lists:</p>
<pre class="Agda"><a id="All-++-⇔"></a><a id="24520" href="/20.07/Lists/#24520" class="Function">All-++-⇔</a> <a id="24529" class="Symbol">:</a> <a id="24531" class="Symbol">∀</a> <a id="24533" class="Symbol">{</a><a id="24534" href="/20.07/Lists/#24534" class="Bound">A</a> <a id="24536" class="Symbol">:</a> <a id="24538" class="PrimitiveType">Set</a><a id="24541" class="Symbol">}</a> <a id="24543" class="Symbol">{</a><a id="24544" href="/20.07/Lists/#24544" class="Bound">P</a> <a id="24546" class="Symbol">:</a> <a id="24548" href="/20.07/Lists/#24534" class="Bound">A</a> <a id="24550" class="Symbol">→</a> <a id="24552" class="PrimitiveType">Set</a><a id="24555" class="Symbol">}</a> <a id="24557" class="Symbol">(</a><a id="24558" href="/20.07/Lists/#24558" class="Bound">xs</a> <a id="24561" href="/20.07/Lists/#24561" class="Bound">ys</a> <a id="24564" class="Symbol">:</a> <a id="24566" href="/20.07/Lists/#1067" class="Datatype">List</a> <a id="24571" href="/20.07/Lists/#24534" class="Bound">A</a><a id="24572" class="Symbol">)</a> <a id="24574" class="Symbol">→</a>
<a id="24578" href="/20.07/Lists/#21529" class="Datatype">All</a> <a id="24582" href="/20.07/Lists/#24544" class="Bound">P</a> <a id="24584" class="Symbol">(</a><a id="24585" href="/20.07/Lists/#24558" class="Bound">xs</a> <a id="24588" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="24591" href="/20.07/Lists/#24561" class="Bound">ys</a><a id="24593" class="Symbol">)</a> <a id="24595" href="/20.07/Isomorphism/#12042" class="Record Operator">⇔</a> <a id="24597" class="Symbol">(</a><a id="24598" href="/20.07/Lists/#21529" class="Datatype">All</a> <a id="24602" href="/20.07/Lists/#24544" class="Bound">P</a> <a id="24604" href="/20.07/Lists/#24558" class="Bound">xs</a> <a id="24607" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1162" class="Function Operator">×</a> <a id="24609" href="/20.07/Lists/#21529" class="Datatype">All</a> <a id="24613" href="/20.07/Lists/#24544" class="Bound">P</a> <a id="24615" href="/20.07/Lists/#24561" class="Bound">ys</a><a id="24617" class="Symbol">)</a>
<a id="24619" href="/20.07/Lists/#24520" class="Function">All-++-⇔</a> <a id="24628" href="/20.07/Lists/#24628" class="Bound">xs</a> <a id="24631" href="/20.07/Lists/#24631" class="Bound">ys</a> <a id="24634" class="Symbol">=</a>
<a id="24638" class="Keyword">record</a>
<a id="24649" class="Symbol">{</a> <a id="24651" href="/20.07/Isomorphism/#12082" class="Field">to</a> <a id="24660" class="Symbol">=</a> <a id="24663" href="/20.07/Lists/#24718" class="Function">to</a> <a id="24666" href="/20.07/Lists/#24628" class="Bound">xs</a> <a id="24669" href="/20.07/Lists/#24631" class="Bound">ys</a>
<a id="24676" class="Symbol">;</a> <a id="24678" href="/20.07/Isomorphism/#12099" class="Field">from</a> <a id="24687" class="Symbol">=</a> <a id="24690" href="/20.07/Lists/#24943" class="Function">from</a> <a id="24695" href="/20.07/Lists/#24628" class="Bound">xs</a> <a id="24698" href="/20.07/Lists/#24631" class="Bound">ys</a>
<a id="24705" class="Symbol">}</a>
<a id="24709" class="Keyword">where</a>
<a id="24718" href="/20.07/Lists/#24718" class="Function">to</a> <a id="24721" class="Symbol">:</a> <a id="24723" class="Symbol">∀</a> <a id="24725" class="Symbol">{</a><a id="24726" href="/20.07/Lists/#24726" class="Bound">A</a> <a id="24728" class="Symbol">:</a> <a id="24730" class="PrimitiveType">Set</a><a id="24733" class="Symbol">}</a> <a id="24735" class="Symbol">{</a><a id="24736" href="/20.07/Lists/#24736" class="Bound">P</a> <a id="24738" class="Symbol">:</a> <a id="24740" href="/20.07/Lists/#24726" class="Bound">A</a> <a id="24742" class="Symbol">→</a> <a id="24744" class="PrimitiveType">Set</a><a id="24747" class="Symbol">}</a> <a id="24749" class="Symbol">(</a><a id="24750" href="/20.07/Lists/#24750" class="Bound">xs</a> <a id="24753" href="/20.07/Lists/#24753" class="Bound">ys</a> <a id="24756" class="Symbol">:</a> <a id="24758" href="/20.07/Lists/#1067" class="Datatype">List</a> <a id="24763" href="/20.07/Lists/#24726" class="Bound">A</a><a id="24764" class="Symbol">)</a> <a id="24766" class="Symbol">→</a>
<a id="24772" href="/20.07/Lists/#21529" class="Datatype">All</a> <a id="24776" href="/20.07/Lists/#24736" class="Bound">P</a> <a id="24778" class="Symbol">(</a><a id="24779" href="/20.07/Lists/#24750" class="Bound">xs</a> <a id="24782" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="24785" href="/20.07/Lists/#24753" class="Bound">ys</a><a id="24787" class="Symbol">)</a> <a id="24789" class="Symbol">→</a> <a id="24791" class="Symbol">(</a><a id="24792" href="/20.07/Lists/#21529" class="Datatype">All</a> <a id="24796" href="/20.07/Lists/#24736" class="Bound">P</a> <a id="24798" href="/20.07/Lists/#24750" class="Bound">xs</a> <a id="24801" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1162" class="Function Operator">×</a> <a id="24803" href="/20.07/Lists/#21529" class="Datatype">All</a> <a id="24807" href="/20.07/Lists/#24736" class="Bound">P</a> <a id="24809" href="/20.07/Lists/#24753" class="Bound">ys</a><a id="24811" class="Symbol">)</a>
<a id="24815" href="/20.07/Lists/#24718" class="Function">to</a> <a id="24818" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a> <a id="24821" href="/20.07/Lists/#24821" class="Bound">ys</a> <a id="24824" href="/20.07/Lists/#24824" class="Bound">Pys</a> <a id="24828" class="Symbol">=</a> <a id="24830" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="24832" href="/20.07/Lists/#21580" class="InductiveConstructor">[]</a> <a id="24835" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="24837" href="/20.07/Lists/#24824" class="Bound">Pys</a> <a id="24841" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="24845" href="/20.07/Lists/#24718" class="Function">to</a> <a id="24848" class="Symbol">(</a><a id="24849" href="/20.07/Lists/#24849" class="Bound">x</a> <a id="24851" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="24853" href="/20.07/Lists/#24853" class="Bound">xs</a><a id="24855" class="Symbol">)</a> <a id="24857" href="/20.07/Lists/#24857" class="Bound">ys</a> <a id="24860" class="Symbol">(</a><a id="24861" href="/20.07/Lists/#24861" class="Bound">Px</a> <a id="24864" href="/20.07/Lists/#21597" class="InductiveConstructor Operator">∷</a> <a id="24866" href="/20.07/Lists/#24866" class="Bound">Pxs++ys</a><a id="24873" class="Symbol">)</a> <a id="24875" class="Keyword">with</a> <a id="24880" href="/20.07/Lists/#24718" class="Function">to</a> <a id="24883" href="/20.07/Lists/#24853" class="Bound">xs</a> <a id="24886" href="/20.07/Lists/#24857" class="Bound">ys</a> <a id="24889" href="/20.07/Lists/#24866" class="Bound">Pxs++ys</a>
<a id="24899" class="Symbol">...</a> <a id="24903" class="Symbol">|</a> <a id="24905" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="24907" href="/20.07/Lists/#24907" class="Bound">Pxs</a> <a id="24911" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="24913" href="/20.07/Lists/#24913" class="Bound">Pys</a> <a id="24917" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="24919" class="Symbol">=</a> <a id="24921" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="24923" class="Bound">Px</a> <a id="24926" href="/20.07/Lists/#21597" class="InductiveConstructor Operator">∷</a> <a id="24928" href="/20.07/Lists/#24907" class="Bound">Pxs</a> <a id="24932" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="24934" href="/20.07/Lists/#24913" class="Bound">Pys</a> <a id="24938" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="24943" href="/20.07/Lists/#24943" class="Function">from</a> <a id="24948" class="Symbol">:</a> <a id="24950" class="Symbol">∀</a> <a id="24952" class="Symbol">{</a> <a id="24954" href="/20.07/Lists/#24954" class="Bound">A</a> <a id="24956" class="Symbol">:</a> <a id="24958" class="PrimitiveType">Set</a><a id="24961" class="Symbol">}</a> <a id="24963" class="Symbol">{</a><a id="24964" href="/20.07/Lists/#24964" class="Bound">P</a> <a id="24966" class="Symbol">:</a> <a id="24968" href="/20.07/Lists/#24954" class="Bound">A</a> <a id="24970" class="Symbol">→</a> <a id="24972" class="PrimitiveType">Set</a><a id="24975" class="Symbol">}</a> <a id="24977" class="Symbol">(</a><a id="24978" href="/20.07/Lists/#24978" class="Bound">xs</a> <a id="24981" href="/20.07/Lists/#24981" class="Bound">ys</a> <a id="24984" class="Symbol">:</a> <a id="24986" href="/20.07/Lists/#1067" class="Datatype">List</a> <a id="24991" href="/20.07/Lists/#24954" class="Bound">A</a><a id="24992" class="Symbol">)</a> <a id="24994" class="Symbol">→</a>
<a id="25000" href="/20.07/Lists/#21529" class="Datatype">All</a> <a id="25004" href="/20.07/Lists/#24964" class="Bound">P</a> <a id="25006" href="/20.07/Lists/#24978" class="Bound">xs</a> <a id="25009" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1162" class="Function Operator">×</a> <a id="25011" href="/20.07/Lists/#21529" class="Datatype">All</a> <a id="25015" href="/20.07/Lists/#24964" class="Bound">P</a> <a id="25017" href="/20.07/Lists/#24981" class="Bound">ys</a> <a id="25020" class="Symbol">→</a> <a id="25022" href="/20.07/Lists/#21529" class="Datatype">All</a> <a id="25026" href="/20.07/Lists/#24964" class="Bound">P</a> <a id="25028" class="Symbol">(</a><a id="25029" href="/20.07/Lists/#24978" class="Bound">xs</a> <a id="25032" href="/20.07/Lists/#3467" class="Function Operator">++</a> <a id="25035" href="/20.07/Lists/#24981" class="Bound">ys</a><a id="25037" class="Symbol">)</a>
<a id="25041" href="/20.07/Lists/#24943" class="Function">from</a> <a id="25046" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a> <a id="25049" href="/20.07/Lists/#25049" class="Bound">ys</a> <a id="25052" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="25054" href="/20.07/Lists/#21580" class="InductiveConstructor">[]</a> <a id="25057" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="25059" href="/20.07/Lists/#25059" class="Bound">Pys</a> <a id="25063" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="25065" class="Symbol">=</a> <a id="25067" href="/20.07/Lists/#25059" class="Bound">Pys</a>
<a id="25073" href="/20.07/Lists/#24943" class="Function">from</a> <a id="25078" class="Symbol">(</a><a id="25079" href="/20.07/Lists/#25079" class="Bound">x</a> <a id="25081" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="25083" href="/20.07/Lists/#25083" class="Bound">xs</a><a id="25085" class="Symbol">)</a> <a id="25087" href="/20.07/Lists/#25087" class="Bound">ys</a> <a id="25090" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="25092" href="/20.07/Lists/#25092" class="Bound">Px</a> <a id="25095" href="/20.07/Lists/#21597" class="InductiveConstructor Operator">∷</a> <a id="25097" href="/20.07/Lists/#25097" class="Bound">Pxs</a> <a id="25101" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="25103" href="/20.07/Lists/#25103" class="Bound">Pys</a> <a id="25107" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="25109" class="Symbol">=</a> <a id="25112" href="/20.07/Lists/#25092" class="Bound">Px</a> <a id="25115" href="/20.07/Lists/#21597" class="InductiveConstructor Operator">∷</a> <a id="25117" href="/20.07/Lists/#24943" class="Function">from</a> <a id="25122" href="/20.07/Lists/#25083" class="Bound">xs</a> <a id="25125" href="/20.07/Lists/#25087" class="Bound">ys</a> <a id="25128" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="25130" href="/20.07/Lists/#25097" class="Bound">Pxs</a> <a id="25134" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="25136" href="/20.07/Lists/#25103" class="Bound">Pys</a> <a id="25140" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
</pre>
<h4 id="exercise-any---recommended">Exercise <code class="language-plaintext highlighter-rouge">Any-++-⇔</code> (recommended)</h4>
<p>Prove a result similar to <code class="language-plaintext highlighter-rouge">All-++-⇔</code>, but with <code class="language-plaintext highlighter-rouge">Any</code> in place of <code class="language-plaintext highlighter-rouge">All</code>, and a suitable
replacement for <code class="language-plaintext highlighter-rouge">_×_</code>. As a consequence, demonstrate an equivalence relating
<code class="language-plaintext highlighter-rouge">_∈_</code> and <code class="language-plaintext highlighter-rouge">_++_</code>.</p>
<pre class="Agda"><a id="25375" class="Comment">-- Your code goes here</a>
</pre>
<h4 id="exercise-all---stretch">Exercise <code class="language-plaintext highlighter-rouge">All-++-≃</code> (stretch)</h4>
<p>Show that the equivalence <code class="language-plaintext highlighter-rouge">All-++-⇔</code> can be extended to an isomorphism.</p>
<pre class="Agda"><a id="25516" class="Comment">-- Your code goes here</a>
</pre>
<h4 id="exercise-anyall-recommended">Exercise <code class="language-plaintext highlighter-rouge">¬Any⇔All¬</code> (recommended)</h4>
<p>Show that <code class="language-plaintext highlighter-rouge">Any</code> and <code class="language-plaintext highlighter-rouge">All</code> satisfy a version of De Morgan’s Law:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>(¬_ ∘ Any P) xs ⇔ All (¬_ ∘ P) xs
</code></pre></div></div>
<p>(Can you see why it is important that here <code class="language-plaintext highlighter-rouge">_∘_</code> is generalised
to arbitrary levels, as described in the section on
<a href="/20.07/Equality/#unipoly">universe polymorphism</a>?)</p>
<p>Do we also have the following?</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>(¬_ ∘ All P) xs ⇔ Any (¬_ ∘ P) xs
</code></pre></div></div>
<p>If so, prove; if not, explain why.</p>
<pre class="Agda"><a id="25982" class="Comment">-- Your code goes here</a>
</pre>
<h4 id="exercise-anyall-stretch">Exercise <code class="language-plaintext highlighter-rouge">¬Any≃All¬</code> (stretch)</h4>
<p>Show that the equivalence <code class="language-plaintext highlighter-rouge">¬Any⇔All¬</code> can be extended to an isomorphism.
You will need to use extensionality.</p>
<pre class="Agda"><a id="26162" class="Comment">-- Your code goes here</a>
</pre>
<h4 id="exercise-all--practice">Exercise <code class="language-plaintext highlighter-rouge">All-∀</code> (practice)</h4>
<p>Show that <code class="language-plaintext highlighter-rouge">All P xs</code> is isomorphic to <code class="language-plaintext highlighter-rouge">∀ {x} → x ∈ xs → P x</code>.</p>
<pre class="Agda"><a id="26291" class="Comment">-- You code goes here</a>
</pre>
<h4 id="exercise-any--practice">Exercise <code class="language-plaintext highlighter-rouge">Any-∃</code> (practice)</h4>
<p>Show that <code class="language-plaintext highlighter-rouge">Any P xs</code> is isomorphic to <code class="language-plaintext highlighter-rouge">∃[ x ] (x ∈ xs × P x)</code>.</p>
<pre class="Agda"><a id="26421" class="Comment">-- You code goes here</a>
</pre>
<h2 id="decidability-of-all">Decidability of All</h2>
<p>If we consider a predicate as a function that yields a boolean,
it is easy to define an analogue of <code class="language-plaintext highlighter-rouge">All</code>, which returns true if
a given predicate returns true for every element of a list:</p>
<pre class="Agda"><a id="all"></a><a id="26666" href="/20.07/Lists/#26666" class="Function">all</a> <a id="26670" class="Symbol">:</a> <a id="26672" class="Symbol">∀</a> <a id="26674" class="Symbol">{</a><a id="26675" href="/20.07/Lists/#26675" class="Bound">A</a> <a id="26677" class="Symbol">:</a> <a id="26679" class="PrimitiveType">Set</a><a id="26682" class="Symbol">}</a> <a id="26684" class="Symbol">→</a> <a id="26686" class="Symbol">(</a><a id="26687" href="/20.07/Lists/#26675" class="Bound">A</a> <a id="26689" class="Symbol">→</a> <a id="26691" href="Agda.Builtin.Bool.html#135" class="Datatype">Bool</a><a id="26695" class="Symbol">)</a> <a id="26697" class="Symbol">→</a> <a id="26699" href="/20.07/Lists/#1067" class="Datatype">List</a> <a id="26704" href="/20.07/Lists/#26675" class="Bound">A</a> <a id="26706" class="Symbol">→</a> <a id="26708" href="Agda.Builtin.Bool.html#135" class="Datatype">Bool</a>
<a id="26713" href="/20.07/Lists/#26666" class="Function">all</a> <a id="26717" href="/20.07/Lists/#26717" class="Bound">p</a> <a id="26720" class="Symbol">=</a> <a id="26723" href="/20.07/Lists/#15291" class="Function">foldr</a> <a id="26729" href="https://agda.github.io/agda-stdlib/v1.1/Data.Bool.Base.html#1015" class="Function Operator">_∧_</a> <a id="26733" href="Agda.Builtin.Bool.html#160" class="InductiveConstructor">true</a> <a id="26738" href="https://agda.github.io/agda-stdlib/v1.1/Function.html#1099" class="Function Operator">∘</a> <a id="26740" href="/20.07/Lists/#12865" class="Function">map</a> <a id="26744" href="/20.07/Lists/#26717" class="Bound">p</a>
</pre>
<p>The function can be written in a particularly compact style by
using the higher-order functions <code class="language-plaintext highlighter-rouge">map</code> and <code class="language-plaintext highlighter-rouge">foldr</code>.</p>
<p>As one would hope, if we replace booleans by decidables there is again
an analogue of <code class="language-plaintext highlighter-rouge">All</code>. First, return to the notion of a predicate <code class="language-plaintext highlighter-rouge">P</code> as
a function of type <code class="language-plaintext highlighter-rouge">A → Set</code>, taking a value <code class="language-plaintext highlighter-rouge">x</code> of type <code class="language-plaintext highlighter-rouge">A</code> into evidence
<code class="language-plaintext highlighter-rouge">P x</code> that a property holds for <code class="language-plaintext highlighter-rouge">x</code>. Say that a predicate <code class="language-plaintext highlighter-rouge">P</code> is <em>decidable</em>
if we have a function that for a given <code class="language-plaintext highlighter-rouge">x</code> can decide <code class="language-plaintext highlighter-rouge">P x</code>:</p>
<pre class="Agda"><a id="Decidable"></a><a id="27228" href="/20.07/Lists/#27228" class="Function">Decidable</a> <a id="27238" class="Symbol">:</a> <a id="27240" class="Symbol">∀</a> <a id="27242" class="Symbol">{</a><a id="27243" href="/20.07/Lists/#27243" class="Bound">A</a> <a id="27245" class="Symbol">:</a> <a id="27247" class="PrimitiveType">Set</a><a id="27250" class="Symbol">}</a> <a id="27252" class="Symbol">→</a> <a id="27254" class="Symbol">(</a><a id="27255" href="/20.07/Lists/#27243" class="Bound">A</a> <a id="27257" class="Symbol">→</a> <a id="27259" class="PrimitiveType">Set</a><a id="27262" class="Symbol">)</a> <a id="27264" class="Symbol">→</a> <a id="27266" class="PrimitiveType">Set</a>
<a id="27270" href="/20.07/Lists/#27228" class="Function">Decidable</a> <a id="27280" class="Symbol">{</a><a id="27281" href="/20.07/Lists/#27281" class="Bound">A</a><a id="27282" class="Symbol">}</a> <a id="27284" href="/20.07/Lists/#27284" class="Bound">P</a> <a id="27287" class="Symbol">=</a> <a id="27290" class="Symbol">∀</a> <a id="27292" class="Symbol">(</a><a id="27293" href="/20.07/Lists/#27293" class="Bound">x</a> <a id="27295" class="Symbol">:</a> <a id="27297" href="/20.07/Lists/#27281" class="Bound">A</a><a id="27298" class="Symbol">)</a> <a id="27300" class="Symbol">→</a> <a id="27302" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#605" class="Datatype">Dec</a> <a id="27306" class="Symbol">(</a><a id="27307" href="/20.07/Lists/#27284" class="Bound">P</a> <a id="27309" href="/20.07/Lists/#27293" class="Bound">x</a><a id="27310" class="Symbol">)</a>
</pre>
<p>Then if predicate <code class="language-plaintext highlighter-rouge">P</code> is decidable, it is also decidable whether every
element of a list satisfies the predicate:</p>
<pre class="Agda"><a id="All?"></a><a id="27434" href="/20.07/Lists/#27434" class="Function">All?</a> <a id="27439" class="Symbol">:</a> <a id="27441" class="Symbol">∀</a> <a id="27443" class="Symbol">{</a><a id="27444" href="/20.07/Lists/#27444" class="Bound">A</a> <a id="27446" class="Symbol">:</a> <a id="27448" class="PrimitiveType">Set</a><a id="27451" class="Symbol">}</a> <a id="27453" class="Symbol">{</a><a id="27454" href="/20.07/Lists/#27454" class="Bound">P</a> <a id="27456" class="Symbol">:</a> <a id="27458" href="/20.07/Lists/#27444" class="Bound">A</a> <a id="27460" class="Symbol">→</a> <a id="27462" class="PrimitiveType">Set</a><a id="27465" class="Symbol">}</a> <a id="27467" class="Symbol">→</a> <a id="27469" href="/20.07/Lists/#27228" class="Function">Decidable</a> <a id="27479" href="/20.07/Lists/#27454" class="Bound">P</a> <a id="27481" class="Symbol">→</a> <a id="27483" href="/20.07/Lists/#27228" class="Function">Decidable</a> <a id="27493" class="Symbol">(</a><a id="27494" href="/20.07/Lists/#21529" class="Datatype">All</a> <a id="27498" href="/20.07/Lists/#27454" class="Bound">P</a><a id="27499" class="Symbol">)</a>
<a id="27501" href="/20.07/Lists/#27434" class="Function">All?</a> <a id="27506" href="/20.07/Lists/#27506" class="Bound">P?</a> <a id="27509" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a> <a id="27544" class="Symbol">=</a> <a id="27547" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a> <a id="27551" href="/20.07/Lists/#21580" class="InductiveConstructor">[]</a>
<a id="27554" href="/20.07/Lists/#27434" class="Function">All?</a> <a id="27559" href="/20.07/Lists/#27559" class="Bound">P?</a> <a id="27562" class="Symbol">(</a><a id="27563" href="/20.07/Lists/#27563" class="Bound">x</a> <a id="27565" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="27567" href="/20.07/Lists/#27567" class="Bound">xs</a><a id="27569" class="Symbol">)</a> <a id="27571" class="Keyword">with</a> <a id="27576" href="/20.07/Lists/#27559" class="Bound">P?</a> <a id="27579" href="/20.07/Lists/#27563" class="Bound">x</a> <a id="27583" class="Symbol">|</a> <a id="27585" href="/20.07/Lists/#27434" class="Function">All?</a> <a id="27590" href="/20.07/Lists/#27559" class="Bound">P?</a> <a id="27593" href="/20.07/Lists/#27567" class="Bound">xs</a>
<a id="27596" class="Symbol">...</a> <a id="27616" class="Symbol">|</a> <a id="27618" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a> <a id="27622" href="/20.07/Lists/#27622" class="Bound">Px</a> <a id="27625" class="Symbol">|</a> <a id="27627" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a> <a id="27631" href="/20.07/Lists/#27631" class="Bound">Pxs</a> <a id="27639" class="Symbol">=</a> <a id="27642" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a> <a id="27646" class="Symbol">(</a><a id="27647" href="/20.07/Lists/#27622" class="Bound">Px</a> <a id="27650" href="/20.07/Lists/#21597" class="InductiveConstructor Operator">∷</a> <a id="27652" href="/20.07/Lists/#27631" class="Bound">Pxs</a><a id="27655" class="Symbol">)</a>
<a id="27657" class="Symbol">...</a> <a id="27677" class="Symbol">|</a> <a id="27679" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="27682" href="/20.07/Lists/#27682" class="Bound">¬Px</a> <a id="27686" class="Symbol">|</a> <a id="27688" class="Symbol">_</a> <a id="27700" class="Symbol">=</a> <a id="27703" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="27706" class="Symbol">λ{</a> <a id="27709" class="Symbol">(</a><a id="27710" href="/20.07/Lists/#27710" class="Bound">Px</a> <a id="27713" href="/20.07/Lists/#21597" class="InductiveConstructor Operator">∷</a> <a id="27715" href="/20.07/Lists/#27715" class="Bound">Pxs</a><a id="27718" class="Symbol">)</a> <a id="27720" class="Symbol">→</a> <a id="27722" href="/20.07/Lists/#27682" class="Bound">¬Px</a> <a id="27726" href="/20.07/Lists/#27710" class="Bound">Px</a> <a id="27731" class="Symbol">}</a>
<a id="27733" class="CatchallClause Symbol">...</a><a id="27736" class="CatchallClause"> </a><a id="27753" class="CatchallClause Symbol">|</a><a id="27754" class="CatchallClause"> </a><a id="27755" class="CatchallClause Symbol">_</a><a id="27756" class="CatchallClause"> </a><a id="27762" class="CatchallClause Symbol">|</a><a id="27763" class="CatchallClause"> </a><a id="27764" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="CatchallClause InductiveConstructor">no</a><a id="27766" class="CatchallClause"> </a><a id="27767" href="/20.07/Lists/#27767" class="CatchallClause Bound">¬Pxs</a> <a id="27776" class="Symbol">=</a> <a id="27779" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="27782" class="Symbol">λ{</a> <a id="27785" class="Symbol">(</a><a id="27786" href="/20.07/Lists/#27786" class="Bound">Px</a> <a id="27789" href="/20.07/Lists/#21597" class="InductiveConstructor Operator">∷</a> <a id="27791" href="/20.07/Lists/#27791" class="Bound">Pxs</a><a id="27794" class="Symbol">)</a> <a id="27796" class="Symbol">→</a> <a id="27798" href="/20.07/Lists/#27767" class="Bound">¬Pxs</a> <a id="27803" href="/20.07/Lists/#27791" class="Bound">Pxs</a> <a id="27807" class="Symbol">}</a>
</pre>
<p>If the list is empty, then trivially <code class="language-plaintext highlighter-rouge">P</code> holds for every element of
the list. Otherwise, the structure of the proof is similar to that
showing that the conjunction of two decidable propositions is itself
decidable, using <code class="language-plaintext highlighter-rouge">_∷_</code> rather than <code class="language-plaintext highlighter-rouge">⟨_,_⟩</code> to combine the evidence for
the head and tail of the list.</p>
<h4 id="exercise-any-stretch">Exercise <code class="language-plaintext highlighter-rouge">Any?</code> (stretch)</h4>
<p>Just as <code class="language-plaintext highlighter-rouge">All</code> has analogues <code class="language-plaintext highlighter-rouge">all</code> and <code class="language-plaintext highlighter-rouge">All?</code> which determine whether a
predicate holds for every element of a list, so does <code class="language-plaintext highlighter-rouge">Any</code> have
analogues <code class="language-plaintext highlighter-rouge">any</code> and <code class="language-plaintext highlighter-rouge">Any?</code> which determine whether a predicate holds
for some element of a list. Give their definitions.</p>
<pre class="Agda"><a id="28416" class="Comment">-- Your code goes here</a>
</pre>
<h4 id="exercise-split-stretch">Exercise <code class="language-plaintext highlighter-rouge">split</code> (stretch)</h4>
<p>The relation <code class="language-plaintext highlighter-rouge">merge</code> holds when two lists merge to give a third list.</p>
<pre class="Agda"><a id="28552" class="Keyword">data</a> <a id="merge"></a><a id="28557" href="/20.07/Lists/#28557" class="Datatype">merge</a> <a id="28563" class="Symbol">{</a><a id="28564" href="/20.07/Lists/#28564" class="Bound">A</a> <a id="28566" class="Symbol">:</a> <a id="28568" class="PrimitiveType">Set</a><a id="28571" class="Symbol">}</a> <a id="28573" class="Symbol">:</a> <a id="28575" class="Symbol">(</a><a id="28576" href="/20.07/Lists/#28576" class="Bound">xs</a> <a id="28579" href="/20.07/Lists/#28579" class="Bound">ys</a> <a id="28582" href="/20.07/Lists/#28582" class="Bound">zs</a> <a id="28585" class="Symbol">:</a> <a id="28587" href="/20.07/Lists/#1067" class="Datatype">List</a> <a id="28592" href="/20.07/Lists/#28564" class="Bound">A</a><a id="28593" class="Symbol">)</a> <a id="28595" class="Symbol">→</a> <a id="28597" class="PrimitiveType">Set</a> <a id="28601" class="Keyword">where</a>
<a id="merge.[]"></a><a id="28610" href="/20.07/Lists/#28610" class="InductiveConstructor">[]</a> <a id="28613" class="Symbol">:</a>
<a id="28621" class="Comment">--------------</a>
<a id="28642" href="/20.07/Lists/#28557" class="Datatype">merge</a> <a id="28648" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a> <a id="28651" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a> <a id="28654" href="/20.07/Lists/#1096" class="InductiveConstructor">[]</a>
<a id="merge.left-∷"></a><a id="28660" href="/20.07/Lists/#28660" class="InductiveConstructor">left-∷</a> <a id="28667" class="Symbol">:</a> <a id="28669" class="Symbol">∀</a> <a id="28671" class="Symbol">{</a><a id="28672" href="/20.07/Lists/#28672" class="Bound">x</a> <a id="28674" href="/20.07/Lists/#28674" class="Bound">xs</a> <a id="28677" href="/20.07/Lists/#28677" class="Bound">ys</a> <a id="28680" href="/20.07/Lists/#28680" class="Bound">zs</a><a id="28682" class="Symbol">}</a>
<a id="28688" class="Symbol">→</a> <a id="28690" href="/20.07/Lists/#28557" class="Datatype">merge</a> <a id="28696" href="/20.07/Lists/#28674" class="Bound">xs</a> <a id="28699" href="/20.07/Lists/#28677" class="Bound">ys</a> <a id="28702" href="/20.07/Lists/#28680" class="Bound">zs</a>
<a id="28711" class="Comment">--------------------------</a>
<a id="28742" class="Symbol">→</a> <a id="28744" href="/20.07/Lists/#28557" class="Datatype">merge</a> <a id="28750" class="Symbol">(</a><a id="28751" href="/20.07/Lists/#28672" class="Bound">x</a> <a id="28753" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="28755" href="/20.07/Lists/#28674" class="Bound">xs</a><a id="28757" class="Symbol">)</a> <a id="28759" href="/20.07/Lists/#28677" class="Bound">ys</a> <a id="28762" class="Symbol">(</a><a id="28763" href="/20.07/Lists/#28672" class="Bound">x</a> <a id="28765" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="28767" href="/20.07/Lists/#28680" class="Bound">zs</a><a id="28769" class="Symbol">)</a>
<a id="merge.right-∷"></a><a id="28774" href="/20.07/Lists/#28774" class="InductiveConstructor">right-∷</a> <a id="28782" class="Symbol">:</a> <a id="28784" class="Symbol">∀</a> <a id="28786" class="Symbol">{</a><a id="28787" href="/20.07/Lists/#28787" class="Bound">y</a> <a id="28789" href="/20.07/Lists/#28789" class="Bound">xs</a> <a id="28792" href="/20.07/Lists/#28792" class="Bound">ys</a> <a id="28795" href="/20.07/Lists/#28795" class="Bound">zs</a><a id="28797" class="Symbol">}</a>
<a id="28803" class="Symbol">→</a> <a id="28805" href="/20.07/Lists/#28557" class="Datatype">merge</a> <a id="28811" href="/20.07/Lists/#28789" class="Bound">xs</a> <a id="28814" href="/20.07/Lists/#28792" class="Bound">ys</a> <a id="28817" href="/20.07/Lists/#28795" class="Bound">zs</a>
<a id="28826" class="Comment">--------------------------</a>
<a id="28857" class="Symbol">→</a> <a id="28859" href="/20.07/Lists/#28557" class="Datatype">merge</a> <a id="28865" href="/20.07/Lists/#28789" class="Bound">xs</a> <a id="28868" class="Symbol">(</a><a id="28869" href="/20.07/Lists/#28787" class="Bound">y</a> <a id="28871" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="28873" href="/20.07/Lists/#28792" class="Bound">ys</a><a id="28875" class="Symbol">)</a> <a id="28877" class="Symbol">(</a><a id="28878" href="/20.07/Lists/#28787" class="Bound">y</a> <a id="28880" href="/20.07/Lists/#1111" class="InductiveConstructor Operator">∷</a> <a id="28882" href="/20.07/Lists/#28795" class="Bound">zs</a><a id="28884" class="Symbol">)</a>
</pre>
<p>For example,</p>
<pre class="Agda"><a id="28908" href="/20.07/Lists/#28908" class="Function">_</a> <a id="28910" class="Symbol">:</a> <a id="28912" href="/20.07/Lists/#28557" class="Datatype">merge</a> <a id="28918" href="/20.07/Lists/#2850" class="InductiveConstructor Operator">[</a> <a id="28920" class="Number">1</a> <a id="28922" href="/20.07/Lists/#2850" class="InductiveConstructor Operator">,</a> <a id="28924" class="Number">4</a> <a id="28926" href="/20.07/Lists/#2850" class="InductiveConstructor Operator">]</a> <a id="28928" href="/20.07/Lists/#2850" class="InductiveConstructor Operator">[</a> <a id="28930" class="Number">2</a> <a id="28932" href="/20.07/Lists/#2850" class="InductiveConstructor Operator">,</a> <a id="28934" class="Number">3</a> <a id="28936" href="/20.07/Lists/#2850" class="InductiveConstructor Operator">]</a> <a id="28938" href="/20.07/Lists/#2920" class="InductiveConstructor Operator">[</a> <a id="28940" class="Number">1</a> <a id="28942" href="/20.07/Lists/#2920" class="InductiveConstructor Operator">,</a> <a id="28944" class="Number">2</a> <a id="28946" href="/20.07/Lists/#2920" class="InductiveConstructor Operator">,</a> <a id="28948" class="Number">3</a> <a id="28950" href="/20.07/Lists/#2920" class="InductiveConstructor Operator">,</a> <a id="28952" class="Number">4</a> <a id="28954" href="/20.07/Lists/#2920" class="InductiveConstructor Operator">]</a>
<a id="28956" class="Symbol">_</a> <a id="28958" class="Symbol">=</a> <a id="28960" href="/20.07/Lists/#28660" class="InductiveConstructor">left-∷</a> <a id="28967" class="Symbol">(</a><a id="28968" href="/20.07/Lists/#28774" class="InductiveConstructor">right-∷</a> <a id="28976" class="Symbol">(</a><a id="28977" href="/20.07/Lists/#28774" class="InductiveConstructor">right-∷</a> <a id="28985" class="Symbol">(</a><a id="28986" href="/20.07/Lists/#28660" class="InductiveConstructor">left-∷</a> <a id="28993" href="/20.07/Lists/#28610" class="InductiveConstructor">[]</a><a id="28995" class="Symbol">)))</a>
</pre>
<p>Given a decidable predicate and a list, we can split the list
into two lists that merge to give the original list, where all
elements of one list satisfy the predicate, and all elements of
the other do not satisfy the predicate.</p>
<p>Define the following variant of the traditional <code class="language-plaintext highlighter-rouge">filter</code> function on
lists, which given a decidable predicate and a list returns a list of
elements that satisfy the predicate and a list of elements that don’t,
with their corresponding proofs.</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>split : ∀ {A : Set} {P : A → Set} (P? : Decidable P) (zs : List A)
→ ∃[ xs ] ∃[ ys ] ( merge xs ys zs × All P xs × All (¬_ ∘ P) ys )
</code></pre></div></div>
<pre class="Agda"><a id="29627" 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="29763" class="Keyword">import</a> <a id="29770" href="https://agda.github.io/agda-stdlib/v1.1/Data.List.html" class="Module">Data.List</a> <a id="29780" class="Keyword">using</a> <a id="29786" class="Symbol">(</a><a id="29787" href="Agda.Builtin.List.html#121" class="Datatype">List</a><a id="29791" class="Symbol">;</a> <a id="29793" href="https://agda.github.io/agda-stdlib/v1.1/Data.List.Base.html#1570" class="Function Operator">_++_</a><a id="29797" class="Symbol">;</a> <a id="29799" href="https://agda.github.io/agda-stdlib/v1.1/Data.List.Base.html#4104" class="Function">length</a><a id="29805" class="Symbol">;</a> <a id="29807" href="https://agda.github.io/agda-stdlib/v1.1/Data.List.Base.html#8564" class="Function">reverse</a><a id="29814" class="Symbol">;</a> <a id="29816" href="https://agda.github.io/agda-stdlib/v1.1/Data.List.Base.html#1304" class="Function">map</a><a id="29819" class="Symbol">;</a> <a id="29821" href="https://agda.github.io/agda-stdlib/v1.1/Data.List.Base.html#3432" class="Function">foldr</a><a id="29826" class="Symbol">;</a> <a id="29828" href="https://agda.github.io/agda-stdlib/v1.1/Data.List.Base.html#5510" class="Function">downFrom</a><a id="29836" class="Symbol">)</a>
<a id="29838" class="Keyword">import</a> <a id="29845" href="https://agda.github.io/agda-stdlib/v1.1/Data.List.All.html" class="Module">Data.List.All</a> <a id="29859" class="Keyword">using</a> <a id="29865" class="Symbol">(</a><a id="29866" href="https://agda.github.io/agda-stdlib/v1.1/Data.List.Relation.Unary.All.html#1176" class="Datatype">All</a><a id="29869" class="Symbol">;</a> <a id="29871" href="https://agda.github.io/agda-stdlib/v1.1/Data.List.Relation.Unary.All.html#1239" class="InductiveConstructor">[]</a><a id="29873" class="Symbol">;</a> <a id="29875" href="https://agda.github.io/agda-stdlib/v1.1/Data.List.Relation.Unary.All.html#1256" class="InductiveConstructor Operator">_∷_</a><a id="29878" class="Symbol">)</a>
<a id="29880" class="Keyword">import</a> <a id="29887" href="https://agda.github.io/agda-stdlib/v1.1/Data.List.Any.html" class="Module">Data.List.Any</a> <a id="29901" class="Keyword">using</a> <a id="29907" class="Symbol">(</a><a id="29908" href="https://agda.github.io/agda-stdlib/v1.1/Data.List.Relation.Unary.Any.html#1052" class="Datatype">Any</a><a id="29911" class="Symbol">;</a> <a id="29913" href="https://agda.github.io/agda-stdlib/v1.1/Data.List.Relation.Unary.Any.html#1115" class="InductiveConstructor">here</a><a id="29917" class="Symbol">;</a> <a id="29919" href="https://agda.github.io/agda-stdlib/v1.1/Data.List.Relation.Unary.Any.html#1168" class="InductiveConstructor">there</a><a id="29924" class="Symbol">)</a>
<a id="29926" class="Keyword">import</a> <a id="29933" href="https://agda.github.io/agda-stdlib/v1.1/Data.List.Membership.Propositional.html" class="Module">Data.List.Membership.Propositional</a> <a id="29968" class="Keyword">using</a> <a id="29974" class="Symbol">(</a><a id="29975" href="https://agda.github.io/agda-stdlib/v1.1/Data.List.Membership.Setoid.html#877" class="Function Operator">_∈_</a><a id="29978" class="Symbol">)</a>
<a id="29980" class="Keyword">import</a> <a id="29987" href="https://agda.github.io/agda-stdlib/v1.1/Data.List.Properties.html" class="Module">Data.List.Properties</a>
<a id="30010" class="Keyword">using</a> <a id="30016" class="Symbol">(</a><a id="30017" href="https://agda.github.io/agda-stdlib/v1.1/Data.List.Properties.html#28549" class="Function">reverse-++-commute</a><a id="30035" class="Symbol">;</a> <a id="30037" href="https://agda.github.io/agda-stdlib/v1.1/Data.List.Properties.html#3412" class="Function">map-compose</a><a id="30048" class="Symbol">;</a> <a id="30050" href="https://agda.github.io/agda-stdlib/v1.1/Data.List.Properties.html#2721" class="Function">map-++-commute</a><a id="30064" class="Symbol">;</a> <a id="30066" href="https://agda.github.io/agda-stdlib/v1.1/Data.List.Properties.html#15835" class="Function">foldr-++</a><a id="30074" class="Symbol">)</a>
<a id="30078" class="Keyword">renaming</a> <a id="30087" class="Symbol">(</a><a id="30088" href="https://agda.github.io/agda-stdlib/v1.1/Data.List.Properties.html#35768" class="Function">mapIsFold</a> <a id="30098" class="Symbol">to</a> <a id="30101" href="https://agda.github.io/agda-stdlib/v1.1/Data.List.Properties.html#35768" class="Function">map-is-foldr</a><a id="30113" class="Symbol">)</a>
<a id="30115" class="Keyword">import</a> <a id="30122" href="https://agda.github.io/agda-stdlib/v1.1/Algebra.Structures.html" class="Module">Algebra.Structures</a> <a id="30141" class="Keyword">using</a> <a id="30147" class="Symbol">(</a><a id="30148" href="https://agda.github.io/agda-stdlib/v1.1/Algebra.Structures.html#2215" class="Record">IsMonoid</a><a id="30156" class="Symbol">)</a>
<a id="30158" class="Keyword">import</a> <a id="30165" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Unary.html" class="Module">Relation.Unary</a> <a id="30180" class="Keyword">using</a> <a id="30186" class="Symbol">(</a><a id="30187" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Unary.html#3474" class="Function">Decidable</a><a id="30196" class="Symbol">)</a>
<a id="30198" class="Keyword">import</a> <a id="30205" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.html" class="Module">Relation.Binary</a> <a id="30221" class="Keyword">using</a> <a id="30227" class="Symbol">(</a><a id="30228" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.Core.html#5557" class="Function">Decidable</a><a id="30237" class="Symbol">)</a>
</pre>
<p>The standard library version of <code class="language-plaintext highlighter-rouge">IsMonoid</code> differs from the
one given here, in that it is also parameterised on an equivalence relation.</p>
<p>Both <code class="language-plaintext highlighter-rouge">Relation.Unary</code> and <code class="language-plaintext highlighter-rouge">Relation.Binary</code> define a version of <code class="language-plaintext highlighter-rouge">Decidable</code>,
one for unary relations (as used in this chapter where <code class="language-plaintext highlighter-rouge">P</code> ranges over
unary predicates) and one for binary relations (as used earlier, where <code class="language-plaintext highlighter-rouge">_≤_</code>
ranges over a binary relation).</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+2237 PROPORTION (\::)
⊗ U+2297 CIRCLED TIMES (\otimes, \ox)
∈ U+2208 ELEMENT OF (\in)
∉ U+2209 NOT AN ELEMENT OF (\inn, \notin)
</code></pre></div></div>
</div>
<p style="text-align:center;">
<a alt="Previous chapter" href="/20.07/Decidable/">Prev</a>
&bullet;
<a alt="Source code" href="https://github.com/plfa/plfa.github.io/blob/dev-20.07/src/plfa/part1/Lists.lagda.md">Source</a>
&bullet;
<a alt="Next chapter" href="/20.07/Lambda/">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>
Reference in a new issue View git blame Copy permalink