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.md | 103 ++++++++++++++++++++++++++++++++++++++++++++++---------- 1 file changed, 85 insertions(+), 18 deletions(-) (limited to 'doc/Tutorial.md') 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)
+
+ + -- cgit v1.2.3