Merge pull request #4831 from nickdrozd/algebra

More algebra proofs

libs/contrib/Control/Algebra/Laws.idr

@@ -1,24 +1,83 @@
 module Control.Algebra.Laws
 
 import Prelude.Algebra as A
-import Control.Algebra
+import Control.Algebra as Alg
 import Interfaces.Verified
 
 %access export
 
+-- Monoids
+
+||| Inverses are unique.
+uniqueInverse : VerifiedMonoid t => (x, y, z : t) ->
+  y <+> x = A.neutral -> x <+> z = A.neutral -> y = z
+uniqueInverse x y z p q =
+  rewrite sym $ monoidNeutralIsNeutralL y in
+    rewrite sym q in
+      rewrite semigroupOpIsAssociative y x z in
+  rewrite p in
+    rewrite monoidNeutralIsNeutralR z in
+      Refl
+
+-- Groups
+
+||| Only identity is self-squaring.
+selfSquareId : VerifiedGroup t => (x : t) ->
+  x <+> x = x -> x = A.neutral
+selfSquareId x p =
+  rewrite sym $ monoidNeutralIsNeutralR x in
+    rewrite sym $ groupInverseIsInverseR x in
+  rewrite sym $ semigroupOpIsAssociative (inverse x) x x in
+    rewrite p in
+      Refl
+
+||| Inverse elements commute.
+inverseCommute : VerifiedGroup t => (x, y : t) ->
+  y <+> x = A.neutral -> x <+> y = A.neutral
+inverseCommute x y p = selfSquareId (x <+> y) prop where
+  prop : (x <+> y) <+> (x <+> y) = x <+> y
+  prop =
+    rewrite sym $ semigroupOpIsAssociative x y (x <+> y) in
+      rewrite semigroupOpIsAssociative y x y in
+    rewrite p in
+      rewrite monoidNeutralIsNeutralR y in
+        Refl
+
+||| Every element has a right inverse.
+groupInverseIsInverseL : VerifiedGroup t => (x : t) ->
+  x <+> inverse x = Algebra.neutral
+groupInverseIsInverseL x =
+  inverseCommute x (inverse x) (groupInverseIsInverseR x)
+
 ||| -(-x) = x in any verified group.
 inverseSquaredIsIdentity : VerifiedGroup t => (x : t) ->
   inverse (inverse x) = x
 inverseSquaredIsIdentity x =
