diff options
| author | Ohad Kammar <ohad.kammar@ed.ac.uk> | 2022-08-08 09:48:04 +0100 |
|---|---|---|
| committer | Ohad Kammar <ohad.kammar@ed.ac.uk> | 2022-08-08 09:48:04 +0100 |
| commit | 4032974f05f80cbab61a26f4b30ce57ec2e43b3b (patch) | |
| tree | 2daa1ef028d41bc2de2060df7eea1307119bea78 | |
| parent | 1aa6b6ef854fc428b888be20ce8321317bb3b627 (diff) | |
Snapshot
| -rw-r--r-- | doc/Tutorial.html | 9 | ||||
| -rw-r--r-- | doc/Tutorial.md | 48 | ||||
| -rw-r--r-- | doc/sources/Tutorial.md | 16 |
3 files changed, 42 insertions, 31 deletions
diff --git a/doc/Tutorial.html b/doc/Tutorial.html index 5336f7a..e10bee7 100644 --- a/doc/Tutorial.html +++ b/doc/Tutorial.html @@ -76,12 +76,15 @@ <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"> Sy<span class="IdrisFunction">mmetric (</span>L<span class="IdrisBound">ist a) Overlap</span> <span class="IdrisKeyword">w</span>h<span class="IdrisData">ere</span><br /> sy<span class="IdrisKeyword">m</span>m<span class="IdrisBound">etric </span>x<span class="IdrisKeyword">s</span>_<span class="IdrisBound">overlaps_ys = </span><span class="IdrisFunction">Overlap</span>ping<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> rhsPos = xs_overlaps_ys.lhsPos<br /> }<br /> </code> However, <code>Overlap</code> is neither reflexive nor transitive:</p> +<p>The <code>Overlap</code> relation from Examples 1 and 2 is symmetric: <code class="IdrisCode"> Symm<span class="IdrisKeyword">e</span>tric (List a) Overlap where<br /> symmetric xs_overlaps_ys = Overlapping<br /> { common = xs_overlaps_ys.common<br /> , lhsPos = xs_overlaps_ys.rhsPos<br /> , rhsPos = xs_overlaps_ys.lhsPos<br /> }<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="IdrisBound">: Not (Overlap [</span>]<span class="IdrisKeyword"> </span>[<span class="IdrisKeyword">])</span><br /> Ex<span class="IdrisKeyword">3</span> <span class="IdrisKeyword">nil_overla</span>ps_nil = case nil_overlaps_nil.lhsPos of<br /> _ impossible<br /> </code></p></li> -<li><p>Two lists may overlap with a middle list, but on different elements. For example: <code class="IdrisCode"> Ex4 : <span class="IdrisType">(</span> <span class="IdrisType">Overlap</span> <span class="IdrisData">[1] [</span>1<span class="IdrisData">,2]</span><br /> <span class="IdrisType">,</span> <span class="IdrisFunction">Ove</span>r<span class="IdrisKeyword">l</span><span class="IdrisType">ap [1,2</span>]<span class="IdrisData"> [2</span>]<br /> <span class="IdrisFunction"> </span> <span class="IdrisKeyword"> </span> , Not (Overlap [1] [2]))<br /> Ex<span class="IdrisKeyword">4</span> <span class="IdrisData">=</span><br /> <span class="IdrisData">(</span> <span class="IdrisData">Overlapping</span> <span class="IdrisData">1</span> <span class="IdrisKeyword">H</span><span class="IdrisData">ere H</span>e<span class="IdrisData">re</span><br /> <span class="IdrisData">,</span> <span class="IdrisKeyword">O</span>v<span class="IdrisBound">erlapping 2 (The</span>r<span class="IdrisKeyword">e </span>H<span class="IdrisKeyword">ere)</span> <span class="IdrisBound">Here</span><br /> , <span class=“IdrisData”> one_</span>o<span class="IdrisKeyword">v</span>e<span class="IdrisKeyword">rlaps_two </span>=> case one_overlaps_two.lhsPos of<br /> <span class="IdrisKeyword"> </span> There _ impossible<br /> )<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> +<li><p>The empty list doesn’t overlap with itself: <code class="IdrisCode"> Ex3 : Not (Overlap [] [])<br /> Ex3 nil_overlaps_nil = case nil_overlaps_nil.lhsPos of<br /> <span class="IdrisFunction"> _</span> <span class="IdrisKeyword">i</span>m<span class="IdrisKeyword">p</span>o<span class="IdrisType">ssible</span><br /> </code></p></li> +<li><p>Two lists may overlap with a middle list, but on different elements. For example: <code class="IdrisCode"> Ex<span class="IdrisData">4</span> <span class="IdrisData">: ( Overlap</span> <span class="IdrisData">[</span>1<span class="IdrisKeyword">]</span><span class="IdrisData"> [1,2</span>]<br /> <span class="IdrisData"> </span> <span class="IdrisKeyword"> </span> <span class="IdrisBound">, Overlap [1,2] </span>[<span class="IdrisKeyword">2]</span><br /> <span class="IdrisData"> , No</span>t<span class="IdrisKeyword"> </span>(<span class="IdrisKeyword">Overlap [1</span>] [2]))<br /> Ex<span class="IdrisKeyword">4</span> =<br /> ( Overlapping 1 Here Here<br /> , Overlapping 2 (There Here) Here<br /> , &nbsp;one_overlaps_two => case one_overlaps_two.lhsPos of<br /> There _ impossible<br /> )<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> diff --git a/doc/Tutorial.md b/doc/Tutorial.md index c0d0896..b9a5896 100644 --- a/doc/Tutorial.md +++ b/doc/Tutorial.md @@ -220,15 +220,19 @@ 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. + 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 @@ -237,32 +241,32 @@ 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"> -Sy<span class="IdrisFunction">mmetric (</span>L<span class="IdrisBound">ist a) Overlap</span> <span class="IdrisKeyword">w</span>h<span class="IdrisData">ere</span><br /> - sy<span class="IdrisKeyword">m</span>m<span class="IdrisBound">etric </span>x<span class="IdrisKeyword">s</span>\_<span class="IdrisBound">overlaps\_ys = </span><span class="IdrisFunction">Overlap</span>ping<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> rhsPos = xs\_overlaps\_ys.lhsPos<br /> +Symm<span class="IdrisKeyword">e</span>tric (List a) Overlap where<br /> + symmetric xs\_overlaps\_ys = Overlapping<br /> + { common = xs\_overlaps\_ys.common<br /> + , lhsPos = xs\_overlaps\_ys.rhsPos<br /> + , rhsPos = xs\_overlaps\_ys.lhsPos<br /> }<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="IdrisBound">: Not (Overlap [</span>]<span class="IdrisKeyword"> </span>[<span class="IdrisKeyword">])</span><br /> -Ex<span class="IdrisKeyword">3</span> <span class="IdrisKeyword">nil\_overla</span>ps\_nil = case nil\_overlaps\_nil.lhsPos of<br /> - \_ impossible<br /> +Ex3 : Not (Overlap [] [])<br /> +Ex3 nil\_overlaps\_nil = case nil\_overlaps\_nil.lhsPos of<br /> +<span class="IdrisFunction"> \_</span> <span class="IdrisKeyword">i</span>m<span class="IdrisKeyword">p</span>o<span class="IdrisType">ssible</span><br /> </code> * Two lists may overlap with a middle list, but on different elements. For example: <code class="IdrisCode"> -Ex4 : <span class="IdrisType">(</span> <span class="IdrisType">Overlap</span> <span class="IdrisData">[1] [</span>1<span class="IdrisData">,2]</span><br /> - <span class="IdrisType">,</span> <span class="IdrisFunction">Ove</span>r<span class="IdrisKeyword">l</span><span class="IdrisType">ap [1,2</span>]<span class="IdrisData"> [2</span>]<br /> -<span class="IdrisFunction"> </span> <span class="IdrisKeyword"> </span> , Not (Overlap [1] [2]))<br /> -Ex<span class="IdrisKeyword">4</span> <span class="IdrisData">=</span><br /> - <span class="IdrisData">(</span> <span class="IdrisData">Overlapping</span> <span class="IdrisData">1</span> <span class="IdrisKeyword">H</span><span class="IdrisData">ere H</span>e<span class="IdrisData">re</span><br /> - <span class="IdrisData">,</span> <span class="IdrisKeyword">O</span>v<span class="IdrisBound">erlapping 2 (The</span>r<span class="IdrisKeyword">e </span>H<span class="IdrisKeyword">ere)</span> <span class="IdrisBound">Here</span><br /> - , \<span class="IdrisData"> one\_</span>o<span class="IdrisKeyword">v</span>e<span class="IdrisKeyword">rlaps\_two </span>=> case one\_overlaps\_two.lhsPos of<br /> - <span class="IdrisKeyword"> </span> There \_ impossible<br /> +Ex<span class="IdrisData">4</span> <span class="IdrisData">: ( Overlap</span> <span class="IdrisData">[</span>1<span class="IdrisKeyword">]</span><span class="IdrisData"> [1,2</span>]<br /> + <span class="IdrisData"> </span> <span class="IdrisKeyword"> </span> <span class="IdrisBound">, Overlap [1,2] </span>[<span class="IdrisKeyword">2]</span><br /> + <span class="IdrisData"> , No</span>t<span class="IdrisKeyword"> </span>(<span class="IdrisKeyword">Overlap [1</span>] [2]))<br /> +Ex<span class="IdrisKeyword">4</span> =<br /> + ( Overlapping 1 Here Here<br /> + , Overlapping 2 (There Here) Here<br /> + , \ one\_overlaps\_two => case one\_overlaps\_two.lhsPos of<br /> + There \_ impossible<br /> )<br /> </code> The outer lists agree on `1` and `2`, respectively, but they can't overlap on diff --git a/doc/sources/Tutorial.md b/doc/sources/Tutorial.md index 85b09c8..a33652f 100644 --- a/doc/sources/Tutorial.md +++ b/doc/sources/Tutorial.md @@ -200,15 +200,19 @@ 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. + 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 |