From 63e894b39a82e5a8b1edd06f1e03e6bfc5aa8c81 Mon Sep 17 00:00:00 2001 From: Ohad Kammar Date: Mon, 8 Aug 2022 17:29:03 +0100 Subject: Snapshot, will continue later --- doc/Tutorial.html | 15 +++---- doc/Tutorial.md | 103 +++++++++++++++++++++++++++++++++++++++--------- doc/setoid-doc.ipkg | 1 + doc/sources/Tutorial.md | 67 +++++++++++++++++++++++++++++++ 4 files changed, 161 insertions(+), 25 deletions(-) (limited to 'doc') diff --git a/doc/Tutorial.html b/doc/Tutorial.html index e10bee7..23a7183 100644 --- a/doc/Tutorial.html +++ b/doc/Tutorial.html @@ -66,14 +66,14 @@

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:

+

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. +
  3.  = xpos + xneg (by reflexivity)"

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:

+

  , 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
@@ -83,8 +83,9 @@

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:

+

-- TODO: clean this up
(.+.) : (x, y : INT) -> INT
x .+. y = (x.pos + y.pos) .-. (x.neg + y.neg)

(.*.) : (x, y : INT) -> INT
x .*. y = (x.pos * y.pos + x.neg * y.neg) .-. (x.pos * y.neg + x.neg * y.pos)

O, I : INT
O = 0 .-. 0
I = 1 .-. 0
plusIntZeroLftNeutral : (x : INT) -> O .+. x SameDiff x
plusIntZeroLftNeutral x = Check Refl

plusIntZeroRgtNeutral : (x : INT) -> x .+. O SameDiff</span><span class="IdrisKeyword"> x
plusIntZeroRgtNeutral x = Check (solve 2 Monoid.Commutative.Free.Free
                                     {a = Nat.Additive} $</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;(X&nbsp;0&nbsp;.+.&nbsp;O1)&nbsp;.+.&nbsp;X&nbsp;1<br /> <span class="IdrisFunction">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;</span>&nbsp;<span class="IdrisKeyword">&nbsp;</span>&nbsp;<span class="IdrisKeyword">&nbsp;</span><span class="IdrisBound">&nbsp;</span><span class="IdrisKeyword">&nbsp;</span><span class="IdrisBound">&nbsp;</span><span class="IdrisKeyword">&nbsp;</span><span class="IdrisBound">&nbsp;</span>&nbsp;<span class="IdrisKeyword">&nbsp;</span>&nbsp;<span class="IdrisType">&nbsp;&nbsp;&nbsp;</span><span class="IdrisKeyword">=</span>-<span class="IdrisKeyword">=&nbsp;</span>X<span class="IdrisBound">&nbsp;</span>0<span class="IdrisFunction">&nbsp;.+</span>.<span class="IdrisKeyword">&nbsp;</span><span class="IdrisBound">(</span>X<span class="IdrisFunction">&nbsp;1&nbsp;</span>.<span class="IdrisBound">+</span><span class="IdrisKeyword">.</span>&nbsp;<span class="IdrisType">O1))</span><br /> <br /> plusInrAssociative&nbsp;:&nbsp;(x,y,z&nbsp;:&nbsp;INT)&nbsp;-&gt;<span class="IdrisKeyword">&nbsp;</span><span class="IdrisBound">x</span>&nbsp;<span class="IdrisKeyword">.</span>+<span class="IdrisFunction">.&nbsp;(y&nbsp;.+.&nbsp;z)&nbsp;</span><span class="IdrisKeyword">`</span>SameDiff`&nbsp;(x&nbsp;.+.&nbsp;y)&nbsp;.+.&nbsp;z<br /> plusInrAssociative&nbsp;x&nbsp;y&nbsp;z&nbsp;=&nbsp;Check&nbsp;$ (solve 6 Monoid.Commutative.Free.Free
                                     {a = Nat.Additive} $
                                  (X 0 .+. (X 1 .+. X 2)) .+. ((X 3 .+. X 4) .+. X 5)
                                  =-= (X 0 .+. X 1 .+. X 2) .+. (X 3 .+. (X 4 .+. X 5)))

