agda-stdlib-doc 0.14-1 / usr / share / doc / agda-stdlib-doc / html / Algebra.CommutativeMonoidSolver.html

This file is indexed.

/usr/share/doc/agda-stdlib-doc/html/Algebra.CommutativeMonoidSolver.html is in agda-stdlib-doc 0.14-1.

This file is owned by root:root, with mode 0o644.

The actual contents of the file can be viewed below. 

  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
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Algebra.CommutativeMonoidSolver</title><link rel="stylesheet" href="Agda.css"></head><body><pre><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">-- Solver for equations in commutative monoids</a>
<a id="153" class="Comment">--</a>
<a id="156" class="Comment">-- Adapted from Algebra.Monoid-solver</a>
<a id="194" class="Comment">------------------------------------------------------------------------</a>

<a id="268" class="Keyword">open</a> <a id="273" class="Keyword">import</a> <a id="280" href="Algebra.html" class="Module">Algebra</a>

<a id="289" class="Keyword">open</a> <a id="294" class="Keyword">import</a> <a id="301" href="Data.Fin.html" class="Module">Data.Fin</a> <a id="310" class="Keyword">using</a> <a id="316" class="Symbol">(</a><a id="317" href="Data.Fin.html#Fin" class="Datatype">Fin</a><a id="320" class="Symbol">;</a> <a id="322" href="Data.Fin.html#Fin.zero" class="InductiveConstructor">zero</a><a id="326" class="Symbol">;</a> <a id="328" href="Data.Fin.html#Fin.suc" class="InductiveConstructor">suc</a><a id="331" class="Symbol">)</a>
<a id="333" class="Keyword">open</a> <a id="338" class="Keyword">import</a> <a id="345" href="Data.Maybe.html" class="Module">Data.Maybe</a> <a id="356" class="Symbol">as</a> <a id="359" class="Module">Maybe</a>
  <a id="367" class="Keyword">using</a> <a id="373" class="Symbol">(</a><a id="374" href="Data.Maybe.Base.html#Maybe" class="Datatype">Maybe</a><a id="379" class="Symbol">;</a> <a id="381" href="Data.Maybe.Base.html#decToMaybe" class="Function">decToMaybe</a><a id="391" class="Symbol">;</a> <a id="393" href="Data.Maybe.Base.html#From-just" class="Function">From-just</a><a id="402" class="Symbol">;</a> <a id="404" href="Data.Maybe.Base.html#from-just" class="Function">from-just</a><a id="413" class="Symbol">)</a>
<a id="415" class="Keyword">open</a> <a id="420" class="Keyword">import</a> <a id="427" href="Data.Nat.Base.html" class="Module">Data.Nat.Base</a> <a id="441" class="Symbol">as</a> <a id="444" class="Module">ℕ</a> <a id="446" class="Keyword">using</a> <a id="452" class="Symbol">(</a><a id="453" href="Agda.Builtin.Nat.html#Nat" class="Datatype">ℕ</a><a id="454" class="Symbol">;</a> <a id="456" href="Agda.Builtin.Nat.html#Nat.zero" class="InductiveConstructor">zero</a><a id="460" class="Symbol">;</a> <a id="462" href="Agda.Builtin.Nat.html#Nat.suc" class="InductiveConstructor">suc</a><a id="465" class="Symbol">;</a> <a id="467" href="Agda.Builtin.Nat.html#_%2B_" class="Primitive Operator">_+_</a><a id="470" class="Symbol">)</a>
<a id="472" class="Keyword">open</a> <a id="477" class="Keyword">import</a> <a id="484" href="Data.Nat.GeneralisedArithmetic.html" class="Module">Data.Nat.GeneralisedArithmetic</a> <a id="515" class="Keyword">using</a> <a id="521" class="Symbol">(</a><a id="522" href="Data.Nat.GeneralisedArithmetic.html#472" class="Function">fold</a><a id="526" class="Symbol">)</a>
<a id="528" class="Keyword">open</a> <a id="533" class="Keyword">import</a> <a id="540" href="Data.Product.html" class="Module">Data.Product</a> <a id="553" class="Keyword">using</a> <a id="559" class="Symbol">(</a><a id="560" href="Data.Product.html#_%C3%97_" class="Function Operator">_×_</a><a id="563" class="Symbol">;</a> <a id="565" href="Data.Product.html#%CE%A3.proj%E2%82%81" class="Field">proj₁</a><a id="570" class="Symbol">;</a> <a id="572" href="Data.Product.html#%CE%A3.proj%E2%82%82" class="Field">proj₂</a><a id="577" class="Symbol">;</a> <a id="579" href="Data.Product.html#uncurry" class="Function">uncurry</a><a id="586" class="Symbol">)</a>
<a id="588" class="Keyword">open</a> <a id="593" class="Keyword">import</a> <a id="600" href="Data.Vec.html" class="Module">Data.Vec</a> <a id="609" class="Keyword">using</a> <a id="615" class="Symbol">(</a><a id="616" href="Data.Vec.html#Vec" class="Datatype">Vec</a><a id="619" class="Symbol">;</a> <a id="621" href="Data.Vec.html#Vec.%5B%5D" class="InductiveConstructor">[]</a><a id="623" class="Symbol">;</a> <a id="625" href="Data.Vec.html#Vec._%E2%88%B7_" class="InductiveConstructor Operator">_∷_</a><a id="628" class="Symbol">;</a> <a id="630" href="Data.Vec.html#lookup" class="Function">lookup</a><a id="636" class="Symbol">;</a> <a id="638" href="Data.Vec.html#replicate" class="Function">replicate</a><a id="647" class="Symbol">)</a>

<a id="650" class="Keyword">open</a> <a id="655" class="Keyword">import</a> <a id="662" href="Function.html" class="Module">Function</a> <a id="671" class="Keyword">using</a> <a id="677" class="Symbol">(</a><a id="678" href="Function.html#_%E2%88%98_" class="Function Operator">_∘_</a><a id="681" class="Symbol">)</a>

<a id="684" class="Keyword">import</a> <a id="691" href="Relation.Binary.EqReasoning.html" class="Module">Relation.Binary.EqReasoning</a>   <a id="721" class="Symbol">as</a> <a id="724" class="Module">EqReasoning</a>
<a id="736" class="Keyword">import</a> <a id="743" href="Relation.Binary.Reflection.html" class="Module">Relation.Binary.Reflection</a>    <a id="773" class="Symbol">as</a> <a id="776" class="Module">Reflection</a>
<a id="787" class="Keyword">import</a> <a id="794" href="Relation.Binary.Vec.Pointwise.html" class="Module">Relation.Binary.Vec.Pointwise</a> <a id="824" class="Symbol">as</a> <a id="827" class="Module">Pointwise</a>
<a id="837" class="Keyword">import</a> <a id="844" href="Relation.Nullary.Decidable.html" class="Module">Relation.Nullary.Decidable</a>    <a id="874" class="Symbol">as</a> <a id="877" class="Module">Dec</a>

<a id="882" class="Keyword">open</a> <a id="887" class="Keyword">import</a> <a id="894" href="Relation.Binary.PropositionalEquality.html" class="Module">Relation.Binary.PropositionalEquality</a> <a id="932" class="Symbol">as</a> <a id="935" class="Module">P</a> <a id="937" class="Keyword">using</a> <a id="943" class="Symbol">(</a><a id="944" href="Agda.Builtin.Equality.html#_%E2%89%A1_" class="Datatype Operator">_≡_</a><a id="947" class="Symbol">;</a> <a id="949" href="Relation.Binary.PropositionalEquality.html#decSetoid" class="Function">decSetoid</a><a id="958" class="Symbol">)</a>
<a id="960" class="Keyword">open</a> <a id="965" class="Keyword">import</a> <a id="972" href="Relation.Nullary.html" class="Module">Relation.Nullary</a> <a id="989" class="Keyword">using</a> <a id="995" class="Symbol">(</a><a id="996" href="Relation.Nullary.html#Dec" class="Datatype">Dec</a><a id="999" class="Symbol">)</a>

<a id="1002" class="Keyword">module</a> <a id="1009" href="Algebra.CommutativeMonoidSolver.html" class="Module">Algebra.CommutativeMonoidSolver</a> <a id="1041" class="Symbol">{</a><a id="1042" href="Algebra.CommutativeMonoidSolver.html#1042" class="Bound">m₁</a> <a id="1045" href="Algebra.CommutativeMonoidSolver.html#1045" class="Bound">m₂</a><a id="1047" class="Symbol">}</a> <a id="1049" class="Symbol">(</a><a id="1050" href="Algebra.CommutativeMonoidSolver.html#1050" class="Bound">M</a> <a id="1052" class="Symbol">:</a> <a id="1054" href="Algebra.html#CommutativeMonoid" class="Record">CommutativeMonoid</a> <a id="1072" href="Algebra.CommutativeMonoidSolver.html#1042" class="Bound">m₁</a> <a id="1075" href="Algebra.CommutativeMonoidSolver.html#1045" class="Bound">m₂</a><a id="1077" class="Symbol">)</a> <a id="1079" class="Keyword">where</a>

<a id="1086" class="Keyword">open</a> <a id="1091" href="Algebra.html#CommutativeMonoid" class="Module">CommutativeMonoid</a> <a id="1109" href="Algebra.CommutativeMonoidSolver.html#1050" class="Bound">M</a>
<a id="1111" class="Keyword">open</a> <a id="1116" href="Relation.Binary.EqReasoning.html" class="Module">EqReasoning</a> <a id="1128" href="Algebra.html#845" class="Function">setoid</a>

<a id="1136" class="Comment">------------------------------------------------------------------------</a>
<a id="1209" class="Comment">-- Monoid expressions</a>

<a id="1232" class="Comment">-- There is one constructor for every operation, plus one for</a>
<a id="1294" class="Comment">-- variables; there may be at most n variables.</a>

<a id="1343" class="Keyword">infixr</a> <a id="1350" class="Number">5</a> <a id="1352" href="Algebra.CommutativeMonoidSolver.html#Expr._%E2%8A%95_" class="InductiveConstructor Operator">_⊕_</a>
<a id="1356" class="Keyword">infixr</a> <a id="1363" class="Number">10</a> <a id="1366" href="Algebra.CommutativeMonoidSolver.html#_%E2%80%A2_" class="Function Operator">_•_</a>

