From 4032974f05f80cbab61a26f4b30ce57ec2e43b3b Mon Sep 17 00:00:00 2001 From: Ohad Kammar Date: Mon, 8 Aug 2022 09:48:04 +0100 Subject: Snapshot --- doc/Tutorial.md | 48 ++++++++++++++++++++++++++---------------------- 1 file changed, 26 insertions(+), 22 deletions(-) (limited to 'doc/Tutorial.md') 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: -Symmetric (List a) Overlap where
-  symmetric xs\_overlaps\_ys = Overlapping
-    { common = xs\_overlaps\_ys.common
-    , lhsPos = xs\_overlaps\_ys.rhsPos
-    , rhsPos = xs\_overlaps\_ys.lhsPos
+Symmetric (List a) Overlap where
+  symmetric xs\_overlaps\_ys = Overlapping
+    { common = xs\_overlaps\_ys.common
+    , lhsPos = xs\_overlaps\_ys.rhsPos
+    , rhsPos = xs\_overlaps\_ys.lhsPos
    }
 However, `Overlap` is neither reflexive nor transitive: * The empty list doesn't overlap with itself: -Ex3 : Not (Overlap [] [])
-Ex3 nil\_overlaps\_nil = case nil\_overlaps\_nil.lhsPos of
-  \_ impossible
+Ex3 : Not (Overlap [] [])
+Ex3 nil\_overlaps\_nil = case nil\_overlaps\_nil.lhsPos of
+  \_ impossible
 * Two lists may overlap with a middle list, but on different elements. For example: -Ex4 : ( Overlap [1] [1,2]
-      , Overlap [1,2] [2]
-      , Not (Overlap [1] [2]))
-Ex4 =
-  ( Overlapping 1 Here Here
-  , Overlapping 2 (There Here) Here
-  , \ one\_overlaps\_two => case one\_overlaps\_two.lhsPos of
-     There \_ impossible
+Ex4 : ( Overlap [1] [1,2]
+      , Overlap [1,2] [2]
+      , Not (Overlap [1] [2]))
+Ex4 =
+  ( Overlapping 1 Here Here
+  , Overlapping 2 (There Here) Here
+  , \ one\_overlaps\_two => case one\_overlaps\_two.lhsPos of
+     There \_ impossible
  )
 The outer lists agree on `1` and `2`, respectively, but they can't overlap on -- cgit v1.2.3