IdrisDoc: Control.Algebra.Laws

Control.Algebra.Laws

cancelLeft : VerifiedGroup t => (x : t) -> (y : t) -> (z : t) -> (x <+> y = x <+> z) -> y = z

y = z if x + y = x + z.

cancelRight : VerifiedGroup t => (x : t) -> (y : t) -> (z : t) -> (y <+> x = z <+> x) -> y = z

y = z if y + x = z + x.

groupInverseIsInverseL : VerifiedGroup t => (x : t) -> x <+> inverse x = neutral

Every element has a right inverse.

inverseCommute : VerifiedGroup t => (x : t) -> (y : t) -> (y <+> x = neutral) -> x <+> y = neutral

Inverse elements commute.

inverseDistributesOverGroupOp : VerifiedAbelianGroup t => (l : t) -> (r : t) -> inverse (l <+> r) = inverse l <+> inverse r

-(x + y) = -x + -y in any verified abelian group.

inverseNeutralIsNeutral : VerifiedGroup t => inverse (the t neutral) = neutral

-0 = 0 in any verified group.

inverseOfSum : VerifiedGroup t => (l : t) -> (r : t) -> inverse (l <+> r) = inverse r <+> inverse l

-(x + y) = -y + -x in any verified group.

inverseOfUnityL : VerifiedRingWithUnity t => (x : t) -> x <.> inverse unity = inverse x
inverseOfUnityR : VerifiedRingWithUnity t => (x : t) -> inverse unity <.> x = inverse x
inverseSquaredIsIdentity : VerifiedGroup t => (x : t) -> inverse (inverse x) = x

-(-x) = x in any verified group.

latinSquareProperty : VerifiedGroup t => (a : t) -> (b : t) -> ((x : t ** a <+> x = b), (y : t ** y <+> a = b))

For any a and b, ax = b and ya = b have solutions.

multInverseInversesL : VerifiedRing t => (l : t) -> (r : t) -> inverse l <.> r = inverse (l <.> r)

Inverse operator can be extracted before multiplication.
(-x)y = -(xy)

multInverseInversesR : VerifiedRing t => (l : t) -> (r : t) -> l <.> inverse r = inverse (l <.> r)

Inverse operator can be extracted before multiplication.
x(-y) = -(xy)

multNegativeByNegativeIsPositive : VerifiedRing t => (l : t) -> (r : t) -> inverse l <.> inverse r = l <.> r

Multiplication of inverses is the same as multiplication of
original elements.
(-x)(-y) = xy

multNeutralAbsorbingL : VerifiedRing t => (r : t) -> neutral <.> r = neutral

Anything multiplied by zero yields zero back in a verified ring.

multNeutralAbsorbingR : VerifiedRing t => (l : t) -> l <.> neutral = neutral

Anything multiplied by zero yields zero back in a verified ring.

selfSquareId : VerifiedGroup t => (x : t) -> (x <+> x = x) -> x = neutral

Only identity is self-squaring.

squareIdCommutative : VerifiedGroup t => (x : t) -> (y : t) -> ((a : t) -> a <+> a = neutral) -> x <+> y = y <+> x

If every square in a group is identity, the group is commutative.

uniqueInverse : VerifiedMonoid t => (x : t) -> (y : t) -> (z : t) -> (y <+> x = neutral) -> (x <+> z = neutral) -> y = z

Inverses are unique.

uniqueSolutionL : VerifiedGroup t => (a : t) -> (b : t) -> (x : t) -> (y : t) -> (x <+> a = b) -> (y <+> a = b) -> x = y

For any a, b, y, the solution to ya = b is unique.

uniqueSolutionR : VerifiedGroup t => (a : t) -> (b : t) -> (x : t) -> (y : t) -> (a <+> x = b) -> (a <+> y = b) -> x = y

For any a, b, x, the solution to ax = b is unique.