@@ -9,83 +9,90 @@ import Interfaces.Verified
9||| A prof that -0 = 0 in any verified group.
9||| A prof that -0 = 0 in any verified group.
10inverseNeutralIsNeutral : VerifiedGroup t => inverse (the t A.neutral) = A.neutral
10inverseNeutralIsNeutral : VerifiedGroup t => inverse (the t A.neutral) = A.neutral
11inverseNeutralIsNeutral {t} =
11inverseNeutralIsNeutral {t} =
12− let zero = the t neutral in
12+ let zero = the t neutral
13− let step1 = cong {f = (<+> inverse zero)} (the (zero = zero) Refl) in
13+ step1 = cong {f = (<+> inverse zero)} (the (zero = zero) Refl)
14− let step2 = replace {P = \x => zero <+> inverse zero = x} (groupInverseIsInverseL zero) step1 in
14+ step2 = replace {P = \x => zero <+> inverse zero = x} (groupInverseIsInverseL zero) step1
15 replace {P = \x => x = neutral} (monoidNeutralIsNeutralR $ inverse zero) step2
16 replace {P = \x => x = neutral} (monoidNeutralIsNeutralR $ inverse zero) step2
17||| A proof that -(-x) = x in any verified group.
18||| A proof that -(-x) = x in any verified group.
18inverseSquaredIsIdentity : VerifiedGroup t => (x : t) -> inverse (inverse x) = x
19inverseSquaredIsIdentity : VerifiedGroup t => (x : t) -> inverse (inverse x) = x
19inverseSquaredIsIdentity {t} x =
20inverseSquaredIsIdentity {t} x =
20− let zero = the t neutral in
21+ let zero = the t neutral
21− let step1 = cong {f = (x <+>)} (groupInverseIsInverseL (inverse x)) in
22+ step1 = cong {f = (x <+>)} (groupInverseIsInverseL (inverse x))
22− let step2 = replace {P = \r => r = x <+> neutral} (semigroupOpIsAssociative x (inverse x) (inverse $ inverse x)) step1 in
23+ step2 = replace {P = \r => r = x <+> neutral} (semigroupOpIsAssociative x (inverse x) (inverse $ inverse x)) step1
23− let step3 = replace {P = \r => r <+> inverse (inverse x) = x <+> neutral} (groupInverseIsInverseL x) step2 in
24+ step3 = replace {P = \r => r <+> inverse (inverse x) = x <+> neutral} (groupInverseIsInverseL x) step2
24− let step4 = replace {P = \r => r = x <+> neutral} (monoidNeutralIsNeutralR (inverse $ inverse x)) step3 in
25+ step4 = replace {P = \r => r = x <+> neutral} (monoidNeutralIsNeutralR (inverse $ inverse x)) step3
25 replace {P = \r => inverse (inverse x) = r} (monoidNeutralIsNeutralL x) step4
27 replace {P = \r => inverse (inverse x) = r} (monoidNeutralIsNeutralL x) step4
27||| A proof that -(x + y) = -x - y in any verified abelian group.
29||| A proof that -(x + y) = -x - y in any verified abelian group.
28inverseDistributesOverGroupOp : VerifiedAbelianGroup t => (l, r : t) -> inverse (l <+> r) = inverse l <+> inverse r
30inverseDistributesOverGroupOp : VerifiedAbelianGroup t => (l, r : t) -> inverse (l <+> r) = inverse l <+> inverse r
29inverseDistributesOverGroupOp {t} l r =
31inverseDistributesOverGroupOp {t} l r =
30− let step1 = replace {P = \x => x = neutral} (sym $ groupInverseIsInverseL (l <+> r)) $ the (the t neutral = neutral) Refl in
32+ let step1 = replace {P = \x => x = neutral} (sym $ groupInverseIsInverseL (l <+> r)) $ the (the t neutral = neutral) Refl
31− let step2 = cong {f = ((inverse r) <+>) . ((inverse l) <+>)} step1 in
33+ step2 = cong {f = ((inverse r) <+>) . ((inverse l) <+>)} step1
32− let step3 = replace {P = \x => inverse r <+> (inverse l <+> (l <+> r <+> inverse (l <+> r))) = inverse r <+> x} (monoidNeutralIsNeutralL (inverse l)) step2 in
34+ step3 = replace {P = \x => inverse r <+> (inverse l <+> (l <+> r <+> inverse (l <+> r))) = inverse r <+> x} (monoidNeutralIsNeutralL (inverse l)) step2
33− let step4 = replace {P = \x => x = inverse r <+> inverse l} (semigroupOpIsAssociative (inverse r) (inverse l) (l <+> r <+> inverse (l <+> r))) step3 in
35+ step4 = replace {P = \x => x = inverse r <+> inverse l} (semigroupOpIsAssociative (inverse r) (inverse l) (l <+> r <+> inverse (l <+> r))) step3
34− let step5 = replace {P = \x => x = inverse r <+> inverse l} (semigroupOpIsAssociative (inverse r <+> inverse l) (l <+> r) (inverse (l <+> r))) step4 in
36+ step5 = replace {P = \x => x = inverse r <+> inverse l} (semigroupOpIsAssociative (inverse r <+> inverse l) (l <+> r) (inverse (l <+> r))) step4
35− let step6 = replace {P = \x => x <+> inverse (l <+> r) = inverse r <+> inverse l} (semigroupOpIsAssociative (inverse r <+> inverse l) l r) step5 in
37+ step6 = replace {P = \x => x <+> inverse (l <+> r) = inverse r <+> inverse l} (semigroupOpIsAssociative (inverse r <+> inverse l) l r) step5
36− let step7 = replace {P = \x => x <+> r <+> inverse (l <+> r) = inverse r <+> inverse l} (sym $ semigroupOpIsAssociative (inverse r) (inverse l) l) step6 in
38+ step7 = replace {P = \x => x <+> r <+> inverse (l <+> r) = inverse r <+> inverse l} (sym $ semigroupOpIsAssociative (inverse r) (inverse l) l) step6
37− let step8 = replace {P = \x => inverse r <+> x <+> r <+> inverse (l <+> r) = inverse r <+> inverse l} (groupInverseIsInverseR l) step7 in
39+ step8 = replace {P = \x => inverse r <+> x <+> r <+> inverse (l <+> r) = inverse r <+> inverse l} (groupInverseIsInverseR l) step7
38− let step9 = replace {P = \x => x <+> r <+> inverse (l <+> r) = inverse r <+> inverse l} (monoidNeutralIsNeutralL (inverse r)) step8 in
40+ step9 = replace {P = \x => x <+> r <+> inverse (l <+> r) = inverse r <+> inverse l} (monoidNeutralIsNeutralL (inverse r)) step8
39− let step10 = replace {P = \x => x <+> inverse (l <+> r) = inverse r <+> inverse l} (groupInverseIsInverseR r) step9 in
41+ step10 = replace {P = \x => x <+> inverse (l <+> r) = inverse r <+> inverse l} (groupInverseIsInverseR r) step9
40− let step11 = replace {P = \x => x = inverse r <+> inverse l} (monoidNeutralIsNeutralR (inverse (l <+> r))) step10 in
42+ step11 = replace {P = \x => x = inverse r <+> inverse l} (monoidNeutralIsNeutralR (inverse (l <+> r))) step10
41 replace {P = \x => inverse (l <+> r) = x} (abelianGroupOpIsCommutative (inverse r) (inverse l)) step11
44 replace {P = \x => inverse (l <+> r) = x} (abelianGroupOpIsCommutative (inverse r) (inverse l)) step11
43||| A proof that anything multiplied by zero yields zero back.
46||| A proof that anything multiplied by zero yields zero back.
44multNeutralAbsorbingL : VerifiedRingWithUnity t => (r : t) -> A.neutral <.> r = A.neutral
47multNeutralAbsorbingL : VerifiedRingWithUnity t => (r : t) -> A.neutral <.> r = A.neutral
45multNeutralAbsorbingL r =
48multNeutralAbsorbingL r =
46− let step1 = the (unity <.> r = r) (ringWithUnityIsUnityR r) in
49+ let step1 = the (unity <.> r = r) (ringWithUnityIsUnityR r)
47− let step2 = replace {P = \x => x <.> r = r} (sym $ monoidNeutralIsNeutralR unity) step1 in
50+ step2 = replace {P = \x => x <.> r = r} (sym $ monoidNeutralIsNeutralR unity) step1
48− let step3 = replace {P = \x => x = r} (ringOpIsDistributiveR neutral unity r) step2 in
51+ step3 = replace {P = \x => x = r} (ringOpIsDistributiveR neutral unity r) step2
49− let step4 = replace {P = \x => neutral <.> r <+> x = r} (ringWithUnityIsUnityR r) step3 in
52+ step4 = replace {P = \x => neutral <.> r <+> x = r} (ringWithUnityIsUnityR r) step3
50− let step5 = cong {f = \x => x <+> inverse r} step4 in
53+ step5 = cong {f = \x => x <+> inverse r} step4
51− let step6 = replace {P = \x => x = r <+> inverse r} (sym $ semigroupOpIsAssociative (neutral <.> r) r (inverse r)) step5 in
54+ step6 = replace {P = \x => x = r <+> inverse r} (sym $ semigroupOpIsAssociative (neutral <.> r) r (inverse r)) step5
52− let step7 = replace {P = \x => neutral <.> r <+> x = x} (groupInverseIsInverseL r) step6 in
55+ step7 = replace {P = \x => neutral <.> r <+> x = x} (groupInverseIsInverseL r) step6
53 replace {P = \x => x = neutral} (monoidNeutralIsNeutralL (neutral <.> r)) step7
57 replace {P = \x => x = neutral} (monoidNeutralIsNeutralL (neutral <.> r)) step7
55||| A proof that anything multiplied by zero yields zero back.
59||| A proof that anything multiplied by zero yields zero back.
56multNeutralAbsorbingR : VerifiedRingWithUnity t => (l : t) -> l <.> A.neutral = A.neutral
60multNeutralAbsorbingR : VerifiedRingWithUnity t => (l : t) -> l <.> A.neutral = A.neutral
57multNeutralAbsorbingR l =
61multNeutralAbsorbingR l =
58− let step1 = the (l <.> unity = l) (ringWithUnityIsUnityL l) in
62+ let step1 = the (l <.> unity = l) (ringWithUnityIsUnityL l)
59− let step2 = replace {P = \x => l <.> x = l} (sym $ monoidNeutralIsNeutralR unity) step1 in
63+ step2 = replace {P = \x => l <.> x = l} (sym $ monoidNeutralIsNeutralR unity) step1
60− let step3 = replace {P = \x => x = l} (ringOpIsDistributiveL l neutral unity) step2 in
64+ step3 = replace {P = \x => x = l} (ringOpIsDistributiveL l neutral unity) step2
61− let step4 = replace {P = \x => l <.> neutral <+> x = l} (ringWithUnityIsUnityL l) step3 in
65+ step4 = replace {P = \x => l <.> neutral <+> x = l} (ringWithUnityIsUnityL l) step3
62− let step5 = cong {f = \x => x <+> inverse l} step4 in
66+ step5 = cong {f = \x => x <+> inverse l} step4
63− let step6 = replace {P = \x => x = l <+> inverse l} (sym $ semigroupOpIsAssociative (l <.> neutral) l (inverse l)) step5 in
67+ step6 = replace {P = \x => x = l <+> inverse l} (sym $ semigroupOpIsAssociative (l <.> neutral) l (inverse l)) step5
64− let step7 = replace {P = \x => l <.> neutral <+> x = x} (groupInverseIsInverseL l) step6 in
68+ step7 = replace {P = \x => l <.> neutral <+> x = x} (groupInverseIsInverseL l) step6
65 replace {P = \x => x = neutral} (monoidNeutralIsNeutralL (l <.> neutral)) step7
70 replace {P = \x => x = neutral} (monoidNeutralIsNeutralL (l <.> neutral)) step7
67||| A proof that inverse operator can be extracted before multiplication
72||| A proof that inverse operator can be extracted before multiplication
68||| (-x)y = -(xy)
73||| (-x)y = -(xy)
69multInverseInversesL : VerifiedRingWithUnity t => (l, r : t) -> inverse l <.> r = inverse (l <.> r)
74multInverseInversesL : VerifiedRingWithUnity t => (l, r : t) -> inverse l <.> r = inverse (l <.> r)
70multInverseInversesL l r =
75multInverseInversesL l r =
71− let step1 = replace {P = \x => x <.> r = neutral} (sym $ groupInverseIsInverseL l) (multNeutralAbsorbingL r) in
76+ let step1 = replace {P = \x => x <.> r = neutral} (sym $ groupInverseIsInverseL l) (multNeutralAbsorbingL r)
72− let step2 = replace {P = \x => x = neutral} (ringOpIsDistributiveR l (inverse l) r) step1 in
77+ step2 = replace {P = \x => x = neutral} (ringOpIsDistributiveR l (inverse l) r) step1
73− let step3 = cong {f = ((inverse (l <.> r)) <+>)} step2 in
78+ step3 = cong {f = ((inverse (l <.> r)) <+>)} step2
74− let step4 = replace {P = \x => inverse (l <.> r) <+> (l <.> r <+> inverse l <.> r) = x} (monoidNeutralIsNeutralL (inverse (l <.> r))) step3 in
79+ step4 = replace {P = \x => inverse (l <.> r) <+> (l <.> r <+> inverse l <.> r) = x} (monoidNeutralIsNeutralL (inverse (l <.> r))) step3
75− let step5 = replace {P = \x => x = inverse (l <.> r)} (semigroupOpIsAssociative (inverse (l <.> r)) (l <.> r) (inverse l <.> r)) step4 in
80+ step5 = replace {P = \x => x = inverse (l <.> r)} (semigroupOpIsAssociative (inverse (l <.> r)) (l <.> r) (inverse l <.> r)) step4
76− let step6 = replace {P = \x => x <+> inverse l <.> r = inverse (l <.> r)} (groupInverseIsInverseR (l <.> r)) step5 in
81+ step6 = replace {P = \x => x <+> inverse l <.> r = inverse (l <.> r)} (groupInverseIsInverseR (l <.> r)) step5
77 replace {P = \x => x = inverse (l <.> r)} (monoidNeutralIsNeutralR (inverse l <.> r)) step6
83 replace {P = \x => x = inverse (l <.> r)} (monoidNeutralIsNeutralR (inverse l <.> r)) step6
79||| A proof that inverse operator can be extracted before multiplication
85||| A proof that inverse operator can be extracted before multiplication
80||| x(-y) = -(xy)
86||| x(-y) = -(xy)
81multInverseInversesR : VerifiedRingWithUnity t => (l, r : t) -> l <.> inverse r = inverse (l <.> r)
87multInverseInversesR : VerifiedRingWithUnity t => (l, r : t) -> l <.> inverse r = inverse (l <.> r)
82multInverseInversesR l r =
88multInverseInversesR l r =
83− let step1 = replace {P = \x => l <.> x = neutral} (sym $ groupInverseIsInverseL r) (multNeutralAbsorbingR l) in
89+ let step1 = replace {P = \x => l <.> x = neutral} (sym $ groupInverseIsInverseL r) (multNeutralAbsorbingR l)
84− let step2 = replace {P = \x => x = neutral} (ringOpIsDistributiveL l r (inverse r)) step1 in
90+ step2 = replace {P = \x => x = neutral} (ringOpIsDistributiveL l r (inverse r)) step1
85− let step3 = cong {f = ((inverse (l <.> r)) <+>)} step2 in
91+ step3 = cong {f = ((inverse (l <.> r)) <+>)} step2
86− let step4 = replace {P = \x => inverse (l <.> r) <+> (l <.> r <+> l <.> inverse r) = x} (monoidNeutralIsNeutralL (inverse (l <.> r))) step3 in
92+ step4 = replace {P = \x => inverse (l <.> r) <+> (l <.> r <+> l <.> inverse r) = x} (monoidNeutralIsNeutralL (inverse (l <.> r))) step3
87− let step5 = replace {P = \x => x = inverse (l <.> r)} (semigroupOpIsAssociative (inverse (l <.> r)) (l <.> r) (l <.> inverse r)) step4 in
93+ step5 = replace {P = \x => x = inverse (l <.> r)} (semigroupOpIsAssociative (inverse (l <.> r)) (l <.> r) (l <.> inverse r)) step4
88− let step6 = replace {P = \x => x <+> l <.> inverse r = inverse (l <.> r)} (groupInverseIsInverseR (l <.> r)) step5 in
94+ step6 = replace {P = \x => x <+> l <.> inverse r = inverse (l <.> r)} (groupInverseIsInverseR (l <.> r)) step5
89 replace {P = \x => x = inverse (l <.> r)} (monoidNeutralIsNeutralR (l <.> inverse r)) step6
96 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
98||| A proof that multiplication of inverses is the same as multiplication of original