leonv/bsc-leon-vatthauer
1
0
Fork 0
mirror of https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git synced 2024-05-31 07:28:34 +02:00
Code Issues Projects Releases Packages Wiki Activity
bsc-leon-vatthauer/public/Induction.html

62 lines
17 KiB
HTML
Raw Normal View History

Changed out to public
2023-08-19 16:11:22 +02:00
<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Induction</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Comment">------------------------------------------------------------------------</a>
<a id="74" class="Comment">-- The Agda standard library</a>
<a id="103" class="Comment">--</a>
<a id="106" class="Comment">-- An abstraction of various forms of recursion/induction</a>
<a id="164" class="Comment">------------------------------------------------------------------------</a>
<a id="238" class="Comment">-- The idea underlying Induction.* comes from Epigram 1, see Section 4</a>
<a id="309" class="Comment">-- of &quot;The view from the left&quot; by McBride and McKinna.</a>
<a id="365" class="Comment">-- Note: The types in this module can perhaps be easier to understand</a>
<a id="435" class="Comment">-- if they are normalised. Note also that Agda can do the</a>
<a id="493" class="Comment">-- normalisation for you.</a>
<a id="520" class="Symbol">{-#</a> <a id="524" class="Keyword">OPTIONS</a> <a id="532" class="Pragma">--cubical-compatible</a> <a id="553" class="Pragma">--safe</a> <a id="560" class="Symbol">#-}</a>
<a id="565" class="Keyword">module</a> <a id="572" href="Induction.html" class="Module">Induction</a> <a id="582" class="Keyword">where</a>
<a id="589" class="Keyword">open</a> <a id="594" class="Keyword">import</a> <a id="601" href="Level.html" class="Module">Level</a>
<a id="607" class="Keyword">open</a> <a id="612" class="Keyword">import</a> <a id="619" href="Relation.Unary.html" class="Module">Relation.Unary</a>
<a id="635" class="Comment">-- A RecStruct describes the allowed structure of recursion. The</a>
<a id="700" class="Comment">-- examples in Induction.Nat should explain what this is all about.</a>
<a id="RecStruct"></a><a id="769" href="Induction.html#769" class="Function">RecStruct</a> <a id="779" class="Symbol">:</a> <a id="781" class="Symbol">∀</a> <a id="783" class="Symbol">{</a><a id="784" href="Induction.html#784" class="Bound">a</a><a id="785" class="Symbol">}</a> <a id="787" class="Symbol">→</a> <a id="789" href="Agda.Primitive.html#320" class="Primitive">Set</a> <a id="793" href="Induction.html#784" class="Bound">a</a> <a id="795" class="Symbol">→</a> <a id="797" class="Symbol">(</a><a id="798" href="Induction.html#798" class="Bound">ℓ₁</a> <a id="801" href="Induction.html#801" class="Bound">ℓ₂</a> <a id="804" class="Symbol">:</a> <a id="806" href="Agda.Primitive.html#591" class="Postulate">Level</a><a id="811" class="Symbol">)</a> <a id="813" class="Symbol">→</a> <a id="815" href="Agda.Primitive.html#320" class="Primitive">Set</a> <a id="819" class="Symbol">_</a>
<a id="821" href="Induction.html#769" class="Function">RecStruct</a> <a id="831" href="Induction.html#831" class="Bound">A</a> <a id="833" href="Induction.html#833" class="Bound">ℓ₁</a> <a id="836" href="Induction.html#836" class="Bound">ℓ₂</a> <a id="839" class="Symbol">=</a> <a id="841" href="Relation.Unary.html#1110" class="Function">Pred</a> <a id="846" href="Induction.html#831" class="Bound">A</a> <a id="848" href="Induction.html#833" class="Bound">ℓ₁</a> <a id="851" class="Symbol">→</a> <a id="853" href="Relation.Unary.html#1110" class="Function">Pred</a> <a id="858" href="Induction.html#831" class="Bound">A</a> <a id="860" href="Induction.html#836" class="Bound">ℓ₂</a>
<a id="864" class="Comment">-- A recursor builder constructs an instance of a recursion structure</a>
<a id="934" class="Comment">-- for a given input.</a>
<a id="RecursorBuilder"></a><a id="957" href="Induction.html#957" class="Function">RecursorBuilder</a> <a id="973" class="Symbol">:</a> <a id="975" class="Symbol">∀</a> <a id="977" class="Symbol">{</a><a id="978" href="Induction.html#978" class="Bound">a</a> <a id="980" href="Induction.html#980" class="Bound">ℓ₁</a> <a id="983" href="Induction.html#983" class="Bound">ℓ₂</a><a id="985" class="Symbol">}</a> <a id="987" class="Symbol">{</a><a id="988" href="Induction.html#988" class="Bound">A</a> <a id="990" class="Symbol">:</a> <a id="992" href="Agda.Primitive.html#320" class="Primitive">Set</a> <a id="996" href="Induction.html#978" class="Bound">a</a><a id="997" class="Symbol">}</a> <a id="999" class="Symbol">→</a> <a id="1001" href="Induction.html#769" class="Function">RecStruct</a> <a id="1011" href="Induction.html#988" class="Bound">A</a> <a id="1013" href="Induction.html#980" class="Bound">ℓ₁</a> <a id="1016" href="Induction.html#983" class="Bound">ℓ₂</a> <a id="1019" class="Symbol">→</a> <a id="1021" href="Agda.Primitive.html#320" class="Primitive">Set</a> <a id="1025" class="Symbol">_</a>
<a id="1027" href="Induction.html#957" class="Function">RecursorBuilder</a> <a id="1043" href="Induction.html#1043" class="Bound">Rec</a> <a id="1047" class="Symbol">=</a> <a id="1049" class="Symbol">∀</a> <a id="1051" href="Induction.html#1051" class="Bound">P</a> <a id="1053" class="Symbol">→</a> <a id="1055" href="Induction.html#1043" class="Bound">Rec</a> <a id="1059" href="Induction.html#1051" class="Bound">P</a> <a id="1061" href="Relation.Unary.html#2345" class="Function Operator">⊆′</a> <a id="1064" href="Induction.html#1051" class="Bound">P</a> <a id="1066" class="Symbol">→</a> <a id="1068" href="Relation.Unary.html#3230" class="Function">Universal</a> <a id="1078" class="Symbol">(</a><a id="1079" href="Induction.html#1043" class="Bound">Rec</a> <a id="1083" href="Induction.html#1051" class="Bound">P</a><a id="1084" class="Symbol">)</a>
<a id="1087" class="Comment">-- A recursor can be used to actually compute/prove something useful.</a>
<a id="Recursor"></a><a id="1158" href="Induction.html#1158" class="Function">Recursor</a> <a id="1167" class="Symbol">:</a> <a id="1169" class="Symbol">∀</a> <a id="1171" class="Symbol">{</a><a id="1172" href="Induction.html#1172" class="Bound">a</a> <a id="1174" href="Induction.html#1174" class="Bound">ℓ₁</a> <a id="1177" href="Induction.html#1177" class="Bound">ℓ₂</a><a id="1179" class="Symbol">}</a> <a id="1181" class="Symbol">{</a><a id="1182" href="Induction.html#1182" class="Bound">A</a> <a id="1184" class="Symbol">:</a> <a id="1186" href="Agda.Primitive.html#320" class="Primitive">Set</a> <a id="1190" href="Induction.html#1172" class="Bound">a</a><a id="1191" class="Symbol">}</a> <a id="1193" class="Symbol">→</a> <a id="1195" href="Induction.html#769" class="Function">RecStruct</a> <a id="1205" href="Induction.html#1182" class="Bound">A</a> <a id="1207" href="Induction.html#1174" class="Bound">ℓ₁</a> <a id="1210" href="Induction.html#1177" class="Bound">ℓ₂</a> <a id="1213" class="Symbol">→</a> <a id="1215" href="Agda.Primitive.html#320" class="Primitive">Set</a> <a id="1219" class="Symbol">_</a>
<a id="1221" href="Induction.html#1158" class="Function">Recursor</a> <a id="1230" href="Induction.html#1230" class="Bound">Rec</a> <a id="1234" class="Symbol">=</a> <a id="1236" class="Symbol">∀</a> <a id="1238" href="Induction.html#1238" class="Bound">P</a> <a id="1240" class="Symbol">→</a> <a id="1242" href="Induction.html#1230" class="Bound">Rec</a> <a id="1246" href="Induction.html#1238" class="Bound">P</a> <a id="1248" href="Relation.Unary.html#2345" class="Function Operator">⊆′</a> <a id="1251" href="Induction.html#1238" class="Bound">P</a> <a id="1253" class="Symbol">→</a> <a id="1255" href="Relation.Unary.html#3230" class="Function">Universal</a> <a id="1265" href="Induction.html#1238" class="Bound">P</a>
<a id="1268" class="Comment">-- And recursors can be constructed from recursor builders.</a>
<a id="build"></a><a id="1329" href="Induction.html#1329" class="Function">build</a> <a id="1335" class="Symbol">:</a> <a id="1337" class="Symbol">∀</a> <a id="1339" class="Symbol">{</a><a id="1340" href="Induction.html#1340" class="Bound">a</a> <a id="1342" href="Induction.html#1342" class="Bound">ℓ₁</a> <a id="1345" href="Induction.html#1345" class="Bound">ℓ₂</a><a id="1347" class="Symbol">}</a> <a id="1349" class="Symbol">{</a><a id="1350" href="Induction.html#1350" class="Bound">A</a> <a id="1352" class="Symbol">:</a> <a id="1354" href="Agda.Primitive.html#320" class="Primitive">Set</a> <a id="1358" href="Induction.html#1340" class="Bound">a</a><a id="1359" class="Symbol">}</a> <a id="1361" class="Symbol">{</a><a id="1362" href="Induction.html#1362" class="Bound">Rec</a> <a id="1366" class="Symbol">:</a> <a id="1368" href="Induction.html#769" class="Function">RecStruct</a> <a id="1378" href="Induction.html#1350" class="Bound">A</a> <a id="1380" href="Induction.html#1342" class="Bound">ℓ₁</a> <a id="1383" href="Induction.html#1345" class="Bound">ℓ₂</a><a id="1385" class="Symbol">}</a> <a id="1387" class="Symbol">→</a>
<a id="1397" href="Induction.html#957" class="Function">RecursorBuilder</a> <a id="1413" href="Induction.html#1362" class="Bound">Rec</a> <a id="1417" class="Symbol">→</a>
<a id="1427" href="Induction.html#1158" class="Function">Recursor</a> <a id="1436" href="Induction.html#1362" class="Bound">Rec</a>
<a id="1440" href="Induction.html#1329" class="Function">build</a> <a id="1446" href="Induction.html#1446" class="Bound">builder</a> <a id="1454" href="Induction.html#1454" class="Bound">P</a> <a id="1456" href="Induction.html#1456" class="Bound">f</a> <a id="1458" href="Induction.html#1458" class="Bound">x</a> <a id="1460" class="Symbol">=</a> <a id="1462" href="Induction.html#1456" class="Bound">f</a> <a id="1464" href="Induction.html#1458" class="Bound">x</a> <a id="1466" class="Symbol">(</a><a id="1467" href="Induction.html#1446" class="Bound">builder</a> <a id="1475" href="Induction.html#1454" class="Bound">P</a> <a id="1477" href="Induction.html#1456" class="Bound">f</a> <a id="1479" href="Induction.html#1458" class="Bound">x</a><a id="1480" class="Symbol">)</a>
<a id="1483" class="Comment">-- We can repeat the exercise above for subsets of the type we are</a>
<a id="1550" class="Comment">-- recursing over.</a>
<a id="SubsetRecursorBuilder"></a><a id="1570" href="Induction.html#1570" class="Function">SubsetRecursorBuilder</a> <a id="1592" class="Symbol">:</a> <a id="1594" class="Symbol">∀</a> <a id="1596" class="Symbol">{</a><a id="1597" href="Induction.html#1597" class="Bound">a</a> <a id="1599" href="Induction.html#1599" class="Bound">ℓ₁</a> <a id="1602" href="Induction.html#1602" class="Bound">ℓ₂</a> <a id="1605" href="Induction.html#1605" class="Bound">ℓ₃</a><a id="1607" class="Symbol">}</a> <a id="1609" class="Symbol">{</a><a id="1610" href="Induction.html#1610" class="Bound">A</a> <a id="1612" class="Symbol">:</a> <a id="1614" href="Agda.Primitive.html#320" class="Primitive">Set</a> <a id="1618" href="Induction.html#1597" class="Bound">a</a><a id="1619" class="Symbol">}</a> <a id="1621" class="Symbol">→</a>
<a id="1647" href="Relation.Unary.html#1110" class="Function">Pred</a> <a id="1652" href="Induction.html#1610" class="Bound">A</a> <a id="1654" href="Induction.html#1599" class="Bound">ℓ₁</a> <a id="1657" class="Symbol">→</a> <a id="1659" href="Induction.html#769" class="Function">RecStruct</a> <a id="1669" href="Induction.html#1610" class="Bound">A</a> <a id="1671" href="Induction.html#1602" class="Bound">ℓ₂</a> <a id="1674" href="Induction.html#1605" class="Bound">ℓ₃</a> <a id="1677" class="Symbol">→</a> <a id="1679" href="Agda.Primitive.html#320" class="Primitive">Set</a> <a id="1683" class="Symbol">_</a>
<a id="1685" href="Induction.html#1570" class="Function">SubsetRecursorBuilder</a> <a id="1707" href="Induction.html#1707" class="Bound">Q</a> <a id="1709" href="Induction.html#1709" class="Bound">Rec</a> <a id="1713" class="Symbol">=</a> <a id="1715" class="Symbol">∀</a> <a id="1717" href="Induction.html#1717" class="Bound">P</a> <a id="1719" class="Symbol">→</a> <a id="1721" href="Induction.html#1709" class="Bound">Rec</a> <a id="1725" href="Induction.html#1717" class="Bound">P</a> <a id="1727" href="Relation.Unary.html#2345" class="Function Operator">⊆′</a> <a id="1730" href="Induction.html#1717" class="Bound">P</a> <a id="1732" class="Symbol">→</a> <a id="1734" href="Induction.html#1707" class="Bound">Q</a> <a id="1736" href="Relation.Unary.html#2345" class="Function Operator">⊆′</a> <a id="1739" href="Induction.html#1709" class="Bound">Rec</a> <a id="1743" href="Induction.html#1717" class="Bound">P</a>
<a id="SubsetRecursor"></a><a id="1746" href="Induction.html#1746" class="Function">SubsetRecursor</a> <a id="1761" class="Symbol">:</a> <a id="1763" class="Symbol">∀</a> <a id="1765" class="Symbol">{</a><a id="1766" href="Induction.html#1766" class="Bound">a</a> <a id="1768" href="Induction.html#1768" class="Bound">ℓ₁</a> <a id="1771" href="Induction.html#1771" class="Bound">ℓ₂</a> <a id="1774" href="Induction.html#1774" class="Bound">ℓ₃</a><a id="1776" class="Symbol">}</a> <a id="1778" class="Symbol">{</a><a id="1779" href="Induction.html#1779" class="Bound">A</a> <a id="1781" class="Symbol">:</a> <a id="1783" href="Agda.Primitive.html#320" class="Primitive">Set</a> <a id="1787" href="Induction.html#1766" class="Bound">a</a><a id="1788" class="Symbol">}</a> <a id="1790" class="Symbol">→</a>
<a id="1809" href="Relation.Unary.html#1110" class="Function">Pred</a> <a id="1814" href="Induction.html#1779" class="Bound">A</a> <a id="1816" href="Induction.html#1768" class="Bound">ℓ₁</a> <a id="1819" class="Symbol">→</a> <a id="1821" href="Induction.html#769" class="Function">RecStruct</a> <a id="1831" href="Induction.html#1779" class="Bound">A</a> <a id="1833" href="Induction.html#1771" class="Bound">ℓ₂</a> <a id="1836" href="Induction.html#1774" class="Bound">ℓ₃</a> <a id="1839" class="Symbol">→</a> <a id="1841" href="Agda.Primitive.html#320" class="Primitive">Set</a> <a id="1845" class="Symbol">_</a>
<a id="1847" href="Induction.html#1746" class="Function">SubsetRecursor</a> <a id="1862" href="Induction.html#1862" class="Bound">Q</a> <a id="1864" href="Induction.html#1864" class="Bound">Rec</a> <a id="1868" class="Symbol">=</a> <a id="1870" class="Symbol">∀</a> <a id="1872" href="Induction.html#1872" class="Bound">P</a> <a id="1874" class="Symbol">→</a> <a id="1876" href="Induction.html#1864" class="Bound">Rec</a> <a id="1880" href="Induction.html#1872" class="Bound">P</a> <a id="1882" href="Relation.Unary.html#2345" class="Function Operator">⊆′</a> <a id="1885" href="Induction.html#1872" class="Bound">P</a> <a id="1887" class="Symbol">→</a> <a id="1889" href="Induction.html#1862" class="Bound">Q</a> <a id="1891" href="Relation.Unary.html#2345" class="Function Operator">⊆′</a> <a id="1894" href="Induction.html#1872" class="Bound">P</a>
<a id="subsetBuild"></a><a id="1897" href="Induction.html#1897" class="Function">subsetBuild</a> <a id="1909" class="Symbol">:</a> <a id="1911" class="Symbol">∀</a> <a id="1913" class="Symbol">{</a><a id="1914" href="Induction.html#1914" class="Bound">a</a> <a id="1916" href="Induction.html#1916" class="Bound">ℓ₁</a> <a id="1919" href="Induction.html#1919" class="Bound">ℓ₂</a> <a id="1922" href="Induction.html#1922" class="Bound">ℓ₃</a><a id="1924" class="Symbol">}</a>
<a id="1942" class="Symbol">{</a><a id="1943" href="Induction.html#1943" class="Bound">A</a> <a id="1945" class="Symbol">:</a> <a id="1947" href="Agda.Primitive.html#320" class="Primitive">Set</a> <a id="1951" href="Induction.html#1914" class="Bound">a</a><a id="1952" class="Symbol">}</a> <a id="1954" class="Symbol">{</a><a id="1955" href="Induction.html#1955" class="Bound">Q</a> <a id="1957" class="Symbol">:</a> <a id="1959" href="Relation.Unary.html#1110" class="Function">Pred</a> <a id="1964" href="Induction.html#1943" class="Bound">A</a> <a id="1966" href="Induction.html#1916" class="Bound">ℓ₁</a><a id="1968" class="Symbol">}</a> <a id="1970" class="Symbol">{</a><a id="1971" href="Induction.html#1971" class="Bound">Rec</a> <a id="1975" class="Symbol">:</a> <a id="1977" href="Induction.html#769" class="Function">RecStruct</a> <a id="1987" href="Induction.html#1943" class="Bound">A</a> <a id="1989" href="Induction.html#1919" class="Bound">ℓ₂</a> <a id="1992" href="Induction.html#1922" class="Bound">ℓ₃</a><a id="1994" class="Symbol">}</a> <a id="1996" class="Symbol">→</a>
<a id="2014" href="Induction.html#1570" class="Function">SubsetRecursorBuilder</a> <a id="2036" href="Induction.html#1955" class="Bound">Q</a> <a id="2038" href="Induction.html#1971" class="Bound">Rec</a> <a id="2042" class="Symbol">→</a>
<a id="2060" href="Induction.html#1746" class="Function">SubsetRecursor</a> <a id="2075" href="Induction.html#1955" class="Bound">Q</a> <a id="2077" href="Induction.html#1971" class="Bound">Rec</a>
<a id="2081" href="Induction.html#1897" class="Function">subsetBuild</a> <a id="2093" href="Induction.html#2093" class="Bound">builder</a> <a id="2101" href="Induction.html#2101" class="Bound">P</a> <a id="2103" href="Induction.html#2103" class="Bound">f</a> <a id="2105" href="Induction.html#2105" class="Bound">x</a> <a id="2107" href="Induction.html#2107" class="Bound">q</a> <a id="2109" class="Symbol">=</a> <a id="2111" href="Induction.html#2103" class="Bound">f</a> <a id="2113" href="Induction.html#2105" class="Bound">x</a> <a id="2115" class="Symbol">(</a><a id="2116" href="Induction.html#2093" class="Bound">builder</a> <a id="2124" href="Induction.html#2101" class="Bound">P</a> <a id="2126" href="Induction.html#2103" class="Bound">f</a> <a id="2128" href="Induction.html#2105" class="Bound">x</a> <a id="2130" href="Induction.html#2107" class="Bound">q</a><a id="2131" class="Symbol">)</a>
</pre></body></html>
Reference in a new issue Copy permalink