<a id="1371" class="Keyword">data</a> <a id="Expr" href="Algebra.CommutativeMonoidSolver.html#Expr" class="Datatype">Expr</a> <a id="1381" class="Symbol">(</a><a id="1382" href="Algebra.CommutativeMonoidSolver.html#1382" class="Bound">n</a> <a id="1384" class="Symbol">:</a> <a id="1386" href="Agda.Builtin.Nat.html#%E2%84%95" class="Datatype">ℕ</a><a id="1387" class="Symbol">)</a> <a id="1389" class="Symbol">:</a> <a id="1391" class="PrimitiveType">Set</a> <a id="1395" class="Keyword">where</a>
  <a id="Expr.var" href="Algebra.CommutativeMonoidSolver.html#Expr.var" class="InductiveConstructor">var</a> <a id="1407" class="Symbol">:</a> <a id="1409" href="Data.Fin.html#Fin" class="Datatype">Fin</a> <a id="1413" href="Algebra.CommutativeMonoidSolver.html#1382" class="Bound">n</a> <a id="1415" class="Symbol">→</a> <a id="1417" href="Algebra.CommutativeMonoidSolver.html#Expr" class="Datatype">Expr</a> <a id="1422" href="Algebra.CommutativeMonoidSolver.html#1382" class="Bound">n</a>
  <a id="Expr.id" href="Algebra.CommutativeMonoidSolver.html#Expr.id" class="InductiveConstructor">id</a>  <a id="1430" class="Symbol">:</a> <a id="1432" href="Algebra.CommutativeMonoidSolver.html#Expr" class="Datatype">Expr</a> <a id="1437" href="Algebra.CommutativeMonoidSolver.html#1382" class="Bound">n</a>
  <a id="Expr._⊕_" href="Algebra.CommutativeMonoidSolver.html#Expr._%E2%8A%95_" class="InductiveConstructor Operator">_⊕_</a> <a id="1445" class="Symbol">:</a> <a id="1447" href="Algebra.CommutativeMonoidSolver.html#Expr" class="Datatype">Expr</a> <a id="1452" href="Algebra.CommutativeMonoidSolver.html#1382" class="Bound">n</a> <a id="1454" class="Symbol">→</a> <a id="1456" href="Algebra.CommutativeMonoidSolver.html#Expr" class="Datatype">Expr</a> <a id="1461" href="Algebra.CommutativeMonoidSolver.html#1382" class="Bound">n</a> <a id="1463" class="Symbol">→</a> <a id="1465" href="Algebra.CommutativeMonoidSolver.html#Expr" class="Datatype">Expr</a> <a id="1470" href="Algebra.CommutativeMonoidSolver.html#1382" class="Bound">n</a>

<a id="1473" class="Comment">-- An environment contains one value for every variable.</a>

<a id="Env" href="Algebra.CommutativeMonoidSolver.html#Env" class="Function">Env</a> <a id="1535" class="Symbol">:</a> <a id="1537" href="Agda.Builtin.Nat.html#%E2%84%95" class="Datatype">ℕ</a> <a id="1539" class="Symbol">→</a> <a id="1541" class="PrimitiveType">Set</a> <a id="1545" class="Symbol">_</a>
<a id="1547" href="Algebra.CommutativeMonoidSolver.html#Env" class="Function">Env</a> <a id="1551" href="Algebra.CommutativeMonoidSolver.html#1551" class="Bound">n</a> <a id="1553" class="Symbol">=</a> <a id="1555" href="Data.Vec.html#Vec" class="Datatype">Vec</a> <a id="1559" href="Algebra.html#1726" class="Field">Carrier</a> <a id="1567" href="Algebra.CommutativeMonoidSolver.html#1551" class="Bound">n</a>

<a id="1570" class="Comment">-- The semantics of an expression is a function from an environment to</a>
<a id="1641" class="Comment">-- a value.</a>

<a id="⟦_⟧" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟦_⟧</a> <a id="1658" class="Symbol">:</a> <a id="1660" class="Symbol">∀</a> <a id="1662" class="Symbol">{</a><a id="1663" href="Algebra.CommutativeMonoidSolver.html#1663" class="Bound">n</a><a id="1664" class="Symbol">}</a> <a id="1666" class="Symbol">→</a> <a id="1668" href="Algebra.CommutativeMonoidSolver.html#Expr" class="Datatype">Expr</a> <a id="1673" href="Algebra.CommutativeMonoidSolver.html#1663" class="Bound">n</a> <a id="1675" class="Symbol">→</a> <a id="1677" href="Algebra.CommutativeMonoidSolver.html#Env" class="Function">Env</a> <a id="1681" href="Algebra.CommutativeMonoidSolver.html#1663" class="Bound">n</a> <a id="1683" class="Symbol">→</a> <a id="1685" href="Algebra.html#1726" class="Field">Carrier</a>
<a id="1693" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟦</a> <a id="1695" href="Algebra.CommutativeMonoidSolver.html#Expr.var" class="InductiveConstructor">var</a> <a id="1699" href="Algebra.CommutativeMonoidSolver.html#1699" class="Bound">x</a>   <a id="1703" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟧</a> <a id="1705" href="Algebra.CommutativeMonoidSolver.html#1705" class="Bound">ρ</a> <a id="1707" class="Symbol">=</a> <a id="1709" href="Data.Vec.html#lookup" class="Function">lookup</a> <a id="1716" href="Algebra.CommutativeMonoidSolver.html#1699" class="Bound">x</a> <a id="1718" href="Algebra.CommutativeMonoidSolver.html#1705" class="Bound">ρ</a>
<a id="1720" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟦</a> <a id="1722" href="Algebra.CommutativeMonoidSolver.html#Expr.id" class="InductiveConstructor">id</a>      <a id="1730" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟧</a> <a id="1732" href="Algebra.CommutativeMonoidSolver.html#1732" class="Bound">ρ</a> <a id="1734" class="Symbol">=</a> <a id="1736" href="Algebra.html#1836" class="Field">ε</a>
<a id="1738" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟦</a> <a id="1740" href="Algebra.CommutativeMonoidSolver.html#1740" class="Bound">e₁</a> <a id="1743" href="Algebra.CommutativeMonoidSolver.html#Expr._%E2%8A%95_" class="InductiveConstructor Operator">⊕</a> <a id="1745" href="Algebra.CommutativeMonoidSolver.html#1745" class="Bound">e₂</a> <a id="1748" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟧</a> <a id="1750" href="Algebra.CommutativeMonoidSolver.html#1750" class="Bound">ρ</a> <a id="1752" class="Symbol">=</a> <a id="1754" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟦</a> <a id="1756" href="Algebra.CommutativeMonoidSolver.html#1740" class="Bound">e₁</a> <a id="1759" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟧</a> <a id="1761" href="Algebra.CommutativeMonoidSolver.html#1750" class="Bound">ρ</a> <a id="1763" href="Algebra.html#1798" class="Field Operator">∙</a> <a id="1765" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟦</a> <a id="1767" href="Algebra.CommutativeMonoidSolver.html#1745" class="Bound">e₂</a> <a id="1770" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟧</a> <a id="1772" href="Algebra.CommutativeMonoidSolver.html#1750" class="Bound">ρ</a>

<a id="1775" class="Comment">------------------------------------------------------------------------</a>
<a id="1848" class="Comment">-- Normal forms</a>

<a id="1865" class="Comment">-- A normal form is a vector of multiplicities (a bag).</a>

<a id="Normal" href="Algebra.CommutativeMonoidSolver.html#Normal" class="Function">Normal</a> <a id="1929" class="Symbol">:</a> <a id="1931" href="Agda.Builtin.Nat.html#%E2%84%95" class="Datatype">ℕ</a> <a id="1933" class="Symbol">→</a> <a id="1935" class="PrimitiveType">Set</a>
<a id="1939" href="Algebra.CommutativeMonoidSolver.html#Normal" class="Function">Normal</a> <a id="1946" href="Algebra.CommutativeMonoidSolver.html#1946" class="Bound">n</a> <a id="1948" class="Symbol">=</a> <a id="1950" href="Data.Vec.html#Vec" class="Datatype">Vec</a> <a id="1954" href="Agda.Builtin.Nat.html#%E2%84%95" class="Datatype">ℕ</a> <a id="1956" href="Algebra.CommutativeMonoidSolver.html#1946" class="Bound">n</a>

<a id="1959" class="Comment">-- The semantics of a normal form.</a>

<a id="⟦_⟧⇓" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7%E2%87%93" class="Function Operator">⟦_⟧⇓</a> <a id="2000" class="Symbol">:</a> <a id="2002" class="Symbol">∀</a> <a id="2004" class="Symbol">{</a><a id="2005" href="Algebra.CommutativeMonoidSolver.html#2005" class="Bound">n</a><a id="2006" class="Symbol">}</a> <a id="2008" class="Symbol">→</a> <a id="2010" href="Algebra.CommutativeMonoidSolver.html#Normal" class="Function">Normal</a> <a id="2017" href="Algebra.CommutativeMonoidSolver.html#2005" class="Bound">n</a> <a id="2019" class="Symbol">→</a> <a id="2021" href="Algebra.CommutativeMonoidSolver.html#Env" class="Function">Env</a> <a id="2025" href="Algebra.CommutativeMonoidSolver.html#2005" class="Bound">n</a> <a id="2027" class="Symbol">→</a> <a id="2029" href="Algebra.html#1726" class="Field">Carrier</a>
<a id="2037" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7%E2%87%93" class="Function Operator">⟦</a> <a id="2039" href="Data.Vec.html#Vec.%5B%5D" class="InductiveConstructor">[]</a>    <a id="2045" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7%E2%87%93" class="Function Operator">⟧⇓</a> <a id="2048" class="Symbol">_</a> <a id="2050" class="Symbol">=</a> <a id="2052" href="Algebra.html#1836" class="Field">ε</a>
<a id="2054" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7%E2%87%93" class="Function Operator">⟦</a> <a id="2056" href="Algebra.CommutativeMonoidSolver.html#2056" class="Bound">n</a> <a id="2058" href="Data.Vec.html#Vec._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="2060" href="Algebra.CommutativeMonoidSolver.html#2060" class="Bound">v</a> <a id="2062" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7%E2%87%93" class="Function Operator">⟧⇓</a> <a id="2065" class="Symbol">(</a><a id="2066" href="Algebra.CommutativeMonoidSolver.html#2066" class="Bound">a</a> <a id="2068" href="Data.Vec.html#Vec._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="2070" href="Algebra.CommutativeMonoidSolver.html#2070" class="Bound">ρ</a><a id="2071" class="Symbol">)</a> <a id="2073" class="Symbol">=</a> <a id="2075" href="Data.Nat.GeneralisedArithmetic.html#472" class="Function">fold</a> <a id="2080" class="Symbol">(</a><a id="2081" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7%E2%87%93" class="Function Operator">⟦</a> <a id="2083" href="Algebra.CommutativeMonoidSolver.html#2060" class="Bound">v</a> <a id="2085" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7%E2%87%93" class="Function Operator">⟧⇓</a> <a id="2088" href="Algebra.CommutativeMonoidSolver.html#2070" class="Bound">ρ</a><a id="2089" class="Symbol">)</a> <a id="2091" class="Symbol">(λ</a> <a id="2094" href="Algebra.CommutativeMonoidSolver.html#2094" class="Bound">b</a> <a id="2096" class="Symbol">→</a> <a id="2098" href="Algebra.CommutativeMonoidSolver.html#2066" class="Bound">a</a> <a id="2100" href="Algebra.html#1798" class="Field Operator">∙</a> <a id="2102" href="Algebra.CommutativeMonoidSolver.html#2094" class="Bound">b</a><a id="2103" class="Symbol">)</a> <a id="2105" href="Algebra.CommutativeMonoidSolver.html#2056" class="Bound">n</a>

<a id="2108" class="Comment">------------------------------------------------------------------------</a>
<a id="2181" class="Comment">-- Constructions on normal forms</a>

<a id="2215" class="Comment">-- The empty bag.</a>

