From 85b191cd3134102c7205c1771806ee16f73b3a89 Mon Sep 17 00:00:00 2001 From: Ohad Kammar Date: Sun, 7 Aug 2022 23:35:19 +0100 Subject: Write about equivalence relations --- doc/Makefile | 4 +- doc/Tutorial.html | 43 +++++++- doc/Tutorial.md | 270 ++++++++++++++++++++++++++++++++++++++++++++++++ doc/pack.toml | 8 +- doc/setoid-doc.ipkg | 6 +- doc/sources/Tutorial.md | 230 ++++++++++++++++++++++++++++++++++++++++- 6 files changed, 553 insertions(+), 8 deletions(-) create mode 100644 doc/Tutorial.md (limited to 'doc') diff --git a/doc/Makefile b/doc/Makefile index ac7e6e3..c50a300 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -6,8 +6,8 @@ ttms: pack build setoid-doc.ipkg %.html: .PHONY - pack run katla markdown --config ./setoid-doc-style.dhall sources/$*.md ./build/ttc/$*.ttm \ - | pandoc -o $*.html + pack run katla markdown --config ./setoid-doc-style.dhall sources/$*.md ./build/ttc/$*.ttm > $*.md + pandoc $*.md -o $*.html install-deps: pack install-deps setoid-doc.ipkg diff --git a/doc/Tutorial.html b/doc/Tutorial.html index ae77959..5336f7a 100644 --- a/doc/Tutorial.html +++ b/doc/Tutorial.html @@ -44,5 +44,44 @@

  • constructing types with an equality relation that’s better behaved than Idris’s built-in Equal type.

  • types with an equality relation that carries additional information

    • -

    Basic interface

    -


    +

    If you want to see the source-code behind this tutorial, check the source-code out.

    +

    Equivalence relations

    +

    A relation over a type ty in Idris is any two-argument type-valued function:

    +
    namespace Control.Relation
