@@ -6,98 +6,146 @@ import Interfaces.Verified
66
77%access export
88
9−||| A prof that -0 = 0 in any verified group.
10−inverseNeutralIsNeutral : VerifiedGroup t => inverse (the t A.neutral) = A.neutral
9+||| -(-x) = x in any verified group.
10+inverseSquaredIsIdentity : VerifiedGroup t => (x : t) ->
11+ inverse (inverse x) = x
12+inverseSquaredIsIdentity x =
13+ let
14+ ix = inverse x
15+ iix = inverse ix
16+ in
17+ rewrite sym $ monoidNeutralIsNeutralR iix in
18+ rewrite sym $ groupInverseIsInverseL x in
19+ rewrite sym $ semigroupOpIsAssociative x ix iix in
20+ rewrite groupInverseIsInverseL ix in
21+ monoidNeutralIsNeutralL x
22+
23+||| -0 = 0 in any verified group.
24+inverseNeutralIsNeutral : VerifiedGroup t =>
25+ inverse (the t A.neutral) = A.neutral
1126inverseNeutralIsNeutral {t} =
12− let zero = the t neutral
13− step1 = cong {f = (<+> inverse zero)} (the (zero = zero) Refl)
14− step2 = replace {P = \x => zero <+> inverse zero = x} (groupInverseIsInverseL zero) step1
15− in
16− replace {P = \x => x = neutral} (monoidNeutralIsNeutralR $ inverse zero) step2
27+ let e = the t neutral in
28+ rewrite sym $ cong {f = inverse} (groupInverseIsInverseL e) in
29+ rewrite monoidNeutralIsNeutralR $ inverse e in
30+ inverseSquaredIsIdentity e
1731
18−||| A proof that -(-x) = x in any verified group.
19−inverseSquaredIsIdentity : VerifiedGroup t => (x : t) -> inverse (inverse x) = x
20−inverseSquaredIsIdentity {t} x =
21− let zero = the t neutral
22− step1 = cong {f = (x <+>)} (groupInverseIsInverseL (inverse x))
23− step2 = replace {P = \r => r = x <+> neutral} (semigroupOpIsAssociative x (inverse x) (inverse $ inverse x)) step1
24− step3 = replace {P = \r => r <+> inverse (inverse x) = x <+> neutral} (groupInverseIsInverseL x) step2
25− step4 = replace {P = \r => r = x <+> neutral} (monoidNeutralIsNeutralR (inverse $ inverse x)) step3
26− in
27− replace {P = \r => inverse (inverse x) = r} (monoidNeutralIsNeutralL x) step4
32+||| -(x + y) = -y + -x in any verified group.
33+inverseOfSum : VerifiedGroup t => (l, r : t) ->
34+ inverse (l <+> r) = inverse r <+> inverse l
35+inverseOfSum {t} l r =
36+ let
37+ e = the t neutral
38+ il = inverse l
39+ ir = inverse r
40+ sum = l <+> r
41+ ilr = inverse sum
42+ iril = ir <+> il
43+ ile = il <+> e
44+ in
45+ -- expand
46+ rewrite sym $ monoidNeutralIsNeutralR ilr in
47+ rewrite sym $ groupInverseIsInverseR r in
48+ rewrite sym $ monoidNeutralIsNeutralL ir in
49+ rewrite sym $ groupInverseIsInverseR l in
50+ -- shuffle
51+ rewrite semigroupOpIsAssociative ir il l in
52+ rewrite sym $ semigroupOpIsAssociative iril l r in
53+ rewrite sym $ semigroupOpIsAssociative iril sum ilr in
54+ -- contract
55+ rewrite sym $ monoidNeutralIsNeutralL il in
56+ rewrite groupInverseIsInverseL sum in
57+ rewrite sym $ semigroupOpIsAssociative (ir <+> ile) l ile in
58+ rewrite semigroupOpIsAssociative l il e in
59+ rewrite groupInverseIsInverseL l in
60+ rewrite monoidNeutralIsNeutralL e in
61+ Refl
2862
29−||| A proof that -(x + y) = -x - y in any verified abelian group.
30−inverseDistributesOverGroupOp : VerifiedAbelianGroup t => (l, r : t) -> inverse (l <+> r) = inverse l <+> inverse r
31−inverseDistributesOverGroupOp {t} l r =
32− let step1 = replace {P = \x => x = neutral} (sym $ groupInverseIsInverseL (l <+> r)) $ the (the t neutral = neutral) Refl
33− step2 = cong {f = ((inverse r) <+>) . ((inverse l) <+>)} step1
34− step3 = replace {P = \x => inverse r <+> (inverse l <+> (l <+> r <+> inverse (l <+> r))) = inverse r <+> x} (monoidNeutralIsNeutralL (inverse l)) step2
35− step4 = replace {P = \x => x = inverse r <+> inverse l} (semigroupOpIsAssociative (inverse r) (inverse l) (l <+> r <+> inverse (l <+> r))) step3
36− step5 = replace {P = \x => x = inverse r <+> inverse l} (semigroupOpIsAssociative (inverse r <+> inverse l) (l <+> r) (inverse (l <+> r))) step4
37− step6 = replace {P = \x => x <+> inverse (l <+> r) = inverse r <+> inverse l} (semigroupOpIsAssociative (inverse r <+> inverse l) l r) step5
38− step7 = replace {P = \x => x <+> r <+> inverse (l <+> r) = inverse r <+> inverse l} (sym $ semigroupOpIsAssociative (inverse r) (inverse l) l) step6
39− step8 = replace {P = \x => inverse r <+> x <+> r <+> inverse (l <+> r) = inverse r <+> inverse l} (groupInverseIsInverseR l) step7
40− step9 = replace {P = \x => x <+> r <+> inverse (l <+> r) = inverse r <+> inverse l} (monoidNeutralIsNeutralL (inverse r)) step8
41− step10 = replace {P = \x => x <+> inverse (l <+> r) = inverse r <+> inverse l} (groupInverseIsInverseR r) step9
42− step11 = replace {P = \x => x = inverse r <+> inverse l} (monoidNeutralIsNeutralR (inverse (l <+> r))) step10
43− in
44− replace {P = \x => inverse (l <+> r) = x} (abelianGroupOpIsCommutative (inverse r) (inverse l)) step11
63+||| -(x + y) = -x + -y in any verified abelian group.
64+inverseDistributesOverGroupOp : VerifiedAbelianGroup t => (l, r : t) ->
65+ inverse (l <+> r) = inverse l <+> inverse r
66+inverseDistributesOverGroupOp l r =
67+ rewrite abelianGroupOpIsCommutative (inverse l) (inverse r) in
68+ inverseOfSum l r
4569
46−||| A proof that anything multiplied by zero yields zero back.
47−multNeutralAbsorbingL : VerifiedRingWithUnity t => (r : t) -> A.neutral <.> r = A.neutral
48−multNeutralAbsorbingL r =
49− let step1 = the (unity <.> r = r) (ringWithUnityIsUnityR r)
50− step2 = replace {P = \x => x <.> r = r} (sym $ monoidNeutralIsNeutralR unity) step1
51− step3 = replace {P = \x => x = r} (ringOpIsDistributiveR neutral unity r) step2
52− step4 = replace {P = \x => neutral <.> r <+> x = r} (ringWithUnityIsUnityR r) step3
53− step5 = cong {f = \x => x <+> inverse r} step4
54− step6 = replace {P = \x => x = r <+> inverse r} (sym $ semigroupOpIsAssociative (neutral <.> r) r (inverse r)) step5
55− step7 = replace {P = \x => neutral <.> r <+> x = x} (groupInverseIsInverseL r) step6
56− in
57− replace {P = \x => x = neutral} (monoidNeutralIsNeutralL (neutral <.> r)) step7
70+||| Anything multiplied by zero yields zero back in a verified ring.
71+multNeutralAbsorbingL : VerifiedRing t => (r : t) ->
72+ A.neutral <.> r = A.neutral
73+multNeutralAbsorbingL {t} r =
74+ let
75+ e = the t neutral
76+ ir = inverse r
77+ exr = e <.> r
78+ iexr = inverse exr
79+ in
80+ rewrite sym $ monoidNeutralIsNeutralR exr in
81+ rewrite sym $ groupInverseIsInverseR exr in
82+ rewrite sym $ semigroupOpIsAssociative iexr exr ((iexr <+> exr) <.> r) in
83+ rewrite groupInverseIsInverseR exr in
84+ rewrite sym $ ringOpIsDistributiveR e e r in
85+ rewrite monoidNeutralIsNeutralR e in
86+ groupInverseIsInverseR exr
5887
59−||| A proof that anything multiplied by zero yields zero back.
60−multNeutralAbsorbingR : VerifiedRingWithUnity t => (l : t) -> l <.> A.neutral = A.neutral
61−multNeutralAbsorbingR l =
62− let step1 = the (l <.> unity = l) (ringWithUnityIsUnityL l)
63− step2 = replace {P = \x => l <.> x = l} (sym $ monoidNeutralIsNeutralR unity) step1
64− step3 = replace {P = \x => x = l} (ringOpIsDistributiveL l neutral unity) step2
65− step4 = replace {P = \x => l <.> neutral <+> x = l} (ringWithUnityIsUnityL l) step3
66− step5 = cong {f = \x => x <+> inverse l} step4
67− step6 = replace {P = \x => x = l <+> inverse l} (sym $ semigroupOpIsAssociative (l <.> neutral) l (inverse l)) step5
68− step7 = replace {P = \x => l <.> neutral <+> x = x} (groupInverseIsInverseL l) step6
69− in
70− replace {P = \x => x = neutral} (monoidNeutralIsNeutralL (l <.> neutral)) step7
88+||| Anything multiplied by zero yields zero back in a verified ring.
89+multNeutralAbsorbingR : VerifiedRing t => (l : t) ->
90+ l <.> A.neutral = A.neutral
91+multNeutralAbsorbingR {t} l =
92+ let
93+ e = the t neutral
94+ il = inverse l
95+ lxe = l <.> e
96+ ilxe = inverse lxe
97+ in
98+ rewrite sym $ monoidNeutralIsNeutralL lxe in
99+ rewrite sym $ groupInverseIsInverseL lxe in
100+ rewrite semigroupOpIsAssociative (l <.> (lxe <+> ilxe)) lxe ilxe in
101+ rewrite groupInverseIsInverseL lxe in
102+ rewrite sym $ ringOpIsDistributiveL l e e in
103+ rewrite monoidNeutralIsNeutralL e in
104+ groupInverseIsInverseL lxe
71105
72−||| A proof that inverse operator can be extracted before multiplication
106+||| Inverse operator can be extracted before multiplication.
73107||| (-x)y = -(xy)
74−multInverseInversesL : VerifiedRingWithUnity t => (l, r : t) -> inverse l <.> r = inverse (l <.> r)
108+multInverseInversesL : VerifiedRing t => (l, r : t) ->
109+ inverse l <.> r = inverse (l <.> r)
75110multInverseInversesL l r =
76− let step1 = replace {P = \x => x <.> r = neutral} (sym $ groupInverseIsInverseL l) (multNeutralAbsorbingL r)
77− step2 = replace {P = \x => x = neutral} (ringOpIsDistributiveR l (inverse l) r) step1
78− step3 = cong {f = ((inverse (l <.> r)) <+>)} step2
79− step4 = replace {P = \x => inverse (l <.> r) <+> (l <.> r <+> inverse l <.> r) = x} (monoidNeutralIsNeutralL (inverse (l <.> r))) step3
80− step5 = replace {P = \x => x = inverse (l <.> r)} (semigroupOpIsAssociative (inverse (l <.> r)) (l <.> r) (inverse l <.> r)) step4
81− step6 = replace {P = \x => x <+> inverse l <.> r = inverse (l <.> r)} (groupInverseIsInverseR (l <.> r)) step5
82− in
83− replace {P = \x => x = inverse (l <.> r)} (monoidNeutralIsNeutralR (inverse l <.> r)) step6
111+ let
112+ il = inverse l
113+ lxr = l <.> r
114+ ilxr = il <.> r
115+ i_lxr = inverse lxr
116+ in
117+ rewrite sym $ monoidNeutralIsNeutralR ilxr in
118+ rewrite sym $ groupInverseIsInverseR lxr in
119+ rewrite sym $ semigroupOpIsAssociative i_lxr lxr ilxr in
120+ rewrite sym $ ringOpIsDistributiveR l il r in
121+ rewrite groupInverseIsInverseL l in
122+ rewrite multNeutralAbsorbingL r in
123+ monoidNeutralIsNeutralL i_lxr
84124
85−||| A proof that inverse operator can be extracted before multiplication
125+||| Inverse operator can be extracted before multiplication.
86126||| x(-y) = -(xy)
87−multInverseInversesR : VerifiedRingWithUnity t => (l, r : t) -> l <.> inverse r = inverse (l <.> r)
127+multInverseInversesR : VerifiedRing t => (l, r : t) ->
128+ l <.> inverse r = inverse (l <.> r)
88129multInverseInversesR l r =
89− let step1 = replace {P = \x => l <.> x = neutral} (sym $ groupInverseIsInverseL r) (multNeutralAbsorbingR l)
90− step2 = replace {P = \x => x = neutral} (ringOpIsDistributiveL l r (inverse r)) step1
91− step3 = cong {f = ((inverse (l <.> r)) <+>)} step2
92− step4 = replace {P = \x => inverse (l <.> r) <+> (l <.> r <+> l <.> inverse r) = x} (monoidNeutralIsNeutralL (inverse (l <.> r))) step3
93− step5 = replace {P = \x => x = inverse (l <.> r)} (semigroupOpIsAssociative (inverse (l <.> r)) (l <.> r) (l <.> inverse r)) step4
94− step6 = replace {P = \x => x <+> l <.> inverse r = inverse (l <.> r)} (groupInverseIsInverseR (l <.> r)) step5
95− in
96− replace {P = \x => x = inverse (l <.> r)} (monoidNeutralIsNeutralR (l <.> inverse r)) step6
130+ let
131+ ir = inverse r
132+ lxr = l <.> r
133+ lxir = l <.> ir
134+ ilxr = inverse lxr
135+ in
136+ rewrite sym $ monoidNeutralIsNeutralL lxir in
137+ rewrite sym $ groupInverseIsInverseL lxr in
138+ rewrite semigroupOpIsAssociative lxir lxr ilxr in
139+ rewrite sym $ ringOpIsDistributiveL l ir r in
140+ rewrite groupInverseIsInverseR r in
141+ rewrite multNeutralAbsorbingR l in
142+ monoidNeutralIsNeutralR ilxr
97143
98−||| A proof that multiplication of inverses is the same as multiplication of original
99−||| elements. (-x)(-y) = xy
100−multNegativeByNegativeIsPositive : VerifiedRingWithUnity t => (l, r : t) -> inverse l <.> inverse r = l <.> r
144+||| Multiplication of inverses is the same as multiplication of
145+||| original elements.
146+||| (-x)(-y) = xy
147+multNegativeByNegativeIsPositive : VerifiedRing t => (l, r : t) ->
148+ inverse l <.> inverse r = l <.> r
101149multNegativeByNegativeIsPositive l r =
102150 rewrite multInverseInversesR (inverse l) r in
103151 rewrite sym $ multInverseInversesL (inverse l) r in