Integers that play nice with typechecking

frex.ipkg

@@ -62,6 +62,8 @@ modules = Frex
         , Frexlet.Monoid.Involutive.Involution
         , Frexlet.Monoid.Involutive.Frex
         , Frexlet.Monoid.Involutive.List
+        , Frexlet.Group
+        , Frexlet.Group.Theory
         -- Should move to contrib
         , Data.Either.Extra
         , Data.Finite
@@ -78,6 +80,12 @@ modules = Frex
         , Data.Setoid.Vect.Functional
         , Data.Setoid.Vect.Inductive
         , Data.Setoid.List
+        , Data.Integer.Quotient
+        , Data.Integer.Quotient.Definition
+        , Data.Integer.Quotient.Operations
+        , Data.Integer.Inductive
+        , Data.Integer.Inductive.Definition
+        , Data.Integer.Connections
         , Data.Unit
         , Data.Vect.Extra1
         , Syntax.PreorderReasoning.Setoid

src/Data/Integer/Connections.idr

@@ -0,0 +1,72 @@
+module Data.Integer.Connections
+
+import Frex
+import Frexlet.Monoid.Commutative
+
+import Data.Integer.Quotient
+import Data.Integer.Inductive.Definition
+
+import Syntax.PreorderReasoning
+
+public export
+normalise : INT -> INTEGER
+normalise x = x.pos `minus` x.neg
+
+public export
+quotient : INTEGER -> INT
+quotient (ANat m) = MkINT {pos = m, neg = 0}
+quotient (NegS m) = MkINT {pos = 0, neg = S m}
+
+public export
+auxBack : (m,n : Nat) -> (IntegerSetoid).equivalence.relation
+  (quotient (m `minus` n))
+  (MkINT m n)
+auxBack  m     0    = (IntegerSetoid).equivalence.reflexive $ MkINT m 0
+auxBack  0    (S m) = (IntegerSetoid).equivalence.reflexive $ MkINT 0 (S m)
+auxBack (S n) (S m) =
+  let q : INT
+      q = quotient (minus n m)
+      IH : q.pos + m === n + q.neg
+         := auxBack n m
+  in Calc $
+  |~ q.pos + (1 + m)
+  ~~ 1 + (q.pos + m) ...(solve 2 (Frex Nat.Additive) $
+                         Dyn 0 .+. (Sta 1 .+. Dyn 1)
+                         =-=
+                         Sta 1 .+. (Dyn 0 .+. Dyn 1))
+  ~~ 1 + (n + q.neg) ...(cong S IH)
+
+public export
+back : (x : INT) -> (IntegerSetoid).equivalence.relation
+   (quotient (normalise x))
+   x
+back x = auxBack x.pos x.neg
+
+public export
+from : (a : INTEGER) ->
+   (normalise (quotient a)) === a
+from (ANat k) = Refl
+from (NegS k) = Refl
+
+public export
+normaliseHom : SetoidHomomorphism IntegerSetoid (cast INTEGER) Connections.normalise
+normaliseHom x y prf = Calc $
+  |~ (x.pos `minus` x.neg)
+  ~~ ((x.pos + y.neg) `minus` (x.neg + y.neg)) ...(sym $ minusCancelRight _ _ _)
+  ~~ ((y.pos + x.neg) `minus` (y.neg + x.neg)) ...(cong2 minus prf (plusCommutative _ _))
+  ~~ (y.pos `minus` y.neg) ...(minusCancelRight _ _ _)
+
+public export
+representationInteger : IntegerSetoid <~> cast INTEGER
+representationInteger = MkIsomorphism
+  { Fwd = MkSetoidHomomorphism
+          { H = normalise
+          , homomorphic = normaliseHom
+          }
+  , Bwd = mate $ quotient
+  , Iso = IsIsomorphism
+    { BwdFwdId = back
+    , FwdBwdId = from
+    }
+  }
+

src/Data/Integer/Inductive.idr

@@ -0,0 +1,55 @@
+module Data.Integer.Inductive
+
+import public Data.Integer.Inductive.Definition
+
+import Data.Setoid
+import Syntax.PreorderReasoning
+
+import Syntax.WithProof
+import Data.Primitives.Views
+
+import Frex
+import Frexlet.Monoid.Commutative
+import Frexlet.Group
+
+import Data.Integer.Quotient
+import Data.Integer.Connections
+
+-- Let's validate the monoid axioms!
+
+%default total
+namespace Monoid
+  public export
+  Additive : Monoid
+  Additive = transportSetoid Quotient.Operations.Monoid.Additive representationInteger
+
+public export
+plus : (m,n : INTEGER) -> INTEGER
+plus m n = (Inductive.Monoid.Additive).Sem Prod [m,n]
+
+public export
+mult : (m,n : INTEGER) -> INTEGER
+-- TODO: implement. Much easier once we have semiring frexlet.
+
+namespace Group
+  public export
+  Additive : Group
+  Additive = transportSetoid Quotient.Operations.Group.Additive representationInteger
+
+public export
+Num INTEGER where
+  fromInteger x = case compare x 0 of
+    LT => NegS (fromInteger $ negate (1 + x))
+    _  => ANat (fromInteger x)
+  (+) = plus
+  (*) = mult
+
+public export
+Neg INTEGER where
+  negate = Algebra.curry $ (Inductive.Group.Additive).Algebra.algebra.Semantics Invert
+  m - n = m + negate n
+
+public export
+Show INTEGER where
+  show (ANat m) = show m
+  show (NegS n) = "-\{show (S n)}"

