[ overhaul, new ] New algebraic tower plus utilities

docs/docs.ipkg

@@ -1,8 +1,7 @@
 package prim-docs
 version    = 0.0.1
 authors    = "Stefan Höck"
-depends    = base      >= 0.5.1
-           , prim
+depends    = prim
 
 modules    = Documentation
 

prim.ipkg

@@ -9,27 +9,18 @@ license    = "BSD-3 Clause"
 sourcedir  = "src"
 depends    = base    >= 0.5.1
 
-modules = Algebra.Semigroup
-        , Algebra.Semiring
-        , Algebra.Monoid
+modules = Algebra.Monoid
+        , Algebra.OrderedSemiring
         , Algebra.Ring
+        , Algebra.Semiring
 
         , Algebra.Solver.CommutativeMonoid
         , Algebra.Solver.Monoid
         , Algebra.Solver.Prod
         , Algebra.Solver.Ring
-        , Algebra.Solver.Ring.Expr
-        , Algebra.Solver.Ring.Prod
-        , Algebra.Solver.Ring.SolvableRing
-        , Algebra.Solver.Ring.Sum
-        , Algebra.Solver.Ring.Util
         , Algebra.Solver.Semigroup
         , Algebra.Solver.Semiring
-        , Algebra.Solver.Semiring.Expr
-        , Algebra.Solver.Semiring.Prod
-        , Algebra.Solver.Semiring.SolvableSemiring
-        , Algebra.Solver.Semiring.Sum
-        , Algebra.Solver.Semiring.Util
+        , Algebra.Solver.Sum
 
         , Data.Maybe.NothingMin
         , Data.Maybe.NothingMax
@@ -49,3 +40,5 @@ modules = Algebra.Semigroup
         , Data.Prim.Ord
         , Data.Prim.String
         , Data.Trichotomy
+
+        , Syntax.Total

src/Algebra/EuclidianRing.idr

@@ -0,0 +1,101 @@
+module Algebra.EuclidianRing
+
+import Data.Nat
+import public Algebra.Ring
+import public Syntax.PreorderReasoning
+
+%default total
+
+public export
+interface Neg a => Integral a => ERing a where
+
+public export %inline
+rngNeg : ERing a -> Neg a
+rngNeg _ = %search
+
+public export
+interface EuclidianRing a (0 rng : ERing a) | a where
+  constructor MkEuclidianRing
+  norm : a -> Nat
+
+  0 err : Ring a (rngNeg rng)
+
+  0 divMod :
+       {n,d : a}
+    -> Not (d === 0)
+    -> d * div n d + mod n d === n
+
+  0 modNegEQ :
+       {n,d : a}
+    -> Not (d === 0)
+    -> mod n d === mod n (negate d)
+
+  0 zeroNotOne : Not (the a 0 === the a 1)
+
+  0 modLT :
+       {n,d : a}
+    -> Not (d === 0)
+    -> norm (mod n d) `LT` norm d
+
+public export %inline %hint
+0 ERR : EuclidianRing a rng => Ring a (rngNeg rng)
+ERR = err
+
+public export %inline %hint
+0 ERSR : EuclidianRing a rng => Semiring a (negNum $ rngNeg rng)
+ERSR = RSR @{ERR}
+
+--------------------------------------------------------------------------------
+--          Division Lemmata
+--------------------------------------------------------------------------------
+
+export
+0 oneNotZero :
+     {rng : _}
+  -> EuclidianRing a rng
+  => Not (the a 1 === the a 0)
+oneNotZero p = zeroNotOne $ sym p
+
+||| Is this an axiom or a lemma
+export
+0 divLeft :
+     {rng : _}
+  -> EuclidianRing a rng
+  => {n,d : a}
+  -> Not (d === 0)
+  -> div (d * n) d === n
+
+export
+0 divRight :
+     {rng : _}
+  -> EuclidianRing a rng
+  => {n,d : a}
+  -> Not (d === 0)
+  -> div (n * d) d === n
+divRight p = Calc $
+  |~ div (n * d) d
+  ~~ div (d * n) d ... cong (`div` d) (multCommutative @{ERSR})
+  ~~ n             ... divLeft p
+
+export
+0 divZero :
+     {rng : _}
+  -> EuclidianRing a rng
+  => {n,d : a}
+  -> Not (d === 0)
+  -> div 0 d === 0
+divZero p = Calc $
+  |~ div 0 d
+  ~~ div (d * 0) d ..< cong (`div` d) (multZeroRightAbsorbs @{ERSR})
+  ~~ 0             ... divLeft p
+
+export
+0 divByOneNeutral :
+     {rng : _}
+  -> EuclidianRing a rng
+  => {n : a}
+  -> div n 1 === n
+divByOneNeutral = Calc $
+  |~ div n 1
+  ~~ div (1 * n) 1 ..< cong (`div` 1) (multOneLeftNeutral @{ERSR})
+  ~~ n             ... divLeft oneNotZero

