@@ -6,146 +6,98 @@ import Interfaces.Verified
66
77%access export
88
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
9+||| A prof that -0 = 0 in any verified group.
10+inverseNeutralIsNeutral : VerifiedGroup t => inverse (the t A.neutral) = A.neutral
2611inverseNeutralIsNeutral {t} =
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
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
3117
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
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
6228
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
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
6945
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
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
8758
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
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
10571
106−||| Inverse operator can be extracted before multiplication.
72+||| A proof that inverse operator can be extracted before multiplication
10773||| (-x)y = -(xy)
108−multInverseInversesL : VerifiedRing t => (l, r : t) ->
109− inverse l <.> r = inverse (l <.> r)
74+multInverseInversesL : VerifiedRingWithUnity t => (l, r : t) -> inverse l <.> r = inverse (l <.> r)
11075multInverseInversesL l r =
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
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
12484
125−||| Inverse operator can be extracted before multiplication.
85+||| A proof that inverse operator can be extracted before multiplication
12686||| x(-y) = -(xy)
127−multInverseInversesR : VerifiedRing t => (l, r : t) ->
128− l <.> inverse r = inverse (l <.> r)
87+multInverseInversesR : VerifiedRingWithUnity t => (l, r : t) -> l <.> inverse r = inverse (l <.> r)
12988multInverseInversesR l r =
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
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
14397
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
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
149101multNegativeByNegativeIsPositive l r =
150102 rewrite multInverseInversesR (inverse l) r in
151103 rewrite sym $ multInverseInversesL (inverse l) r in