mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-19 17:21:59 +03:00
* [ fix #72 ] remove the broken modules People are still hitting the same issueT There has been no movement towards fixing it It is IMO unfixable Let's drop it. * [ fix #72 ] Remove dependencies of Control.Algebra Follow-up to the commit by gallais, this removes the contrib libraries which were using `Control.Algebra`. * [ fix #72 ] Record changes in CHANGELOG_NEXT * [ lint ] Move Algebra changes to existing header --------- Co-authored-by: Thomas E. Hansen <teh6@st-andrews.ac.uk>
This commit is contained in:
G. Allais
GitHub
parent
02e5468551
commit
3f985bcefa
@ -199,6 +199,23 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
|
|||||||
* Function `invFin` from `Data.Fin.Extra` was deprecated in favour of
|
* Function `invFin` from `Data.Fin.Extra` was deprecated in favour of
|
||||||
`Data.Fin.complement` from `base`.
|
`Data.Fin.complement` from `base`.
|
||||||
|
|
||||||
|
* The `Control.Algebra` library from `contrib` has been removed due to being
|
||||||
|
broken, unfixed for years, and on several independent occasions causing
|
||||||
|
confusion with people picking up Idris and trying to use it.
|
||||||
|
- Detailed discussion can be found in
|
||||||
|
[Idris2#72](https://github.com/idris-lang/Idris2/issues/72).
|
||||||
|
- For reasoning about algebraic structures and proofs, please see
|
||||||
|
[Frex](https://github.com/frex-project/idris-frex/) and
|
||||||
|
[idris2-algebra](https://github.com/stefan-hoeck/idris2-algebra/).
|
||||||
|
|
||||||
|
* Since they depend on `Control.Algebra`, the following `contrib` libraries have
|
||||||
|
also been removed:
|
||||||
|
- `Control/Monad/Algebra.idr`
|
||||||
|
- `Data/Bool/Algebra.idr`
|
||||||
|
- `Data/List/Algebra.idr`
|
||||||
|
- `Data/Morphisms/Algebra.idr`
|
||||||
|
- `Data/Nat/Algebra.idr`
|
||||||
|
|
||||||
#### Network
|
#### Network
|
||||||
|
|
||||||
* Add a missing function parameter (the flag) in the C implementation of `idrnet_recv_bytes`
|
* Add a missing function parameter (the flag) in the C implementation of `idrnet_recv_bytes`
|
||||||
|
|||||||
@ -1,154 +0,0 @@
|
|||||||
module Control.Algebra
|
|
||||||
|
|
||||||
export infixl 6 <->
|
|
||||||
export infixl 7 <.>
|
|
||||||
|
|
||||||
public export
|
|
||||||
interface Semigroup ty => SemigroupV ty where
|
|
||||||
semigroupOpIsAssociative : (l, c, r : ty) ->
|
|
||||||
l <+> (c <+> r) = (l <+> c) <+> r
|
|
||||||
|
|
||||||
public export
|
|
||||||
interface (Monoid ty, SemigroupV ty) => MonoidV ty where
|
|
||||||
monoidNeutralIsNeutralL : (l : ty) -> l <+> neutral {ty} = l
|
|
||||||
monoidNeutralIsNeutralR : (r : ty) -> neutral {ty} <+> r = r
|
|
||||||
|
|
||||||
||| Sets equipped with a single binary operation that is associative,
|
|
||||||
||| along with a neutral element for that binary operation and
|
|
||||||
||| inverses for all elements. Satisfies the following laws:
|
|
||||||
|||
|
|
||||||
||| + Associativity of `<+>`:
|
|
||||||
||| forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
|
|
||||||
||| + Neutral for `<+>`:
|
|
||||||
||| forall a, a <+> neutral == a
|
|
||||||
||| forall a, neutral <+> a == a
|
|
||||||
||| + Inverse for `<+>`:
|
|
||||||
||| forall a, a <+> inverse a == neutral
|
|
||||||
||| forall a, inverse a <+> a == neutral
|
|
||||||
public export
|
|
||||||
interface MonoidV ty => Group ty where
|
|
||||||
inverse : ty -> ty
|
|
||||||
|
|
||||||
groupInverseIsInverseR : (r : ty) -> inverse r <+> r = neutral {ty}
|
|
||||||
|
|
||||||
(<->) : Group ty => ty -> ty -> ty
|
|
||||||
(<->) left right = left <+> (inverse right)
|
|
||||||
|
|
||||||
||| Sets equipped with a single binary operation that is associative
|
|
||||||
||| and commutative, along with a neutral element for that binary
|
|
||||||
||| operation and inverses for all elements. Satisfies the following
|
|
||||||
||| laws:
|
|
||||||
|||
|
|
||||||
||| + Associativity of `<+>`:
|
|
||||||
||| forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
|
|
||||||
||| + Commutativity of `<+>`:
|
|
||||||
||| forall a b, a <+> b == b <+> a
|
|
||||||
||| + Neutral for `<+>`:
|
|
||||||
||| forall a, a <+> neutral == a
|
|
||||||
||| forall a, neutral <+> a == a
|
|
||||||
||| + Inverse for `<+>`:
|
|
||||||
||| forall a, a <+> inverse a == neutral
|
|
||||||
||| forall a, inverse a <+> a == neutral
|
|
||||||
public export
|
|
||||||
interface Group ty => AbelianGroup ty where
|
|
||||||
groupOpIsCommutative : (l, r : ty) -> l <+> r = r <+> l
|
|
||||||
|
|
||||||
||| A homomorphism is a mapping that preserves group structure.
|
|
||||||
public export
|
|
||||||
interface (Group a, Group b) => GroupHomomorphism a b where
|
|
||||||
to : a -> b
|
|
||||||
|
|
||||||
toGroup : (x, y : a) ->
|
|
||||||
to (x <+> y) = (to x) <+> (to y)
|
|
||||||
|
|
||||||
||| Sets equipped with two binary operations, one associative and
|
|
||||||
||| commutative supplied with a neutral element, and the other
|
|
||||||
||| associative, with distributivity laws relating the two operations.
|
|
||||||
||| Satisfies the following laws:
|
|
||||||
|||
|
|
||||||
||| + Associativity of `<+>`:
|
|
||||||
||| forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
|
|
||||||
||| + Commutativity of `<+>`:
|
|
||||||
||| forall a b, a <+> b == b <+> a
|
|
||||||
||| + Neutral for `<+>`:
|
|
||||||
||| forall a, a <+> neutral == a
|
|
||||||
||| forall a, neutral <+> a == a
|
|
||||||
||| + Inverse for `<+>`:
|
|
||||||
||| forall a, a <+> inverse a == neutral
|
|
||||||
||| forall a, inverse a <+> a == neutral
|
|
||||||
||| + Associativity of `<.>`:
|
|
||||||
||| forall a b c, a <.> (b <.> c) == (a <.> b) <.> c
|
|
||||||
||| + Distributivity of `<.>` and `<+>`:
|
|
||||||
||| forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
|
|
||||||
||| forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)
|
|
||||||
public export
|
|
||||||
interface Group ty => Ring ty where
|
|
||||||
(<.>) : ty -> ty -> ty
|
|
||||||
|
|
||||||
ringOpIsAssociative : (l, c, r : ty) ->
|
|
||||||
l <.> (c <.> r) = (l <.> c) <.> r
|
|
||||||
ringOpIsDistributiveL : (l, c, r : ty) ->
|
|
||||||
l <.> (c <+> r) = (l <.> c) <+> (l <.> r)
|
|
||||||
ringOpIsDistributiveR : (l, c, r : ty) ->
|
|
||||||
(l <+> c) <.> r = (l <.> r) <+> (c <.> r)
|
|
||||||
|
|
||||||
||| Sets equipped with two binary operations, one associative and
|
|
||||||
||| commutative supplied with a neutral element, and the other
|
|
||||||
||| associative supplied with a neutral element, with distributivity
|
|
||||||
||| laws relating the two operations. Satisfies the following laws:
|
|
||||||
|||
|
|
||||||
||| + Associativity of `<+>`:
|
|
||||||
||| forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
|
|
||||||
||| + Commutativity of `<+>`:
|
|
||||||
||| forall a b, a <+> b == b <+> a
|
|
||||||
||| + Neutral for `<+>`:
|
|
||||||
||| forall a, a <+> neutral == a
|
|
||||||
||| forall a, neutral <+> a == a
|
|
||||||
||| + Inverse for `<+>`:
|
|
||||||
||| forall a, a <+> inverse a == neutral
|
|
||||||
||| forall a, inverse a <+> a == neutral
|
|
||||||
||| + Associativity of `<.>`:
|
|
||||||
||| forall a b c, a <.> (b <.> c) == (a <.> b) <.> c
|
|
||||||
||| + Neutral for `<.>`:
|
|
||||||
||| forall a, a <.> unity == a
|
|
||||||
||| forall a, unity <.> a == a
|
|
||||||
||| + Distributivity of `<.>` and `<+>`:
|
|
||||||
||| forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
|
|
||||||
||| forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)
|
|
||||||
public export
|
|
||||||
interface Ring ty => RingWithUnity ty where
|
|
||||||
unity : ty
|
|
||||||
|
|
||||||
unityIsRingIdL : (l : ty) -> l <.> unity = l
|
|
||||||
unityIsRingIdR : (r : ty) -> unity <.> r = r
|
|
||||||
|
|
||||||
||| Sets equipped with two binary operations – both associative,
|
|
||||||
||| commutative and possessing a neutral element – and distributivity
|
|
||||||
||| laws relating the two operations. All elements except the additive
|
|
||||||
||| identity should have a multiplicative inverse. Should (but may
|
|
||||||
||| not) satisfy the following laws:
|
|
||||||
|||
|
|
||||||
||| + Associativity of `<+>`:
|
|
||||||
||| forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
|
|
||||||
||| + Commutativity of `<+>`:
|
|
||||||
||| forall a b, a <+> b == b <+> a
|
|
||||||
||| + Neutral for `<+>`:
|
|
||||||
||| forall a, a <+> neutral == a
|
|
||||||
||| forall a, neutral <+> a == a
|
|
||||||
||| + Inverse for `<+>`:
|
|
||||||
||| forall a, a <+> inverse a == neutral
|
|
||||||
||| forall a, inverse a <+> a == neutral
|
|
||||||
||| + Associativity of `<.>`:
|
|
||||||
||| forall a b c, a <.> (b <.> c) == (a <.> b) <.> c
|
|
||||||
||| + Unity for `<.>`:
|
|
||||||
||| forall a, a <.> unity == a
|
|
||||||
||| forall a, unity <.> a == a
|
|
||||||
||| + InverseM of `<.>`, except for neutral
|
|
||||||
||| forall a /= neutral, a <.> inverseM a == unity
|
|
||||||
||| forall a /= neutral, inverseM a <.> a == unity
|
|
||||||
||| + Distributivity of `<.>` and `<+>`:
|
|
||||||
||| forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
|
|
||||||
||| forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)
|
|
||||||
public export
|
|
||||||
interface RingWithUnity ty => Field ty where
|
|
||||||
inverseM : (x : ty) -> Not (x = neutral {ty}) -> ty
|
|
||||||
@ -1,22 +0,0 @@
|
|||||||
module Control.Algebra.Implementations
|
|
||||||
|
|
||||||
import Control.Algebra
|
|
||||||
|
|
||||||
-- This file is for algebra implementations with nowhere else to go.
|
|
||||||
|
|
||||||
%default total
|
|
||||||
|
|
||||||
-- Functions ---------------------------
|
|
||||||
|
|
||||||
Semigroup (ty -> ty) where
|
|
||||||
(<+>) = (.)
|
|
||||||
|
|
||||||
SemigroupV (ty -> ty) where
|
|
||||||
semigroupOpIsAssociative _ _ _ = Refl
|
|
||||||
|
|
||||||
Monoid (ty -> ty) where
|
|
||||||
neutral = id
|
|
||||||
|
|
||||||
MonoidV (ty -> ty) where
|
|
||||||
monoidNeutralIsNeutralL _ = Refl
|
|
||||||
monoidNeutralIsNeutralR _ = Refl
|
|
||||||
@ -1,290 +0,0 @@
|
|||||||
module Control.Algebra.Laws
|
|
||||||
|
|
||||||
import Control.Algebra
|
|
||||||
|
|
||||||
%default total
|
|
||||||
|
|
||||||
-- Monoids
|
|
||||||
|
|
||||||
||| Inverses are unique.
|
|
||||||
public export
|
|
||||||
uniqueInverse : MonoidV ty => (x, y, z : ty) ->
|
|
||||||
y <+> x = neutral {ty} -> x <+> z = neutral {ty} -> 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.
|
|
||||||
public export
|
|
||||||
selfSquareId : Group ty => (x : ty) ->
|
|
||||||
x <+> x = x -> x = neutral {ty}
|
|
||||||
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.
|
|
||||||
public export
|
|
||||||
inverseCommute : Group ty => (x, y : ty) ->
|
|
||||||
y <+> x = neutral {ty} -> x <+> y = neutral {ty}
|
|
||||||
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.
|
|
||||||
public export
|
|
||||||
groupInverseIsInverseL : Group ty => (x : ty) ->
|
|
||||||
x <+> inverse x = neutral {ty}
|
|
||||||
groupInverseIsInverseL x =
|
|
||||||
inverseCommute x (inverse x) (groupInverseIsInverseR x)
|
|
||||||
|
|
||||||
||| -(-x) = x
|
|
||||||
public export
|
|
||||||
inverseSquaredIsIdentity : Group ty => (x : ty) ->
|
|
||||||
inverse (inverse x) = x
|
|
||||||
inverseSquaredIsIdentity {ty} x =
|
|
||||||
uniqueInverse
|
|
||||||
(inverse x)
|
|
||||||
(inverse $ inverse x)
|
|
||||||
x
|
|
||||||
(groupInverseIsInverseR $ inverse x)
|
|
||||||
(groupInverseIsInverseR x)
|
|
||||||
|
|
||||||
||| If every square in a group is identity, the group is commutative.
|
|
||||||
public export
|
|
||||||
squareIdCommutative : Group ty => (x, y : ty) ->
|
|
||||||
((a : ty) -> a <+> a = neutral {ty}) ->
|
|
||||||
x <+> y = y <+> x
|
|
||||||
squareIdCommutative x y p =
|
|
||||||
uniqueInverse (x <+> y) (x <+> y) (y <+> x) (p (x <+> y)) prop where
|
|
||||||
prop : (x <+> y) <+> (y <+> x) = neutral {ty}
|
|
||||||
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
|
|
||||||
public export
|
|
||||||
inverseNeutralIsNeutral : Group ty =>
|
|
||||||
inverse (neutral {ty}) = neutral {ty}
|
|
||||||
inverseNeutralIsNeutral {ty} =
|
|
||||||
rewrite sym $ cong inverse (groupInverseIsInverseL (neutral {ty})) in
|
|
||||||
rewrite monoidNeutralIsNeutralR $ inverse (neutral {ty}) in
|
|
||||||
inverseSquaredIsIdentity (neutral {ty})
|
|
||||||
|
|
||||||
-- ||| -(x + y) = -y + -x
|
|
||||||
-- public export
|
|
||||||
-- inverseOfSum : Group ty => (l, r : ty) ->
|
|
||||||
-- inverse (l <+> r) = inverse r <+> inverse l
|
|
||||||
-- inverseOfSum {ty} l r =
|
|
||||||
-- -- expand
|
|
||||||
-- rewrite sym $ monoidNeutralIsNeutralR $ inverse $ l <+> r in
|
|
||||||
-- rewrite sym $ groupInverseIsInverseR r in
|
|
||||||
-- rewrite sym $ monoidNeutralIsNeutralL $ inverse r in
|
|
||||||
-- rewrite sym $ groupInverseIsInverseR l in
|
|
||||||
-- -- shuffle
|
|
||||||
-- rewrite semigroupOpIsAssociative (inverse r) (inverse l) l in
|
|
||||||
-- rewrite sym $ semigroupOpIsAssociative (inverse r <+> inverse l) l r in
|
|
||||||
-- rewrite sym $ semigroupOpIsAssociative (inverse r <+> inverse l) (l <+> r) (inverse $ l <+> r) in
|
|
||||||
-- -- contract
|
|
||||||
-- rewrite sym $ monoidNeutralIsNeutralL $ inverse l in
|
|
||||||
-- rewrite groupInverseIsInverseL $ l <+> r in
|
|
||||||
-- rewrite sym $ semigroupOpIsAssociative (inverse r <+> (inverse l <+> neutral)) l (inverse l <+> neutral) in
|
|
||||||
-- rewrite semigroupOpIsAssociative l (inverse l) neutral in
|
|
||||||
-- rewrite groupInverseIsInverseL l in
|
|
||||||
-- rewrite monoidNeutralIsNeutralL $ the ty neutral in
|
|
||||||
-- Refl
|
|
||||||
|
|
||||||
||| y = z if x + y = x + z
|
|
||||||
public export
|
|
||||||
cancelLeft : Group ty => (x, y, z : ty) ->
|
|
||||||
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.
|
|
||||||
public export
|
|
||||||
cancelRight : Group ty => (x, y, z : ty) ->
|
|
||||||
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
|
|
||||||
|
|
||||||
||| ab = 0 -> a = b^-1
|
|
||||||
public export
|
|
||||||
neutralProductInverseR : Group ty => (a, b : ty) ->
|
|
||||||
a <+> b = neutral {ty} -> a = inverse b
|
|
||||||
neutralProductInverseR a b prf =
|
|
||||||
cancelRight b a (inverse b) $
|
|
||||||
trans prf $ sym $ groupInverseIsInverseR b
|
|
||||||
|
|
||||||
||| ab = 0 -> a^-1 = b
|
|
||||||
public export
|
|
||||||
neutralProductInverseL : Group ty => (a, b : ty) ->
|
|
||||||
a <+> b = neutral {ty} -> inverse a = b
|
|
||||||
neutralProductInverseL a b prf =
|
|
||||||
cancelLeft a (inverse a) b $
|
|
||||||
trans (groupInverseIsInverseL a) $ sym prf
|
|
||||||
|
|
||||||
||| For any a and b, ax = b and ya = b have solutions.
|
|
||||||
public export
|
|
||||||
latinSquareProperty : Group ty => (a, b : ty) ->
|
|
||||||
((x : ty ** a <+> x = b),
|
|
||||||
(y : ty ** y <+> a = b))
|
|
||||||
latinSquareProperty a b =
|
|
||||||
((((inverse a) <+> b) **
|
|
||||||
rewrite semigroupOpIsAssociative a (inverse a) b in
|
|
||||||
rewrite groupInverseIsInverseL a in
|
|
||||||
monoidNeutralIsNeutralR b),
|
|
||||||
(b <+> (inverse a) **
|
|
||||||
rewrite sym $ semigroupOpIsAssociative b (inverse a) a in
|
|
||||||
rewrite groupInverseIsInverseR a in
|
|
||||||
monoidNeutralIsNeutralL b))
|
|
||||||
|
|
||||||
||| For any a, b, x, the solution to ax = b is unique.
|
|
||||||
public export
|
|
||||||
uniqueSolutionR : Group ty => (a, b, x, y : ty) ->
|
|
||||||
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.
|
|
||||||
public export
|
|
||||||
uniqueSolutionL : Group 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
|
|
||||||
-- public export
|
|
||||||
-- inverseDistributesOverGroupOp : AbelianGroup ty => (l, r : ty) ->
|
|
||||||
-- inverse (l <+> r) = inverse l <+> inverse r
|
|
||||||
-- inverseDistributesOverGroupOp l r =
|
|
||||||
-- rewrite groupOpIsCommutative (inverse l) (inverse r) in
|
|
||||||
-- inverseOfSum l r
|
|
||||||
|
|
||||||
||| Homomorphism preserves neutral.
|
|
||||||
public export
|
|
||||||
homoNeutral : GroupHomomorphism a b =>
|
|
||||||
to (neutral {ty=a}) = neutral {ty=b}
|
|
||||||
homoNeutral =
|
|
||||||
selfSquareId (to neutral) $
|
|
||||||
trans (sym $ toGroup neutral neutral) $
|
|
||||||
cong to $ monoidNeutralIsNeutralL neutral
|
|
||||||
|
|
||||||
||| Homomorphism preserves inverses.
|
|
||||||
public export
|
|
||||||
homoInverse : GroupHomomorphism a b => (x : a) ->
|
|
||||||
the b (to $ inverse x) = the b (inverse $ to x)
|
|
||||||
homoInverse x =
|
|
||||||
cancelRight (to x) (to $ inverse x) (inverse $ to x) $
|
|
||||||
trans (sym $ toGroup (inverse x) x) $
|
|
||||||
trans (cong to $ groupInverseIsInverseR x) $
|
|
||||||
trans homoNeutral $
|
|
||||||
sym $ groupInverseIsInverseR (to x)
|
|
||||||
|
|
||||||
-- Rings
|
|
||||||
|
|
||||||
||| 0x = x
|
|
||||||
public export
|
|
||||||
multNeutralAbsorbingL : Ring ty => (r : ty) ->
|
|
||||||
neutral {ty} <.> r = neutral {ty}
|
|
||||||
multNeutralAbsorbingL {ty} r =
|
|
||||||
rewrite sym $ monoidNeutralIsNeutralR $ neutral <.> r in
|
|
||||||
rewrite sym $ groupInverseIsInverseR $ neutral <.> r in
|
|
||||||
rewrite sym $ semigroupOpIsAssociative (inverse $ neutral <.> r) (neutral <.> r) (((inverse $ neutral <.> r) <+> (neutral <.> r)) <.> r) in
|
|
||||||
rewrite groupInverseIsInverseR $ neutral <.> r in
|
|
||||||
rewrite sym $ ringOpIsDistributiveR neutral neutral r in
|
|
||||||
rewrite monoidNeutralIsNeutralR $ the ty neutral in
|
|
||||||
groupInverseIsInverseR $ neutral <.> r
|
|
||||||
|
|
||||||
||| x0 = 0
|
|
||||||
public export
|
|
||||||
multNeutralAbsorbingR : Ring ty => (l : ty) ->
|
|
||||||
l <.> neutral {ty} = neutral {ty}
|
|
||||||
multNeutralAbsorbingR {ty} l =
|
|
||||||
rewrite sym $ monoidNeutralIsNeutralL $ l <.> neutral in
|
|
||||||
rewrite sym $ groupInverseIsInverseL $ l <.> neutral in
|
|
||||||
rewrite semigroupOpIsAssociative (l <.> ((l <.> neutral) <+> (inverse $ l <.> neutral))) (l <.> neutral) (inverse $ l <.> neutral) in
|
|
||||||
rewrite groupInverseIsInverseL $ l <.> neutral in
|
|
||||||
rewrite sym $ ringOpIsDistributiveL l neutral neutral in
|
|
||||||
rewrite monoidNeutralIsNeutralL $ the ty neutral in
|
|
||||||
groupInverseIsInverseL $ l <.> neutral
|
|
||||||
|
|
||||||
||| (-x)y = -(xy)
|
|
||||||
public export
|
|
||||||
multInverseInversesL : Ring ty => (l, r : ty) ->
|
|
||||||
inverse l <.> r = inverse (l <.> r)
|
|
||||||
multInverseInversesL l r =
|
|
||||||
rewrite sym $ monoidNeutralIsNeutralR $ inverse l <.> r in
|
|
||||||
rewrite sym $ groupInverseIsInverseR $ l <.> r in
|
|
||||||
rewrite sym $ semigroupOpIsAssociative (inverse $ l <.> r) (l <.> r) (inverse l <.> r) in
|
|
||||||
rewrite sym $ ringOpIsDistributiveR l (inverse l) r in
|
|
||||||
rewrite groupInverseIsInverseL l in
|
|
||||||
rewrite multNeutralAbsorbingL r in
|
|
||||||
monoidNeutralIsNeutralL $ inverse $ l <.> r
|
|
||||||
|
|
||||||
||| x(-y) = -(xy)
|
|
||||||
public export
|
|
||||||
multInverseInversesR : Ring ty => (l, r : ty) ->
|
|
||||||
l <.> inverse r = inverse (l <.> r)
|
|
||||||
multInverseInversesR l r =
|
|
||||||
rewrite sym $ monoidNeutralIsNeutralL $ l <.> (inverse r) in
|
|
||||||
rewrite sym $ groupInverseIsInverseL (l <.> r) in
|
|
||||||
rewrite semigroupOpIsAssociative (l <.> (inverse r)) (l <.> r) (inverse $ l <.> r) in
|
|
||||||
rewrite sym $ ringOpIsDistributiveL l (inverse r) r in
|
|
||||||
rewrite groupInverseIsInverseR r in
|
|
||||||
rewrite multNeutralAbsorbingR l in
|
|
||||||
monoidNeutralIsNeutralR $ inverse $ l <.> r
|
|
||||||
|
|
||||||
||| (-x)(-y) = xy
|
|
||||||
public export
|
|
||||||
multNegativeByNegativeIsPositive : Ring ty => (l, r : ty) ->
|
|
||||||
inverse l <.> inverse r = l <.> r
|
|
||||||
multNegativeByNegativeIsPositive l r =
|
|
||||||
rewrite multInverseInversesR (inverse l) r in
|
|
||||||
rewrite sym $ multInverseInversesL (inverse l) r in
|
|
||||||
rewrite inverseSquaredIsIdentity l in
|
|
||||||
Refl
|
|
||||||
|
|
||||||
||| (-1)x = -x
|
|
||||||
public export
|
|
||||||
inverseOfUnityR : RingWithUnity ty => (x : ty) ->
|
|
||||||
inverse (unity {ty}) <.> x = inverse x
|
|
||||||
inverseOfUnityR x =
|
|
||||||
rewrite multInverseInversesL unity x in
|
|
||||||
rewrite unityIsRingIdR x in
|
|
||||||
Refl
|
|
||||||
|
|
||||||
||| x(-1) = -x
|
|
||||||
public export
|
|
||||||
inverseOfUnityL : RingWithUnity ty => (x : ty) ->
|
|
||||||
x <.> inverse (unity {ty}) = inverse x
|
|
||||||
inverseOfUnityL x =
|
|
||||||
rewrite multInverseInversesR x unity in
|
|
||||||
rewrite unityIsRingIdL x in
|
|
||||||
Refl
|
|
||||||
@ -1,18 +0,0 @@
|
|||||||
module Control.Monad.Algebra
|
|
||||||
|
|
||||||
import Control.Algebra
|
|
||||||
import Control.Monad.Identity
|
|
||||||
|
|
||||||
%default total
|
|
||||||
|
|
||||||
public export
|
|
||||||
SemigroupV ty => SemigroupV (Identity ty) where
|
|
||||||
semigroupOpIsAssociative (Id l) (Id c) (Id r) =
|
|
||||||
rewrite semigroupOpIsAssociative l c r in Refl
|
|
||||||
|
|
||||||
public export
|
|
||||||
MonoidV ty => MonoidV (Identity ty) where
|
|
||||||
monoidNeutralIsNeutralL (Id l) =
|
|
||||||
rewrite monoidNeutralIsNeutralL l in Refl
|
|
||||||
monoidNeutralIsNeutralR (Id r) =
|
|
||||||
rewrite monoidNeutralIsNeutralR r in Refl
|
|
||||||
@ -1,77 +0,0 @@
|
|||||||
module Data.Bool.Algebra
|
|
||||||
|
|
||||||
import Control.Algebra
|
|
||||||
import Data.Bool.Xor
|
|
||||||
|
|
||||||
%default total
|
|
||||||
|
|
||||||
-- && is Bool -> Lazy Bool -> Bool,
|
|
||||||
-- but Bool -> Bool -> Bool is required
|
|
||||||
and : Bool -> Bool -> Bool
|
|
||||||
and True True = True
|
|
||||||
and _ _ = False
|
|
||||||
|
|
||||||
Semigroup Bool where
|
|
||||||
(<+>) = xor
|
|
||||||
|
|
||||||
SemigroupV Bool where
|
|
||||||
semigroupOpIsAssociative = xorAssociative
|
|
||||||
|
|
||||||
Monoid Bool where
|
|
||||||
neutral = False
|
|
||||||
|
|
||||||
MonoidV Bool where
|
|
||||||
monoidNeutralIsNeutralL True = Refl
|
|
||||||
monoidNeutralIsNeutralL False = Refl
|
|
||||||
|
|
||||||
monoidNeutralIsNeutralR True = Refl
|
|
||||||
monoidNeutralIsNeutralR False = Refl
|
|
||||||
|
|
||||||
Group Bool where
|
|
||||||
-- Each Bool is its own additive inverse.
|
|
||||||
inverse = id
|
|
||||||
|
|
||||||
groupInverseIsInverseR True = Refl
|
|
||||||
groupInverseIsInverseR False = Refl
|
|
||||||
|
|
||||||
AbelianGroup Bool where
|
|
||||||
groupOpIsCommutative = xorCommutative
|
|
||||||
|
|
||||||
Ring Bool where
|
|
||||||
(<.>) = and
|
|
||||||
|
|
||||||
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
|
|
||||||
|
|
||||||
RingWithUnity Bool where
|
|
||||||
unity = True
|
|
||||||
|
|
||||||
unityIsRingIdL True = Refl
|
|
||||||
unityIsRingIdL False = Refl
|
|
||||||
|
|
||||||
unityIsRingIdR True = Refl
|
|
||||||
unityIsRingIdR False = Refl
|
|
||||||
@ -1,15 +0,0 @@
|
|||||||
module Data.List.Algebra
|
|
||||||
|
|
||||||
import Control.Algebra
|
|
||||||
import Data.List
|
|
||||||
|
|
||||||
%default total
|
|
||||||
|
|
||||||
public export
|
|
||||||
SemigroupV (List ty) where
|
|
||||||
semigroupOpIsAssociative = appendAssociative
|
|
||||||
|
|
||||||
public export
|
|
||||||
MonoidV (List ty) where
|
|
||||||
monoidNeutralIsNeutralL = appendNilRightNeutral
|
|
||||||
monoidNeutralIsNeutralR _ = Refl
|
|
||||||
@ -1,15 +0,0 @@
|
|||||||
module Data.Morphisms.Algebra
|
|
||||||
|
|
||||||
import Control.Algebra
|
|
||||||
import Data.Morphisms
|
|
||||||
|
|
||||||
%default total
|
|
||||||
|
|
||||||
public export
|
|
||||||
SemigroupV (Endomorphism ty) where
|
|
||||||
semigroupOpIsAssociative (Endo _) (Endo _) (Endo _) = Refl
|
|
||||||
|
|
||||||
public export
|
|
||||||
MonoidV (Endomorphism ty) where
|
|
||||||
monoidNeutralIsNeutralL (Endo _) = Refl
|
|
||||||
monoidNeutralIsNeutralR (Endo _) = Refl
|
|
||||||
@ -1,19 +0,0 @@
|
|||||||
module Data.Nat.Algebra
|
|
||||||
|
|
||||||
import Control.Algebra
|
|
||||||
import Data.Nat
|
|
||||||
|
|
||||||
%default total
|
|
||||||
|
|
||||||
namespace SemigroupV
|
|
||||||
|
|
||||||
public export
|
|
||||||
[Additive] SemigroupV Nat using Semigroup.Additive where
|
|
||||||
semigroupOpIsAssociative = plusAssociative
|
|
||||||
|
|
||||||
namespace MonoidV
|
|
||||||
|
|
||||||
public export
|
|
||||||
[Additive] MonoidV Nat using Monoid.Additive SemigroupV.Additive where
|
|
||||||
monoidNeutralIsNeutralL = plusZeroRightNeutral
|
|
||||||
monoidNeutralIsNeutralR = plusZeroLeftNeutral
|
|
||||||
@ -9,12 +9,6 @@ modules = Control.ANSI,
|
|||||||
|
|
||||||
Control.Delayed,
|
Control.Delayed,
|
||||||
|
|
||||||
Control.Monad.Algebra,
|
|
||||||
|
|
||||||
Control.Algebra,
|
|
||||||
Control.Algebra.Laws,
|
|
||||||
Control.Algebra.Implementations,
|
|
||||||
|
|
||||||
Control.Arrow,
|
Control.Arrow,
|
||||||
Control.Category,
|
Control.Category,
|
||||||
|
|
||||||
@ -23,8 +17,6 @@ modules = Control.ANSI,
|
|||||||
Data.Binary.Digit,
|
Data.Binary.Digit,
|
||||||
Data.Binary,
|
Data.Binary,
|
||||||
|
|
||||||
Data.Bool.Algebra,
|
|
||||||
|
|
||||||
Data.Fin.Extra,
|
Data.Fin.Extra,
|
||||||
|
|
||||||
Data.Fun.Extra,
|
Data.Fun.Extra,
|
||||||
@ -40,7 +32,6 @@ modules = Control.ANSI,
|
|||||||
|
|
||||||
Data.Linear.Array,
|
Data.Linear.Array,
|
||||||
|
|
||||||
Data.List.Algebra,
|
|
||||||
Data.List.TailRec,
|
Data.List.TailRec,
|
||||||
Data.List.Equalities,
|
Data.List.Equalities,
|
||||||
Data.List.Extra,
|
Data.List.Extra,
|
||||||
@ -56,9 +47,6 @@ modules = Control.ANSI,
|
|||||||
|
|
||||||
Data.Monoid.Exponentiation,
|
Data.Monoid.Exponentiation,
|
||||||
|
|
||||||
Data.Morphisms.Algebra,
|
|
||||||
|
|
||||||
Data.Nat.Algebra,
|
|
||||||
Data.Nat.Ack,
|
Data.Nat.Ack,
|
||||||
Data.Nat.Division,
|
Data.Nat.Division,
|
||||||
Data.Nat.Equational,
|
Data.Nat.Equational,
|
||||||
|
|||||||
Loading…
Reference in New Issue
Block a user