+  Rel : Type -> Type
+  Rel ty = ty -> ty -> Type
    +

    This definition and its associated interfaces ship with idris’s standard library. Given a relation rel : Rel ty and x,y : ty, we can form x `rel` y : Type: the type of ways in which x and y can be related.

    +

    For example, two lists overlap when they have a common element: record Overlap {0 a : Type} (xs,ys : List a) where
      constructor Overlapping
      common : a
      lhsPos : common Elem xs
      rhsPos : common Elem ys

     Lists can overlap in exactly one position: Ex1 : Overlap [1,2,3] [6,7,2,8]
    Ex1 = Overlapping
      { common = 2
      , lhsPos = There Here
      , rhsPos = There (There Here)
      }
     But they can overlap in several ways: Ex2a ,
    Ex2b ,
    Ex2c : Overlap [1,2,3] [2,3,2]
    Ex2a = Overlapping
      { common = 3
      , lhsPos = There (There Here)
      , rhsPos = There Here
      }
    Ex2b = Overlapping
      { common = 2
      , lhsPos = There Here
      , rhsPos = Here
      }
    Ex2c = Overlapping
      { common = 2
      , lhsPos = There Here
      , rhsPos = There (There Here)
      }
     We can think of a relation rel : Rel ty as the type of edges in a directed graph between vertices in ty:

    + +

    An equivalence relation is a relation that’s:

    + +

    record Equivalence (A : Type) where
      constructor MkEquivalence
      0 relation: Rel A
      reflexive : (x       : A) -> relation x x
      symmetric : (x, y    : A) -> relation x y -> relation y x
      transitive: (x, y, z : A) -> relation x y -> relation y z
                                -> relation x z

    +

    We equip the built-in relation Equal with the structure of an equivalence relation, using the constructor Refl and the stdlib functions sym, and trans: EqualityEquivalence : Equivalence a
    EqualityEquivalence = MkEquivalence
      { relation = (===)
      , reflexive = </span>x => Refl
      , symmetric = </span>x,y,x_eq_y => sym x_eq_y
      , transitive = </span>x,y,z,x_eq_y,y_eq_z => trans x_eq_y y_eq_z
      }

    +

    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: infix 8 .-.

    record INT where
      constructor (.-.)
      pos, neg : Nat

    record SameDiff (x, y : INT) where
      constructor Check
      same : (x.pos + y.neg === y.pos + x.neg)
     The SameDiff x y relation is equivalent to mathematical equation that states that the difference between the positive and negative parts is identical:
    xpos − xneg = ypos − yneg
    But, unlike the last equation which requires us to define integers and subtraction, its equivalent (.same) is expressed using only addition, and so addition on Nat is enough.

    +

    The relation SameDiff is an equivalence relation. The proofs are straightforward, and a good opportunity to practice Idris’s equational reasoning combinators from Syntax.PreorderReasoning: SameDiffEquivalence : Equivalence INT
    SameDiffEquivalence = MkEquivalence
      { relation = SameDiff
      , reflexive = </span>x => Check $&nbsp;<span class="IdrisFunction">Calc</span>&nbsp;$
          |~ x.pos + x.neg
          ~~ x.pos + x.neg …(Refl)
     This equational proof represents the single-step equational proof:

    +

    "Calculate:

    +
      +
    1. xpos + xneg
      2. +
    2.  = xpos + xneg (by reflexivity)"
      3. +
    +

    The mnemonic behind the ASCII-art is that the first step in the proof starts with a logical-judgement symbol ⊢, each step continues with an equality sign =, and justified by a thought bubble (...).

    +

      , 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. +
    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.
      3. +
    +

    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:

    + diff --git a/doc/Tutorial.md b/doc/Tutorial.md new file mode 100644 index 0000000..c0d0896 --- /dev/null +++ b/doc/Tutorial.md @@ -0,0 +1,270 @@ + + +# Tutorial: Setoids + +A _setoid_ 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: + +1. Know the user interface to the `setoid` package. +2. Know two different applications in which it can be used: + + constructing types with an equality relation that's better behaved than + Idris's built-in `Equal` type. + + + types with an equality relation that carries additional information + +If you want to see the source-code behind this tutorial, check the +[source-code](sources/Tutorial.md) out. + +## Equivalence relations + +A _relation_ over a type `ty` in Idris is any two-argument type-valued function: +``` +namespace Control.Relation + Rel : Type -> Type + Rel ty = ty -> ty -> Type +``` +This definition and its associated interfaces ship with idris's standard +library. Given a relation `rel : Rel ty` and `x,y : ty`, we can form +```x `rel` y : Type```: the type of ways in which `x` and `y` can be related. + +For example, two lists _overlap_ when they have a common element: + +record Overlap {0 a : Type} (xs,ys : List a) where
    +  constructor Overlapping
    +  common : a
    +  lhsPos : common `Elem` xs
    +  rhsPos : common `Elem` ys
    +
    +     +Lists can overlap in exactly one position: + +Ex1 : Overlap [1,2,3] [6,7,2,8]
    +Ex1 = Overlapping
    +  { common = 2
    +  , lhsPos = There Here
    +  , rhsPos = There (There Here)
    +  }
    +     +But they can overlap in several ways: + +Ex2a ,
    +Ex2b ,
    +Ex2c : Overlap [1,2,3] [2,3,2]
    +Ex2a = Overlapping
    +  { common = 3
    +  , lhsPos = There (There Here)
    +  , rhsPos = There Here
    +  }
    +Ex2b = Overlapping
    +  { common = 2
    +  , lhsPos = There Here
    +  , rhsPos = Here
    +  }
    +Ex2c = Overlapping
    +  { common = 2
    +  , lhsPos = There Here
    +  , rhsPos = There (There Here)
    +  }
    +     +We can think of a relation `rel : Rel ty` as the type of edges in a directed +graph between vertices in `ty`: + +* edges have a direction: the type `rel x y` is different to `rel y x` + +* multiple different edges between the same vertices `e1, e2 : rel x y` + +* self-loops between the same vertex are allowed `loop : rel x x`. + +An _equivalence relation_ is a relation that's: + +* _reflexive_: we guarantee a specific way in which every element is related to + itself; + +* _symmetric_: we can reverse an edge between two edges; and + +* _transitive_: we can compose paths of related elements into a single edge. + + +record Equivalence (A : Type) where
    +  constructor MkEquivalence
    +  0 relation: Rel A
    +  reflexive : (x       : A) -> relation x x
    +  symmetric : (x, y    : A) -> relation x y -> relation y x
    +  transitive: (x, y, z : A) -> relation x y -> relation y z
    +                            -> relation x z
    +     + +We equip the built-in relation `Equal` with the structure of an equivalence +relation, using the constructor `Refl` and the stdlib functions `sym`, and +`trans`: + +EqualityEquivalence : Equivalence a
    +EqualityEquivalence = MkEquivalence
    +  { relation = (===)
    +  , reflexive = \x => Refl
    +  , symmetric = \x,y,x\_eq\_y => sym x\_eq\_y
    +  , transitive = \x,y,z,x\_eq\_y,y\_eq\_z => trans x\_eq\_y y\_eq\_z
    +  }
    +     + +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: + +infix 8 .-.
    +
    +record INT where
    +  constructor (.-.)
    +  pos, neg : Nat
    +
    +record SameDiff (x, y : INT) where
    +  constructor Check
    +  same : (x.pos + y.neg === y.pos + x.neg)
    +     +The `SameDiff x y` relation is equivalent to mathematical equation that states +that the difference between the positive and negative parts is identical: +$$x_{pos} - x_{neg} = y_{pos} - y_{neg}$$ +But, unlike the last equation which requires us to define integers and +subtraction, its equivalent `(.same)` is expressed using only addition, and +so addition on `Nat` is enough. + +The relation `SameDiff` is an equivalence relation. The proofs are +straightforward, and a good opportunity to practice Idris's equational +reasoning combinators from `Syntax.PreorderReasoning`: + +SameDiffEquivalence : Equivalence INT
    +SameDiffEquivalence = MkEquivalence
    +  { relation = SameDiff
    +  , reflexive = \x => Check $ Calc $
    +      |~ x.pos + x.neg
    +      ~~ x.pos + x.neg ...(Refl)
    +     +This equational proof represents the single-step equational proof: + +"Calculate: + +1. $x_{pos} + x_{neg}$ +2. $= x_{pos} + x_{neg}$ (by reflexivity)" + +The mnemonic behind the ASCII-art is that the first step in the proof +starts with a logical-judgement symbol $\vdash$, each step continues with an +equality sign $=$, and justified by a thought bubble `(...)`. + + +  , symmetric = \x,y,x\_eq\_y => Check $ Calc $
    +      |~ 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 = \x,y,z,x\_eq\_y,y\_eq\_z => Check $ plusRightCancel \_ \_ y.pos
    +      $ Calc $
    +      |~ x.pos + z.neg + y.pos
    +      ~~ x.pos + (y.pos + z.neg) ...(solve 3 Monoid.Commutative.Free.Free
    +                                     {a = Nat.Additive} $
    +                                     (X 0 .+. X 1) .+. X 2
    +                                  =-= X 0 .+. (X 2 .+. X 1))
    +      ~~ x.pos + (z.pos + y.neg) ...(cong (x.pos +) $ y\_eq\_z.same)
    +      ~~ (x.pos + y.neg) + z.pos ...(solve 3 Monoid.Commutative.Free.Free
    +                                     {a = Nat.Additive} $
    +                                     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 \Rightarrow a = b$ +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. + + +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 empty list doesn't overlap with itself: + +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
    +  )
    +     +The outer lists agree on `1` and `2`, respectively, but they can't overlap on +on the first element of either, which exhausts all possibilities of overlap. + diff --git a/doc/pack.toml b/doc/pack.toml index d555f03..3aff702 100644 --- a/doc/pack.toml +++ b/doc/pack.toml @@ -1,4 +1,10 @@ -[doc.setoid] +[custom.all.setoid] type = "local" path = ".." ipkg = "setoid.ipkg" + +[custom.all.frex] +type = "github" +url = "https://github.com/frex-project/idris-frex" +commit = "latest:main" +ipkg = "frex.ipkg" diff --git a/doc/setoid-doc.ipkg b/doc/setoid-doc.ipkg index 5d183fd..b97fb59 100644 --- a/doc/setoid-doc.ipkg +++ b/doc/setoid-doc.ipkg @@ -13,8 +13,10 @@ authors = "Ohad Kammar" -- langversion -- packages to add to search path --- depends = - +depends + = contrib + , setoid + , frex modules = Tutorial diff --git a/doc/sources/Tutorial.md b/doc/sources/Tutorial.md index f143d45..85b09c8 100644 --- a/doc/sources/Tutorial.md +++ b/doc/sources/Tutorial.md @@ -1,5 +1,17 @@ ```idris hide module Tutorial + +import Data.Setoid +import Syntax.PreorderReasoning +import Syntax.PreorderReasoning.Setoid +import Data.List.Elem +import Data.List +import Data.Nat +import Frex +import Frexlet.Monoid.Commutative +import Notation.Additive +import Frexlet.Monoid.Notation.Additive +import Frexlet.Monoid.Commutative.Nat ``` # Tutorial: Setoids @@ -15,7 +27,223 @@ tutorial you will: + types with an equality relation that carries additional information -## Basic interface +If you want to see the source-code behind this tutorial, check the +[source-code](sources/Tutorial.md) out. + +## Equivalence relations + +A _relation_ over a type `ty` in Idris is any two-argument type-valued function: +``` +namespace Control.Relation + Rel : Type -> Type + Rel ty = ty -> ty -> Type +``` +This definition and its associated interfaces ship with idris's standard +library. Given a relation `rel : Rel ty` and `x,y : ty`, we can form +```x `rel` y : Type```: the type of ways in which `x` and `y` can be related. + +For example, two lists _overlap_ when they have a common element: +```idris +record Overlap {0 a : Type} (xs,ys : List a) where + constructor Overlapping + common : a + lhsPos : common `Elem` xs + rhsPos : common `Elem` ys + +``` +Lists can overlap in exactly one position: +```idris +Ex1 : Overlap [1,2,3] [6,7,2,8] +Ex1 = Overlapping + { common = 2 + , lhsPos = There Here + , rhsPos = There (There Here) + } +``` +But they can overlap in several ways: ```idris +Ex2a , +Ex2b , +Ex2c : Overlap [1,2,3] [2,3,2] +Ex2a = Overlapping + { common = 3 + , lhsPos = There (There Here) + , rhsPos = There Here + } +Ex2b = Overlapping + { common = 2 + , lhsPos = There Here + , rhsPos = Here + } +Ex2c = Overlapping + { common = 2 + , lhsPos = There Here + , rhsPos = There (There Here) + } +``` +We can think of a relation `rel : Rel ty` as the type of edges in a directed +graph between vertices in `ty`: + +* edges have a direction: the type `rel x y` is different to `rel y x` + +* multiple different edges between the same vertices `e1, e2 : rel x y` +* self-loops between the same vertex are allowed `loop : rel x x`. + +An _equivalence relation_ is a relation that's: + +* _reflexive_: we guarantee a specific way in which every element is related to + itself; + +* _symmetric_: we can reverse an edge between two edges; and + +* _transitive_: we can compose paths of related elements into a single edge. + +```idris +record Equivalence (A : Type) where + constructor MkEquivalence + 0 relation: Rel A + reflexive : (x : A) -> relation x x + symmetric : (x, y : A) -> relation x y -> relation y x + transitive: (x, y, z : A) -> relation x y -> relation y z + -> relation x z +``` +```idris hide +%hide Tutorial.Equivalence +``` +We equip the built-in relation `Equal` with the structure of an equivalence +relation, using the constructor `Refl` and the stdlib functions `sym`, and +`trans`: +```idris +EqualityEquivalence : Equivalence a +EqualityEquivalence = MkEquivalence + { relation = (===) + , reflexive = \x => Refl + , symmetric = \x,y,x_eq_y => sym x_eq_y + , transitive = \x,y,z,x_eq_y,y_eq_z => trans x_eq_y y_eq_z + } +``` + +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: +```idris +infix 8 .-. + +record INT where + constructor (.-.) + pos, neg : Nat + +record SameDiff (x, y : INT) where + constructor Check + same : (x.pos + y.neg === y.pos + x.neg) +``` +The `SameDiff x y` relation is equivalent to mathematical equation that states +that the difference between the positive and negative parts is identical: +$$x_{pos} - x_{neg} = y_{pos} - y_{neg}$$ +But, unlike the last equation which requires us to define integers and +subtraction, its equivalent `(.same)` is expressed using only addition, and +so addition on `Nat` is enough. + +The relation `SameDiff` is an equivalence relation. The proofs are +straightforward, and a good opportunity to practice Idris's equational +reasoning combinators from `Syntax.PreorderReasoning`: +```idris +SameDiffEquivalence : Equivalence INT +SameDiffEquivalence = MkEquivalence + { relation = SameDiff + , reflexive = \x => Check $ Calc $ + |~ x.pos + x.neg + ~~ x.pos + x.neg ...(Refl) +``` +This equational proof represents the single-step equational proof: + +"Calculate: + +1. $x_{pos} + x_{neg}$ +2. $= x_{pos} + x_{neg}$ (by reflexivity)" + +The mnemonic behind the ASCII-art is that the first step in the proof +starts with a logical-judgement symbol $\vdash$, each step continues with an +equality sign $=$, and justified by a thought bubble `(...)`. + +```idris + , symmetric = \x,y,x_eq_y => Check $ Calc $ + |~ 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. +```idris + , transitive = \x,y,z,x_eq_y,y_eq_z => Check $ plusRightCancel _ _ y.pos + $ Calc $ + |~ x.pos + z.neg + y.pos + ~~ x.pos + (y.pos + z.neg) ...(solve 3 Monoid.Commutative.Free.Free + {a = Nat.Additive} $ + (X 0 .+. X 1) .+. X 2 + =-= X 0 .+. (X 2 .+. X 1)) + ~~ x.pos + (z.pos + y.neg) ...(cong (x.pos +) $ y_eq_z.same) + ~~ (x.pos + y.neg) + z.pos ...(solve 3 Monoid.Commutative.Free.Free + {a = Nat.Additive} $ + 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 \Rightarrow a = b$ +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. + + +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: +```idris +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: +```idris +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: +```idris +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 +on the first element of either, which exhausts all possibilities of overlap. -- cgit v1.2.3