sites/pmikkelsen.com/_tmp/agda-dfa/DFA.html


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115

<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>DFA</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Keyword">module</a> <a id="8" href="DFA.html" class="Module">DFA</a> <a id="12" class="Keyword">where</a>

<a id="19" class="Comment">-- A pair type </a>
<a id="35" class="Keyword">record</a> <a id="_×_"></a><a id="42" href="DFA.html#42" class="Record Operator">_×_</a> <a id="46" class="Symbol">(</a><a id="47" href="DFA.html#47" class="Bound">A</a> <a id="49" href="DFA.html#49" class="Bound">B</a> <a id="51" class="Symbol">:</a> <a id="53" class="PrimitiveType">Set</a><a id="56" class="Symbol">)</a> <a id="58" class="Symbol">:</a> <a id="60" class="PrimitiveType">Set</a> <a id="64" class="Keyword">where</a>
  <a id="72" class="Keyword">constructor</a> <a id="_,_"></a><a id="84" href="DFA.html#84" class="InductiveConstructor Operator">_,_</a>
  <a id="90" class="Keyword">field</a>
    <a id="_×_.fst"></a><a id="100" href="DFA.html#100" class="Field">fst</a> <a id="104" class="Symbol">:</a> <a id="106" href="DFA.html#47" class="Bound">A</a>
    <a id="_×_.snd"></a><a id="112" href="DFA.html#112" class="Field">snd</a> <a id="116" class="Symbol">:</a> <a id="118" href="DFA.html#49" class="Bound">B</a>

<a id="121" class="Comment">-- A list type</a>
<a id="136" class="Keyword">infixr</a> <a id="143" class="Number">5</a> <a id="145" href="DFA.html#197" class="InductiveConstructor Operator">_∷_</a>
<a id="149" class="Keyword">data</a> <a id="List"></a><a id="154" href="DFA.html#154" class="Datatype">List</a> <a id="159" class="Symbol">(</a><a id="160" href="DFA.html#160" class="Bound">a</a> <a id="162" class="Symbol">:</a> <a id="164" class="PrimitiveType">Set</a><a id="167" class="Symbol">)</a> <a id="169" class="Symbol">:</a> <a id="171" class="PrimitiveType">Set</a> <a id="175" class="Keyword">where</a>
  <a id="List.[]"></a><a id="183" href="DFA.html#183" class="InductiveConstructor">[]</a> <a id="186" class="Symbol">:</a> <a id="188" href="DFA.html#154" class="Datatype">List</a> <a id="193" href="DFA.html#160" class="Bound">a</a>
  <a id="List._∷_"></a><a id="197" href="DFA.html#197" class="InductiveConstructor Operator">_∷_</a> <a id="201" class="Symbol">:</a> <a id="203" href="DFA.html#160" class="Bound">a</a> <a id="205" class="Symbol">→</a> <a id="207" href="DFA.html#154" class="Datatype">List</a> <a id="212" href="DFA.html#160" class="Bound">a</a> <a id="214" class="Symbol">→</a> <a id="216" href="DFA.html#154" class="Datatype">List</a> <a id="221" href="DFA.html#160" class="Bound">a</a>

<a id="224" class="Comment">-- Elements of type x ∈ xs is a proof that x is somewhere in xs</a>
<a id="288" class="Keyword">data</a> <a id="_∈_"></a><a id="293" href="DFA.html#293" class="Datatype Operator">_∈_</a> <a id="297" class="Symbol">{</a><a id="298" href="DFA.html#298" class="Bound">A</a> <a id="300" class="Symbol">:</a> <a id="302" class="PrimitiveType">Set</a><a id="305" class="Symbol">}(</a><a id="307" href="DFA.html#307" class="Bound">x</a> <a id="309" class="Symbol">:</a> <a id="311" href="DFA.html#298" class="Bound">A</a><a id="312" class="Symbol">)</a> <a id="314" class="Symbol">:</a> <a id="316" class="Symbol">(</a><a id="317" href="DFA.html#317" class="Bound">xs</a> <a id="320" class="Symbol">:</a> <a id="322" href="DFA.html#154" class="Datatype">List</a> <a id="327" href="DFA.html#298" class="Bound">A</a><a id="328" class="Symbol">)</a> <a id="330" class="Symbol">→</a> <a id="332" class="PrimitiveType">Set</a> <a id="336" class="Keyword">where</a>
  <a id="_∈_.here"></a><a id="344" href="DFA.html#344" class="InductiveConstructor">here</a> <a id="349" class="Symbol">:</a> <a id="351" class="Symbol">∀</a> <a id="353" class="Symbol">{</a><a id="354" href="DFA.html#354" class="Bound">xs</a><a id="356" class="Symbol">}</a> <a id="358" class="Symbol">→</a> <a id="360" href="DFA.html#307" class="Bound">x</a> <a id="362" href="DFA.html#293" class="Datatype Operator">∈</a> <a id="364" class="Symbol">(</a><a id="365" href="DFA.html#307" class="Bound">x</a> <a id="367" href="DFA.html#197" class="InductiveConstructor Operator">∷</a> <a id="369" href="DFA.html#354" class="Bound">xs</a><a id="371" class="Symbol">)</a>
  <a id="_∈_.there"></a><a id="375" href="DFA.html#375" class="InductiveConstructor">there</a> <a id="381" class="Symbol">:</a> <a id="383" class="Symbol">∀</a> <a id="385" class="Symbol">{</a><a id="386" href="DFA.html#386" class="Bound">y</a> <a id="388" href="DFA.html#388" class="Bound">xs</a><a id="390" class="Symbol">}</a> <a id="392" class="Symbol">→</a> <a id="394" href="DFA.html#307" class="Bound">x</a> <a id="396" href="DFA.html#293" class="Datatype Operator">∈</a> <a id="398" href="DFA.html#388" class="Bound">xs</a> <a id="401" class="Symbol">→</a> <a id="403" href="DFA.html#307" class="Bound">x</a> <a id="405" href="DFA.html#293" class="Datatype Operator">∈</a> <a id="407" class="Symbol">(</a><a id="408" href="DFA.html#386" class="Bound">y</a> <a id="410" href="DFA.html#197" class="InductiveConstructor Operator">∷</a> <a id="412" href="DFA.html#388" class="Bound">xs</a><a id="414" class="Symbol">)</a>

