diff options
Diffstat (limited to 'doc/Tutorial.md')
| -rw-r--r-- | doc/Tutorial.md | 48 |
1 files changed, 26 insertions, 22 deletions
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 |