src/Algebra/Monoid.idr

@@ -1,38 +1,198 @@
 module Algebra.Monoid
 
+
 import Data.List
+import Data.List1
+import Data.List1.Properties
+import Syntax.PreorderReasoning
 
 %default total
 
+||| This interface is a witness that for a
+||| type `a` the axioms of a semigroup hold: `(<+>)` is associative.
+|||
+||| Note: If the type is actually a monoid, use `Data.Algebra.MonoidV` instead.
+public export
+interface SemigroupV a (0 sem : Semigroup a) | a where
+  constructor MkSemigroupV
+  0 appendAssociative : {x,y,z : a} -> x <+> (y <+> z) === (x <+> y) <+> z
+
+--------------------------------------------------------------------------------
+--          Implementations
+--------------------------------------------------------------------------------
+
+export %inline
+SemigroupV (List1 a) %search where
+  appendAssociative = Properties.appendAssociative _ _ _
+
+--------------------------------------------------------------------------------
+--          Monoid
+--------------------------------------------------------------------------------
+
+public export
+monSem : Monoid a -> Semigroup a
+monSem _ = %search
+
 ||| This interface is a witness that for a
 ||| type `a` the axioms of a monoid hold: `(<+>)` is associative
 ||| with `neutral` being the neutral element.
 public export
-interface Monoid a => LMonoid a where
-  0 appendAssociative : {x,y,z : a} -> x <+> (y <+> z) === (x <+> y) <+> z
+interface MonoidV a (0 mon : Monoid a) | a where
+  constructor MkMonoidV
+  0 m_sem : SemigroupV a (monSem mon)
 
   0 appendLeftNeutral : {x : a} -> Prelude.neutral <+> x === x
 
   0 appendRightNeutral : {x : a} -> x <+> Prelude.neutral === x
 
+----------------------------------------------------------------------------------
+----          Derived Implementations
+----------------------------------------------------------------------------------
+
+export %hint
+0 MonSem : MonoidV a mon => SemigroupV a (monSem mon)
+MonSem = m_sem
+
+----------------------------------------------------------------------------------
+----          Implementations
+----------------------------------------------------------------------------------
+
 export
-LMonoid (List a) where
-  appendAssociative = Data.List.appendAssociative _ _ _
-  appendRightNeutral = appendNilRightNeutral _
-  appendLeftNeutral = Refl
+MonoidV (List a) %search where
+  m_sem = MkSemigroupV (Data.List.appendAssociative _ _ _)
+  appendRightNeutral  = appendNilRightNeutral _
+  appendLeftNeutral   = Refl
 
 unsafeRefl : a === b
 unsafeRefl = believe_me (Refl {x = a})
 
 export
-LMonoid String where
-  appendAssociative = unsafeRefl
-  appendRightNeutral = unsafeRefl
-  appendLeftNeutral = unsafeRefl
+MonoidV String %search where
+  m_sem = MkSemigroupV unsafeRefl
+  appendRightNeutral  = unsafeRefl
+  appendLeftNeutral   = unsafeRefl
+
+----------------------------------------------------------------------------------
+----          CommutativeSemigroup
+----------------------------------------------------------------------------------
 
 ||| This interface is a witness that for a
-||| type `a` the axioms of a commutative monoid hold:
+||| type `a` the axioms of a commutative semigroup hold:
 ||| `(<+>)` is commutative.
 public export
-interface LMonoid a => CommutativeMonoid a where
+interface CommutativeSemigroup a (0 sem : Semigroup a) | a where
+  constructor MkCSemigroup
+  0 cs_sem : SemigroupV a sem
   0 appendCommutative : {x,y : a} -> x <+> y === y <+> x