<a id="417" class="Comment">-- Elements of type a ≡ b is a proof that a and b are the same</a>
<a id="480" class="Keyword">data</a> <a id="_≡_"></a><a id="485" href="DFA.html#485" class="Datatype Operator">_≡_</a> <a id="489" class="Symbol">{</a><a id="490" href="DFA.html#490" class="Bound">A</a> <a id="492" class="Symbol">:</a> <a id="494" class="PrimitiveType">Set</a><a id="497" class="Symbol">}(</a><a id="499" href="DFA.html#499" class="Bound">x</a> <a id="501" class="Symbol">:</a> <a id="503" href="DFA.html#490" class="Bound">A</a><a id="504" class="Symbol">)</a> <a id="506" class="Symbol">:</a> <a id="508" href="DFA.html#490" class="Bound">A</a> <a id="510" class="Symbol">→</a> <a id="512" class="PrimitiveType">Set</a> <a id="516" class="Keyword">where</a>
  <a id="_≡_.refl"></a><a id="524" href="DFA.html#524" class="InductiveConstructor">refl</a> <a id="529" class="Symbol">:</a> <a id="531" href="DFA.html#499" class="Bound">x</a> <a id="533" href="DFA.html#485" class="Datatype Operator">≡</a> <a id="535" href="DFA.html#499" class="Bound">x</a>

<a id="538" class="Comment">-- The empty type. There are no members of this type, so it is the same as false</a>
<a id="619" class="Keyword">data</a> <a id="⊥"></a><a id="624" href="DFA.html#624" class="Datatype">⊥</a> <a id="626" class="Symbol">:</a> <a id="628" class="PrimitiveType">Set</a> <a id="632" class="Keyword">where</a>

<a id="639" class="Comment">-- Negation is defined by a function that takes a proof and returns ⊥, which is impossible. In agda an inhabited type means a proof, and an uninhabited means no proof.</a>
<a id="¬_"></a><a id="807" href="DFA.html#807" class="Function Operator">¬_</a> <a id="810" class="Symbol">:</a> <a id="812" class="PrimitiveType">Set</a> <a id="816" class="Symbol">→</a> <a id="818" class="PrimitiveType">Set</a>
<a id="822" href="DFA.html#807" class="Function Operator">¬</a> <a id="824" href="DFA.html#824" class="Bound">A</a> <a id="826" class="Symbol">=</a> <a id="828" href="DFA.html#824" class="Bound">A</a> <a id="830" class="Symbol">→</a> <a id="832" href="DFA.html#624" class="Datatype">⊥</a>

<a id="835" class="Comment">-- A DFA is a five tuple of Q Σ q₀ δ F</a>
<a id="874" class="Keyword">record</a> <a id="DFA"></a><a id="881" href="DFA.html#881" class="Record">DFA</a> <a id="885" class="Symbol">(</a><a id="886" href="DFA.html#886" class="Bound">Q</a> <a id="888" class="Symbol">:</a> <a id="890" class="PrimitiveType">Set</a><a id="893" class="Symbol">)</a> <a id="895" class="Symbol">(</a><a id="896" href="DFA.html#896" class="Bound">Σ</a> <a id="898" class="Symbol">:</a> <a id="900" class="PrimitiveType">Set</a><a id="903" class="Symbol">)</a> <a id="905" class="Symbol">(</a><a id="906" href="DFA.html#906" class="Bound">q₀</a> <a id="909" class="Symbol">:</a> <a id="911" href="DFA.html#886" class="Bound">Q</a><a id="912" class="Symbol">)</a> <a id="914" class="Symbol">(</a><a id="915" href="DFA.html#915" class="Bound">δ</a> <a id="917" class="Symbol">:</a> <a id="919" href="DFA.html#886" class="Bound">Q</a> <a id="921" href="DFA.html#42" class="Record Operator">×</a> <a id="923" href="DFA.html#896" class="Bound">Σ</a> <a id="925" class="Symbol">→</a> <a id="927" href="DFA.html#886" class="Bound">Q</a><a id="928" class="Symbol">)</a> <a id="930" class="Symbol">(</a><a id="931" href="DFA.html#931" class="Bound">F</a> <a id="933" class="Symbol">:</a> <a id="935" href="DFA.html#154" class="Datatype">List</a> <a id="940" href="DFA.html#886" class="Bound">Q</a><a id="941" class="Symbol">)</a> <a id="943" class="Symbol">:</a> <a id="945" class="PrimitiveType">Set</a> <a id="949" class="Keyword">where</a>

