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.html | 9 ++++++--- doc/Tutorial.md | 48 ++++++++++++++++++++++++++---------------------- doc/sources/Tutorial.md | 16 ++++++++++------ 3 files changed, 42 insertions(+), 31 deletions(-) (limited to 'doc') 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 @@

  , symmetric = </span>x,y,x_eq_y => Check $&nbsp;<span class="IdrisFunction">Calc</span>&nbsp;$
      |~ y.pos + x.neg
      ~~ x.pos + y.neg ..<(x_eq_y.same)
 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.   , transitive = </span>x,y,z,x_eq_y,y_eq_z => Check $&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;$ Calc $<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;$
                                     (X 0 .+. X 1) .+. X 2
                                  =-= X 0 .+. (X 2 .+. X 1))
      ~~ x.pos + (z.pos + y.neg) …(cong (x.pos +) $&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;$
                                     X 0 .+. (X 1 .+. X 2)
                                 =-= (X 0 .+. X 2) .+. X 1)
      ~~ (y.pos + x.neg) + z.pos …(cong (+ z.pos) ?h2)
      ~~ z.pos + x.neg + y.pos   …(solve 3 Monoid.Commutative.Free.Free
                                     {a = Nat.Additive} $
                                     (X 0 .+. X 1) .+. X 2
                                 =-= (X 2 .+. X 1) .+. X 0)
  }
 This proof is a lot more involved:

  1. We appeal to the cancellation property of addition: a + c = b + c ⇒ a = b
    2. +
+

This construction relies crucially on the cancellation property. Later, we will learn about its general form, called the INT-construction.

+
  1. 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 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 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: 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 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
    }
 However, Overlap is neither reflexive nor transitive:

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 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 -- cgit v1.2.3