+
+----------------------------------------------------------------------------------
+----          Derived Implementation
+----------------------------------------------------------------------------------
+
+export %hint
+0 CSemSem : CommutativeSemigroup a sem => SemigroupV a sem
+CSemSem = cs_sem
+
+----------------------------------------------------------------------------------
+----          Commutative Monoid
+----------------------------------------------------------------------------------
+
+||| This interface is a witness that for a
+||| type `a` the axioms of a commutative monoid hold:
+||| `(<+>)` is commutative.
+public export
+interface CommutativeMonoid a (0 mon : Monoid a) | a where
+  constructor MkCMonoid
+  0 cm_sem : CommutativeSemigroup a (monSem mon)
+
+  0 cm_mon : MonoidV a mon
+
+----------------------------------------------------------------------------------
+----          Derived Implementations
+----------------------------------------------------------------------------------
+
+export %hint
+0 CMonMon : CommutativeMonoid a mon => MonoidV a mon
+CMonMon = cm_mon
+
+export %hint
+0 CMonCSem : CommutativeMonoid a mon => CommutativeSemigroup a (monSem mon)
+CMonCSem = cm_sem
+
+export
+0 CMonSem : CommutativeMonoid a mon => SemigroupV a (monSem mon)
+CMonSem = CSemSem @{CMonCSem}
+
+--------------------------------------------------------------------------------
+--          Utilities
+--------------------------------------------------------------------------------
+
+||| A utility proof that is used several times internally
+export
+0 lemma1324 :
+     {sem : _}
+  -> CommutativeSemigroup a sem
+  => {k,l,m,n : a}
+  -> (k <+> l) <+> (m <+> n) === (k <+> m) <+> (l <+> n)
+lemma1324 = Calc $
+  |~ (k <+> l) <+> (m <+> n)
+  ~~ ((k <+> l) <+> m) <+> n ... appendAssociative
+  ~~ (k <+> (l <+> m)) <+> n ..< cong (<+>n) appendAssociative
+  ~~ (k <+> (m <+> l)) <+> n ... cong (\x => (k <+> x) <+> n) appendCommutative
+  ~~ ((k <+> m) <+> l) <+> n ... cong (<+>n) appendAssociative
+  ~~ (k <+> m) <+> (l <+> n) ..< appendAssociative
+
+||| A utility proof that is used several times internally
+export
+0 lemma213 :
+     {sem : _}
+  -> CommutativeSemigroup a sem
+  => {k,m,n : a}
+  -> k <+> (m <+> n) === m <+> (k <+> n)
+lemma213 = Calc $
+  |~ k <+> (m <+> n)
+  ~~ (k <+> m) <+> n   ... appendAssociative
+  ~~ (m <+> k) <+> n   ... cong (<+> n) appendCommutative
+  ~~ m <+> (k <+> n)   ..< appendAssociative
+
+--------------------------------------------------------------------------------
+--          Tests
+--------------------------------------------------------------------------------
+
+0 monToSem :
+     {mon : _}
+  -> MonoidV a mon
+  => {x,y,z : a}
+  -> x <+> (y <+> z) === (x <+> y) <+> z
+monToSem = appendAssociative
+
+0 testListToSem : {x,y,z : List a} -> x <+> (y <+> z) === (x <+> y) <+> z
+testListToSem = appendAssociative
+
+0 csemToSem :
+     {sem : _}
+  -> CommutativeSemigroup a sem
+  => {x,y,z : a}
+  -> x <+> (y <+> z) === (x <+> y) <+> z
+csemToSem = appendAssociative
+
+0 cmonToSem :
+     {mon : _}
+  -> CommutativeMonoid a mon
+  => {x,y,z : a}
+  -> x <+> (y <+> z) === (x <+> y) <+> z
+cmonToSem = appendAssociative
+
+0 cmonToMon :
+     {mon : _}
+  -> CommutativeMonoid a mon
+  => {x,y,z : a}
+  -> x <+> Prelude.neutral === x
+cmonToMon = appendRightNeutral
+
+0 cmonToCSem :
+     {mon : _}
+  -> CommutativeMonoid a mon
+  => {x,y,z : a}
+  -> x <+> y === y <+> x
+cmonToCSem = appendCommutative