data INT‘ : Type where
  IPos  : Nat -> INT’
  INegS : Nat -> INT'

Cast INT‘ Integer where
  cast (IPos k) = cast k
  cast (INegS k) = - cast (S k)

Cast INT' INT where
  cast (IPos k) = k .-. 0
  cast (INegS k) = 0 .-. (S k)

normalise : INT -> INT
normalise i@(0 .-. neg      ) = i
normalise i@((S k) .-. 0    ) = i
normalise i@((S k) .-. (S j)) = normalise (k .-. j)

normaliseEitherZero : (x : INT) -> Either ((normalise x).pos = Z) ((normalise x).neg = Z)
normaliseEitherZero i@(0 .-. neg      ) = Left Refl
normaliseEitherZero i@((S k) .-. 0    ) = Right Refl
normaliseEitherZero i@((S k) .-. (S j)) = normaliseEitherZero (k .-. j)

Cast INT INT' where
  cast x = let (pos .-. neg) = normalise x in
    case normaliseEitherZero x of
      (Left y) => case neg of
        0 => IPos 0
        (S k) => INegS k
      (Right y) => IPos pos

– stuff you can show:

-- x <span class="IdrisBound">S</span>a<span class="IdrisKeyword">m</span>e<span class="IdrisFunction">Diff</span> y -> normalise x = normalise y
(:*:), (:+:) : (x,y : INT') -> INT’
x :+: y = cast (cast x .+. cast y)
x :*: y = cast (cast x .*. cast y)

diff --git a/doc/Tutorial.md b/doc/Tutorial.md index b9a5896..439d245 100644 --- a/doc/Tutorial.md +++ b/doc/Tutorial.md @@ -241,34 +241,101 @@ 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 on the first element of either, which exhausts all possibilities of overlap. + + + +-- TODO: clean this up
+(.+.) : (x, y : INT) -> INT
+x .+. y = (x.pos + y.pos) .-. (x.neg + y.neg)
+
+(.\*.) : (x, y : INT) -> INT
+x .\*. y = (x.pos \* y.pos + x.neg \* y.neg) .-. (x.pos \* y.neg + x.neg \* y.pos)
+
+O, I : INT
+O = 0 .-. 0
+I = 1 .-. 0
+plusIntZeroLftNeutral : (x : INT) -> O .+. x `SameDiff` x
+plusIntZeroLftNeutral x = Check Refl
+
+plusIntZeroRgtNeutral : (x : INT) -> x .+. O `SameDiff` x
+plusIntZeroRgtNeutral x = Check (solve 2 Monoid.Commutative.Free.Free
+                                     {a = Nat.Additive} $
+                                     (X 0 .+. O1) .+. X 1
+                                 =-= X 0 .+. (X 1 .+. O1))
+
+plusInrAssociative : (x,y,z : INT) -> x .+. (y .+. z) `SameDiff` (x .+. y) .+. z
+plusInrAssociative x y z = Check $ (solve 6 Monoid.Commutative.Free.Free
+                                     {a = Nat.Additive} $
+                                  (X 0 .+. (X 1 .+. X 2)) .+. ((X 3 .+. X 4) .+. X 5)
+                                  =-= (X 0 .+. X 1 .+. X 2) .+. (X 3 .+. (X 4 .+. X 5)))
+
+data INT' : Type where
+  IPos  : Nat -> INT'
+  INegS : Nat -> INT'
+
+Cast INT' Integer where
+  cast (IPos k) = cast k
+  cast (INegS k) = - cast (S k)
+
+Cast INT' INT where
+  cast (IPos k) = k .-. 0
+  cast (INegS k) = 0 .-. (S k)
+
+normalise : INT -> INT
+normalise i@(0 .-. neg      ) = i
+normalise i@((S k) .-. 0    ) = i
+normalise i@((S k) .-. (S j)) = normalise (k .-. j)
+
+normaliseEitherZero : (x : INT) -> Either ((normalise x).pos = Z) ((normalise x).neg = Z)
+normaliseEitherZero i@(0 .-. neg      ) = Left Refl
+normaliseEitherZero i@((S k) .-. 0    ) = Right Refl
+normaliseEitherZero i@((S k) .-. (S j)) = normaliseEitherZero (k .-. j)
+
+Cast INT INT' where
+  cast x = let (pos .-. neg) = normalise x in
+    case normaliseEitherZero x of
+      (Left y) => case neg of
+        0 => IPos 0
+        (S k) => INegS k
+      (Right y) => IPos pos
+
+-- stuff you can show:
+
+-- x `SameDiff` y -> normalise x = normalise y
+(:\*:), (:+:) : (x,y : INT') -> INT'
+x :+: y = cast (cast x .+. cast y)
+x :\*: y = cast (cast x .\*. cast y)
+
+ + diff --git a/doc/setoid-doc.ipkg b/doc/setoid-doc.ipkg index b97fb59..9bce2e7 100644 --- a/doc/setoid-doc.ipkg +++ b/doc/setoid-doc.ipkg @@ -19,6 +19,7 @@ depends , frex modules = Tutorial + , Minh -- name of executable sourcedir = "sources" diff --git a/doc/sources/Tutorial.md b/doc/sources/Tutorial.md index a33652f..68dda37 100644 --- a/doc/sources/Tutorial.md +++ b/doc/sources/Tutorial.md @@ -251,3 +251,70 @@ Ex4 = ``` 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. + + + +```idris +-- TODO: clean this up +(.+.) : (x, y : INT) -> INT +x .+. y = (x.pos + y.pos) .-. (x.neg + y.neg) + +(.*.) : (x, y : INT) -> INT +x .*. y = (x.pos * y.pos + x.neg * y.neg) .-. (x.pos * y.neg + x.neg * y.pos) + +O, I : INT +O = 0 .-. 0 +I = 1 .-. 0 +plusIntZeroLftNeutral : (x : INT) -> O .+. x `SameDiff` x +plusIntZeroLftNeutral x = Check Refl + +plusIntZeroRgtNeutral : (x : INT) -> x .+. O `SameDiff` x +plusIntZeroRgtNeutral x = Check (solve 2 Monoid.Commutative.Free.Free + {a = Nat.Additive} $ + (X 0 .+. O1) .+. X 1 + =-= X 0 .+. (X 1 .+. O1)) + +plusInrAssociative : (x,y,z : INT) -> x .+. (y .+. z) `SameDiff` (x .+. y) .+. z +plusInrAssociative x y z = Check $ (solve 6 Monoid.Commutative.Free.Free + {a = Nat.Additive} $ + (X 0 .+. (X 1 .+. X 2)) .+. ((X 3 .+. X 4) .+. X 5) + =-= (X 0 .+. X 1 .+. X 2) .+. (X 3 .+. (X 4 .+. X 5))) + +data INT' : Type where + IPos : Nat -> INT' + INegS : Nat -> INT' + +Cast INT' Integer where + cast (IPos k) = cast k + cast (INegS k) = - cast (S k) + +Cast INT' INT where + cast (IPos k) = k .-. 0 + cast (INegS k) = 0 .-. (S k) + +normalise : INT -> INT +normalise i@(0 .-. neg ) = i +normalise i@((S k) .-. 0 ) = i +normalise i@((S k) .-. (S j)) = normalise (k .-. j) + +normaliseEitherZero : (x : INT) -> Either ((normalise x).pos = Z) ((normalise x).neg = Z) +normaliseEitherZero i@(0 .-. neg ) = Left Refl +normaliseEitherZero i@((S k) .-. 0 ) = Right Refl +normaliseEitherZero i@((S k) .-. (S j)) = normaliseEitherZero (k .-. j) + +Cast INT INT' where + cast x = let (pos .-. neg) = normalise x in + case normaliseEitherZero x of + (Left y) => case neg of + 0 => IPos 0 + (S k) => INegS k + (Right y) => IPos pos + +-- stuff you can show: + +-- x `SameDiff` y -> normalise x = normalise y +(:*:), (:+:) : (x,y : INT') -> INT' +x :+: y = cast (cast x .+. cast y) +x :*: y = cast (cast x .*. cast y) + +``` -- cgit v1.2.3