+  let x' = inverse x in
+    uniqueInverse
+      x'
+      (inverse x')
+      x
+      (groupInverseIsInverseR x')
+      (groupInverseIsInverseR x)
+
+||| If every square in a group is identity, the group is commutative.
+squareIdCommutative : VerifiedGroup t => (x, y : t) ->
+  ((a : t) -> a <+> a = A.neutral) ->
+  x <+> y = y <+> x
+squareIdCommutative x y p =
   let
-    ix = inverse x
-    iix = inverse ix
+    xy = x <+> y
+    yx = y <+> x
       in
-  rewrite sym $ monoidNeutralIsNeutralR iix in
-    rewrite sym $ groupInverseIsInverseL x in
-      rewrite sym $ semigroupOpIsAssociative x ix iix in
-    rewrite groupInverseIsInverseL ix in
-  monoidNeutralIsNeutralL x
+  uniqueInverse xy xy yx (p xy) prop where
+    prop : (x <+> y) <+> (y <+> x) = A.neutral
+    prop =
+      rewrite sym $ semigroupOpIsAssociative x y (y <+> x) in
+        rewrite semigroupOpIsAssociative y y x in
+      rewrite p y in
+        rewrite monoidNeutralIsNeutralR x in
+          p x
 
 ||| -0 = 0 in any verified group.
 inverseNeutralIsNeutral : VerifiedGroup t =>
@@ -37,8 +96,8 @@ inverseOfSum {t} l r =
     e = the t neutral
     il = inverse l
     ir = inverse r
-    sum = l <+> r
-    ilr = inverse sum
+    lr = l <+> r
+    ilr = inverse lr
     iril = ir <+> il
     ile = il <+> e
       in
@@ -50,23 +109,74 @@ inverseOfSum {t} l r =
   -- shuffle
   rewrite semigroupOpIsAssociative ir il l in
     rewrite sym $ semigroupOpIsAssociative iril l r in
-      rewrite sym $ semigroupOpIsAssociative iril sum ilr in
+      rewrite sym $ semigroupOpIsAssociative iril lr ilr in
   -- contract
   rewrite sym $ monoidNeutralIsNeutralL il in
-    rewrite groupInverseIsInverseL sum in
+    rewrite groupInverseIsInverseL lr in
       rewrite sym $ semigroupOpIsAssociative (ir <+> ile) l ile in
         rewrite semigroupOpIsAssociative l il e in
           rewrite groupInverseIsInverseL l in
             rewrite monoidNeutralIsNeutralL e in
               Refl
 
+||| y = z if x + y = x + z.
+cancelLeft : VerifiedGroup t => (x, y, z : t) ->
+  x <+> y = x <+> z -> y = z
+cancelLeft x y z p =
+  rewrite sym $ monoidNeutralIsNeutralR y in
+    rewrite sym $ groupInverseIsInverseR x in
+      rewrite sym $ semigroupOpIsAssociative (inverse x) x y in
+        rewrite p in
+      rewrite semigroupOpIsAssociative (inverse x) x z in
+    rewrite groupInverseIsInverseR x in
+  monoidNeutralIsNeutralR z
+
+||| y = z if y + x = z + x.
+cancelRight : VerifiedGroup t => (x, y, z : t) ->
+  y <+> x = z <+> x -> y = z
+cancelRight x y z p =
+  rewrite sym $ monoidNeutralIsNeutralL y in
+    rewrite sym $ groupInverseIsInverseL x in
+      rewrite semigroupOpIsAssociative y x (inverse x) in
+        rewrite p in
+      rewrite sym $ semigroupOpIsAssociative z x (inverse x) in
+    rewrite groupInverseIsInverseL x in
+  monoidNeutralIsNeutralL z
+
+||| For any a and b, ax = b and ya = b have solutions.
+latinSquareProperty : VerifiedGroup t => (a, b : t) ->
+  ((x : t ** a <+> x = b),
+    (y : t ** y <+> a = b))
+latinSquareProperty a b =
+  let a' = inverse a in
+    (((a' <+> b) **
+      rewrite semigroupOpIsAssociative a a' b in
+        rewrite groupInverseIsInverseL a in
+          monoidNeutralIsNeutralR b),
+    (b <+> a' **
+      rewrite sym $ semigroupOpIsAssociative b a' a in
+        rewrite groupInverseIsInverseR a in
+          monoidNeutralIsNeutralL b))
+
+||| For any a, b, x, the solution to ax = b is unique.
+uniqueSolutionR : VerifiedGroup t => (a, b, x, y : t) ->
+  a <+> x = b -> a <+> y = b -> x = y
+uniqueSolutionR a b x y p q = cancelLeft a x y $ trans p (sym q)
+
+||| For any a, b, y, the solution to ya = b is unique.
+uniqueSolutionL : VerifiedGroup t => (a, b, x, y : t) ->
+  x <+> a = b -> y <+> a = b -> x = y
+uniqueSolutionL a b x y p q = cancelRight a x y $ trans p (sym q)
+
 ||| -(x + y) = -x + -y in any verified abelian group.
 inverseDistributesOverGroupOp : VerifiedAbelianGroup t => (l, r : t) ->
   inverse (l <+> r) = inverse l <+> inverse r
 inverseDistributesOverGroupOp l r =
   rewrite abelianGroupOpIsCommutative (inverse l) (inverse r) in
     inverseOfSum l r
 
+-- Rings
+
 ||| Anything multiplied by zero yields zero back in a verified ring.
 multNeutralAbsorbingL : VerifiedRing t => (r : t) ->
   A.neutral <.> r = A.neutral
@@ -151,3 +261,17 @@ multNegativeByNegativeIsPositive l r =
     rewrite sym $ multInverseInversesL (inverse l) r in
     rewrite inverseSquaredIsIdentity l in
     Refl
+
+inverseOfUnityR : VerifiedRingWithUnity t => (x : t) ->
+  inverse Alg.unity <.> x = inverse x
+inverseOfUnityR x =
+  rewrite multInverseInversesL Alg.unity x in
+    rewrite ringWithUnityIsUnityR x in
+      Refl
+
+inverseOfUnityL : VerifiedRingWithUnity t => (x : t) ->
+  x <.> inverse Alg.unity = inverse x
+inverseOfUnityL x =
+  rewrite multInverseInversesR x Alg.unity in
+    rewrite ringWithUnityIsUnityL x in
+      Refl

libs/contrib/Data/Bool/Algebra.idr

@@ -0,0 +1,98 @@
+module Data.Bool.Algebra
+
+import Control.Algebra
+import Interfaces.Verified
+
+%access public export
+%default total
+
+-- && is Bool -> Lazy Bool -> Bool,
+-- but Bool -> Bool -> Bool is required
+and : Bool -> Bool -> Bool
+and True True = True
+and _ _ = False
+
+xor : Bool -> Bool -> Bool
+xor True True = False
+xor False False = False
+xor _ _ = True
+
+[PlusBoolSemi] Semigroup Bool where
+  (<+>) = xor
+
+[PlusBoolSemiV] VerifiedSemigroup Bool using PlusBoolSemi where
+  semigroupOpIsAssociative True True True = Refl
+  semigroupOpIsAssociative True True False = Refl
+  semigroupOpIsAssociative True False True = Refl
+  semigroupOpIsAssociative True False False = Refl
+  semigroupOpIsAssociative False True True = Refl
+  semigroupOpIsAssociative False False True = Refl
+  semigroupOpIsAssociative False True False = Refl
+  semigroupOpIsAssociative False False False = Refl
+
+[PlusBoolMonoid] Monoid Bool using PlusBoolSemi where
+  neutral = False
+
+[PlusBoolMonoidV] VerifiedMonoid Bool using PlusBoolSemiV, PlusBoolMonoid where
+  monoidNeutralIsNeutralL True = Refl
+  monoidNeutralIsNeutralL False = Refl
+
+  monoidNeutralIsNeutralR True = Refl
+  monoidNeutralIsNeutralR False = Refl
+
+[PlusBoolGroup] Group Bool using PlusBoolMonoid where
+  -- Each Bool is its own additive inverse.
+  inverse = id
+
+[PlusBoolGroupV] VerifiedGroup Bool using PlusBoolMonoidV, PlusBoolGroup where
+  groupInverseIsInverseR True = Refl
+  groupInverseIsInverseR False = Refl
+
+[PlusBoolAbel] AbelianGroup Bool using PlusBoolGroup where
+
+[PlusBoolAbelV] VerifiedAbelianGroup Bool using PlusBoolGroupV, PlusBoolAbel where
+  abelianGroupOpIsCommutative True True = Refl
+  abelianGroupOpIsCommutative True False = Refl
+  abelianGroupOpIsCommutative False True = Refl
+  abelianGroupOpIsCommutative False False = Refl
+
+[RingBool] Ring Bool using PlusBoolAbel where
+  (<.>) = and
+
+[RingBoolV] VerifiedRing Bool using RingBool, PlusBoolAbelV where
+  ringOpIsAssociative True True True = Refl
+  ringOpIsAssociative True True False = Refl
+  ringOpIsAssociative True False True = Refl
+  ringOpIsAssociative True False False = Refl
+  ringOpIsAssociative False True True = Refl
+  ringOpIsAssociative False False True = Refl
+  ringOpIsAssociative False True False = Refl
+  ringOpIsAssociative False False False = Refl
+
+  ringOpIsDistributiveL True True True = Refl
+  ringOpIsDistributiveL True True False = Refl
+  ringOpIsDistributiveL True False True = Refl
+  ringOpIsDistributiveL True False False = Refl
+  ringOpIsDistributiveL False True True = Refl
+  ringOpIsDistributiveL False False True = Refl
+  ringOpIsDistributiveL False True False = Refl
+  ringOpIsDistributiveL False False False = Refl
+
+  ringOpIsDistributiveR True True True = Refl
+  ringOpIsDistributiveR True True False = Refl
+  ringOpIsDistributiveR True False True = Refl
+  ringOpIsDistributiveR True False False = Refl
+  ringOpIsDistributiveR False True True = Refl
+  ringOpIsDistributiveR False False True = Refl
+  ringOpIsDistributiveR False True False = Refl
+  ringOpIsDistributiveR False False False = Refl
+
+[RingUnBool] RingWithUnity Bool using RingBool where
+  unity = True
+
+VerifiedRingWithUnity Bool using RingUnBool, RingBoolV where
+  ringWithUnityIsUnityL True = Refl
+  ringWithUnityIsUnityL False = Refl
+
+  ringWithUnityIsUnityR True = Refl
+  ringWithUnityIsUnityR False = Refl

libs/contrib/Data/Monoid.idr

@@ -8,18 +8,6 @@ module Data.Monoid
 -- TODO: These instances exist, but can't be named the same.
 -- Decide on names for these
 
--- [all] Semigroup Bool where
---   a <+> b = a && b
---
--- [all] Monoid Bool where
---   neutral = True
---
--- [any] Semigroup Bool where
---   a <+> b = a || b
---
--- [any] Monoid Bool where
---   neutral = False
-
 Semigroup () where
   (<+>) _ _ = ()
 

libs/contrib/Interfaces/Verified.idr

@@ -82,7 +82,7 @@ VerifiedApplicative (Either a) where
   applicativeHomomorphism x g = Refl
   applicativeInterchange x (Left y) = Refl
   applicativeInterchange x (Right y) = Refl
-  
+
 private
 foldrConcatEq : (g1 : List (a -> b)) -> (g2 : List (a -> b)) ->
                 (xs : List a) ->
@@ -276,14 +276,9 @@ implementation VerifiedMonoid (List a) where
   monoidNeutralIsNeutralR xs = Refl
 
 interface (VerifiedMonoid a, Group a) => VerifiedGroup a where
-  groupInverseIsInverseL : (l : a) -> l <+> inverse l = Algebra.neutral
   groupInverseIsInverseR : (r : a) -> inverse r <+> r = Algebra.neutral
 
 VerifiedGroup ZZ using PlusZZMonoidV where
-  groupInverseIsInverseL k = rewrite sym $ multCommutativeZ (NegS 0) k in
-                             rewrite multNegLeftZ 0 k in
-                             rewrite multOneLeftNeutralZ k in
-                             plusNegateInverseLZ k
   groupInverseIsInverseR k = rewrite sym $ multCommutativeZ (NegS 0) k in
                              rewrite multNegLeftZ 0 k in
                              rewrite multOneLeftNeutralZ k in
@@ -351,7 +346,7 @@ VerifiedBoundedJoinSemilattice Nat where
 
 VerifiedBoundedJoinSemilattice Bool where
   joinBottomIsIdentity = orFalseNeutral
-  
+
 interface (VerifiedMeetSemilattice a, BoundedMeetSemilattice a) => VerifiedBoundedMeetSemilattice a where
   meetTopIsIdentity : (x : a) -> meet x Lattice.top = x
 

libs/contrib/contrib.ipkg

@@ -30,6 +30,7 @@ modules = CFFI
         , Control.ST.File
 
         , Data.Bool.Extra
+        , Data.Bool.Algebra
         , Data.BoundedList
         , Data.Chain
         , Data.CoList
@@ -50,6 +51,9 @@ modules = CFFI
         , Data.Matrix.Numeric
 
         , Data.Nat
+        , Data.Nat.Ack
+        , Data.Nat.Fact
+        , Data.Nat.Fib
         , Data.Nat.Parity
         , Data.Nat.DivMod
         , Data.Nat.DivMod.IteratedSubtraction