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
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
|
<style>
.IdrisData {
color: darkred
}
.IdrisType {
color: blue
}
.IdrisBound {
color: black
}
.IdrisFunction {
color: darkgreen
}
.IdrisKeyword {
font-weight: bold;
}
.IdrisComment {
color: #b22222
}
.IdrisNamespace {
font-style: italic;
color: black
}
.IdrisPostulate {
font-weight: bold;
color: red
}
.IdrisModule {
font-style: italic;
color: black
}
.IdrisCode {
display: block;
background-color: whitesmoke;
}
</style>
# Tutorial: Setoids
A _setoid_ is a type equipped with an equivalence relation. Setoids come up when
you need types with a better behaved equality relation, or when you want the
equality relation to carry additional information. After completing this
tutorial you will:
1. Know the user interface to the `setoid` package.
2. Know two different applications in which it can be used:
+ constructing types with an equality relation that's better behaved than
Idris's built-in `Equal` type.
+ types with an equality relation that carries additional information
If you want to see the source-code behind this tutorial, check the
[source-code](sources/Tutorial.md) out.
## Equivalence relations
A _relation_ over a type `ty` in Idris is any two-argument type-valued function:
```
namespace Control.Relation
Rel : Type -> Type
Rel ty = ty -> ty -> Type
```
This definition and its associated interfaces ship with idris's standard
library. Given a relation `rel : Rel ty` and `x,y : ty`, we can form
```x `rel` y : Type```: the type of ways in which `x` and `y` can be related.
For example, two lists _overlap_ when they have a common element:
<code class="IdrisCode">
<span class="IdrisKeyword">record</span> <span class="IdrisType">Overlap</span> <span class="IdrisKeyword">{0</span> <span class="IdrisBound">a</span> <span class="IdrisKeyword">:</span> <span class="IdrisType">Type</span><span class="IdrisKeyword">}</span> <span class="IdrisKeyword">(</span><span class="IdrisBound">xs</span><span class="IdrisKeyword">,</span><span class="IdrisBound">ys</span> <span class="IdrisKeyword">:</span> <span class="IdrisType">List</span> <span class="IdrisBound">a</span><span class="IdrisKeyword">)</span> <span class="IdrisKeyword">where</span><br />
constructor <span class="IdrisData">Overlapping</span><br />
<span class="IdrisFunction">common</span> <span class="IdrisKeyword">:</span> <span class="IdrisBound">a</span><br />
<span class="IdrisFunction">lhsPos</span> <span class="IdrisKeyword">:</span> <span class="IdrisBound">common</span> <span class="IdrisType">`Elem`</span> <span class="IdrisBound">xs</span><br />
<span class="IdrisFunction">rhsPos</span> <span class="IdrisKeyword">:</span> <span class="IdrisBound">common</span> <span class="IdrisType">`Elem`</span> <span class="IdrisBound">ys</span><br />
<br />
</code>
Lists can overlap in exactly one position:
<code class="IdrisCode">
<span class="IdrisFunction">Ex1</span> <span class="IdrisKeyword">:</span> <span class="IdrisType">Overlap</span> <span class="IdrisData">[1,2,3]</span> <span class="IdrisData">[6,7,2,8]</span><br />
<span class="IdrisFunction">Ex1</span> <span class="IdrisKeyword">=</span> <span class="IdrisData">Overlapping</span><br />
<span class="IdrisKeyword">{</span> <span class="IdrisBound">common</span> <span class="IdrisKeyword">=</span> <span class="IdrisData">2</span><br />
<span class="IdrisKeyword">,</span> <span class="IdrisBound">lhsPos</span> <span class="IdrisKeyword">=</span> <span class="IdrisData">There</span> <span class="IdrisData">Here</span><br />
<span class="IdrisKeyword">,</span> <span class="IdrisBound">rhsPos</span> <span class="IdrisKeyword">=</span> <span class="IdrisData">There</span> <span class="IdrisKeyword">(</span><span class="IdrisData">There</span> <span class="IdrisData">Here</span><span class="IdrisKeyword">)</span><br />
<span class="IdrisKeyword">}</span><br />
</code>
But they can overlap in several ways:
<code class="IdrisCode">
<span class="IdrisFunction">Ex2a</span> <span class="IdrisKeyword">,</span><br />
<span class="IdrisFunction">Ex2b</span> <span class="IdrisKeyword">,</span><br />
<span class="IdrisFunction">Ex2c</span> <span class="IdrisKeyword">:</span> <span class="IdrisType">Overlap</span> <span class="IdrisData">[1,2,3]</span> <span class="IdrisData">[2,3,2]</span><br />
<span class="IdrisFunction">Ex2a</span> <span class="IdrisKeyword">=</span> <span class="IdrisData">Overlapping</span><br />
<span class="IdrisKeyword">{</span> <span class="IdrisBound">common</span> <span class="IdrisKeyword">=</span> <span class="IdrisData">3</span><br />
<span class="IdrisKeyword">,</span> <span class="IdrisBound">lhsPos</span> <span class="IdrisKeyword">=</span> <span class="IdrisData">There</span> <span class="IdrisKeyword">(</span><span class="IdrisData">There</span> <span class="IdrisData">Here</span><span class="IdrisKeyword">)</span><br />
<span class="IdrisKeyword">,</span> <span class="IdrisBound">rhsPos</span> <span class="IdrisKeyword">=</span> <span class="IdrisData">There</span> <span class="IdrisData">Here</span><br />
<span class="IdrisKeyword">}</span><br />
<span class="IdrisFunction">Ex2b</span> <span class="IdrisKeyword">=</span> <span class="IdrisData">Overlapping</span><br />
<span class="IdrisKeyword">{</span> <span class="IdrisBound">common</span> <span class="IdrisKeyword">=</span> <span class="IdrisData">2</span><br />
<span class="IdrisKeyword">,</span> <span class="IdrisBound">lhsPos</span> <span class="IdrisKeyword">=</span> <span class="IdrisData">There</span> <span class="IdrisData">Here</span><br />
<span class="IdrisKeyword">,</span> <span class="IdrisBound">rhsPos</span> <span class="IdrisKeyword">=</span> <span class="IdrisData">Here</span><br />
<span class="IdrisKeyword">}</span><br />
<span class="IdrisFunction">Ex2c</span> <span class="IdrisKeyword">=</span> <span class="IdrisData">Overlapping</span><br />
<span class="IdrisKeyword">{</span> <span class="IdrisBound">common</span> <span class="IdrisKeyword">=</span> <span class="IdrisData">2</span><br />
<span class="IdrisKeyword">,</span> <span class="IdrisBound">lhsPos</span> <span class="IdrisKeyword">=</span> <span class="IdrisData">There</span> <span class="IdrisData">Here</span><br />
<span class="IdrisKeyword">,</span> <span class="IdrisBound">rhsPos</span> <span class="IdrisKeyword">=</span> <span class="IdrisData">There</span> <span class="IdrisKeyword">(</span><span class="IdrisData">There</span> <span class="IdrisData">Here</span><span class="IdrisKeyword">)</span><br />
<span class="IdrisKeyword">}</span><br />
</code>
We can think of a relation `rel : Rel ty` as the type of edges in a directed
graph between vertices in `ty`:
* edges have a direction: the type `rel x y` is different to `rel y x`
* multiple different edges between the same vertices `e1, e2 : rel x y`
* self-loops between the same vertex are allowed `loop : rel x x`.
An _equivalence relation_ is a relation that's:
* _reflexive_: we guarantee a specific way in which every element is related to
itself;
* _symmetric_: we can reverse an edge between two edges; and
* _transitive_: we can compose paths of related elements into a single edge.
<code class="IdrisCode">
<span class="IdrisKeyword">record</span> <span class="IdrisType">Equivalence</span> <span class="IdrisKeyword">(</span><span class="IdrisBound">A</span> <span class="IdrisKeyword">:</span> <span class="IdrisType">Type</span><span class="IdrisKeyword">)</span> <span class="IdrisKeyword">where</span><br />
constructor <span class="IdrisData">MkEquivalence</span><br />
<span class="IdrisKeyword">0</span> <span class="IdrisFunction">relation</span><span class="IdrisKeyword">:</span> <span class="IdrisFunction">Rel</span> <span class="IdrisBound">A</span><br />
<span class="IdrisFunction">reflexive</span> <span class="IdrisKeyword">:</span> <span class="IdrisKeyword">(</span><span class="IdrisBound">x</span> <span class="IdrisKeyword">:</span> <span class="IdrisBound">A</span><span class="IdrisKeyword">)</span> <span class="IdrisKeyword">-></span> <span class="IdrisBound">relation</span> <span class="IdrisBound">x</span> <span class="IdrisBound">x</span><br />
<span class="IdrisFunction">symmetric</span> <span class="IdrisKeyword">:</span> <span class="IdrisKeyword">(</span><span class="IdrisBound">x</span><span class="IdrisKeyword">,</span> <span class="IdrisBound">y</span> <span class="IdrisKeyword">:</span> <span class="IdrisBound">A</span><span class="IdrisKeyword">)</span> <span class="IdrisKeyword">-></span> <span class="IdrisBound">relation</span> <span class="IdrisBound">x</span> <span class="IdrisBound">y</span> <span class="IdrisKeyword">-></span> <span class="IdrisBound">relation</span> <span class="IdrisBound">y</span> <span class="IdrisBound">x</span><br />
<span class="IdrisFunction">transitive</span><span class="IdrisKeyword">:</span> <span class="IdrisKeyword">(</span><span class="IdrisBound">x</span><span class="IdrisKeyword">,</span> <span class="IdrisBound">y</span><span class="IdrisKeyword">,</span> <span class="IdrisBound">z</span> <span class="IdrisKeyword">:</span> <span class="IdrisBound">A</span><span class="IdrisKeyword">)</span> <span class="IdrisKeyword">-></span> <span class="IdrisBound">relation</span> <span class="IdrisBound">x</span> <span class="IdrisBound">y</span> <span class="IdrisKeyword">-></span> <span class="IdrisBound">relation</span> <span class="IdrisBound">y</span> <span class="IdrisBound">z</span><br />
<span class="IdrisKeyword">-></span> <span class="IdrisBound">relation</span> <span class="IdrisBound">x</span> <span class="IdrisBound">z</span><br />
</code>
We equip the built-in relation `Equal` with the structure of an equivalence
relation, using the constructor `Refl` and the stdlib functions `sym`, and
`trans`:
<code class="IdrisCode">
<span class="IdrisFunction">EqualityEquivalence</span> <span class="IdrisKeyword">:</span> <span class="IdrisType">Equivalence</span> <span class="IdrisBound">a</span><br />
<span class="IdrisFunction">EqualityEquivalence</span> <span class="IdrisKeyword">=</span> <span class="IdrisData">MkEquivalence</span><br />
<span class="IdrisKeyword">{</span> <span class="IdrisBound">relation</span> <span class="IdrisKeyword">=</span> <span class="IdrisFunction">(===)</span><br />
<span class="IdrisKeyword">,</span> <span class="IdrisBound">reflexive</span> <span class="IdrisKeyword">=</span> <span class="IdrisKeyword">\</span><span class="IdrisBound">x</span> <span class="IdrisKeyword">=></span> <span class="IdrisData">Refl</span><br />
<span class="IdrisKeyword">,</span> <span class="IdrisBound">symmetric</span> <span class="IdrisKeyword">=</span> <span class="IdrisKeyword">\</span><span class="IdrisBound">x</span><span class="IdrisKeyword">,</span><span class="IdrisBound">y</span><span class="IdrisKeyword">,</span><span class="IdrisBound">x\_eq\_y</span> <span class="IdrisKeyword">=></span> <span class="IdrisFunction">sym</span> <span class="IdrisBound">x\_eq\_y</span><br />
<span class="IdrisKeyword">,</span> <span class="IdrisBound">transitive</span> <span class="IdrisKeyword">=</span> <span class="IdrisKeyword">\</span><span class="IdrisBound">x</span><span class="IdrisKeyword">,</span><span class="IdrisBound">y</span><span class="IdrisKeyword">,</span><span class="IdrisBound">z</span><span class="IdrisKeyword">,</span><span class="IdrisBound">x\_eq\_y</span><span class="IdrisKeyword">,</span><span class="IdrisBound">y\_eq\_z</span> <span class="IdrisKeyword">=></span> <span class="IdrisFunction">trans</span> <span class="IdrisBound">x\_eq\_y</span> <span class="IdrisBound">y\_eq\_z</span><br />
<span class="IdrisKeyword">}</span><br />
</code>
We'll use the following relation on pairs of natural numbers as a running
example. We can represent an integer as the difference between a pair of natural
numbers:
<code class="IdrisCode">
<span class="IdrisKeyword">infix</span> <span class="IdrisKeyword">8</span> .-.<br />
<br />
<span class="IdrisKeyword">record</span> <span class="IdrisType">INT</span> <span class="IdrisKeyword">where</span><br />
constructor <span class="IdrisData">(.-.)</span><br />
<span class="IdrisFunction">pos</span><span class="IdrisKeyword">,</span> <span class="IdrisFunction">neg</span> <span class="IdrisKeyword">:</span> <span class="IdrisType">Nat</span><br />
<br />
<span class="IdrisKeyword">record</span> <span class="IdrisType">SameDiff</span> <span class="IdrisKeyword">(</span><span class="IdrisBound">x</span><span class="IdrisKeyword">,</span> <span class="IdrisBound">y</span> <span class="IdrisKeyword">:</span> <span class="IdrisType">INT</span><span class="IdrisKeyword">)</span> <span class="IdrisKeyword">where</span><br />
constructor <span class="IdrisData">Check</span><br />
<span class="IdrisFunction">same</span> <span class="IdrisKeyword">:</span> <span class="IdrisKeyword">(</span><span class="IdrisBound">x</span><span class="IdrisFunction">.pos + </span><span class="IdrisBound">y</span><span class="IdrisFunction">.neg === </span><span class="IdrisBound">y</span><span class="IdrisFunction">.pos + </span><span class="IdrisBound">x</span><span class="IdrisFunction">.neg</span><span class="IdrisKeyword">)</span><br />
</code>
The `SameDiff x y` relation is equivalent to mathematical equation that states
that the difference between the positive and negative parts is identical:
$$x_{pos} - x_{neg} = y_{pos} - y_{neg}$$
But, unlike the last equation which requires us to define integers and
subtraction, its equivalent `(.same)` is expressed using only addition, and
so addition on `Nat` is enough.
The relation `SameDiff` is an equivalence relation. The proofs are
straightforward, and a good opportunity to practice Idris's equational
reasoning combinators from `Syntax.PreorderReasoning`:
<code class="IdrisCode">
<span class="IdrisFunction">SameDiffEquivalence</span> <span class="IdrisKeyword">:</span> <span class="IdrisType">Equivalence</span> <span class="IdrisType">INT</span><br />
<span class="IdrisFunction">SameDiffEquivalence</span> <span class="IdrisKeyword">=</span> <span class="IdrisData">MkEquivalence</span><br />
<span class="IdrisKeyword">{</span> <span class="IdrisBound">relation</span> <span class="IdrisKeyword">=</span> <span class="IdrisType">SameDiff</span><br />
<span class="IdrisKeyword">,</span> <span class="IdrisBound">reflexive</span> <span class="IdrisKeyword">=</span> <span class="IdrisKeyword">\</span><span class="IdrisBound">x</span> <span class="IdrisKeyword">=></span> <span class="IdrisData">Check</span> $ <span class="IdrisFunction">Calc</span> $<br />
<span class="IdrisData">|~</span> <span class="IdrisBound">x</span><span class="IdrisFunction">.pos</span> <span class="IdrisFunction">+</span> <span class="IdrisBound">x</span><span class="IdrisFunction">.neg</span><br />
<span class="IdrisData">~~</span> <span class="IdrisBound">x</span><span class="IdrisFunction">.pos</span> <span class="IdrisFunction">+</span> <span class="IdrisBound">x</span><span class="IdrisFunction">.neg</span> <span class="IdrisData">...</span><span class="IdrisKeyword">(</span><span class="IdrisData">Refl</span><span class="IdrisKeyword">)</span><br />
</code>
This equational proof represents the single-step equational proof:
"Calculate:
1. $x_{pos} + x_{neg}$
2. $= x_{pos} + x_{neg}$ (by reflexivity)"
The mnemonic behind the ASCII-art is that the first step in the proof
starts with a logical-judgement symbol $\vdash$, each step continues with an
equality sign $=$, and justified by a thought bubble `(...)`.
<code class="IdrisCode">
<span class="IdrisKeyword">,</span> <span class="IdrisBound">symmetric</span> <span class="IdrisKeyword">=</span> <span class="IdrisKeyword">\</span><span class="IdrisBound">x</span><span class="IdrisKeyword">,</span><span class="IdrisBound">y</span><span class="IdrisKeyword">,</span><span class="IdrisBound">x\_eq\_y</span> <span class="IdrisKeyword">=></span> <span class="IdrisData">Check</span> $ <span class="IdrisFunction">Calc</span> $<br />
<span class="IdrisData">|~</span> <span class="IdrisBound">y</span><span class="IdrisFunction">.pos</span> <span class="IdrisFunction">+</span> <span class="IdrisBound">x</span><span class="IdrisFunction">.neg</span><br />
<span class="IdrisData">~~</span> <span class="IdrisBound">x</span><span class="IdrisFunction">.pos</span> <span class="IdrisFunction">+</span> <span class="IdrisBound">y</span><span class="IdrisFunction">.neg</span> <span class="IdrisFunction">..<</span><span class="IdrisKeyword">(</span><span class="IdrisBound">x\_eq\_y</span><span class="IdrisFunction">.same</span><span class="IdrisKeyword">)</span><br />
</code>
In this proof, we were given the proof `x_eq_y.same : x.pos + y.neg = y.pos + x.neg`
and so we appealed to the symmetric equation. The mnemonic here is that the
last bubble in the thought bubble `(...)` is replace with a left-pointing arrow,
reversing the reasoning step.
<code class="IdrisCode">
<span class="IdrisKeyword">,</span> <span class="IdrisBound">transitive</span> <span class="IdrisKeyword">=</span> <span class="IdrisKeyword">\</span><span class="IdrisBound">x</span><span class="IdrisKeyword">,</span><span class="IdrisBound">y</span><span class="IdrisKeyword">,</span><span class="IdrisBound">z</span><span class="IdrisKeyword">,</span><span class="IdrisBound">x\_eq\_y</span><span class="IdrisKeyword">,</span><span class="IdrisBound">y\_eq\_z</span> <span class="IdrisKeyword">=></span> <span class="IdrisData">Check</span> $ <span class="IdrisFunction">plusRightCancel</span> <span class="IdrisKeyword">\_</span> <span class="IdrisKeyword">\_</span> <span class="IdrisBound">y</span><span class="IdrisFunction">.pos</span><br />
$ <span class="IdrisFunction">Calc</span> $<br />
<span class="IdrisData">|~</span> <span class="IdrisBound">x</span><span class="IdrisFunction">.pos</span> <span class="IdrisFunction">+</span> <span class="IdrisBound">z</span><span class="IdrisFunction">.neg</span> <span class="IdrisFunction">+</span> <span class="IdrisBound">y</span><span class="IdrisFunction">.pos</span><br />
<span class="IdrisData">~~</span> <span class="IdrisBound">x</span><span class="IdrisFunction">.pos</span> <span class="IdrisFunction">+</span> <span class="IdrisKeyword">(</span><span class="IdrisBound">y</span><span class="IdrisFunction">.pos</span> <span class="IdrisFunction">+</span> <span class="IdrisBound">z</span><span class="IdrisFunction">.neg</span><span class="IdrisKeyword">)</span> <span class="IdrisData">...</span><span class="IdrisKeyword">(</span><span class="IdrisFunction">solve</span> <span class="IdrisData">3</span> <span class="IdrisFunction">Monoid.Commutative.Free.Free</span><br />
<span class="IdrisKeyword">{</span><span class="IdrisBound">a</span> <span class="IdrisKeyword">=</span> <span class="IdrisFunction">Nat.Additive</span><span class="IdrisKeyword">}</span> $<br />
<span class="IdrisKeyword">(</span><span class="IdrisFunction">X</span> <span class="IdrisData">0</span> <span class="IdrisFunction">.+.</span> <span class="IdrisFunction">X</span> <span class="IdrisData">1</span><span class="IdrisKeyword">)</span> <span class="IdrisFunction">.+.</span> <span class="IdrisFunction">X</span> <span class="IdrisData">2</span><br />
<span class="IdrisFunction">=-=</span> <span class="IdrisFunction">X</span> <span class="IdrisData">0</span> <span class="IdrisFunction">.+.</span> <span class="IdrisKeyword">(</span><span class="IdrisFunction">X</span> <span class="IdrisData">2</span> <span class="IdrisFunction">.+.</span> <span class="IdrisFunction">X</span> <span class="IdrisData">1</span><span class="IdrisKeyword">))</span><br />
<span class="IdrisData">~~</span> <span class="IdrisBound">x</span><span class="IdrisFunction">.pos</span> <span class="IdrisFunction">+</span> <span class="IdrisKeyword">(</span><span class="IdrisBound">z</span><span class="IdrisFunction">.pos</span> <span class="IdrisFunction">+</span> <span class="IdrisBound">y</span><span class="IdrisFunction">.neg</span><span class="IdrisKeyword">)</span> <span class="IdrisData">...</span><span class="IdrisKeyword">(</span><span class="IdrisFunction">cong</span> <span class="IdrisKeyword">(</span><span class="IdrisBound">x</span><span class="IdrisFunction">.pos</span> <span class="IdrisFunction">+</span><span class="IdrisKeyword">)</span> $ <span class="IdrisBound">y\_eq\_z</span><span class="IdrisFunction">.same</span><span class="IdrisKeyword">)</span><br />
<span class="IdrisData">~~</span> <span class="IdrisKeyword">(</span><span class="IdrisBound">x</span><span class="IdrisFunction">.pos</span> <span class="IdrisFunction">+</span> <span class="IdrisBound">y</span><span class="IdrisFunction">.neg</span><span class="IdrisKeyword">)</span> <span class="IdrisFunction">+</span> <span class="IdrisBound">z</span><span class="IdrisFunction">.pos</span> <span class="IdrisData">...</span><span class="IdrisKeyword">(</span><span class="IdrisFunction">solve</span> <span class="IdrisData">3</span> <span class="IdrisFunction">Monoid.Commutative.Free.Free</span><br />
<span class="IdrisKeyword">{</span><span class="IdrisBound">a</span> <span class="IdrisKeyword">=</span> <span class="IdrisFunction">Nat.Additive</span><span class="IdrisKeyword">}</span> $<br />
<span class="IdrisFunction">X</span> <span class="IdrisData">0</span> <span class="IdrisFunction">.+.</span> <span class="IdrisKeyword">(</span><span class="IdrisFunction">X</span> <span class="IdrisData">1</span> <span class="IdrisFunction">.+.</span> <span class="IdrisFunction">X</span> <span class="IdrisData">2</span><span class="IdrisKeyword">)</span><br />
<span class="IdrisFunction">=-=</span> <span class="IdrisKeyword">(</span><span class="IdrisFunction">X</span> <span class="IdrisData">0</span> <span class="IdrisFunction">.+.</span> <span class="IdrisFunction">X</span> <span class="IdrisData">2</span><span class="IdrisKeyword">)</span> <span class="IdrisFunction">.+.</span> <span class="IdrisFunction">X</span> <span class="IdrisData">1</span><span class="IdrisKeyword">)</span><br />
<span class="IdrisData">~~</span> <span class="IdrisKeyword">(</span><span class="IdrisBound">y</span><span class="IdrisFunction">.pos</span> <span class="IdrisFunction">+</span> <span class="IdrisBound">x</span><span class="IdrisFunction">.neg</span><span class="IdrisKeyword">)</span> <span class="IdrisFunction">+</span> <span class="IdrisBound">z</span><span class="IdrisFunction">.pos</span> <span class="IdrisData">...</span><span class="IdrisKeyword">(</span><span class="IdrisFunction">cong</span> <span class="IdrisKeyword">(</span><span class="IdrisFunction">+</span> <span class="IdrisBound">z</span><span class="IdrisFunction">.pos</span><span class="IdrisKeyword">)</span> ?h2<span class="IdrisKeyword">)</span><br />
<span class="IdrisData">~~</span> <span class="IdrisBound">z</span><span class="IdrisFunction">.pos</span> <span class="IdrisFunction">+</span> <span class="IdrisBound">x</span><span class="IdrisFunction">.neg</span> <span class="IdrisFunction">+</span> <span class="IdrisBound">y</span><span class="IdrisFunction">.pos</span> <span class="IdrisData">...</span><span class="IdrisKeyword">(</span><span class="IdrisFunction">solve</span> <span class="IdrisData">3</span> <span class="IdrisFunction">Monoid.Commutative.Free.Free</span><br />
<span class="IdrisKeyword">{</span><span class="IdrisBound">a</span> <span class="IdrisKeyword">=</span> <span class="IdrisFunction">Nat.Additive</span><span class="IdrisKeyword">}</span> $<br />
<span class="IdrisKeyword">(</span><span class="IdrisFunction">X</span> <span class="IdrisData">0</span> <span class="IdrisFunction">.+.</span> <span class="IdrisFunction">X</span> <span class="IdrisData">1</span><span class="IdrisKeyword">)</span> <span class="IdrisFunction">.+.</span> <span class="IdrisFunction">X</span> <span class="IdrisData">2</span><br />
<span class="IdrisFunction">=-=</span> <span class="IdrisKeyword">(</span><span class="IdrisFunction">X</span> <span class="IdrisData">2</span> <span class="IdrisFunction">.+.</span> <span class="IdrisFunction">X</span> <span class="IdrisData">1</span><span class="IdrisKeyword">)</span> <span class="IdrisFunction">.+.</span> <span class="IdrisFunction">X</span> <span class="IdrisData">0</span><span class="IdrisKeyword">)</span><br />
<span class="IdrisKeyword">}</span><br />
</code>
This proof is a lot more involved:
1. We appeal to the cancellation property of addition:
$a + c = b + c \Rightarrow a = b$
This construction relies crucially on the cancellation property. Later, we
will learn about its general form, called the INT-construction.
2. We rearrange the term, bringing the appropriate part of `y` into contact with
the appropriate part of `z` and `x` to transform the term.
Here we use the idris library [`Frex`](http://www.github.com/frex-project/idris-frex)
that can perform such routine
rearrangements for common algebraic structures. In this case, we use the
commutative monoid simplifier from `Frex`.
If you want to read more about `Frex`, check the
[paper](https://www.denotational.co.uk/drafts/allais-brady-corbyn-kammar-yallop-frex-dependently-typed-algebraic-simplification.pdf) out.
Idris's `Control.Relation` defines interfaces for properties like reflexivity
and transitivity. While the
setoid package doesn't use them, we'll use them in a few examples.
The `Overlap` relation from Examples 1 and 2 is symmetric:
<code class="IdrisCode">
<span class="IdrisType">Symmetric</span> <span class="IdrisKeyword">(</span><span class="IdrisType">List</span> <span class="IdrisBound">a</span><span class="IdrisKeyword">)</span> <span class="IdrisType">Overlap</span> <span class="IdrisKeyword">where</span><br />
<span class="IdrisFunction">symmetric</span> <span class="IdrisBound">xs\_overlaps\_ys</span> <span class="IdrisKeyword">=</span> <span class="IdrisData">Overlapping</span><br />
<span class="IdrisKeyword">{</span> <span class="IdrisBound">common</span> <span class="IdrisKeyword">=</span> <span class="IdrisBound">xs\_overlaps\_ys</span><span class="IdrisFunction">.common</span><br />
<span class="IdrisKeyword">,</span> <span class="IdrisBound">lhsPos</span> <span class="IdrisKeyword">=</span> <span class="IdrisBound">xs\_overlaps\_ys</span><span class="IdrisFunction">.rhsPos</span><br />
<span class="IdrisKeyword">,</span> <span class="IdrisBound">rhsPos</span> <span class="IdrisKeyword">=</span> <span class="IdrisBound">xs\_overlaps\_ys</span><span class="IdrisFunction">.lhsPos</span><br />
<span class="IdrisKeyword">}</span><br />
</code>
However, `Overlap` is neither reflexive nor transitive:
* The empty list doesn't overlap with itself:
<code class="IdrisCode">
<span class="IdrisFunction">Ex3</span> <span class="IdrisKeyword">:</span> <span class="IdrisFunction">Not</span> <span class="IdrisKeyword">(</span><span class="IdrisType">Overlap</span> <span class="IdrisData">[]</span> <span class="IdrisData">[]</span><span class="IdrisKeyword">)</span><br />
<span class="IdrisFunction">Ex3</span> <span class="IdrisBound">nil\_overlaps\_nil</span> <span class="IdrisKeyword">=</span> <span class="IdrisKeyword">case</span> <span class="IdrisBound">nil\_overlaps\_nil</span><span class="IdrisFunction">.lhsPos</span> <span class="IdrisKeyword">of</span><br />
<span class="IdrisKeyword">\_</span> <span class="IdrisKeyword">impossible</span><br />
</code>
* Two lists may overlap with a middle list, but on different elements. For example:
<code class="IdrisCode">
<span class="IdrisFunction">Ex4</span> <span class="IdrisKeyword">:</span> <span class="IdrisKeyword">(</span> <span class="IdrisType">Overlap</span> <span class="IdrisData">[1]</span> <span class="IdrisData">[1,2]</span><br />
<span class="IdrisType">,</span> <span class="IdrisType">Overlap</span> <span class="IdrisData">[1,2]</span> <span class="IdrisData">[2]</span><br />
<span class="IdrisType">,</span> <span class="IdrisFunction">Not</span> <span class="IdrisKeyword">(</span><span class="IdrisType">Overlap</span> <span class="IdrisData">[1]</span> <span class="IdrisData">[2]</span><span class="IdrisKeyword">))</span><br />
<span class="IdrisFunction">Ex4</span> <span class="IdrisKeyword">=</span><br />
<span class="IdrisKeyword">(</span> <span class="IdrisData">Overlapping</span> <span class="IdrisData">1</span> <span class="IdrisData">Here</span> <span class="IdrisData">Here</span><br />
<span class="IdrisData">,</span> <span class="IdrisData">Overlapping</span> <span class="IdrisData">2</span> <span class="IdrisKeyword">(</span><span class="IdrisData">There</span> <span class="IdrisData">Here</span><span class="IdrisKeyword">)</span> <span class="IdrisData">Here</span><br />
<span class="IdrisData">,</span> <span class="IdrisKeyword">\</span> <span class="IdrisBound">one\_overlaps\_two</span> <span class="IdrisKeyword">=></span> <span class="IdrisKeyword">case</span> <span class="IdrisBound">one\_overlaps\_two</span><span class="IdrisFunction">.lhsPos</span> <span class="IdrisKeyword">of</span><br />
<span class="IdrisData">There</span> <span class="IdrisKeyword">\_</span> <span class="IdrisKeyword">impossible</span><br />
<span class="IdrisKeyword">)</span><br />
</code>
The outer lists agree on `1` and `2`, respectively, but they can't overlap on
on the first element of either, which exhausts all possibilities of overlap.
<code class="IdrisCode">
<span class="IdrisBound">-</span>-<span class="IdrisFunction"> TO</span>D<span class="IdrisBound">O</span>:<span class="IdrisKeyword"> </span>c<span class="IdrisKeyword">l</span><span class="IdrisBound">e</span><span class="IdrisFunction">an t</span>h<span class="IdrisFunction">i</span>s<span class="IdrisBound"> </span><span class="IdrisFunction">up</span><br />
(.+.) : (x, y : INT) -> INT<br />
<span class="IdrisFunction">x .+.</span> <span class="IdrisKeyword">y</span> <span class="IdrisKeyword">=</span><span class="IdrisBound"> </span><span class="IdrisKeyword">(</span>x<span class="IdrisBound">.</span>p<span class="IdrisKeyword">o</span>s<span class="IdrisType"> + </span><span class="IdrisKeyword">y</span>.<span class="IdrisKeyword">po</span>s<span class="IdrisType">) .</span>-. (x.neg + y.neg)<br />
<br />
(.\*.) : (x, y : INT) -> INT<br />
<span class="IdrisFunction">x</span><span class="IdrisKeyword"> </span>.<span class="IdrisFunction">\*</span>.<span class="IdrisKeyword"> </span>y<span class="IdrisType"> = </span>(x.pos \* y.pos + x.neg \* y.neg) .-. (x.pos \* y.neg + x.neg \* y.pos)<br />
<br />
<span class="IdrisFunction">O</span>,<span class="IdrisKeyword"> </span>I<span class="IdrisData"> </span>:<span class="IdrisData"> IN</span>T<br />
<span class="IdrisFunction">O = 0 .-. 0</span><br />
<span class="IdrisFunction">I = 1 .-. 0</span><br />
plusIntZeroLftNeutral : (x : INT) -> O .+. x `SameDiff` x<br />
<span class="IdrisFunction">plusIntZeroLftNeutral</span> <span class="IdrisKeyword">x</span> <span class="IdrisKeyword">=</span><span class="IdrisBound"> </span>C<span class="IdrisKeyword">h</span>e<span class="IdrisType">ck </span><span class="IdrisKeyword">R</span>e<span class="IdrisKeyword">fl</span><br />
<br />
plusIntZeroRgtNeutral : (x : INT) -> <span class="IdrisKeyword">x</span><span class="IdrisBound"> </span>.<span class="IdrisKeyword">+</span>.<span class="IdrisFunction"> O `SameDiff</span><span class="IdrisKeyword">`</span> x<br />
plusIntZeroRgtNeutral x = Check (solv<span class="IdrisKeyword">e</span><span class="IdrisFunction"> </span>2<span class="IdrisData"> </span>M<span class="IdrisFunction">ono</span>i<span class="IdrisFunction">d.</span><span class="IdrisKeyword">C</span>o<span class="IdrisFunction">mmu</span>t<span class="IdrisFunction">a</span>t<span class="IdrisData">i</span>ve.Free.Free<br />
<span class="IdrisFunction"> </span> <span class="IdrisFunction">{</span>a<span class="IdrisData"> </span>=<span class="IdrisFunction"> Na</span>t<span class="IdrisKeyword">.</span><span class="IdrisFunction">A</span>d<span class="IdrisData">d</span>i<span class="IdrisFunction">tiv</span>e<span class="IdrisFunction">} </span><span class="IdrisKeyword">$</span><br />
(X 0 .+. O1) .+. X 1<br />
<span class="IdrisFunction"> </span> <span class="IdrisKeyword"> </span> <span class="IdrisKeyword"> </span><span class="IdrisBound"> </span><span class="IdrisKeyword"> </span><span class="IdrisBound"> </span><span class="IdrisKeyword"> </span><span class="IdrisBound"> </span> <span class="IdrisKeyword"> </span> <span class="IdrisType"> </span><span class="IdrisKeyword">=</span>-<span class="IdrisKeyword">= </span>X<span class="IdrisBound"> </span>0<span class="IdrisFunction"> .+</span>.<span class="IdrisKeyword"> </span><span class="IdrisBound">(</span>X<span class="IdrisFunction"> 1 </span>.<span class="IdrisBound">+</span><span class="IdrisKeyword">.</span> <span class="IdrisType">O1))</span><br />
<br />
plusInrAssociative : (x,y,z : INT) -><span class="IdrisKeyword"> </span><span class="IdrisBound">x</span> <span class="IdrisKeyword">.</span>+<span class="IdrisFunction">. (y .+. z) </span><span class="IdrisKeyword">`</span>SameDiff` (x .+. y) .+. z<br />
plusInrAssociative x y z = Check $<span class="IdrisKeyword"> </span><span class="IdrisFunction">(</span>s<span class="IdrisData">o</span>l<span class="IdrisFunction">ve </span>6<span class="IdrisKeyword"> </span><span class="IdrisFunction">M</span>o<span class="IdrisData">n</span>o<span class="IdrisFunction">id.</span>C<span class="IdrisFunction">o</span>m<span class="IdrisData">m</span><span class="IdrisKeyword">ut</span>a<span class="IdrisFunction">tiv</span>e<span class="IdrisKeyword">.F</span><span class="IdrisFunction">r</span>e<span class="IdrisData">e</span>.<span class="IdrisFunction">Fre</span>e<br />
<span class="IdrisFunction"> </span>{<span class="IdrisKeyword">a</span><span class="IdrisFunction"> </span>=<span class="IdrisData"> </span>N<span class="IdrisFunction">at.</span>A<span class="IdrisFunction">d</span>d<span class="IdrisData">i</span>t<span class="IdrisFunction">ive</span>}<span class="IdrisFunction"> </span>$<br />
(X 0 .+. (X 1 .+. X 2)) .+. ((X 3 .+. X 4) .+. X 5)<br />
<span class="IdrisKeyword"> </span> <span class="IdrisType"> </span> <span class="IdrisKeyword"> </span> <span class="IdrisType"> </span> <span class="IdrisKeyword"> </span> =-= (X 0 .+. X 1 .+. X 2) .+. (X 3 .+. (X 4 .+. X 5)))<br />
<br />
da<span class="IdrisData">ta IN</span>T<span class="IdrisKeyword">'</span> <span class="IdrisType">: T</span>y<span class="IdrisKeyword">pe</span> <span class="IdrisType">wher</span>e<br />
IPos : Nat -> INT'<br />
<span class="IdrisType"> IN</span>e<span class="IdrisType">gS :</span> <span class="IdrisType">Nat -> </span>I<span class="IdrisKeyword">NT'</span><br />
<br />
Ca<span class="IdrisFunction">st I</span>N<span class="IdrisKeyword">T</span><span class="IdrisData">' Int</span>e<span class="IdrisBound">g</span><span class="IdrisKeyword">e</span>r<span class="IdrisKeyword"> </span>w<span class="IdrisFunction">h</span>e<span class="IdrisFunction">re</span><br />
cast (IPos k) = cast k<br />
<span class="IdrisType"> ca</span>s<span class="IdrisType">t (I</span>N<span class="IdrisType">egS</span> <span class="IdrisKeyword">k) = </span>- cast (S k)<br />
<br />
Ca<span class="IdrisFunction">st I</span>N<span class="IdrisKeyword">T</span><span class="IdrisData">' INT</span> <span class="IdrisBound">w</span><span class="IdrisKeyword">h</span>e<span class="IdrisKeyword">r</span>e<br />
cast (IPos k) = k .-. 0<br />
<span class="IdrisFunction"> cast (I</span>N<span class="IdrisKeyword">e</span>g<span class="IdrisType">S k</span>)<span class="IdrisKeyword"> =</span> <span class="IdrisType">0 .</span>-. (S k)<br />
<br />
<span class="IdrisFunction">normalise</span> <span class="IdrisBound">:</span><span class="IdrisKeyword"> IN</span><span class="IdrisData">T</span> <span class="IdrisBound">-</span><span class="IdrisKeyword">></span> <span class="IdrisData">INT</span><br />
<span class="IdrisFunction">normalise</span> <span class="IdrisBound">i</span><span class="IdrisKeyword">@(0</span><span class="IdrisData"> </span>.<span class="IdrisBound">-</span><span class="IdrisKeyword">.</span> <span class="IdrisData">neg</span> <span class="IdrisKeyword"> </span><span class="IdrisData"> </span> <span class="IdrisBound"> </span><span class="IdrisKeyword"> )</span> <span class="IdrisKeyword">=</span> <span class="IdrisFunction">i</span><br />
normalise i@((S k) .-. 0 ) = i<br />
<span class="IdrisFunction">normalise i@((S k) </span>.<span class="IdrisKeyword">-</span>.<span class="IdrisKeyword"> </span><span class="IdrisBound">(</span>S<span class="IdrisKeyword"> </span>j<span class="IdrisType">)) </span><span class="IdrisKeyword">=</span> <span class="IdrisKeyword">no</span>r<span class="IdrisType">malise</span> <span class="IdrisKeyword">(k</span><span class="IdrisFunction"> .-. j)</span><br />
<br />
<span class="IdrisFunction">normaliseEitherZero</span> <span class="IdrisBound">:</span><span class="IdrisKeyword"> (x</span><span class="IdrisData"> </span>:<span class="IdrisBound"> </span><span class="IdrisKeyword">I</span>N<span class="IdrisData">T) </span>-<span class="IdrisData">></span> Eit<span class="IdrisKeyword">h</span>e<span class="IdrisKeyword">r</span> <span class="IdrisData">((nor</span>m<span class="IdrisData">alis</span>e x).pos = Z) ((normalise x).neg = Z)<br />
<span class="IdrisFunction">normaliseEitherZero</span> <span class="IdrisBound">i</span><span class="IdrisKeyword">@(0</span><span class="IdrisData"> </span>.<span class="IdrisBound">-</span><span class="IdrisKeyword">.</span> <span class="IdrisData">neg</span> <span class="IdrisKeyword"> </span><span class="IdrisData"> </span> <span class="IdrisBound"> </span><span class="IdrisKeyword"> )</span> <span class="IdrisKeyword">=</span> <span class="IdrisFunction">Left Refl</span><br />
normaliseEitherZero i@((S k) .-. 0 ) = Right Refl<br />
<span class="IdrisType">norm</span>a<span class="IdrisType">lis</span>e<span class="IdrisType">Eith</span>e<span class="IdrisKeyword">rZero</span> i@((S k) .-. (S j)) = normaliseEitherZero (k .-. j)<br />
<br />
Cast<span class="IdrisKeyword"> INT</span> <span class="IdrisFunction">INT' where</span><br />
cast<span class="IdrisKeyword"> </span><span class="IdrisData">x = </span>l<span class="IdrisBound">e</span><span class="IdrisKeyword">t</span> <span class="IdrisKeyword">(p</span>o<span class="IdrisKeyword">s .-</span>.<span class="IdrisBound"> ne</span>g<span class="IdrisKeyword">) </span>= normalise x in<br />
case<span class="IdrisData"> </span>n<span class="IdrisKeyword">or</span>m<span class="IdrisData">alis</span>e<span class="IdrisData">E</span>itherZero x of<br />
(L<span class="IdrisKeyword">e</span><span class="IdrisData">f</span>t<span class="IdrisBound"> </span><span class="IdrisKeyword">y</span>)<span class="IdrisKeyword"> =</span>><span class="IdrisData"> case</span> <span class="IdrisBound">n</span>eg of<br />
<span class="IdrisKeyword"> </span><span class="IdrisData"> 0 =></span> <span class="IdrisBound">I</span><span class="IdrisKeyword">P</span>o<span class="IdrisKeyword">s </span>0<br />
(S k) => INegS k<br />
<span class="IdrisComment"> (Right y) => IPo</span>s pos<br />
<br />
<span class="IdrisComment">-- stuff you can show:</span><br />
<br />
<span class="IdrisBound">-</span>-<span class="IdrisFunction"> x </span>`<span class="IdrisBound">S</span>a<span class="IdrisKeyword">m</span>e<span class="IdrisFunction">Diff</span>`<span class="IdrisKeyword"> </span><span class="IdrisFunction">y -></span> <span class="IdrisBound">n</span>o<span class="IdrisFunction">rma</span>l<span class="IdrisFunction">ise </span>x<span class="IdrisBound"> </span><span class="IdrisKeyword">=</span> normalise y<br />
<span class="IdrisBound">(</span>:<span class="IdrisFunction">\*:)</span>,<span class="IdrisBound"> </span>(<span class="IdrisKeyword">:</span>+<span class="IdrisFunction">:) :</span> <span class="IdrisKeyword">(</span><span class="IdrisFunction">x,y </span>:<span class="IdrisBound"> </span>I<span class="IdrisFunction">NT'</span>)<span class="IdrisFunction"> -> </span>I<span class="IdrisBound">N</span><span class="IdrisKeyword">T</span>'<br />
x :+: y = cast (cast x .+. cast y)<br />
x :\*: y = cast (cast x .\*. cast y)<br />
<br />
</code>
|
