@@ -6,6 +6,7 @@ import Interfaces.Verified
7%access export
7%access export
9+||| A prof that -0 = 0 in any verified group.
9inverseNeutralIsNeutral : VerifiedGroup t => inverse (the t A.neutral) = A.neutral
10inverseNeutralIsNeutral : VerifiedGroup t => inverse (the t A.neutral) = A.neutral
10inverseNeutralIsNeutral {t} =
11inverseNeutralIsNeutral {t} =
11 let zero = the t neutral in
12 let zero = the t neutral in
@@ -13,6 +14,7 @@ inverseNeutralIsNeutral {t} =
13 let step2 = replace {P = \x => zero <+> inverse zero = x} (groupInverseIsInverseL zero) step1 in
14 let step2 = replace {P = \x => zero <+> inverse zero = x} (groupInverseIsInverseL zero) step1 in
14 replace {P = \x => x = neutral} (monoidNeutralIsNeutralR $ inverse zero) step2
15 replace {P = \x => x = neutral} (monoidNeutralIsNeutralR $ inverse zero) step2
17+||| A proof that -(-x) = x in any verified group.
16inverseSquaredIsIdentity : VerifiedGroup t => (x : t) -> inverse (inverse x) = x
18inverseSquaredIsIdentity : VerifiedGroup t => (x : t) -> inverse (inverse x) = x
17inverseSquaredIsIdentity {t} x =
19inverseSquaredIsIdentity {t} x =
18 let zero = the t neutral in
20 let zero = the t neutral in
@@ -22,6 +24,7 @@ inverseSquaredIsIdentity {t} x =
22 let step4 = replace {P = \r => r = x <+> neutral} (monoidNeutralIsNeutralR (inverse $ inverse x)) step3 in
24 let step4 = replace {P = \r => r = x <+> neutral} (monoidNeutralIsNeutralR (inverse $ inverse x)) step3 in
23 replace {P = \r => inverse (inverse x) = r} (monoidNeutralIsNeutralL x) step4
25 replace {P = \r => inverse (inverse x) = r} (monoidNeutralIsNeutralL x) step4
27+||| A proof that -(x + y) = -x - y in any verified abelian group.
25inverseDistributesOverGroupOp : VerifiedAbelianGroup t => (l, r : t) -> inverse (l <+> r) = inverse l <+> inverse r
28inverseDistributesOverGroupOp : VerifiedAbelianGroup t => (l, r : t) -> inverse (l <+> r) = inverse l <+> inverse r
26inverseDistributesOverGroupOp {t} l r =
29inverseDistributesOverGroupOp {t} l r =
27 let step1 = replace {P = \x => x = neutral} (sym $ groupInverseIsInverseL (l <+> r)) $ the (the t neutral = neutral) Refl in
30 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 =
37 let step11 = replace {P = \x => x = inverse r <+> inverse l} (monoidNeutralIsNeutralR (inverse (l <+> r))) step10 in
40 let step11 = replace {P = \x => x = inverse r <+> inverse l} (monoidNeutralIsNeutralR (inverse (l <+> r))) step10 in
38 replace {P = \x => inverse (l <+> r) = x} (abelianGroupOpIsCommutative (inverse r) (inverse l)) step11
41 replace {P = \x => inverse (l <+> r) = x} (abelianGroupOpIsCommutative (inverse r) (inverse l)) step11
43+||| A proof that anything multiplied by zero yields zero back.
40multNeutralAbsorbingL : VerifiedRingWithUnity t => (r : t) -> A.neutral <.> r = A.neutral
44multNeutralAbsorbingL : VerifiedRingWithUnity t => (r : t) -> A.neutral <.> r = A.neutral
41multNeutralAbsorbingL r =
45multNeutralAbsorbingL r =
42 let step1 = the (unity <.> r = r) (ringWithUnityIsUnityR r) in
46 let step1 = the (unity <.> r = r) (ringWithUnityIsUnityR r) in
@@ -48,6 +52,7 @@ multNeutralAbsorbingL r =
48 let step7 = replace {P = \x => neutral <.> r <+> x = x} (groupInverseIsInverseL r) step6 in
52 let step7 = replace {P = \x => neutral <.> r <+> x = x} (groupInverseIsInverseL r) step6 in
49 replace {P = \x => x = neutral} (monoidNeutralIsNeutralL (neutral <.> r)) step7
53 replace {P = \x => x = neutral} (monoidNeutralIsNeutralL (neutral <.> r)) step7
55+||| A proof that anything multiplied by zero yields zero back.
51multNeutralAbsorbingR : VerifiedRingWithUnity t => (l : t) -> l <.> A.neutral = A.neutral
56multNeutralAbsorbingR : VerifiedRingWithUnity t => (l : t) -> l <.> A.neutral = A.neutral
52multNeutralAbsorbingR l =
57multNeutralAbsorbingR l =
53 let step1 = the (l <.> unity = l) (ringWithUnityIsUnityL l) in
58 let step1 = the (l <.> unity = l) (ringWithUnityIsUnityL l) in
@@ -59,6 +64,8 @@ multNeutralAbsorbingR l =
59 let step7 = replace {P = \x => l <.> neutral <+> x = x} (groupInverseIsInverseL l) step6 in
64 let step7 = replace {P = \x => l <.> neutral <+> x = x} (groupInverseIsInverseL l) step6 in
60 replace {P = \x => x = neutral} (monoidNeutralIsNeutralL (l <.> neutral)) step7
65 replace {P = \x => x = neutral} (monoidNeutralIsNeutralL (l <.> neutral)) step7
67+||| A proof that inverse operator can be extracted before multiplication
62multInverseInversesL : VerifiedRingWithUnity t => (l, r : t) -> inverse l <.> r = inverse (l <.> r)
69multInverseInversesL : VerifiedRingWithUnity t => (l, r : t) -> inverse l <.> r = inverse (l <.> r)
63multInverseInversesL l r =
70multInverseInversesL l r =
64 let step1 = replace {P = \x => x <.> r = neutral} (sym $ groupInverseIsInverseL l) (multNeutralAbsorbingL r) in
71 let step1 = replace {P = \x => x <.> r = neutral} (sym $ groupInverseIsInverseL l) (multNeutralAbsorbingL r) in
@@ -69,6 +76,8 @@ multInverseInversesL l r =
69 let step6 = replace {P = \x => x <+> inverse l <.> r = inverse (l <.> r)} (groupInverseIsInverseR (l <.> r)) step5 in
76 let step6 = replace {P = \x => x <+> inverse l <.> r = inverse (l <.> r)} (groupInverseIsInverseR (l <.> r)) step5 in
70 replace {P = \x => x = inverse (l <.> r)} (monoidNeutralIsNeutralR (inverse l <.> r)) step6
77 replace {P = \x => x = inverse (l <.> r)} (monoidNeutralIsNeutralR (inverse l <.> r)) step6
79+||| A proof that inverse operator can be extracted before multiplication
72multInverseInversesR : VerifiedRingWithUnity t => (l, r : t) -> l <.> inverse r = inverse (l <.> r)
81multInverseInversesR : VerifiedRingWithUnity t => (l, r : t) -> l <.> inverse r = inverse (l <.> r)
73multInverseInversesR l r =
82multInverseInversesR l r =
74 let step1 = replace {P = \x => l <.> x = neutral} (sym $ groupInverseIsInverseL r) (multNeutralAbsorbingR l) in
83 let step1 = replace {P = \x => l <.> x = neutral} (sym $ groupInverseIsInverseL r) (multNeutralAbsorbingR l) in
@@ -79,6 +88,8 @@ multInverseInversesR l r =
79 let step6 = replace {P = \x => x <+> l <.> inverse r = inverse (l <.> r)} (groupInverseIsInverseR (l <.> r)) step5 in
88 let step6 = replace {P = \x => x <+> l <.> inverse r = inverse (l <.> r)} (groupInverseIsInverseR (l <.> r)) step5 in
80 replace {P = \x => x = inverse (l <.> r)} (monoidNeutralIsNeutralR (l <.> inverse r)) step6
89 replace {P = \x => x = inverse (l <.> r)} (monoidNeutralIsNeutralR (l <.> inverse r)) step6
91+||| A proof that multiplication of inverses is the same as multiplication of original
92+||| elements. (-x)(-y) = xy
82multNegativeByNegativeIsPositive : VerifiedRingWithUnity t => (l, r : t) -> inverse l <.> inverse r = l <.> r
93multNegativeByNegativeIsPositive : VerifiedRingWithUnity t => (l, r : t) -> inverse l <.> inverse r = l <.> r
83multNegativeByNegativeIsPositive l r =
94multNegativeByNegativeIsPositive l r =
84 rewrite multInverseInversesR (inverse l) r in
95 rewrite multInverseInversesR (inverse l) r in