<a id="956" class="Comment">-- The DFArun data type keeps track of a running dfa.</a>
<a id="1010" class="Keyword">data</a> <a id="DFArun"></a><a id="1015" href="DFA.html#1015" class="Datatype">DFArun</a> <a id="1022" class="Symbol">{</a><a id="1023" href="DFA.html#1023" class="Bound">Q</a> <a id="1025" href="DFA.html#1025" class="Bound">Σ</a> <a id="1027" href="DFA.html#1027" class="Bound">q₀</a> <a id="1030" href="DFA.html#1030" class="Bound">δ</a> <a id="1032" href="DFA.html#1032" class="Bound">F</a><a id="1033" class="Symbol">}(</a><a id="1035" href="DFA.html#1035" class="Bound">dfa</a> <a id="1039" class="Symbol">:</a> <a id="1041" href="DFA.html#881" class="Record">DFA</a> <a id="1045" href="DFA.html#1023" class="Bound">Q</a> <a id="1047" href="DFA.html#1025" class="Bound">Σ</a> <a id="1049" href="DFA.html#1027" class="Bound">q₀</a> <a id="1052" href="DFA.html#1030" class="Bound">δ</a> <a id="1054" href="DFA.html#1032" class="Bound">F</a><a id="1055" class="Symbol">)</a> <a id="1057" class="Symbol">:</a> <a id="1059" class="Symbol">(</a><a id="1060" href="DFA.html#1060" class="Bound">q</a> <a id="1062" class="Symbol">:</a> <a id="1064" href="DFA.html#1023" class="Bound">Q</a><a id="1065" class="Symbol">)</a> <a id="1067" class="Symbol">→</a> <a id="1069" class="Symbol">(</a><a id="1070" href="DFA.html#1070" class="Bound">w</a> <a id="1072" class="Symbol">:</a> <a id="1074" href="DFA.html#154" class="Datatype">List</a> <a id="1079" href="DFA.html#1025" class="Bound">Σ</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="DFArun.empty"></a><a id="1096" href="DFA.html#1096" class="InductiveConstructor">empty</a> <a id="1102" class="Symbol">:</a> <a id="1104" class="Symbol">{</a><a id="1105" href="DFA.html#1105" class="Bound">q</a> <a id="1107" class="Symbol">:</a> <a id="1109" href="DFA.html#1023" class="Bound">Q</a><a id="1110" class="Symbol">}</a> <a id="1112" class="Symbol">→</a> <a id="1114" href="DFA.html#1105" class="Bound">q</a> <a id="1116" href="DFA.html#293" class="Datatype Operator">∈</a> <a id="1118" href="DFA.html#1032" class="Bound">F</a> <a id="1120" class="Symbol">→</a> <a id="1122" href="DFA.html#1015" class="Datatype">DFArun</a> <a id="1129" href="DFA.html#1035" class="Bound">dfa</a> <a id="1133" href="DFA.html#1105" class="Bound">q</a> <a id="1135" href="DFA.html#183" class="InductiveConstructor">[]</a>
  <a id="DFArun.acceptOne"></a><a id="1140" href="DFA.html#1140" class="InductiveConstructor">acceptOne</a> <a id="1150" class="Symbol">:</a> <a id="1152" class="Symbol">{</a><a id="1153" href="DFA.html#1153" class="Bound">ws</a> <a id="1156" class="Symbol">:</a> <a id="1158" href="DFA.html#154" class="Datatype">List</a> <a id="1163" href="DFA.html#1025" class="Bound">Σ</a><a id="1164" class="Symbol">}</a> <a id="1166" class="Symbol">→</a>
              <a id="1182" class="Symbol">(</a><a id="1183" href="DFA.html#1183" class="Bound">w</a> <a id="1185" class="Symbol">:</a> <a id="1187" href="DFA.html#1025" class="Bound">Σ</a><a id="1188" class="Symbol">)</a> <a id="1190" class="Symbol">→</a>
              <a id="1206" class="Symbol">(</a><a id="1207" href="DFA.html#1207" class="Bound">q</a> <a id="1209" class="Symbol">:</a> <a id="1211" href="DFA.html#1023" class="Bound">Q</a><a id="1212" class="Symbol">)</a> <a id="1214" class="Symbol">→</a>
              <a id="1230" href="DFA.html#1015" class="Datatype">DFArun</a> <a id="1237" href="DFA.html#1035" class="Bound">dfa</a> <a id="1241" class="Symbol">(</a><a id="1242" href="DFA.html#1030" class="Bound">δ</a> <a id="1244" class="Symbol">(</a><a id="1245" href="DFA.html#1207" class="Bound">q</a> <a id="1247" href="DFA.html#84" class="InductiveConstructor Operator">,</a> <a id="1249" href="DFA.html#1183" class="Bound">w</a><a id="1250" class="Symbol">))</a> <a id="1253" href="DFA.html#1153" class="Bound">ws</a> <a id="1256" class="Symbol">→</a>
              <a id="1272" href="DFA.html#1015" class="Datatype">DFArun</a> <a id="1279" href="DFA.html#1035" class="Bound">dfa</a> <a id="1283" href="DFA.html#1207" class="Bound">q</a> <a id="1285" class="Symbol">(</a><a id="1286" href="DFA.html#1183" class="Bound">w</a> <a id="1288" href="DFA.html#197" class="InductiveConstructor Operator">∷</a> <a id="1290" href="DFA.html#1153" class="Bound">ws</a><a id="1292" class="Symbol">)</a>

<a id="1295" class="Comment">-- Accepts dfa w is a proof that running the dfa with input w is possible form the start state q₀</a>
<a id="1393" class="Keyword">data</a> <a id="Accepts"></a><a id="1398" href="DFA.html#1398" class="Datatype">Accepts</a> <a id="1406" class="Symbol">{</a><a id="1407" href="DFA.html#1407" class="Bound">Q</a> <a id="1409" href="DFA.html#1409" class="Bound">Σ</a> <a id="1411" href="DFA.html#1411" class="Bound">q₀</a> <a id="1414" href="DFA.html#1414" class="Bound">δ</a> <a id="1416" href="DFA.html#1416" class="Bound">F</a><a id="1417" class="Symbol">}(</a><a id="1419" href="DFA.html#1419" class="Bound">dfa</a> <a id="1423" class="Symbol">:</a> <a id="1425" href="DFA.html#881" class="Record">DFA</a> <a id="1429" href="DFA.html#1407" class="Bound">Q</a> <a id="1431" href="DFA.html#1409" class="Bound">Σ</a> <a id="1433" href="DFA.html#1411" class="Bound">q₀</a> <a id="1436" href="DFA.html#1414" class="Bound">δ</a> <a id="1438" href="DFA.html#1416" class="Bound">F</a><a id="1439" class="Symbol">)</a> <a id="1441" class="Symbol">:</a> <a id="1443" class="Symbol">(</a><a id="1444" href="DFA.html#1444" class="Bound">w</a> <a id="1446" class="Symbol">:</a> <a id="1448" href="DFA.html#154" class="Datatype">List</a> <a id="1453" href="DFA.html#1409" class="Bound">Σ</a><a id="1454" class="Symbol">)</a> <a id="1456" class="Symbol">→</a> <a id="1458" class="PrimitiveType">Set</a> <a id="1462" class="Keyword">where</a>
  <a id="Accepts.accepts"></a><a id="1470" href="DFA.html#1470" class="InductiveConstructor">accepts</a> <a id="1478" class="Symbol">:</a> <a id="1480" class="Symbol">∀{</a><a id="1482" href="DFA.html#1482" class="Bound">w</a><a id="1483" class="Symbol">}</a> <a id="1485" class="Symbol">→</a> <a id="1487" href="DFA.html#1015" class="Datatype">DFArun</a> <a id="1494" href="DFA.html#1419" class="Bound">dfa</a> <a id="1498" href="DFA.html#1411" class="Bound">q₀</a> <a id="1501" href="DFA.html#1482" class="Bound">w</a> <a id="1503" class="Symbol">→</a> <a id="1505" href="DFA.html#1398" class="Datatype">Accepts</a> <a id="1513" href="DFA.html#1419" class="Bound">dfa</a> <a id="1517" href="DFA.html#1482" class="Bound">w</a>

<a id="1520" class="Comment">-- CantAccept dfa q w is a proof that running the dfa on imput w is impossible if we want to start at state q₀. It has to start in q instead.</a>
<a id="1662" class="Keyword">data</a> <a id="CantAccept"></a><a id="1667" href="DFA.html#1667" class="Datatype">CantAccept</a> <a id="1678" class="Symbol">{</a><a id="1679" href="DFA.html#1679" class="Bound">Q</a> <a id="1681" href="DFA.html#1681" class="Bound">Σ</a> <a id="1683" href="DFA.html#1683" class="Bound">q₀</a> <a id="1686" href="DFA.html#1686" class="Bound">δ</a> <a id="1688" href="DFA.html#1688" class="Bound">F</a><a id="1689" class="Symbol">}(</a><a id="1691" href="DFA.html#1691" class="Bound">dfa</a> <a id="1695" class="Symbol">:</a> <a id="1697" href="DFA.html#881" class="Record">DFA</a> <a id="1701" href="DFA.html#1679" class="Bound">Q</a> <a id="1703" href="DFA.html#1681" class="Bound">Σ</a> <a id="1705" href="DFA.html#1683" class="Bound">q₀</a> <a id="1708" href="DFA.html#1686" class="Bound">δ</a> <a id="1710" href="DFA.html#1688" class="Bound">F</a><a id="1711" class="Symbol">)</a> <a id="1713" class="Symbol">:</a> <a id="1715" class="Symbol">(</a><a id="1716" href="DFA.html#1716" class="Bound">q</a> <a id="1718" class="Symbol">:</a> <a id="1720" href="DFA.html#1679" class="Bound">Q</a><a id="1721" class="Symbol">)</a> <a id="1723" class="Symbol">→</a> <a id="1725" class="Symbol">(</a><a id="1726" href="DFA.html#1726" class="Bound">w</a> <a id="1728" class="Symbol">:</a> <a id="1730" href="DFA.html#154" class="Datatype">List</a> <a id="1735" href="DFA.html#1681" class="Bound">Σ</a><a id="1736" class="Symbol">)</a> <a id="1738" class="Symbol">→</a> <a id="1740" class="PrimitiveType">Set</a> <a id="1744" class="Keyword">where</a>
  <a id="CantAccept.cantAccept"></a><a id="1752" href="DFA.html#1752" class="InductiveConstructor">cantAccept</a> <a id="1763" class="Symbol">:</a> <a id="1765" class="Symbol">∀</a> <a id="1767" class="Symbol">{</a><a id="1768" href="DFA.html#1768" class="Bound">w</a> <a id="1770" href="DFA.html#1770" class="Bound">q</a><a id="1771" class="Symbol">}</a> <a id="1773" class="Symbol">→</a> <a id="1775" href="DFA.html#1015" class="Datatype">DFArun</a> <a id="1782" href="DFA.html#1691" class="Bound">dfa</a> <a id="1786" href="DFA.html#1770" class="Bound">q</a> <a id="1788" href="DFA.html#1768" class="Bound">w</a> <a id="1790" class="Symbol">→</a> <a id="1792" href="DFA.html#807" class="Function Operator">¬</a><a id="1793" class="Symbol">(</a><a id="1794" href="DFA.html#1770" class="Bound">q</a> <a id="1796" href="DFA.html#485" class="Datatype Operator">≡</a> <a id="1798" href="DFA.html#1683" class="Bound">q₀</a><a id="1800" class="Symbol">)</a> <a id="1802" class="Symbol">→</a> <a id="1804" href="DFA.html#1667" class="Datatype">CantAccept</a> <a id="1815" href="DFA.html#1691" class="Bound">dfa</a> <a id="1819" href="DFA.html#1770" class="Bound">q</a> <a id="1821" href="DFA.html#1768" class="Bound">w</a>


<a id="1825" class="Comment">-- w ∈Lang dfa gives either a proof that w is in the language of the dfa, or that it isn&#39;t.</a>
<a id="1917" class="Keyword">data</a> <a id="_∈Lang_"></a><a id="1922" href="DFA.html#1922" class="Datatype Operator">_∈Lang_</a> <a id="1930" class="Symbol">{</a><a id="1931" href="DFA.html#1931" class="Bound">Q</a> <a id="1933" href="DFA.html#1933" class="Bound">Σ</a> <a id="1935" href="DFA.html#1935" class="Bound">q₀</a> <a id="1938" href="DFA.html#1938" class="Bound">δ</a> <a id="1940" href="DFA.html#1940" class="Bound">F</a><a id="1941" class="Symbol">}(</a><a id="1943" href="DFA.html#1943" class="Bound">w</a> <a id="1945" class="Symbol">:</a> <a id="1947" href="DFA.html#154" class="Datatype">List</a> <a id="1952" href="DFA.html#1933" class="Bound">Σ</a><a id="1953" class="Symbol">)(</a><a id="1955" href="DFA.html#1955" class="Bound">dfa</a> <a id="1959" class="Symbol">:</a> <a id="1961" href="DFA.html#881" class="Record">DFA</a> <a id="1965" href="DFA.html#1931" class="Bound">Q</a> <a id="1967" href="DFA.html#1933" class="Bound">Σ</a> <a id="1969" href="DFA.html#1935" class="Bound">q₀</a> <a id="1972" href="DFA.html#1938" class="Bound">δ</a> <a id="1974" href="DFA.html#1940" class="Bound">F</a><a id="1975" class="Symbol">)</a> <a id="1977" class="Symbol">:</a> <a id="1979" class="PrimitiveType">Set</a> <a id="1983" class="Keyword">where</a>
  <a id="_∈Lang_.inLang"></a><a id="1991" href="DFA.html#1991" class="InductiveConstructor">inLang</a> <a id="1998" class="Symbol">:</a> <a id="2000" href="DFA.html#1398" class="Datatype">Accepts</a> <a id="2008" href="DFA.html#1955" class="Bound">dfa</a> <a id="2012" href="DFA.html#1943" class="Bound">w</a> <a id="2014" class="Symbol">→</a> <a id="2016" href="DFA.html#1943" class="Bound">w</a> <a id="2018" href="DFA.html#1922" class="Datatype Operator">∈Lang</a> <a id="2024" href="DFA.html#1955" class="Bound">dfa</a>
  <a id="_∈Lang_.notInLang"></a><a id="2030" href="DFA.html#2030" class="InductiveConstructor">notInLang</a> <a id="2040" class="Symbol">:</a> <a id="2042" class="Symbol">∀{</a><a id="2044" href="DFA.html#2044" class="Bound">q</a><a id="2045" class="Symbol">}</a> <a id="2047" class="Symbol">→</a> <a id="2049" href="DFA.html#1667" class="Datatype">CantAccept</a> <a id="2060" href="DFA.html#1955" class="Bound">dfa</a> <a id="2064" href="DFA.html#2044" class="Bound">q</a> <a id="2066" href="DFA.html#1943" class="Bound">w</a> <a id="2068" class="Symbol">→</a> <a id="2070" href="DFA.html#1943" class="Bound">w</a> <a id="2072" href="DFA.html#1922" class="Datatype Operator">∈Lang</a> <a id="2078" href="DFA.html#1955" class="Bound">dfa</a>


<a id="2086" class="Comment">-- Test stuff. Create a DFA which only accepts an input with an even number of a&#39;s</a>

<a id="2170" class="Keyword">data</a> <a id="TestQ"></a><a id="2175" href="DFA.html#2175" class="Datatype">TestQ</a> <a id="2181" class="Symbol">:</a> <a id="2183" class="PrimitiveType">Set</a> <a id="2187" class="Keyword">where</a>
  <a id="TestQ.evenNumberOfAs"></a><a id="2195" href="DFA.html#2195" class="InductiveConstructor">evenNumberOfAs</a> <a id="2210" class="Symbol">:</a> <a id="2212" href="DFA.html#2175" class="Datatype">TestQ</a>
  <a id="TestQ.oddNumberOfAs"></a><a id="2220" href="DFA.html#2220" class="InductiveConstructor">oddNumberOfAs</a> <a id="2234" class="Symbol">:</a> <a id="2236" href="DFA.html#2175" class="Datatype">TestQ</a>

<a id="2243" class="Keyword">data</a> <a id="TestΣ"></a><a id="2248" href="DFA.html#2248" class="Datatype">TestΣ</a> <a id="2254" class="Symbol">:</a> <a id="2256" class="PrimitiveType">Set</a> <a id="2260" class="Keyword">where</a>
  <a id="TestΣ.a"></a><a id="2268" href="DFA.html#2268" class="InductiveConstructor">a</a> <a id="2270" class="Symbol">:</a> <a id="2272" href="DFA.html#2248" class="Datatype">TestΣ</a>
  <a id="TestΣ.b"></a><a id="2280" href="DFA.html#2280" class="InductiveConstructor">b</a> <a id="2282" class="Symbol">:</a> <a id="2284" href="DFA.html#2248" class="Datatype">TestΣ</a>

<a id="Testδ"></a><a id="2291" href="DFA.html#2291" class="Function">Testδ</a> <a id="2297" class="Symbol">:</a> <a id="2299" href="DFA.html#2175" class="Datatype">TestQ</a> <a id="2305" href="DFA.html#42" class="Record Operator">×</a> <a id="2307" href="DFA.html#2248" class="Datatype">TestΣ</a> <a id="2313" class="Symbol">→</a> <a id="2315" href="DFA.html#2175" class="Datatype">TestQ</a>
<a id="2321" href="DFA.html#2291" class="Function">Testδ</a> <a id="2327" class="Symbol">(</a><a id="2328" href="DFA.html#2195" class="InductiveConstructor">evenNumberOfAs</a> <a id="2343" href="DFA.html#84" class="InductiveConstructor Operator">,</a> <a id="2345" href="DFA.html#2268" class="InductiveConstructor">a</a><a id="2346" class="Symbol">)</a> <a id="2348" class="Symbol">=</a> <a id="2350" href="DFA.html#2220" class="InductiveConstructor">oddNumberOfAs</a>
<a id="2364" href="DFA.html#2291" class="Function">Testδ</a> <a id="2370" class="Symbol">(</a><a id="2371" href="DFA.html#2195" class="InductiveConstructor">evenNumberOfAs</a> <a id="2386" href="DFA.html#84" class="InductiveConstructor Operator">,</a> <a id="2388" href="DFA.html#2280" class="InductiveConstructor">b</a><a id="2389" class="Symbol">)</a> <a id="2391" class="Symbol">=</a> <a id="2393" href="DFA.html#2195" class="InductiveConstructor">evenNumberOfAs</a>
<a id="2408" href="DFA.html#2291" class="Function">Testδ</a> <a id="2414" class="Symbol">(</a><a id="2415" href="DFA.html#2220" class="InductiveConstructor">oddNumberOfAs</a> <a id="2429" href="DFA.html#84" class="InductiveConstructor Operator">,</a> <a id="2431" href="DFA.html#2268" class="InductiveConstructor">a</a><a id="2432" class="Symbol">)</a> <a id="2434" class="Symbol">=</a> <a id="2436" href="DFA.html#2195" class="InductiveConstructor">evenNumberOfAs</a>
<a id="2451" href="DFA.html#2291" class="Function">Testδ</a> <a id="2457" class="Symbol">(</a><a id="2458" href="DFA.html#2220" class="InductiveConstructor">oddNumberOfAs</a> <a id="2472" href="DFA.html#84" class="InductiveConstructor Operator">,</a> <a id="2474" href="DFA.html#2280" class="InductiveConstructor">b</a><a id="2475" class="Symbol">)</a> <a id="2477" class="Symbol">=</a> <a id="2479" href="DFA.html#2220" class="InductiveConstructor">oddNumberOfAs</a>

<a id="TestF"></a><a id="2494" href="DFA.html#2494" class="Function">TestF</a> <a id="2500" class="Symbol">:</a> <a id="2502" href="DFA.html#154" class="Datatype">List</a> <a id="2507" href="DFA.html#2175" class="Datatype">TestQ</a>
<a id="2513" href="DFA.html#2494" class="Function">TestF</a> <a id="2519" class="Symbol">=</a> <a id="2521" href="DFA.html#2195" class="InductiveConstructor">evenNumberOfAs</a> <a id="2536" href="DFA.html#197" class="InductiveConstructor Operator">∷</a> <a id="2538" href="DFA.html#183" class="InductiveConstructor">[]</a>

<a id="TestDFA"></a><a id="2542" href="DFA.html#2542" class="Function">TestDFA</a> <a id="2550" class="Symbol">:</a> <a id="2552" href="DFA.html#881" class="Record">DFA</a> <a id="2556" href="DFA.html#2175" class="Datatype">TestQ</a> <a id="2562" href="DFA.html#2248" class="Datatype">TestΣ</a> <a id="2568" href="DFA.html#2195" class="InductiveConstructor">evenNumberOfAs</a> <a id="2583" href="DFA.html#2291" class="Function">Testδ</a> <a id="2589" href="DFA.html#2494" class="Function">TestF</a>
<a id="2595" href="DFA.html#2542" class="Function">TestDFA</a> <a id="2603" class="Symbol">=</a> <a id="2605" class="Symbol">_</a> <a id="2607" class="Comment">-- Since a DFA is a record with no fields, agda can infer it</a>

<a id="2669" class="Comment">-- Try to construct proofs for different input strings</a>

<a id="input₁"></a><a id="2725" href="DFA.html#2725" class="Function">input₁</a> <a id="input₂"></a><a id="2732" href="DFA.html#2732" class="Function">input₂</a> <a id="input₃"></a><a id="2739" href="DFA.html#2739" class="Function">input₃</a> <a id="2746" class="Symbol">:</a> <a id="2748" href="DFA.html#154" class="Datatype">List</a> <a id="2753" href="DFA.html#2248" class="Datatype">TestΣ</a>
<a id="2759" href="DFA.html#2725" class="Function">input₁</a> <a id="2766" class="Symbol">=</a> <a id="2768" href="DFA.html#183" class="InductiveConstructor">[]</a> <a id="2771" class="Comment">-- Empty string</a>
<a id="2787" href="DFA.html#2732" class="Function">input₂</a> <a id="2794" class="Symbol">=</a> <a id="2796" href="DFA.html#2268" class="InductiveConstructor">a</a> <a id="2798" href="DFA.html#197" class="InductiveConstructor Operator">∷</a> <a id="2800" href="DFA.html#2280" class="InductiveConstructor">b</a> <a id="2802" href="DFA.html#197" class="InductiveConstructor Operator">∷</a> <a id="2804" href="DFA.html#2268" class="InductiveConstructor">a</a> <a id="2806" href="DFA.html#197" class="InductiveConstructor Operator">∷</a> <a id="2808" href="DFA.html#2268" class="InductiveConstructor">a</a> <a id="2810" href="DFA.html#197" class="InductiveConstructor Operator">∷</a> <a id="2812" href="DFA.html#2280" class="InductiveConstructor">b</a> <a id="2814" href="DFA.html#197" class="InductiveConstructor Operator">∷</a> <a id="2816" href="DFA.html#183" class="InductiveConstructor">[]</a> <a id="2819" class="Comment">-- Three a&#39;s</a>
<a id="2832" href="DFA.html#2739" class="Function">input₃</a> <a id="2839" class="Symbol">=</a> <a id="2841" href="DFA.html#2280" class="InductiveConstructor">b</a> <a id="2843" href="DFA.html#197" class="InductiveConstructor Operator">∷</a> <a id="2845" href="DFA.html#2280" class="InductiveConstructor">b</a> <a id="2847" href="DFA.html#197" class="InductiveConstructor Operator">∷</a> <a id="2849" href="DFA.html#2268" class="InductiveConstructor">a</a> <a id="2851" href="DFA.html#197" class="InductiveConstructor Operator">∷</a> <a id="2853" href="DFA.html#2280" class="InductiveConstructor">b</a> <a id="2855" href="DFA.html#197" class="InductiveConstructor Operator">∷</a> <a id="2857" href="DFA.html#2268" class="InductiveConstructor">a</a> <a id="2859" href="DFA.html#197" class="InductiveConstructor Operator">∷</a> <a id="2861" href="DFA.html#183" class="InductiveConstructor">[]</a> <a id="2864" class="Comment">-- Two a&#39;s</a>


<a id="2877" class="Comment">-- The proofs are found automatically by agda, and no other proofs would type check</a>
<a id="proof₁"></a><a id="2961" href="DFA.html#2961" class="Function">proof₁</a> <a id="2968" class="Symbol">:</a> <a id="2970" href="DFA.html#2725" class="Function">input₁</a> <a id="2977" href="DFA.html#1922" class="Datatype Operator">∈Lang</a> <a id="2983" href="DFA.html#2542" class="Function">TestDFA</a> <a id="2991" class="Comment">-- Proof that input₁ is in the language</a>
<a id="3031" href="DFA.html#2961" class="Function">proof₁</a> <a id="3038" class="Symbol">=</a> <a id="3040" href="DFA.html#1991" class="InductiveConstructor">inLang</a> <a id="3047" class="Symbol">(</a><a id="3048" href="DFA.html#1470" class="InductiveConstructor">accepts</a> <a id="3056" class="Symbol">(</a><a id="3057" href="DFA.html#1096" class="InductiveConstructor">empty</a> <a id="3063" href="DFA.html#344" class="InductiveConstructor">here</a><a id="3067" class="Symbol">))</a>

<a id="proof₂"></a><a id="3071" href="DFA.html#3071" class="Function">proof₂</a> <a id="3078" class="Symbol">:</a> <a id="3080" href="DFA.html#2732" class="Function">input₂</a> <a id="3087" href="DFA.html#1922" class="Datatype Operator">∈Lang</a> <a id="3093" href="DFA.html#2542" class="Function">TestDFA</a> <a id="3101" class="Comment">-- Proof that input₂ is not in the language</a>
<a id="3145" href="DFA.html#3071" class="Function">proof₂</a> <a id="3152" class="Symbol">=</a> <a id="3154" href="DFA.html#2030" class="InductiveConstructor">notInLang</a>
           <a id="3175" class="Symbol">(</a><a id="3176" href="DFA.html#1752" class="InductiveConstructor">cantAccept</a>
            <a id="3199" class="Symbol">(</a><a id="3200" href="DFA.html#1140" class="InductiveConstructor">acceptOne</a> <a id="3210" href="DFA.html#2268" class="InductiveConstructor">a</a> <a id="3212" href="DFA.html#2220" class="InductiveConstructor">oddNumberOfAs</a>
             <a id="3239" class="Symbol">(</a><a id="3240" href="DFA.html#1140" class="InductiveConstructor">acceptOne</a> <a id="3250" href="DFA.html#2280" class="InductiveConstructor">b</a> <a id="3252" href="DFA.html#2195" class="InductiveConstructor">evenNumberOfAs</a>
              <a id="3281" class="Symbol">(</a><a id="3282" href="DFA.html#1140" class="InductiveConstructor">acceptOne</a> <a id="3292" href="DFA.html#2268" class="InductiveConstructor">a</a> <a id="3294" href="DFA.html#2195" class="InductiveConstructor">evenNumberOfAs</a>
               <a id="3324" class="Symbol">(</a><a id="3325" href="DFA.html#1140" class="InductiveConstructor">acceptOne</a> <a id="3335" href="DFA.html#2268" class="InductiveConstructor">a</a> <a id="3337" href="DFA.html#2220" class="InductiveConstructor">oddNumberOfAs</a>
                <a id="3367" class="Symbol">(</a><a id="3368" href="DFA.html#1140" class="InductiveConstructor">acceptOne</a> <a id="3378" href="DFA.html#2280" class="InductiveConstructor">b</a> <a id="3380" href="DFA.html#2195" class="InductiveConstructor">evenNumberOfAs</a> <a id="3395" class="Symbol">(</a><a id="3396" href="DFA.html#1096" class="InductiveConstructor">empty</a> <a id="3402" href="DFA.html#344" class="InductiveConstructor">here</a><a id="3406" class="Symbol">))))))</a>
            <a id="3425" class="Symbol">(λ</a> <a id="3428" class="Symbol">()))</a>

<a id="proof₃"></a><a id="3434" href="DFA.html#3434" class="Function">proof₃</a> <a id="3441" class="Symbol">:</a> <a id="3443" href="DFA.html#2739" class="Function">input₃</a> <a id="3450" href="DFA.html#1922" class="Datatype Operator">∈Lang</a> <a id="3456" href="DFA.html#2542" class="Function">TestDFA</a> <a id="3464" class="Comment">-- Proof that input₃ is in the language</a>
<a id="3504" href="DFA.html#3434" class="Function">proof₃</a> <a id="3511" class="Symbol">=</a> <a id="3513" href="DFA.html#1991" class="InductiveConstructor">inLang</a>
           <a id="3531" class="Symbol">(</a><a id="3532" href="DFA.html#1470" class="InductiveConstructor">accepts</a>
            <a id="3552" class="Symbol">(</a><a id="3553" href="DFA.html#1140" class="InductiveConstructor">acceptOne</a> <a id="3563" href="DFA.html#2280" class="InductiveConstructor">b</a> <a id="3565" href="DFA.html#2195" class="InductiveConstructor">evenNumberOfAs</a>
             <a id="3593" class="Symbol">(</a><a id="3594" href="DFA.html#1140" class="InductiveConstructor">acceptOne</a> <a id="3604" href="DFA.html#2280" class="InductiveConstructor">b</a> <a id="3606" href="DFA.html#2195" class="InductiveConstructor">evenNumberOfAs</a>
              <a id="3635" class="Symbol">(</a><a id="3636" href="DFA.html#1140" class="InductiveConstructor">acceptOne</a> <a id="3646" href="DFA.html#2268" class="InductiveConstructor">a</a> <a id="3648" href="DFA.html#2195" class="InductiveConstructor">evenNumberOfAs</a>
               <a id="3678" class="Symbol">(</a><a id="3679" href="DFA.html#1140" class="InductiveConstructor">acceptOne</a> <a id="3689" href="DFA.html#2280" class="InductiveConstructor">b</a> <a id="3691" href="DFA.html#2220" class="InductiveConstructor">oddNumberOfAs</a>
                <a id="3721" class="Symbol">(</a><a id="3722" href="DFA.html#1140" class="InductiveConstructor">acceptOne</a> <a id="3732" href="DFA.html#2268" class="InductiveConstructor">a</a> <a id="3734" href="DFA.html#2220" class="InductiveConstructor">oddNumberOfAs</a> <a id="3748" class="Symbol">(</a><a id="3749" href="DFA.html#1096" class="InductiveConstructor">empty</a> <a id="3755" href="DFA.html#344" class="InductiveConstructor">here</a><a id="3759" class="Symbol">)))))))</a>

</pre></body></html>