src/Data/Integer/Inductive/Definition.idr

@@ -0,0 +1,41 @@
+module Data.Integer.Inductive.Definition
+
+import Data.Setoid
+import Syntax.PreorderReasoning
+
+import Syntax.WithProof
+import Data.Primitives.Views
+
+import Frex
+import Frexlet.Monoid.Commutative
+
+%default total
+
+-- TODO: multiplication. Much easier once we have semiring frexlet.
+
+public export
+data INTEGER : Type where
+  ||| ANat n : the integer n
+  ANat : Nat -> INTEGER
+  ||| NegS n : the integer -(S n)
+  NegS : Nat -> INTEGER
+
+public export
+minus : (m, n : Nat) -> INTEGER
+minus    m   0    = ANat m
+minus  0    (S n) = NegS n
+minus (S m) (S n) = minus m n
+
+public export
+minusCancelLeft : (left,mid,right : Nat) ->
+  (left + mid) `Definition.minus` (left + right) = mid `minus` right
+minusCancelLeft 0       mid rgt  = Refl
+minusCancelLeft (S lft) mid rgt  = minusCancelLeft lft mid rgt
+
+public export
+minusCancelRight : (left,mid,right : Nat) -> (left + right) `Definition.minus` (mid + right) = left `minus` mid
+minusCancelRight a b c = Calc $
+  |~ ((a + c) `minus` (b + c))
+  ~~ ((c + a) `minus` (c + b)) ...(cong2 minus (plusCommutative _ _) (plusCommutative _ _))
+  ~~ (a `minus` b)             ...(minusCancelLeft _ _ _)
+

src/Data/Integer/Quotient.idr

@@ -0,0 +1,25 @@
+||| Representation of the integers using the INT-construction on Nat,
+||| and quotients. Hopefully it'll be easier to prove its properties
+module Data.Integer.Quotient
+
+import public Data.Integer.Quotient.Definition
+import public Data.Integer.Quotient.Operations
+
+import Frex
+import Frexlet.Monoid.Commutative
+import Frexlet.Monoid.Commutative.Nat
+
+import Frexlet.Group
+
+import Frexlet.Monoid.Notation
+
+import Data.Primitives.Views
+import Data.Setoid
+import Syntax.PreorderReasoning
+
+import Syntax.WithProof
+-- Let's validate the monoid axioms!
+
+%default total
+
+-- TODO: multiplication. Much easier once we have semiring frexlet.

src/Data/Integer/Quotient/Definition.idr

@@ -0,0 +1,52 @@
+module Data.Integer.Quotient.Definition
+
+import Data.Setoid
+import Syntax.PreorderReasoning
+
+import Frex
+import Frexlet.Monoid.Commutative.Nat
+import Frexlet.Monoid.Commutative
+import Frexlet.Monoid.Notation.Additive
+
+import Data.Nat
+
+-- import Frex.Magic
+-- %language ElabReflection
+%default total
+
+public export
+record INT where
+  constructor MkINT
+  pos,neg : Nat
+
+public export
+INTEq : (x,y : INT) -> Type
+INTEq x y = x.pos + y.neg === y.pos + x.neg
+
+public export
+IntegerSetoid : Setoid
+IntegerSetoid = MkSetoid
+  { U = INT
+  , equivalence  = MkEquivalence
+    { relation   = INTEq
+    , reflexive  = \x => Refl
+    , symmetric  = \x,y,prf => sym prf
+    , transitive = \x,y,z,x_eq_y,y_eq_z =>
+      plusRightCancel _ _ y.pos $
+      Calc $
+      |~ (x.pos + z.neg) + y.pos
+      ~~  x.pos +(y.pos + z.neg) ...(solve 3 {a = Additive} (Commutative.Free.Free) $
+                                    (X 0 .+. X 2) .+. X 1 =-=
+                                    X 0 .+. (X 1 .+. X 2))
+                                -- ^ Getting weird errors with this alternative:
+                                -- (%runElab frexMagic Frex Additive)
+      ~~  x.pos +(z.pos + y.neg) ...(cong (x.pos +) y_eq_z)
+      ~~  z.pos +(x.pos + y.neg) ...(solve 3 {a = Additive} (Commutative.Free.Free) $
+                                    X 0 .+. (X 2 .+. X 1) =-=
+                                    X 2 .+. (X 0 .+. X 1))
+      ~~  z.pos +(y.pos + x.neg) ...(cong (z.pos +) x_eq_y)
+      ~~ (z.pos + x.neg) + y.pos ...(solve 3 {a = Additive} (Commutative.Free.Free) $
+                                    X 2 .+. (X 1 .+. X 0) =-=
+                                    (X 2 .+. X 0).+. X 1)
+    }
+  }