<a id="empty" href="Algebra.CommutativeMonoidSolver.html#empty" class="Function">empty</a> <a id="2240" class="Symbol">:</a> <a id="2242" class="Symbol">∀{</a><a id="2244" href="Algebra.CommutativeMonoidSolver.html#2244" class="Bound">n</a><a id="2245" class="Symbol">}</a> <a id="2247" class="Symbol">→</a> <a id="2249" href="Algebra.CommutativeMonoidSolver.html#Normal" class="Function">Normal</a> <a id="2256" href="Algebra.CommutativeMonoidSolver.html#2244" class="Bound">n</a>
<a id="2258" href="Algebra.CommutativeMonoidSolver.html#empty" class="Function">empty</a> <a id="2264" class="Symbol">=</a> <a id="2266" href="Data.Vec.html#replicate" class="Function">replicate</a> <a id="2276" class="Number">0</a>

<a id="2279" class="Comment">-- A singleton bag.</a>

<a id="sg" href="Algebra.CommutativeMonoidSolver.html#sg" class="Function">sg</a> <a id="2303" class="Symbol">:</a> <a id="2305" class="Symbol">∀{</a><a id="2307" href="Algebra.CommutativeMonoidSolver.html#2307" class="Bound">n</a><a id="2308" class="Symbol">}</a> <a id="2310" class="Symbol">(</a><a id="2311" href="Algebra.CommutativeMonoidSolver.html#2311" class="Bound">i</a> <a id="2313" class="Symbol">:</a> <a id="2315" href="Data.Fin.html#Fin" class="Datatype">Fin</a> <a id="2319" href="Algebra.CommutativeMonoidSolver.html#2307" class="Bound">n</a><a id="2320" class="Symbol">)</a> <a id="2322" class="Symbol">→</a> <a id="2324" href="Algebra.CommutativeMonoidSolver.html#Normal" class="Function">Normal</a> <a id="2331" href="Algebra.CommutativeMonoidSolver.html#2307" class="Bound">n</a>
<a id="2333" href="Algebra.CommutativeMonoidSolver.html#sg" class="Function">sg</a> <a id="2336" href="Data.Fin.html#Fin.zero" class="InductiveConstructor">zero</a>    <a id="2344" class="Symbol">=</a> <a id="2346" class="Number">1</a> <a id="2348" href="Data.Vec.html#Vec._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="2350" href="Algebra.CommutativeMonoidSolver.html#empty" class="Function">empty</a>
<a id="2356" href="Algebra.CommutativeMonoidSolver.html#sg" class="Function">sg</a> <a id="2359" class="Symbol">(</a><a id="2360" href="Data.Fin.html#Fin.suc" class="InductiveConstructor">suc</a> <a id="2364" href="Algebra.CommutativeMonoidSolver.html#2364" class="Bound">i</a><a id="2365" class="Symbol">)</a> <a id="2367" class="Symbol">=</a> <a id="2369" class="Number">0</a> <a id="2371" href="Data.Vec.html#Vec._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="2373" href="Algebra.CommutativeMonoidSolver.html#sg" class="Function">sg</a> <a id="2376" href="Algebra.CommutativeMonoidSolver.html#2364" class="Bound">i</a>

<a id="2379" class="Comment">-- The composition of normal forms.</a>

