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
|
<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>
<h1 id="tutorial-setoids">Tutorial: Setoids</h1>
<p>A <em>setoid</em> 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:</p>
<ol type="1">
<li>Know the user interface to the <code>setoid</code> package.</li>
<li>Know two different applications in which it can be used:</li>
</ol>
<ul>
<li><p>constructing types with an equality relation that’s better behaved than Idris’s built-in <code>Equal</code> type.</p></li>
<li><p>types with an equality relation that carries additional information</p></li>
</ul>
<p>If you want to see the source-code behind this tutorial, check the <a href="sources/Tutorial.md">source-code</a> out.</p>
<h2 id="equivalence-relations">Equivalence relations</h2>
<p>A <em>relation</em> over a type <code>ty</code> in Idris is any two-argument type-valued function:</p>
<pre><code>namespace Control.Relation
Rel : Type -> Type
Rel ty = ty -> ty -> Type</code></pre>
<p>This definition and its associated interfaces ship with idris’s standard library. Given a relation <code>rel : Rel ty</code> and <code>x,y : ty</code>, we can form <code>x `rel` y : Type</code>: the type of ways in which <code>x</code> and <code>y</code> can be related.</p>
<p>For example, two lists <em>overlap</em> 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"><code>Elem</code></span> <span class="IdrisBound">xs</span><br /> <span class="IdrisFunction">rhsPos</span> <span class="IdrisKeyword">:</span> <span class="IdrisBound">common</span> <span class="IdrisType"><code>Elem</code></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 <code>rel : Rel ty</code> as the type of edges in a directed graph between vertices in <code>ty</code>:</p>
<ul>
<li><p>edges have a direction: the type <code>rel x y</code> is different to <code>rel y x</code></p></li>
<li><p>multiple different edges between the same vertices <code>e1, e2 : rel x y</code></p></li>
<li><p>self-loops between the same vertex are allowed <code>loop : rel x x</code>.</p></li>
</ul>
<p>An <em>equivalence relation</em> is a relation that’s:</p>
<ul>
<li><p><em>reflexive</em>: we guarantee a specific way in which every element is related to itself;</p></li>
<li><p><em>symmetric</em>: we can reverse an edge between two edges; and</p></li>
<li><p><em>transitive</em>: we can compose paths of related elements into a single edge.</p></li>
</ul>
<p><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></p>
<p>We equip the built-in relation <code>Equal</code> with the structure of an equivalence relation, using the constructor <code>Refl</code> and the stdlib functions <code>sym</code>, and <code>trans</code>: <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></p>
<p>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 <code>SameDiff x y</code> relation is equivalent to mathematical equation that states that the difference between the positive and negative parts is identical: <br /><span class="math display"><em>x</em><sub><em>p</em><em>o</em><em>s</em></sub> − <em>x</em><sub><em>n</em><em>e</em><em>g</em></sub> = <em>y</em><sub><em>p</em><em>o</em><em>s</em></sub> − <em>y</em><sub><em>n</em><em>e</em><em>g</em></sub></span><br /> But, unlike the last equation which requires us to define integers and subtraction, its equivalent <code>(.same)</code> is expressed using only addition, and so addition on <code>Nat</code> is enough.</p>
<p>The relation <code>SameDiff</code> is an equivalence relation. The proofs are straightforward, and a good opportunity to practice Idris’s equational reasoning combinators from <code>Syntax.PreorderReasoning</code>: <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="math inline">$&nbsp;<span class="IdrisFunction">Calc</span>&nbsp;$</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:</p>
<p>"Calculate:</p>
<ol type="1">
<li><span class="math inline"><em>x</em><sub><em>p</em><em>o</em><em>s</em></sub> + <em>x</em><sub><em>n</em><em>e</em><em>g</em></sub></span></li>
<li><span class="math inline"> = <em>x</em><sub><em>p</em><em>o</em><em>s</em></sub> + <em>x</em><sub><em>n</em><em>e</em><em>g</em></sub></span> (by reflexivity)"</li>
</ol>
<p>The mnemonic behind the ASCII-art is that the first step in the proof starts with a logical-judgement symbol <span class="math inline">⊢</span>, each step continues with an equality sign <span class="math inline">=</span>, and justified by a thought bubble <code>(...)</code>.</p>
<p><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="math inline">$&nbsp;<span class="IdrisFunction">Calc</span>&nbsp;$</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 <code>x_eq_y.same : x.pos + y.neg = y.pos + x.neg</code> and so we appealed to the symmetric equation. The mnemonic here is that the last bubble in the thought bubble <code>(...)</code> 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="math inline">$&nbsp;<span class="IdrisFunction">plusRightCancel</span>&nbsp;<span class="IdrisKeyword">\_</span>&nbsp;<span class="IdrisKeyword">\_</span>&nbsp;<span class="IdrisBound">y</span><span class="IdrisFunction">.pos</span><br /> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;$</span> <span class="IdrisFunction">Calc</span> <span class="math inline">$<br /> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="IdrisData">|~</span>&nbsp;<span class="IdrisBound">x</span><span class="IdrisFunction">.pos</span>&nbsp;<span class="IdrisFunction">+</span>&nbsp;<span class="IdrisBound">z</span><span class="IdrisFunction">.neg</span>&nbsp;<span class="IdrisFunction">+</span>&nbsp;<span class="IdrisBound">y</span><span class="IdrisFunction">.pos</span><br /> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="IdrisData">~~</span>&nbsp;<span class="IdrisBound">x</span><span class="IdrisFunction">.pos</span>&nbsp;<span class="IdrisFunction">+</span>&nbsp;<span class="IdrisKeyword">(</span><span class="IdrisBound">y</span><span class="IdrisFunction">.pos</span>&nbsp;<span class="IdrisFunction">+</span>&nbsp;<span class="IdrisBound">z</span><span class="IdrisFunction">.neg</span><span class="IdrisKeyword">)</span>&nbsp;<span class="IdrisData">...</span><span class="IdrisKeyword">(</span><span class="IdrisFunction">solve</span>&nbsp;<span class="IdrisData">3</span>&nbsp;<span class="IdrisFunction">Monoid.Commutative.Free.Free</span><br /> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="IdrisKeyword">{</span><span class="IdrisBound">a</span>&nbsp;<span class="IdrisKeyword">=</span>&nbsp;<span class="IdrisFunction">Nat.Additive</span><span class="IdrisKeyword">}</span>&nbsp;$</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="math inline">$&nbsp;<span class="IdrisBound">y\_eq\_z</span><span class="IdrisFunction">.same</span><span class="IdrisKeyword">)</span><br /> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="IdrisData">~~</span>&nbsp;<span class="IdrisKeyword">(</span><span class="IdrisBound">x</span><span class="IdrisFunction">.pos</span>&nbsp;<span class="IdrisFunction">+</span>&nbsp;<span class="IdrisBound">y</span><span class="IdrisFunction">.neg</span><span class="IdrisKeyword">)</span>&nbsp;<span class="IdrisFunction">+</span>&nbsp;<span class="IdrisBound">z</span><span class="IdrisFunction">.pos</span>&nbsp;<span class="IdrisData">...</span><span class="IdrisKeyword">(</span><span class="IdrisFunction">solve</span>&nbsp;<span class="IdrisData">3</span>&nbsp;<span class="IdrisFunction">Monoid.Commutative.Free.Free</span><br /> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="IdrisKeyword">{</span><span class="IdrisBound">a</span>&nbsp;<span class="IdrisKeyword">=</span>&nbsp;<span class="IdrisFunction">Nat.Additive</span><span class="IdrisKeyword">}</span>&nbsp;$</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:</p>
<ol type="1">
<li>We appeal to the cancellation property of addition: <span class="math inline"><em>a</em> + <em>c</em> = <em>b</em> + <em>c</em> ⇒ <em>a</em> = <em>b</em></span></li>
</ol>
<p>This construction relies crucially on the cancellation property. Later, we will learn about its general form, called the INT-construction.</p>
<ol start="2" type="1">
<li>We rearrange the term, bringing the appropriate part of <code>y</code> into contact with the appropriate part of <code>z</code> and <code>x</code> to transform the term.</li>
</ol>
<p>Here we use the idris library <a href="http://www.github.com/frex-project/idris-frex"><code>Frex</code></a> that can perform such routine rearrangements for common algebraic structures. In this case, we use the commutative monoid simplifier from <code>Frex</code>. If you want to read more about <code>Frex</code>, check the <a href="https://www.denotational.co.uk/drafts/allais-brady-corbyn-kammar-yallop-frex-dependently-typed-algebraic-simplification.pdf">paper</a> out.</p>
<p>Idris’s <code>Control.Relation</code> defines interfaces for properties like reflexivity and transitivity. While the setoid package doesn’t use them, we’ll use them in a few examples.</p>
<p>The <code>Overlap</code> 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, <code>Overlap</code> is neither reflexive nor transitive:</p>
<ul>
<li><p>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></p></li>
<li><p>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 <code>1</code> and <code>2</code>, respectively, but they can’t overlap on on the first element of either, which exhausts all possibilities of overlap.</p></li>
</ul>
<p><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 <code>SameDiff</code> 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 <code>SameDiff</span><span class="IdrisKeyword"></code></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 class="math inline">$</span><br /> &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(X&nbsp;0&nbsp;.+.&nbsp;O1)&nbsp;.+.&nbsp;X&nbsp;1<br /> <span class="IdrisFunction">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;</span>&nbsp;<span class="IdrisKeyword">&nbsp;</span>&nbsp;<span class="IdrisKeyword">&nbsp;</span><span class="IdrisBound">&nbsp;</span><span class="IdrisKeyword">&nbsp;</span><span class="IdrisBound">&nbsp;</span><span class="IdrisKeyword">&nbsp;</span><span class="IdrisBound">&nbsp;</span>&nbsp;<span class="IdrisKeyword">&nbsp;</span>&nbsp;<span class="IdrisType">&nbsp;&nbsp;&nbsp;</span><span class="IdrisKeyword">=</span>-<span class="IdrisKeyword">=&nbsp;</span>X<span class="IdrisBound">&nbsp;</span>0<span class="IdrisFunction">&nbsp;.+</span>.<span class="IdrisKeyword">&nbsp;</span><span class="IdrisBound">(</span>X<span class="IdrisFunction">&nbsp;1&nbsp;</span>.<span class="IdrisBound">+</span><span class="IdrisKeyword">.</span>&nbsp;<span class="IdrisType">O1))</span><br /> <br /> plusInrAssociative&nbsp;:&nbsp;(x,y,z&nbsp;:&nbsp;INT)&nbsp;-&gt;<span class="IdrisKeyword">&nbsp;</span><span class="IdrisBound">x</span>&nbsp;<span class="IdrisKeyword">.</span>+<span class="IdrisFunction">.&nbsp;(y&nbsp;.+.&nbsp;z)&nbsp;</span><span class="IdrisKeyword">`</span>SameDiff`&nbsp;(x&nbsp;.+.&nbsp;y)&nbsp;.+.&nbsp;z<br /> plusInrAssociative&nbsp;x&nbsp;y&nbsp;z&nbsp;=&nbsp;Check&nbsp;$</span><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><code><span class="IdrisBound">S</span>a<span class="IdrisKeyword">m</span>e<span class="IdrisFunction">Diff</span></code><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></p>
|
