@@ -6,6 +6,7 @@ import Interfaces.Verified
66
77%access export
88
9+||| A prof that -0 = 0 in any verified group.
910inverseNeutralIsNeutral : VerifiedGroup t => inverse (the t A.neutral) = A.neutral
1011inverseNeutralIsNeutral {t} =
1112 let zero = the t neutral in
@@ -13,6 +14,7 @@ inverseNeutralIsNeutral {t} =
1314 let step2 = replace {P = \x => zero <+> inverse zero = x} (groupInverseIsInverseL zero) step1 in
1415 replace {P = \x => x = neutral} (monoidNeutralIsNeutralR $ inverse zero) step2
1516
17+||| A proof that -(-x) = x in any verified group.
1618inverseSquaredIsIdentity : VerifiedGroup t => (x : t) -> inverse (inverse x) = x
1719inverseSquaredIsIdentity {t} x =
1820 let zero = the t neutral in
@@ -22,6 +24,7 @@ inverseSquaredIsIdentity {t} x =
2224 let step4 = replace {P = \r => r = x <+> neutral} (monoidNeutralIsNeutralR (inverse $ inverse x)) step3 in
2325 replace {P = \r => inverse (inverse x) = r} (monoidNeutralIsNeutralL x) step4
2426
27+||| A proof that -(x + y) = -x - y in any verified abelian group.
2528inverseDistributesOverGroupOp : VerifiedAbelianGroup t => (l, r : t) -> inverse (l <+> r) = inverse l <+> inverse r
2629inverseDistributesOverGroupOp {t} l r =
2730 let step1 = replace {P = \x => x = neutral} (sym $ groupInverseIsInverseL (l <+> r)) $ the (the t neutral = neutral) Refl in
@@ -37,6 +40,7 @@ inverseDistributesOverGroupOp {t} l r =
3740 let step11 = replace {P = \x => x = inverse r <+> inverse l} (monoidNeutralIsNeutralR (inverse (l <+> r))) step10 in
3841 replace {P = \x => inverse (l <+> r) = x} (abelianGroupOpIsCommutative (inverse r) (inverse l)) step11
3942
43+||| A proof that anything multiplied by zero yields zero back.
4044multNeutralAbsorbingL : VerifiedRingWithUnity t => (r : t) -> A.neutral <.> r = A.neutral
4145multNeutralAbsorbingL r =
4246 let step1 = the (unity <.> r = r) (ringWithUnityIsUnityR r) in
@@ -48,6 +52,7 @@ multNeutralAbsorbingL r =
4852 let step7 = replace {P = \x => neutral <.> r <+> x = x} (groupInverseIsInverseL r) step6 in
4953 replace {P = \x => x = neutral} (monoidNeutralIsNeutralL (neutral <.> r)) step7
5054
55+||| A proof that anything multiplied by zero yields zero back.
5156multNeutralAbsorbingR : VerifiedRingWithUnity t => (l : t) -> l <.> A.neutral = A.neutral
5257multNeutralAbsorbingR l =
5358 let step1 = the (l <.> unity = l) (ringWithUnityIsUnityL l) in
@@ -59,6 +64,8 @@ multNeutralAbsorbingR l =
5964 let step7 = replace {P = \x => l <.> neutral <+> x = x} (groupInverseIsInverseL l) step6 in
6065 replace {P = \x => x = neutral} (monoidNeutralIsNeutralL (l <.> neutral)) step7
6166
67+||| A proof that inverse operator can be extracted before multiplication
68+||| (-x)y = -(xy)
6269multInverseInversesL : VerifiedRingWithUnity t => (l, r : t) -> inverse l <.> r = inverse (l <.> r)
6370multInverseInversesL l r =
6471 let step1 = replace {P = \x => x <.> r = neutral} (sym $ groupInverseIsInverseL l) (multNeutralAbsorbingL r) in
@@ -69,6 +76,8 @@ multInverseInversesL l r =
6976 let step6 = replace {P = \x => x <+> inverse l <.> r = inverse (l <.> r)} (groupInverseIsInverseR (l <.> r)) step5 in
7077 replace {P = \x => x = inverse (l <.> r)} (monoidNeutralIsNeutralR (inverse l <.> r)) step6
7178
79+||| A proof that inverse operator can be extracted before multiplication
80+||| x(-y) = -(xy)
7281multInverseInversesR : VerifiedRingWithUnity t => (l, r : t) -> l <.> inverse r = inverse (l <.> r)
7382multInverseInversesR l r =
7483 let step1 = replace {P = \x => l <.> x = neutral} (sym $ groupInverseIsInverseL r) (multNeutralAbsorbingR l) in
@@ -79,6 +88,8 @@ multInverseInversesR l r =
7988 let step6 = replace {P = \x => x <+> l <.> inverse r = inverse (l <.> r)} (groupInverseIsInverseR (l <.> r)) step5 in
8089 replace {P = \x => x = inverse (l <.> r)} (monoidNeutralIsNeutralR (l <.> inverse r)) step6
8190
91+||| A proof that multiplication of inverses is the same as multiplication of original
92+||| elements. (-x)(-y) = xy
8293multNegativeByNegativeIsPositive : VerifiedRingWithUnity t => (l, r : t) -> inverse l <.> inverse r = l <.> r
8394multNegativeByNegativeIsPositive l r =
8495 rewrite multInverseInversesR (inverse l) r in