<a id="_•_" href="Algebra.CommutativeMonoidSolver.html#_%E2%80%A2_" class="Function Operator">_•_</a>  <a id="2421" class="Symbol">:</a> <a id="2423" class="Symbol">∀{</a><a id="2425" href="Algebra.CommutativeMonoidSolver.html#2425" class="Bound">n</a><a id="2426" class="Symbol">}</a> <a id="2428" class="Symbol">(</a><a id="2429" href="Algebra.CommutativeMonoidSolver.html#2429" class="Bound">v</a> <a id="2431" href="Algebra.CommutativeMonoidSolver.html#2431" class="Bound">w</a> <a id="2433" class="Symbol">:</a> <a id="2435" href="Algebra.CommutativeMonoidSolver.html#Normal" class="Function">Normal</a> <a id="2442" href="Algebra.CommutativeMonoidSolver.html#2425" class="Bound">n</a><a id="2443" class="Symbol">)</a> <a id="2445" class="Symbol">→</a> <a id="2447" href="Algebra.CommutativeMonoidSolver.html#Normal" class="Function">Normal</a> <a id="2454" href="Algebra.CommutativeMonoidSolver.html#2425" class="Bound">n</a>
<a id="2456" href="Data.Vec.html#Vec.%5B%5D" class="InductiveConstructor">[]</a>      <a id="2464" href="Algebra.CommutativeMonoidSolver.html#_%E2%80%A2_" class="Function Operator">•</a> <a id="2466" href="Data.Vec.html#Vec.%5B%5D" class="InductiveConstructor">[]</a>      <a id="2474" class="Symbol">=</a> <a id="2476" href="Data.Vec.html#Vec.%5B%5D" class="InductiveConstructor">[]</a>
<a id="2479" class="Symbol">(</a><a id="2480" href="Algebra.CommutativeMonoidSolver.html#2480" class="Bound">l</a> <a id="2482" href="Data.Vec.html#Vec._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="2484" href="Algebra.CommutativeMonoidSolver.html#2484" class="Bound">v</a><a id="2485" class="Symbol">)</a> <a id="2487" href="Algebra.CommutativeMonoidSolver.html#_%E2%80%A2_" class="Function Operator">•</a> <a id="2489" class="Symbol">(</a><a id="2490" href="Algebra.CommutativeMonoidSolver.html#2490" class="Bound">m</a> <a id="2492" href="Data.Vec.html#Vec._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="2494" href="Algebra.CommutativeMonoidSolver.html#2494" class="Bound">w</a><a id="2495" class="Symbol">)</a> <a id="2497" class="Symbol">=</a> <a id="2499" href="Algebra.CommutativeMonoidSolver.html#2480" class="Bound">l</a> <a id="2501" href="Agda.Builtin.Nat.html#_%2B_" class="Primitive Operator">+</a> <a id="2503" href="Algebra.CommutativeMonoidSolver.html#2490" class="Bound">m</a> <a id="2505" href="Data.Vec.html#Vec._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="2507" href="Algebra.CommutativeMonoidSolver.html#2484" class="Bound">v</a> <a id="2509" href="Algebra.CommutativeMonoidSolver.html#_%E2%80%A2_" class="Function Operator">•</a> <a id="2511" href="Algebra.CommutativeMonoidSolver.html#2494" class="Bound">w</a>

<a id="2514" class="Comment">------------------------------------------------------------------------</a>
<a id="2587" class="Comment">-- Correctness of the constructions on normal forms</a>

<a id="2640" class="Comment">-- The empty bag stands for the unit ε.</a>

<a id="empty-correct" href="Algebra.CommutativeMonoidSolver.html#empty-correct" class="Function">empty-correct</a> <a id="2695" class="Symbol">:</a> <a id="2697" class="Symbol">∀{</a><a id="2699" href="Algebra.CommutativeMonoidSolver.html#2699" class="Bound">n</a><a id="2700" class="Symbol">}</a> <a id="2702" class="Symbol">(</a><a id="2703" href="Algebra.CommutativeMonoidSolver.html#2703" class="Bound">ρ</a> <a id="2705" class="Symbol">:</a> <a id="2707" href="Algebra.CommutativeMonoidSolver.html#Env" class="Function">Env</a> <a id="2711" href="Algebra.CommutativeMonoidSolver.html#2699" class="Bound">n</a><a id="2712" class="Symbol">)</a> <a id="2714" class="Symbol">→</a> <a id="2716" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7%E2%87%93" class="Function Operator">⟦</a> <a id="2718" href="Algebra.CommutativeMonoidSolver.html#empty" class="Function">empty</a> <a id="2724" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7%E2%87%93" class="Function Operator">⟧⇓</a> <a id="2727" href="Algebra.CommutativeMonoidSolver.html#2703" class="Bound">ρ</a> <a id="2729" href="Algebra.html#1758" class="Field Operator">≈</a> <a id="2731" href="Algebra.html#1836" class="Field">ε</a>
<a id="2733" href="Algebra.CommutativeMonoidSolver.html#empty-correct" class="Function">empty-correct</a> <a id="2747" href="Data.Vec.html#Vec.%5B%5D" class="InductiveConstructor">[]</a> <a id="2750" class="Symbol">=</a> <a id="2752" href="Relation.Binary.Core.html#refl" class="Function">refl</a>
<a id="2757" href="Algebra.CommutativeMonoidSolver.html#empty-correct" class="Function">empty-correct</a> <a id="2771" class="Symbol">(</a><a id="2772" href="Algebra.CommutativeMonoidSolver.html#2772" class="Bound">a</a> <a id="2774" href="Data.Vec.html#Vec._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="2776" href="Algebra.CommutativeMonoidSolver.html#2776" class="Bound">ρ</a><a id="2777" class="Symbol">)</a> <a id="2779" class="Symbol">=</a> <a id="2781" href="Algebra.CommutativeMonoidSolver.html#empty-correct" class="Function">empty-correct</a> <a id="2795" href="Algebra.CommutativeMonoidSolver.html#2776" class="Bound">ρ</a>

<a id="2798" class="Comment">-- The singleton bag stands for a single variable.</a>

<a id="sg-correct" href="Algebra.CommutativeMonoidSolver.html#sg-correct" class="Function">sg-correct</a> <a id="2861" class="Symbol">:</a> <a id="2863" class="Symbol">∀{</a><a id="2865" href="Algebra.CommutativeMonoidSolver.html#2865" class="Bound">n</a><a id="2866" class="Symbol">}</a> <a id="2868" class="Symbol">(</a><a id="2869" href="Algebra.CommutativeMonoidSolver.html#2869" class="Bound">x</a> <a id="2871" class="Symbol">:</a> <a id="2873" href="Data.Fin.html#Fin" class="Datatype">Fin</a> <a id="2877" href="Algebra.CommutativeMonoidSolver.html#2865" class="Bound">n</a><a id="2878" class="Symbol">)</a> <a id="2880" class="Symbol">(</a><a id="2881" href="Algebra.CommutativeMonoidSolver.html#2881" class="Bound">ρ</a> <a id="2883" class="Symbol">:</a> <a id="2885" href="Algebra.CommutativeMonoidSolver.html#Env" class="Function">Env</a> <a id="2889" href="Algebra.CommutativeMonoidSolver.html#2865" class="Bound">n</a><a id="2890" class="Symbol">)</a> <a id="2892" class="Symbol">→</a>  <a id="2895" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7%E2%87%93" class="Function Operator">⟦</a> <a id="2897" href="Algebra.CommutativeMonoidSolver.html#sg" class="Function">sg</a> <a id="2900" href="Algebra.CommutativeMonoidSolver.html#2869" class="Bound">x</a> <a id="2902" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7%E2%87%93" class="Function Operator">⟧⇓</a> <a id="2905" href="Algebra.CommutativeMonoidSolver.html#2881" class="Bound">ρ</a> <a id="2907" href="Algebra.html#1758" class="Field Operator">≈</a> <a id="2909" href="Data.Vec.html#lookup" class="Function">lookup</a> <a id="2916" href="Algebra.CommutativeMonoidSolver.html#2869" class="Bound">x</a> <a id="2918" href="Algebra.CommutativeMonoidSolver.html#2881" class="Bound">ρ</a>
<a id="2920" href="Algebra.CommutativeMonoidSolver.html#sg-correct" class="Function">sg-correct</a> <a id="2931" href="Data.Fin.html#Fin.zero" class="InductiveConstructor">zero</a> <a id="2936" class="Symbol">(</a><a id="2937" href="Algebra.CommutativeMonoidSolver.html#2937" class="Bound">x</a> <a id="2939" href="Data.Vec.html#Vec._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="2941" href="Algebra.CommutativeMonoidSolver.html#2941" class="Bound">ρ</a><a id="2942" class="Symbol">)</a> <a id="2944" class="Symbol">=</a> <a id="2946" href="Relation.Binary.PreorderReasoning.html#begin_" class="Function Operator">begin</a>
    <a id="2956" href="Algebra.CommutativeMonoidSolver.html#2937" class="Bound">x</a> <a id="2958" href="Algebra.html#1798" class="Field Operator">∙</a> <a id="2960" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7%E2%87%93" class="Function Operator">⟦</a> <a id="2962" href="Algebra.CommutativeMonoidSolver.html#empty" class="Function">empty</a> <a id="2968" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7%E2%87%93" class="Function Operator">⟧⇓</a> <a id="2971" href="Algebra.CommutativeMonoidSolver.html#2941" class="Bound">ρ</a>   <a id="2975" href="Relation.Binary.PreorderReasoning.html#_%E2%89%88%E2%9F%A8_%E2%9F%A9_" class="Function Operator">≈⟨</a> <a id="2978" href="Algebra.Structures.html#845" class="Function">∙-cong</a> <a id="2985" href="Relation.Binary.Core.html#refl" class="Function">refl</a> <a id="2990" class="Symbol">(</a><a id="2991" href="Algebra.CommutativeMonoidSolver.html#empty-correct" class="Function">empty-correct</a> <a id="3005" href="Algebra.CommutativeMonoidSolver.html#2941" class="Bound">ρ</a><a id="3006" class="Symbol">)</a> <a id="3008" href="Relation.Binary.PreorderReasoning.html#_%E2%89%88%E2%9F%A8_%E2%9F%A9_" class="Function Operator">⟩</a>
    <a id="3014" href="Algebra.CommutativeMonoidSolver.html#2937" class="Bound">x</a> <a id="3016" href="Algebra.html#1798" class="Field Operator">∙</a> <a id="3018" href="Algebra.html#1836" class="Field">ε</a>              <a id="3033" href="Relation.Binary.PreorderReasoning.html#_%E2%89%88%E2%9F%A8_%E2%9F%A9_" class="Function Operator">≈⟨</a> <a id="3036" href="Data.Product.html#%CE%A3.proj%E2%82%82" class="Field">proj₂</a> <a id="3042" href="Algebra.Structures.html#1486" class="Function">identity</a> <a id="3051" class="Symbol">_</a> <a id="3053" href="Relation.Binary.PreorderReasoning.html#_%E2%89%88%E2%9F%A8_%E2%9F%A9_" class="Function Operator">⟩</a>
    <a id="3059" href="Algebra.CommutativeMonoidSolver.html#2937" class="Bound">x</a>                  <a id="3078" href="Relation.Binary.PreorderReasoning.html#_%E2%88%8E" class="Function Operator">∎</a>
<a id="3080" href="Algebra.CommutativeMonoidSolver.html#sg-correct" class="Function">sg-correct</a> <a id="3091" class="Symbol">(</a><a id="3092" href="Data.Fin.html#Fin.suc" class="InductiveConstructor">suc</a> <a id="3096" href="Algebra.CommutativeMonoidSolver.html#3096" class="Bound">x</a><a id="3097" class="Symbol">)</a> <a id="3099" class="Symbol">(</a><a id="3100" href="Algebra.CommutativeMonoidSolver.html#3100" class="Bound">m</a> <a id="3102" href="Data.Vec.html#Vec._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="3104" href="Algebra.CommutativeMonoidSolver.html#3104" class="Bound">ρ</a><a id="3105" class="Symbol">)</a> <a id="3107" class="Symbol">=</a> <a id="3109" href="Algebra.CommutativeMonoidSolver.html#sg-correct" class="Function">sg-correct</a> <a id="3120" href="Algebra.CommutativeMonoidSolver.html#3096" class="Bound">x</a> <a id="3122" href="Algebra.CommutativeMonoidSolver.html#3104" class="Bound">ρ</a>

<a id="3125" class="Comment">-- Normal form composition corresponds to the composition of the monoid.</a>

<a id="comp-correct" href="Algebra.CommutativeMonoidSolver.html#comp-correct" class="Function">comp-correct</a> <a id="3212" class="Symbol">:</a> <a id="3214" class="Symbol">∀</a> <a id="3216" class="Symbol">{</a><a id="3217" href="Algebra.CommutativeMonoidSolver.html#3217" class="Bound">n</a><a id="3218" class="Symbol">}</a> <a id="3220" class="Symbol">(</a><a id="3221" href="Algebra.CommutativeMonoidSolver.html#3221" class="Bound">v</a> <a id="3223" href="Algebra.CommutativeMonoidSolver.html#3223" class="Bound">w</a> <a id="3225" class="Symbol">:</a> <a id="3227" href="Algebra.CommutativeMonoidSolver.html#Normal" class="Function">Normal</a> <a id="3234" href="Algebra.CommutativeMonoidSolver.html#3217" class="Bound">n</a><a id="3235" class="Symbol">)</a> <a id="3237" class="Symbol">(</a><a id="3238" href="Algebra.CommutativeMonoidSolver.html#3238" class="Bound">ρ</a> <a id="3240" class="Symbol">:</a> <a id="3242" href="Algebra.CommutativeMonoidSolver.html#Env" class="Function">Env</a> <a id="3246" href="Algebra.CommutativeMonoidSolver.html#3217" class="Bound">n</a><a id="3247" class="Symbol">)</a> <a id="3249" class="Symbol">→</a>
              <a id="3265" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7%E2%87%93" class="Function Operator">⟦</a> <a id="3267" href="Algebra.CommutativeMonoidSolver.html#3221" class="Bound">v</a> <a id="3269" href="Algebra.CommutativeMonoidSolver.html#_%E2%80%A2_" class="Function Operator">•</a> <a id="3271" href="Algebra.CommutativeMonoidSolver.html#3223" class="Bound">w</a> <a id="3273" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7%E2%87%93" class="Function Operator">⟧⇓</a> <a id="3276" href="Algebra.CommutativeMonoidSolver.html#3238" class="Bound">ρ</a> <a id="3278" href="Algebra.html#1758" class="Field Operator">≈</a> <a id="3280" class="Symbol">(</a><a id="3281" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7%E2%87%93" class="Function Operator">⟦</a> <a id="3283" href="Algebra.CommutativeMonoidSolver.html#3221" class="Bound">v</a> <a id="3285" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7%E2%87%93" class="Function Operator">⟧⇓</a> <a id="3288" href="Algebra.CommutativeMonoidSolver.html#3238" class="Bound">ρ</a> <a id="3290" href="Algebra.html#1798" class="Field Operator">∙</a> <a id="3292" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7%E2%87%93" class="Function Operator">⟦</a> <a id="3294" href="Algebra.CommutativeMonoidSolver.html#3223" class="Bound">w</a> <a id="3296" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7%E2%87%93" class="Function Operator">⟧⇓</a> <a id="3299" href="Algebra.CommutativeMonoidSolver.html#3238" class="Bound">ρ</a><a id="3300" class="Symbol">)</a>
<a id="3302" href="Algebra.CommutativeMonoidSolver.html#comp-correct" class="Function">comp-correct</a> <a id="3315" href="Data.Vec.html#Vec.%5B%5D" class="InductiveConstructor">[]</a> <a id="3318" href="Data.Vec.html#Vec.%5B%5D" class="InductiveConstructor">[]</a> <a id="3321" href="Algebra.CommutativeMonoidSolver.html#3321" class="Bound">ρ</a> <a id="3323" class="Symbol">=</a>  <a id="3326" href="Relation.Binary.Core.html#sym" class="Function">sym</a> <a id="3330" class="Symbol">(</a><a id="3331" href="Data.Product.html#%CE%A3.proj%E2%82%81" class="Field">proj₁</a> <a id="3337" href="Algebra.Structures.html#1486" class="Function">identity</a> <a id="3346" class="Symbol">_)</a>
<a id="3349" href="Algebra.CommutativeMonoidSolver.html#comp-correct" class="Function">comp-correct</a> <a id="3362" class="Symbol">(</a><a id="3363" href="Algebra.CommutativeMonoidSolver.html#3363" class="Bound">l</a> <a id="3365" href="Data.Vec.html#Vec._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="3367" href="Algebra.CommutativeMonoidSolver.html#3367" class="Bound">v</a><a id="3368" class="Symbol">)</a> <a id="3370" class="Symbol">(</a><a id="3371" href="Algebra.CommutativeMonoidSolver.html#3371" class="Bound">m</a> <a id="3373" href="Data.Vec.html#Vec._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="3375" href="Algebra.CommutativeMonoidSolver.html#3375" class="Bound">w</a><a id="3376" class="Symbol">)</a> <a id="3378" class="Symbol">(</a><a id="3379" href="Algebra.CommutativeMonoidSolver.html#3379" class="Bound">a</a> <a id="3381" href="Data.Vec.html#Vec._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="3383" href="Algebra.CommutativeMonoidSolver.html#3383" class="Bound">ρ</a><a id="3384" class="Symbol">)</a> <a id="3386" class="Symbol">=</a> <a id="3388" href="Algebra.CommutativeMonoidSolver.html#3659" class="Function">lemma</a> <a id="3394" href="Algebra.CommutativeMonoidSolver.html#3363" class="Bound">l</a> <a id="3396" href="Algebra.CommutativeMonoidSolver.html#3371" class="Bound">m</a> <a id="3398" class="Symbol">(</a><a id="3399" href="Algebra.CommutativeMonoidSolver.html#comp-correct" class="Function">comp-correct</a> <a id="3412" href="Algebra.CommutativeMonoidSolver.html#3367" class="Bound">v</a> <a id="3414" href="Algebra.CommutativeMonoidSolver.html#3375" class="Bound">w</a> <a id="3416" href="Algebra.CommutativeMonoidSolver.html#3383" class="Bound">ρ</a><a id="3417" class="Symbol">)</a>
  <a id="3421" class="Keyword">where</a>
    <a id="3431" href="Algebra.CommutativeMonoidSolver.html#3431" class="Function">flip12</a> <a id="3438" class="Symbol">:</a> <a id="3440" class="Symbol">∀</a> <a id="3442" href="Algebra.CommutativeMonoidSolver.html#3442" class="Bound">a</a> <a id="3444" href="Algebra.CommutativeMonoidSolver.html#3444" class="Bound">b</a> <a id="3446" href="Algebra.CommutativeMonoidSolver.html#3446" class="Bound">c</a> <a id="3448" class="Symbol">→</a> <a id="3450" href="Algebra.CommutativeMonoidSolver.html#3442" class="Bound">a</a> <a id="3452" href="Algebra.html#1798" class="Field Operator">∙</a> <a id="3454" class="Symbol">(</a><a id="3455" href="Algebra.CommutativeMonoidSolver.html#3444" class="Bound">b</a> <a id="3457" href="Algebra.html#1798" class="Field Operator">∙</a> <a id="3459" href="Algebra.CommutativeMonoidSolver.html#3446" class="Bound">c</a><a id="3460" class="Symbol">)</a> <a id="3462" href="Algebra.html#1758" class="Field Operator">≈</a> <a id="3464" href="Algebra.CommutativeMonoidSolver.html#3444" class="Bound">b</a> <a id="3466" href="Algebra.html#1798" class="Field Operator">∙</a> <a id="3468" class="Symbol">(</a><a id="3469" href="Algebra.CommutativeMonoidSolver.html#3442" class="Bound">a</a> <a id="3471" href="Algebra.html#1798" class="Field Operator">∙</a> <a id="3473" href="Algebra.CommutativeMonoidSolver.html#3446" class="Bound">c</a><a id="3474" class="Symbol">)</a>
    <a id="3480" href="Algebra.CommutativeMonoidSolver.html#3431" class="Function">flip12</a> <a id="3487" href="Algebra.CommutativeMonoidSolver.html#3487" class="Bound">a</a> <a id="3489" href="Algebra.CommutativeMonoidSolver.html#3489" class="Bound">b</a> <a id="3491" href="Algebra.CommutativeMonoidSolver.html#3491" class="Bound">c</a> <a id="3493" class="Symbol">=</a> <a id="3495" href="Relation.Binary.PreorderReasoning.html#begin_" class="Function Operator">begin</a>
        <a id="3509" href="Algebra.CommutativeMonoidSolver.html#3487" class="Bound">a</a> <a id="3511" href="Algebra.html#1798" class="Field Operator">∙</a> <a id="3513" class="Symbol">(</a><a id="3514" href="Algebra.CommutativeMonoidSolver.html#3489" class="Bound">b</a> <a id="3516" href="Algebra.html#1798" class="Field Operator">∙</a> <a id="3518" href="Algebra.CommutativeMonoidSolver.html#3491" class="Bound">c</a><a id="3519" class="Symbol">)</a>  <a id="3522" href="Relation.Binary.PreorderReasoning.html#_%E2%89%88%E2%9F%A8_%E2%9F%A9_" class="Function Operator">≈⟨</a> <a id="3525" href="Relation.Binary.Core.html#sym" class="Function">sym</a> <a id="3529" class="Symbol">(</a><a id="3530" href="Algebra.Structures.html#811" class="Function">assoc</a> <a id="3536" class="Symbol">_</a> <a id="3538" class="Symbol">_</a> <a id="3540" class="Symbol">_)</a> <a id="3543" href="Relation.Binary.PreorderReasoning.html#_%E2%89%88%E2%9F%A8_%E2%9F%A9_" class="Function Operator">⟩</a>
        <a id="3553" class="Symbol">(</a><a id="3554" href="Algebra.CommutativeMonoidSolver.html#3487" class="Bound">a</a> <a id="3556" href="Algebra.html#1798" class="Field Operator">∙</a> <a id="3558" href="Algebra.CommutativeMonoidSolver.html#3489" class="Bound">b</a><a id="3559" class="Symbol">)</a> <a id="3561" href="Algebra.html#1798" class="Field Operator">∙</a> <a id="3563" href="Algebra.CommutativeMonoidSolver.html#3491" class="Bound">c</a>  <a id="3566" href="Relation.Binary.PreorderReasoning.html#_%E2%89%88%E2%9F%A8_%E2%9F%A9_" class="Function Operator">≈⟨</a> <a id="3569" href="Algebra.Structures.html#845" class="Function">∙-cong</a> <a id="3576" class="Symbol">(</a><a id="3577" href="Algebra.Structures.html#1414" class="Function">comm</a> <a id="3582" class="Symbol">_</a> <a id="3584" class="Symbol">_)</a> <a id="3587" href="Relation.Binary.Core.html#refl" class="Function">refl</a> <a id="3592" href="Relation.Binary.PreorderReasoning.html#_%E2%89%88%E2%9F%A8_%E2%9F%A9_" class="Function Operator">⟩</a>
        <a id="3602" class="Symbol">(</a><a id="3603" href="Algebra.CommutativeMonoidSolver.html#3489" class="Bound">b</a> <a id="3605" href="Algebra.html#1798" class="Field Operator">∙</a> <a id="3607" href="Algebra.CommutativeMonoidSolver.html#3487" class="Bound">a</a><a id="3608" class="Symbol">)</a> <a id="3610" href="Algebra.html#1798" class="Field Operator">∙</a> <a id="3612" href="Algebra.CommutativeMonoidSolver.html#3491" class="Bound">c</a>  <a id="3615" href="Relation.Binary.PreorderReasoning.html#_%E2%89%88%E2%9F%A8_%E2%9F%A9_" class="Function Operator">≈⟨</a> <a id="3618" href="Algebra.Structures.html#811" class="Function">assoc</a> <a id="3624" class="Symbol">_</a> <a id="3626" class="Symbol">_</a> <a id="3628" class="Symbol">_</a> <a id="3630" href="Relation.Binary.PreorderReasoning.html#_%E2%89%88%E2%9F%A8_%E2%9F%A9_" class="Function Operator">⟩</a>
        <a id="3640" href="Algebra.CommutativeMonoidSolver.html#3489" class="Bound">b</a> <a id="3642" href="Algebra.html#1798" class="Field Operator">∙</a> <a id="3644" class="Symbol">(</a><a id="3645" href="Algebra.CommutativeMonoidSolver.html#3487" class="Bound">a</a> <a id="3647" href="Algebra.html#1798" class="Field Operator">∙</a> <a id="3649" href="Algebra.CommutativeMonoidSolver.html#3491" class="Bound">c</a><a id="3650" class="Symbol">)</a>  <a id="3653" href="Relation.Binary.PreorderReasoning.html#_%E2%88%8E" class="Function Operator">∎</a>
    <a id="3659" href="Algebra.CommutativeMonoidSolver.html#3659" class="Function">lemma</a> <a id="3665" class="Symbol">:</a> <a id="3667" class="Symbol">∀</a> <a id="3669" href="Algebra.CommutativeMonoidSolver.html#3669" class="Bound">l</a> <a id="3671" href="Algebra.CommutativeMonoidSolver.html#3671" class="Bound">m</a> <a id="3673" class="Symbol">{</a><a id="3674" href="Algebra.CommutativeMonoidSolver.html#3674" class="Bound">d</a> <a id="3676" href="Algebra.CommutativeMonoidSolver.html#3676" class="Bound">b</a> <a id="3678" href="Algebra.CommutativeMonoidSolver.html#3678" class="Bound">c</a><a id="3679" class="Symbol">}</a> <a id="3681" class="Symbol">(</a><a id="3682" href="Algebra.CommutativeMonoidSolver.html#3682" class="Bound">p</a> <a id="3684" class="Symbol">:</a> <a id="3686" href="Algebra.CommutativeMonoidSolver.html#3674" class="Bound">d</a> <a id="3688" href="Algebra.html#1758" class="Field Operator">≈</a> <a id="3690" href="Algebra.CommutativeMonoidSolver.html#3676" class="Bound">b</a> <a id="3692" href="Algebra.html#1798" class="Field Operator">∙</a> <a id="3694" href="Algebra.CommutativeMonoidSolver.html#3678" class="Bound">c</a><a id="3695" class="Symbol">)</a> <a id="3697" class="Symbol">→</a>
      <a id="3705" href="Data.Nat.GeneralisedArithmetic.html#472" class="Function">fold</a> <a id="3710" href="Algebra.CommutativeMonoidSolver.html#3674" class="Bound">d</a> <a id="3712" class="Symbol">(</a><a id="3713" href="Algebra.CommutativeMonoidSolver.html#3379" class="Bound">a</a> <a id="3715" href="Algebra.html#1798" class="Field Operator">∙_</a><a id="3717" class="Symbol">)</a> <a id="3719" class="Symbol">(</a><a id="3720" href="Algebra.CommutativeMonoidSolver.html#3669" class="Bound">l</a> <a id="3722" href="Agda.Builtin.Nat.html#_%2B_" class="Primitive Operator">+</a> <a id="3724" href="Algebra.CommutativeMonoidSolver.html#3671" class="Bound">m</a><a id="3725" class="Symbol">)</a> <a id="3727" href="Algebra.html#1758" class="Field Operator">≈</a> <a id="3729" href="Data.Nat.GeneralisedArithmetic.html#472" class="Function">fold</a> <a id="3734" href="Algebra.CommutativeMonoidSolver.html#3676" class="Bound">b</a> <a id="3736" class="Symbol">(</a><a id="3737" href="Algebra.CommutativeMonoidSolver.html#3379" class="Bound">a</a> <a id="3739" href="Algebra.html#1798" class="Field Operator">∙_</a><a id="3741" class="Symbol">)</a> <a id="3743" href="Algebra.CommutativeMonoidSolver.html#3669" class="Bound">l</a> <a id="3745" href="Algebra.html#1798" class="Field Operator">∙</a> <a id="3747" href="Data.Nat.GeneralisedArithmetic.html#472" class="Function">fold</a> <a id="3752" href="Algebra.CommutativeMonoidSolver.html#3678" class="Bound">c</a> <a id="3754" class="Symbol">(</a><a id="3755" href="Algebra.CommutativeMonoidSolver.html#3379" class="Bound">a</a> <a id="3757" href="Algebra.html#1798" class="Field Operator">∙_</a><a id="3759" class="Symbol">)</a> <a id="3761" href="Algebra.CommutativeMonoidSolver.html#3671" class="Bound">m</a>
    <a id="3767" href="Algebra.CommutativeMonoidSolver.html#3659" class="Function">lemma</a> <a id="3773" href="Agda.Builtin.Nat.html#Nat.zero" class="InductiveConstructor">zero</a> <a id="3778" href="Agda.Builtin.Nat.html#Nat.zero" class="InductiveConstructor">zero</a> <a id="3783" href="Algebra.CommutativeMonoidSolver.html#3783" class="Bound">p</a> <a id="3785" class="Symbol">=</a> <a id="3787" href="Algebra.CommutativeMonoidSolver.html#3783" class="Bound">p</a>
    <a id="3793" href="Algebra.CommutativeMonoidSolver.html#3659" class="Function">lemma</a> <a id="3799" href="Agda.Builtin.Nat.html#Nat.zero" class="InductiveConstructor">zero</a> <a id="3804" class="Symbol">(</a><a id="3805" href="Agda.Builtin.Nat.html#Nat.suc" class="InductiveConstructor">suc</a> <a id="3809" href="Algebra.CommutativeMonoidSolver.html#3809" class="Bound">m</a><a id="3810" class="Symbol">)</a> <a id="3812" href="Algebra.CommutativeMonoidSolver.html#3812" class="Bound">p</a> <a id="3814" class="Symbol">=</a> <a id="3816" href="Relation.Binary.Core.html#trans" class="Function">trans</a> <a id="3822" class="Symbol">(</a><a id="3823" href="Algebra.Structures.html#845" class="Function">∙-cong</a> <a id="3830" href="Relation.Binary.Core.html#refl" class="Function">refl</a> <a id="3835" class="Symbol">(</a><a id="3836" href="Algebra.CommutativeMonoidSolver.html#3659" class="Function">lemma</a> <a id="3842" href="Agda.Builtin.Nat.html#Nat.zero" class="InductiveConstructor">zero</a> <a id="3847" href="Algebra.CommutativeMonoidSolver.html#3809" class="Bound">m</a> <a id="3849" href="Algebra.CommutativeMonoidSolver.html#3812" class="Bound">p</a><a id="3850" class="Symbol">))</a> <a id="3853" class="Symbol">(</a><a id="3854" href="Algebra.CommutativeMonoidSolver.html#3431" class="Function">flip12</a> <a id="3861" class="Symbol">_</a> <a id="3863" class="Symbol">_</a> <a id="3865" class="Symbol">_)</a>
    <a id="3872" href="Algebra.CommutativeMonoidSolver.html#3659" class="Function">lemma</a> <a id="3878" class="Symbol">(</a><a id="3879" href="Agda.Builtin.Nat.html#Nat.suc" class="InductiveConstructor">suc</a> <a id="3883" href="Algebra.CommutativeMonoidSolver.html#3883" class="Bound">l</a><a id="3884" class="Symbol">)</a> <a id="3886" href="Algebra.CommutativeMonoidSolver.html#3886" class="Bound">m</a> <a id="3888" href="Algebra.CommutativeMonoidSolver.html#3888" class="Bound">p</a> <a id="3890" class="Symbol">=</a> <a id="3892" href="Relation.Binary.Core.html#trans" class="Function">trans</a> <a id="3898" class="Symbol">(</a><a id="3899" href="Algebra.Structures.html#845" class="Function">∙-cong</a> <a id="3906" href="Relation.Binary.Core.html#refl" class="Function">refl</a> <a id="3911" class="Symbol">(</a><a id="3912" href="Algebra.CommutativeMonoidSolver.html#3659" class="Function">lemma</a> <a id="3918" href="Algebra.CommutativeMonoidSolver.html#3883" class="Bound">l</a> <a id="3920" href="Algebra.CommutativeMonoidSolver.html#3886" class="Bound">m</a> <a id="3922" href="Algebra.CommutativeMonoidSolver.html#3888" class="Bound">p</a><a id="3923" class="Symbol">))</a> <a id="3926" class="Symbol">(</a><a id="3927" href="Relation.Binary.Core.html#sym" class="Function">sym</a> <a id="3931" class="Symbol">(</a><a id="3932" href="Algebra.Structures.html#811" class="Function">assoc</a> <a id="3938" href="Algebra.CommutativeMonoidSolver.html#3379" class="Bound">a</a> <a id="3940" class="Symbol">_</a> <a id="3942" class="Symbol">_))</a>

<a id="3947" class="Comment">------------------------------------------------------------------------</a>
<a id="4020" class="Comment">-- Normalization</a>

<a id="4038" class="Comment">-- A normaliser.</a>

<a id="normalise" href="Algebra.CommutativeMonoidSolver.html#normalise" class="Function">normalise</a> <a id="4066" class="Symbol">:</a> <a id="4068" class="Symbol">∀</a> <a id="4070" class="Symbol">{</a><a id="4071" href="Algebra.CommutativeMonoidSolver.html#4071" class="Bound">n</a><a id="4072" class="Symbol">}</a> <a id="4074" class="Symbol">→</a> <a id="4076" href="Algebra.CommutativeMonoidSolver.html#Expr" class="Datatype">Expr</a> <a id="4081" href="Algebra.CommutativeMonoidSolver.html#4071" class="Bound">n</a> <a id="4083" class="Symbol">→</a> <a id="4085" href="Algebra.CommutativeMonoidSolver.html#Normal" class="Function">Normal</a> <a id="4092" href="Algebra.CommutativeMonoidSolver.html#4071" class="Bound">n</a>
<a id="4094" href="Algebra.CommutativeMonoidSolver.html#normalise" class="Function">normalise</a> <a id="4104" class="Symbol">(</a><a id="4105" href="Algebra.CommutativeMonoidSolver.html#Expr.var" class="InductiveConstructor">var</a> <a id="4109" href="Algebra.CommutativeMonoidSolver.html#4109" class="Bound">x</a><a id="4110" class="Symbol">)</a>   <a id="4114" class="Symbol">=</a> <a id="4116" href="Algebra.CommutativeMonoidSolver.html#sg" class="Function">sg</a> <a id="4119" href="Algebra.CommutativeMonoidSolver.html#4109" class="Bound">x</a>
<a id="4121" href="Algebra.CommutativeMonoidSolver.html#normalise" class="Function">normalise</a> <a id="4131" href="Algebra.CommutativeMonoidSolver.html#Expr.id" class="InductiveConstructor">id</a>        <a id="4141" class="Symbol">=</a> <a id="4143" href="Algebra.CommutativeMonoidSolver.html#empty" class="Function">empty</a>
<a id="4149" href="Algebra.CommutativeMonoidSolver.html#normalise" class="Function">normalise</a> <a id="4159" class="Symbol">(</a><a id="4160" href="Algebra.CommutativeMonoidSolver.html#4160" class="Bound">e₁</a> <a id="4163" href="Algebra.CommutativeMonoidSolver.html#Expr._%E2%8A%95_" class="InductiveConstructor Operator">⊕</a> <a id="4165" href="Algebra.CommutativeMonoidSolver.html#4165" class="Bound">e₂</a><a id="4167" class="Symbol">)</a> <a id="4169" class="Symbol">=</a> <a id="4171" href="Algebra.CommutativeMonoidSolver.html#normalise" class="Function">normalise</a> <a id="4181" href="Algebra.CommutativeMonoidSolver.html#4160" class="Bound">e₁</a> <a id="4184" href="Algebra.CommutativeMonoidSolver.html#_%E2%80%A2_" class="Function Operator">•</a> <a id="4186" href="Algebra.CommutativeMonoidSolver.html#normalise" class="Function">normalise</a> <a id="4196" href="Algebra.CommutativeMonoidSolver.html#4165" class="Bound">e₂</a>

<a id="4200" class="Comment">-- The normaliser preserves the semantics of the expression.</a>

<a id="normalise-correct" href="Algebra.CommutativeMonoidSolver.html#normalise-correct" class="Function">normalise-correct</a> <a id="4280" class="Symbol">:</a> <a id="4282" class="Symbol">∀</a> <a id="4284" class="Symbol">{</a><a id="4285" href="Algebra.CommutativeMonoidSolver.html#4285" class="Bound">n</a><a id="4286" class="Symbol">}</a> <a id="4288" class="Symbol">(</a><a id="4289" href="Algebra.CommutativeMonoidSolver.html#4289" class="Bound">e</a> <a id="4291" class="Symbol">:</a> <a id="4293" href="Algebra.CommutativeMonoidSolver.html#Expr" class="Datatype">Expr</a> <a id="4298" href="Algebra.CommutativeMonoidSolver.html#4285" class="Bound">n</a><a id="4299" class="Symbol">)</a> <a id="4301" class="Symbol">(</a><a id="4302" href="Algebra.CommutativeMonoidSolver.html#4302" class="Bound">ρ</a> <a id="4304" class="Symbol">:</a> <a id="4306" href="Algebra.CommutativeMonoidSolver.html#Env" class="Function">Env</a> <a id="4310" href="Algebra.CommutativeMonoidSolver.html#4285" class="Bound">n</a><a id="4311" class="Symbol">)</a> <a id="4313" class="Symbol">→</a>
    <a id="4319" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7%E2%87%93" class="Function Operator">⟦</a> <a id="4321" href="Algebra.CommutativeMonoidSolver.html#normalise" class="Function">normalise</a> <a id="4331" href="Algebra.CommutativeMonoidSolver.html#4289" class="Bound">e</a> <a id="4333" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7%E2%87%93" class="Function Operator">⟧⇓</a> <a id="4336" href="Algebra.CommutativeMonoidSolver.html#4302" class="Bound">ρ</a> <a id="4338" href="Algebra.html#1758" class="Field Operator">≈</a> <a id="4340" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟦</a> <a id="4342" href="Algebra.CommutativeMonoidSolver.html#4289" class="Bound">e</a> <a id="4344" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟧</a> <a id="4346" href="Algebra.CommutativeMonoidSolver.html#4302" class="Bound">ρ</a>
<a id="4348" href="Algebra.CommutativeMonoidSolver.html#normalise-correct" class="Function">normalise-correct</a> <a id="4366" class="Symbol">(</a><a id="4367" href="Algebra.CommutativeMonoidSolver.html#Expr.var" class="InductiveConstructor">var</a> <a id="4371" href="Algebra.CommutativeMonoidSolver.html#4371" class="Bound">x</a><a id="4372" class="Symbol">)</a>   <a id="4376" href="Algebra.CommutativeMonoidSolver.html#4376" class="Bound">ρ</a> <a id="4378" class="Symbol">=</a> <a id="4380" href="Algebra.CommutativeMonoidSolver.html#sg-correct" class="Function">sg-correct</a> <a id="4391" href="Algebra.CommutativeMonoidSolver.html#4371" class="Bound">x</a> <a id="4393" href="Algebra.CommutativeMonoidSolver.html#4376" class="Bound">ρ</a>
<a id="4395" href="Algebra.CommutativeMonoidSolver.html#normalise-correct" class="Function">normalise-correct</a> <a id="4413" href="Algebra.CommutativeMonoidSolver.html#Expr.id" class="InductiveConstructor">id</a>        <a id="4423" href="Algebra.CommutativeMonoidSolver.html#4423" class="Bound">ρ</a> <a id="4425" class="Symbol">=</a> <a id="4427" href="Algebra.CommutativeMonoidSolver.html#empty-correct" class="Function">empty-correct</a> <a id="4441" href="Algebra.CommutativeMonoidSolver.html#4423" class="Bound">ρ</a>
<a id="4443" href="Algebra.CommutativeMonoidSolver.html#normalise-correct" class="Function">normalise-correct</a> <a id="4461" class="Symbol">(</a><a id="4462" href="Algebra.CommutativeMonoidSolver.html#4462" class="Bound">e₁</a> <a id="4465" href="Algebra.CommutativeMonoidSolver.html#Expr._%E2%8A%95_" class="InductiveConstructor Operator">⊕</a> <a id="4467" href="Algebra.CommutativeMonoidSolver.html#4467" class="Bound">e₂</a><a id="4469" class="Symbol">)</a> <a id="4471" href="Algebra.CommutativeMonoidSolver.html#4471" class="Bound">ρ</a> <a id="4473" class="Symbol">=</a>  <a id="4476" href="Relation.Binary.PreorderReasoning.html#begin_" class="Function Operator">begin</a>

    <a id="4487" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7%E2%87%93" class="Function Operator">⟦</a> <a id="4489" href="Algebra.CommutativeMonoidSolver.html#normalise" class="Function">normalise</a> <a id="4499" href="Algebra.CommutativeMonoidSolver.html#4462" class="Bound">e₁</a> <a id="4502" href="Algebra.CommutativeMonoidSolver.html#_%E2%80%A2_" class="Function Operator">•</a> <a id="4504" href="Algebra.CommutativeMonoidSolver.html#normalise" class="Function">normalise</a> <a id="4514" href="Algebra.CommutativeMonoidSolver.html#4467" class="Bound">e₂</a> <a id="4517" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7%E2%87%93" class="Function Operator">⟧⇓</a> <a id="4520" href="Algebra.CommutativeMonoidSolver.html#4471" class="Bound">ρ</a>

  <a id="4525" href="Relation.Binary.PreorderReasoning.html#_%E2%89%88%E2%9F%A8_%E2%9F%A9_" class="Function Operator">≈⟨</a> <a id="4528" href="Algebra.CommutativeMonoidSolver.html#comp-correct" class="Function">comp-correct</a> <a id="4541" class="Symbol">(</a><a id="4542" href="Algebra.CommutativeMonoidSolver.html#normalise" class="Function">normalise</a> <a id="4552" href="Algebra.CommutativeMonoidSolver.html#4462" class="Bound">e₁</a><a id="4554" class="Symbol">)</a> <a id="4556" class="Symbol">(</a><a id="4557" href="Algebra.CommutativeMonoidSolver.html#normalise" class="Function">normalise</a> <a id="4567" href="Algebra.CommutativeMonoidSolver.html#4467" class="Bound">e₂</a><a id="4569" class="Symbol">)</a> <a id="4571" href="Algebra.CommutativeMonoidSolver.html#4471" class="Bound">ρ</a> <a id="4573" href="Relation.Binary.PreorderReasoning.html#_%E2%89%88%E2%9F%A8_%E2%9F%A9_" class="Function Operator">⟩</a>

    <a id="4580" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7%E2%87%93" class="Function Operator">⟦</a> <a id="4582" href="Algebra.CommutativeMonoidSolver.html#normalise" class="Function">normalise</a> <a id="4592" href="Algebra.CommutativeMonoidSolver.html#4462" class="Bound">e₁</a> <a id="4595" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7%E2%87%93" class="Function Operator">⟧⇓</a> <a id="4598" href="Algebra.CommutativeMonoidSolver.html#4471" class="Bound">ρ</a> <a id="4600" href="Algebra.html#1798" class="Field Operator">∙</a> <a id="4602" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7%E2%87%93" class="Function Operator">⟦</a> <a id="4604" href="Algebra.CommutativeMonoidSolver.html#normalise" class="Function">normalise</a> <a id="4614" href="Algebra.CommutativeMonoidSolver.html#4467" class="Bound">e₂</a> <a id="4617" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7%E2%87%93" class="Function Operator">⟧⇓</a> <a id="4620" href="Algebra.CommutativeMonoidSolver.html#4471" class="Bound">ρ</a>

  <a id="4625" href="Relation.Binary.PreorderReasoning.html#_%E2%89%88%E2%9F%A8_%E2%9F%A9_" class="Function Operator">≈⟨</a> <a id="4628" href="Algebra.Structures.html#845" class="Function">∙-cong</a> <a id="4635" class="Symbol">(</a><a id="4636" href="Algebra.CommutativeMonoidSolver.html#normalise-correct" class="Function">normalise-correct</a> <a id="4654" href="Algebra.CommutativeMonoidSolver.html#4462" class="Bound">e₁</a> <a id="4657" href="Algebra.CommutativeMonoidSolver.html#4471" class="Bound">ρ</a><a id="4658" class="Symbol">)</a> <a id="4660" class="Symbol">(</a><a id="4661" href="Algebra.CommutativeMonoidSolver.html#normalise-correct" class="Function">normalise-correct</a> <a id="4679" href="Algebra.CommutativeMonoidSolver.html#4467" class="Bound">e₂</a> <a id="4682" href="Algebra.CommutativeMonoidSolver.html#4471" class="Bound">ρ</a><a id="4683" class="Symbol">)</a> <a id="4685" href="Relation.Binary.PreorderReasoning.html#_%E2%89%88%E2%9F%A8_%E2%9F%A9_" class="Function Operator">⟩</a>

    <a id="4692" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟦</a> <a id="4694" href="Algebra.CommutativeMonoidSolver.html#4462" class="Bound">e₁</a> <a id="4697" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟧</a> <a id="4699" href="Algebra.CommutativeMonoidSolver.html#4471" class="Bound">ρ</a> <a id="4701" href="Algebra.html#1798" class="Field Operator">∙</a> <a id="4703" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟦</a> <a id="4705" href="Algebra.CommutativeMonoidSolver.html#4467" class="Bound">e₂</a> <a id="4708" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟧</a> <a id="4710" href="Algebra.CommutativeMonoidSolver.html#4471" class="Bound">ρ</a>
  <a id="4714" href="Relation.Binary.PreorderReasoning.html#_%E2%88%8E" class="Function Operator">∎</a>

<a id="4717" class="Comment">------------------------------------------------------------------------</a>
<a id="4790" class="Comment">-- &quot;Tactics&quot;</a>

<a id="4804" class="Keyword">open</a> <a id="4809" class="Keyword">module</a> <a id="R" href="Algebra.CommutativeMonoidSolver.html#R" class="Module">R</a> <a id="4818" class="Symbol">=</a> <a id="4820" href="Relation.Binary.Reflection.html" class="Module">Reflection</a>
                  <a id="4849" href="Algebra.html#845" class="Function">setoid</a> <a id="4856" href="Algebra.CommutativeMonoidSolver.html#Expr.var" class="InductiveConstructor">var</a> <a id="4860" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟦_⟧</a> <a id="4864" class="Symbol">(</a><a id="4865" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7%E2%87%93" class="Function Operator">⟦_⟧⇓</a> <a id="4870" href="Function.html#_%E2%88%98_" class="Function Operator">∘</a> <a id="4872" href="Algebra.CommutativeMonoidSolver.html#normalise" class="Function">normalise</a><a id="4881" class="Symbol">)</a> <a id="4883" href="Algebra.CommutativeMonoidSolver.html#normalise-correct" class="Function">normalise-correct</a>
  <a id="4903" class="Keyword">public</a> <a id="4910" class="Keyword">using</a> <a id="4916" class="Symbol">(</a><a id="4917" href="Relation.Binary.Reflection.html#solve" class="Function">solve</a><a id="4922" class="Symbol">;</a> <a id="4924" href="Relation.Binary.Reflection.html#_%E2%8A%9C_" class="Function Operator">_⊜_</a><a id="4927" class="Symbol">)</a>

<a id="4930" class="Comment">-- We can decide if two normal forms are /syntactically/ equal.</a>

<a id="4995" class="Keyword">infix</a> <a id="5001" class="Number">5</a> <a id="5003" href="Algebra.CommutativeMonoidSolver.html#_%E2%89%9F_" class="Function Operator">_≟_</a>

<a id="_≟_" href="Algebra.CommutativeMonoidSolver.html#_%E2%89%9F_" class="Function Operator">_≟_</a> <a id="5012" class="Symbol">:</a> <a id="5014" class="Symbol">∀</a> <a id="5016" class="Symbol">{</a><a id="5017" href="Algebra.CommutativeMonoidSolver.html#5017" class="Bound">n</a><a id="5018" class="Symbol">}</a> <a id="5020" class="Symbol">(</a><a id="5021" href="Algebra.CommutativeMonoidSolver.html#5021" class="Bound">nf₁</a> <a id="5025" href="Algebra.CommutativeMonoidSolver.html#5025" class="Bound">nf₂</a> <a id="5029" class="Symbol">:</a> <a id="5031" href="Algebra.CommutativeMonoidSolver.html#Normal" class="Function">Normal</a> <a id="5038" href="Algebra.CommutativeMonoidSolver.html#5017" class="Bound">n</a><a id="5039" class="Symbol">)</a> <a id="5041" class="Symbol">→</a> <a id="5043" href="Relation.Nullary.html#Dec" class="Datatype">Dec</a> <a id="5047" class="Symbol">(</a><a id="5048" href="Algebra.CommutativeMonoidSolver.html#5021" class="Bound">nf₁</a> <a id="5052" href="Agda.Builtin.Equality.html#_%E2%89%A1_" class="Datatype Operator">≡</a> <a id="5054" href="Algebra.CommutativeMonoidSolver.html#5025" class="Bound">nf₂</a><a id="5057" class="Symbol">)</a>
<a id="5059" href="Algebra.CommutativeMonoidSolver.html#5059" class="Bound">nf₁</a> <a id="5063" href="Algebra.CommutativeMonoidSolver.html#_%E2%89%9F_" class="Function Operator">≟</a> <a id="5065" href="Algebra.CommutativeMonoidSolver.html#5065" class="Bound">nf₂</a> <a id="5069" class="Symbol">=</a> <a id="5071" href="Relation.Nullary.Decidable.html#map" class="Function">Dec.map</a> <a id="5079" href="Relation.Binary.Vec.Pointwise.html#Pointwise-%E2%89%A1" class="Function">Pointwise-≡</a> <a id="5091" class="Symbol">(</a><a id="5092" href="Relation.Binary.Vec.Pointwise.html#decidable" class="Function">decidable</a> <a id="5102" href="Data.Nat.Base.html#_%E2%89%9F_" class="Function Operator">ℕ._≟_</a> <a id="5108" href="Algebra.CommutativeMonoidSolver.html#5059" class="Bound">nf₁</a> <a id="5112" href="Algebra.CommutativeMonoidSolver.html#5065" class="Bound">nf₂</a><a id="5115" class="Symbol">)</a>
  <a id="5119" class="Keyword">where</a> <a id="5125" class="Keyword">open</a> <a id="5130" href="Relation.Binary.Vec.Pointwise.html" class="Module">Pointwise</a>

<a id="5141" class="Comment">-- We can also give a sound, but not necessarily complete, procedure</a>
<a id="5210" class="Comment">-- for determining if two expressions have the same semantics.</a>

<a id="prove′" href="Algebra.CommutativeMonoidSolver.html#prove%E2%80%B2" class="Function">prove′</a> <a id="5281" class="Symbol">:</a> <a id="5283" class="Symbol">∀</a> <a id="5285" class="Symbol">{</a><a id="5286" href="Algebra.CommutativeMonoidSolver.html#5286" class="Bound">n</a><a id="5287" class="Symbol">}</a> <a id="5289" class="Symbol">(</a><a id="5290" href="Algebra.CommutativeMonoidSolver.html#5290" class="Bound">e₁</a> <a id="5293" href="Algebra.CommutativeMonoidSolver.html#5293" class="Bound">e₂</a> <a id="5296" class="Symbol">:</a> <a id="5298" href="Algebra.CommutativeMonoidSolver.html#Expr" class="Datatype">Expr</a> <a id="5303" href="Algebra.CommutativeMonoidSolver.html#5286" class="Bound">n</a><a id="5304" class="Symbol">)</a> <a id="5306" class="Symbol">→</a> <a id="5308" href="Data.Maybe.Base.html#Maybe" class="Datatype">Maybe</a> <a id="5314" class="Symbol">(∀</a> <a id="5317" href="Algebra.CommutativeMonoidSolver.html#5317" class="Bound">ρ</a> <a id="5319" class="Symbol">→</a> <a id="5321" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟦</a> <a id="5323" href="Algebra.CommutativeMonoidSolver.html#5290" class="Bound">e₁</a> <a id="5326" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟧</a> <a id="5328" href="Algebra.CommutativeMonoidSolver.html#5317" class="Bound">ρ</a> <a id="5330" href="Algebra.html#1758" class="Field Operator">≈</a> <a id="5332" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟦</a> <a id="5334" href="Algebra.CommutativeMonoidSolver.html#5293" class="Bound">e₂</a> <a id="5337" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟧</a> <a id="5339" href="Algebra.CommutativeMonoidSolver.html#5317" class="Bound">ρ</a><a id="5340" class="Symbol">)</a>
<a id="5342" href="Algebra.CommutativeMonoidSolver.html#prove%E2%80%B2" class="Function">prove′</a> <a id="5349" href="Algebra.CommutativeMonoidSolver.html#5349" class="Bound">e₁</a> <a id="5352" href="Algebra.CommutativeMonoidSolver.html#5352" class="Bound">e₂</a> <a id="5355" class="Symbol">=</a>
  <a id="5359" href="Data.Maybe.Base.html#map" class="Function">Maybe.map</a> <a id="5369" href="Algebra.CommutativeMonoidSolver.html#5428" class="Function">lemma</a> <a id="5375" class="Symbol">(</a><a id="5376" href="Data.Maybe.Base.html#decToMaybe" class="Function">decToMaybe</a> <a id="5387" class="Symbol">(</a><a id="5388" href="Algebra.CommutativeMonoidSolver.html#normalise" class="Function">normalise</a> <a id="5398" href="Algebra.CommutativeMonoidSolver.html#5349" class="Bound">e₁</a> <a id="5401" href="Algebra.CommutativeMonoidSolver.html#_%E2%89%9F_" class="Function Operator">≟</a> <a id="5403" href="Algebra.CommutativeMonoidSolver.html#normalise" class="Function">normalise</a> <a id="5413" href="Algebra.CommutativeMonoidSolver.html#5352" class="Bound">e₂</a><a id="5415" class="Symbol">))</a>
  <a id="5420" class="Keyword">where</a>
  <a id="5428" href="Algebra.CommutativeMonoidSolver.html#5428" class="Function">lemma</a> <a id="5434" class="Symbol">:</a> <a id="5436" href="Algebra.CommutativeMonoidSolver.html#normalise" class="Function">normalise</a> <a id="5446" href="Algebra.CommutativeMonoidSolver.html#5349" class="Bound">e₁</a> <a id="5449" href="Agda.Builtin.Equality.html#_%E2%89%A1_" class="Datatype Operator">≡</a> <a id="5451" href="Algebra.CommutativeMonoidSolver.html#normalise" class="Function">normalise</a> <a id="5461" href="Algebra.CommutativeMonoidSolver.html#5352" class="Bound">e₂</a> <a id="5464" class="Symbol">→</a> <a id="5466" class="Symbol">∀</a> <a id="5468" href="Algebra.CommutativeMonoidSolver.html#5468" class="Bound">ρ</a> <a id="5470" class="Symbol">→</a> <a id="5472" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟦</a> <a id="5474" href="Algebra.CommutativeMonoidSolver.html#5349" class="Bound">e₁</a> <a id="5477" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟧</a> <a id="5479" href="Algebra.CommutativeMonoidSolver.html#5468" class="Bound">ρ</a> <a id="5481" href="Algebra.html#1758" class="Field Operator">≈</a> <a id="5483" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟦</a> <a id="5485" href="Algebra.CommutativeMonoidSolver.html#5352" class="Bound">e₂</a> <a id="5488" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟧</a> <a id="5490" href="Algebra.CommutativeMonoidSolver.html#5468" class="Bound">ρ</a>
  <a id="5494" href="Algebra.CommutativeMonoidSolver.html#5428" class="Function">lemma</a> <a id="5500" href="Algebra.CommutativeMonoidSolver.html#5500" class="Bound">eq</a> <a id="5503" href="Algebra.CommutativeMonoidSolver.html#5503" class="Bound">ρ</a> <a id="5505" class="Symbol">=</a>
    <a id="5511" href="Relation.Binary.Reflection.html#prove" class="Function">R.prove</a> <a id="5519" href="Algebra.CommutativeMonoidSolver.html#5503" class="Bound">ρ</a> <a id="5521" href="Algebra.CommutativeMonoidSolver.html#5349" class="Bound">e₁</a> <a id="5524" href="Algebra.CommutativeMonoidSolver.html#5352" class="Bound">e₂</a> <a id="5527" class="Symbol">(</a><a id="5528" href="Relation.Binary.PreorderReasoning.html#begin_" class="Function Operator">begin</a>
      <a id="5540" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7%E2%87%93" class="Function Operator">⟦</a> <a id="5542" href="Algebra.CommutativeMonoidSolver.html#normalise" class="Function">normalise</a> <a id="5552" href="Algebra.CommutativeMonoidSolver.html#5349" class="Bound">e₁</a> <a id="5555" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7%E2%87%93" class="Function Operator">⟧⇓</a> <a id="5558" href="Algebra.CommutativeMonoidSolver.html#5503" class="Bound">ρ</a>  <a id="5561" href="Relation.Binary.PreorderReasoning.html#_%E2%89%A1%E2%9F%A8_%E2%9F%A9_" class="Function Operator">≡⟨</a> <a id="5564" href="Relation.Binary.PropositionalEquality.html#cong" class="Function">P.cong</a> <a id="5571" class="Symbol">(λ</a> <a id="5574" href="Algebra.CommutativeMonoidSolver.html#5574" class="Bound">e</a> <a id="5576" class="Symbol">→</a> <a id="5578" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7%E2%87%93" class="Function Operator">⟦</a> <a id="5580" href="Algebra.CommutativeMonoidSolver.html#5574" class="Bound">e</a> <a id="5582" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7%E2%87%93" class="Function Operator">⟧⇓</a> <a id="5585" href="Algebra.CommutativeMonoidSolver.html#5503" class="Bound">ρ</a><a id="5586" class="Symbol">)</a> <a id="5588" href="Algebra.CommutativeMonoidSolver.html#5500" class="Bound">eq</a> <a id="5591" href="Relation.Binary.PreorderReasoning.html#_%E2%89%A1%E2%9F%A8_%E2%9F%A9_" class="Function Operator">⟩</a>
      <a id="5599" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7%E2%87%93" class="Function Operator">⟦</a> <a id="5601" href="Algebra.CommutativeMonoidSolver.html#normalise" class="Function">normalise</a> <a id="5611" href="Algebra.CommutativeMonoidSolver.html#5352" class="Bound">e₂</a> <a id="5614" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7%E2%87%93" class="Function Operator">⟧⇓</a> <a id="5617" href="Algebra.CommutativeMonoidSolver.html#5503" class="Bound">ρ</a>  <a id="5620" href="Relation.Binary.PreorderReasoning.html#_%E2%88%8E" class="Function Operator">∎</a><a id="5621" class="Symbol">)</a>

<a id="5624" class="Comment">-- This procedure can be combined with from-just.</a>

<a id="prove" href="Algebra.CommutativeMonoidSolver.html#prove" class="Function">prove</a> <a id="5681" class="Symbol">:</a> <a id="5683" class="Symbol">∀</a> <a id="5685" href="Algebra.CommutativeMonoidSolver.html#5685" class="Bound">n</a> <a id="5687" class="Symbol">(</a><a id="5688" href="Algebra.CommutativeMonoidSolver.html#5688" class="Bound">e₁</a> <a id="5691" href="Algebra.CommutativeMonoidSolver.html#5691" class="Bound">e₂</a> <a id="5694" class="Symbol">:</a> <a id="5696" href="Algebra.CommutativeMonoidSolver.html#Expr" class="Datatype">Expr</a> <a id="5701" href="Algebra.CommutativeMonoidSolver.html#5685" class="Bound">n</a><a id="5702" class="Symbol">)</a> <a id="5704" class="Symbol">→</a>
  <a id="5708" href="Data.Maybe.Base.html#From-just" class="Function">From-just</a> <a id="5718" class="Symbol">(∀</a> <a id="5721" href="Algebra.CommutativeMonoidSolver.html#5721" class="Bound">ρ</a> <a id="5723" class="Symbol">→</a> <a id="5725" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟦</a> <a id="5727" href="Algebra.CommutativeMonoidSolver.html#5688" class="Bound">e₁</a> <a id="5730" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟧</a> <a id="5732" href="Algebra.CommutativeMonoidSolver.html#5721" class="Bound">ρ</a> <a id="5734" href="Algebra.html#1758" class="Field Operator">≈</a> <a id="5736" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟦</a> <a id="5738" href="Algebra.CommutativeMonoidSolver.html#5691" class="Bound">e₂</a> <a id="5741" href="Algebra.CommutativeMonoidSolver.html#%E2%9F%A6_%E2%9F%A7" class="Function Operator">⟧</a> <a id="5743" href="Algebra.CommutativeMonoidSolver.html#5721" class="Bound">ρ</a><a id="5744" class="Symbol">)</a> <a id="5746" class="Symbol">(</a><a id="5747" href="Algebra.CommutativeMonoidSolver.html#prove%E2%80%B2" class="Function">prove′</a>  <a id="5755" href="Algebra.CommutativeMonoidSolver.html#5688" class="Bound">e₁</a> <a id="5758" href="Algebra.CommutativeMonoidSolver.html#5691" class="Bound">e₂</a><a id="5760" class="Symbol">)</a>
<a id="5762" href="Algebra.CommutativeMonoidSolver.html#prove" class="Function">prove</a> <a id="5768" class="Symbol">_</a> <a id="5770" href="Algebra.CommutativeMonoidSolver.html#5770" class="Bound">e₁</a> <a id="5773" href="Algebra.CommutativeMonoidSolver.html#5773" class="Bound">e₂</a> <a id="5776" class="Symbol">=</a> <a id="5778" href="Data.Maybe.Base.html#from-just" class="Function">from-just</a> <a id="5788" class="Symbol">(</a><a id="5789" href="Algebra.CommutativeMonoidSolver.html#prove%E2%80%B2" class="Function">prove′</a> <a id="5796" href="Algebra.CommutativeMonoidSolver.html#5770" class="Bound">e₁</a> <a id="5799" href="Algebra.CommutativeMonoidSolver.html#5773" class="Bound">e₂</a><a id="5801" class="Symbol">)</a>

<a id="5804" class="Comment">-- prove : ∀ n (es : Expr n × Expr n) →</a>
<a id="5844" class="Comment">--         From-just (∀ ρ → ⟦ proj₁ es ⟧ ρ ≈ ⟦ proj₂ es ⟧ ρ)</a>
<a id="5905" class="Comment">--                   (uncurry prove′ es)</a>
<a id="5946" class="Comment">-- prove _ = from-just ∘ uncurry prove′</a>
</pre></body></html>

APT Browse - Built by Thomas Orozco.