mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-09-11 08:55:23 +03:00
Simplify proofs of algebra laws
This commit is contained in:
Nick Drozd
parent
1f56ca89e3
commit
76c37e765c
@ -6,98 +6,146 @@ import Interfaces.Verified
|
||||
|
||||
%access export
|
||||
|
||||
||| A prof that -0 = 0 in any verified group.
|
||||
inverseNeutralIsNeutral : VerifiedGroup t => inverse (the t A.neutral) = A.neutral
|
||||
||| -(-x) = x in any verified group.
|
||||
inverseSquaredIsIdentity : VerifiedGroup t => (x : t) ->
|
||||
inverse (inverse x) = x
|
||||
inverseSquaredIsIdentity x =
|
||||
let
|
||||
ix = inverse x
|
||||
iix = inverse ix
|
||||
in
|
||||
rewrite sym $ monoidNeutralIsNeutralR iix in
|
||||
rewrite sym $ groupInverseIsInverseL x in
|
||||
rewrite sym $ semigroupOpIsAssociative x ix iix in
|
||||
rewrite groupInverseIsInverseL ix in
|
||||
monoidNeutralIsNeutralL x
|
||||
|
||||
||| -0 = 0 in any verified group.
|
||||
inverseNeutralIsNeutral : VerifiedGroup t =>
|
||||
inverse (the t A.neutral) = A.neutral
|
||||
inverseNeutralIsNeutral {t} =
|
||||
let zero = the t neutral
|
||||
step1 = cong {f = (<+> inverse zero)} (the (zero = zero) Refl)
|
||||
step2 = replace {P = \x => zero <+> inverse zero = x} (groupInverseIsInverseL zero) step1
|
||||
in
|
||||
replace {P = \x => x = neutral} (monoidNeutralIsNeutralR $ inverse zero) step2
|
||||
let e = the t neutral in
|
||||
rewrite sym $ cong {f = inverse} (groupInverseIsInverseL e) in
|
||||
rewrite monoidNeutralIsNeutralR $ inverse e in
|
||||
inverseSquaredIsIdentity e
|
||||
|
||||
||| A proof that -(-x) = x in any verified group.
|
||||
inverseSquaredIsIdentity : VerifiedGroup t => (x : t) -> inverse (inverse x) = x
|
||||
inverseSquaredIsIdentity {t} x =
|
||||
let zero = the t neutral
|
||||
step1 = cong {f = (x <+>)} (groupInverseIsInverseL (inverse x))
|
||||
step2 = replace {P = \r => r = x <+> neutral} (semigroupOpIsAssociative x (inverse x) (inverse $ inverse x)) step1
|
||||
step3 = replace {P = \r => r <+> inverse (inverse x) = x <+> neutral} (groupInverseIsInverseL x) step2
|
||||
step4 = replace {P = \r => r = x <+> neutral} (monoidNeutralIsNeutralR (inverse $ inverse x)) step3
|
||||
in
|
||||
replace {P = \r => inverse (inverse x) = r} (monoidNeutralIsNeutralL x) step4
|
||||
||| -(x + y) = -y + -x in any verified group.
|
||||
inverseOfSum : VerifiedGroup t => (l, r : t) ->
|
||||
inverse (l <+> r) = inverse r <+> inverse l
|
||||
inverseOfSum {t} l r =
|
||||
let
|
||||
e = the t neutral
|
||||
il = inverse l
|
||||
ir = inverse r
|
||||
sum = l <+> r
|
||||
ilr = inverse sum
|
||||
iril = ir <+> il
|
||||
ile = il <+> e
|
||||
in
|
||||
-- expand
|
||||
rewrite sym $ monoidNeutralIsNeutralR ilr in
|
||||
rewrite sym $ groupInverseIsInverseR r in
|
||||
rewrite sym $ monoidNeutralIsNeutralL ir in
|
||||
rewrite sym $ groupInverseIsInverseR l in
|
||||
-- shuffle
|
||||
rewrite semigroupOpIsAssociative ir il l in
|
||||
rewrite sym $ semigroupOpIsAssociative iril l r in
|
||||
rewrite sym $ semigroupOpIsAssociative iril sum ilr in
|
||||
-- contract
|
||||
rewrite sym $ monoidNeutralIsNeutralL il in
|
||||
rewrite groupInverseIsInverseL sum in
|
||||
rewrite sym $ semigroupOpIsAssociative (ir <+> ile) l ile in
|
||||
rewrite semigroupOpIsAssociative l il e in
|
||||
rewrite groupInverseIsInverseL l in
|
||||
rewrite monoidNeutralIsNeutralL e in
|
||||
Refl
|
||||
|
||||
||| A proof that -(x + y) = -x - y in any verified abelian group.
|
||||
inverseDistributesOverGroupOp : VerifiedAbelianGroup t => (l, r : t) -> inverse (l <+> r) = inverse l <+> inverse r
|
||||
inverseDistributesOverGroupOp {t} l r =
|
||||
let step1 = replace {P = \x => x = neutral} (sym $ groupInverseIsInverseL (l <+> r)) $ the (the t neutral = neutral) Refl
|
||||
step2 = cong {f = ((inverse r) <+>) . ((inverse l) <+>)} step1
|
||||
step3 = replace {P = \x => inverse r <+> (inverse l <+> (l <+> r <+> inverse (l <+> r))) = inverse r <+> x} (monoidNeutralIsNeutralL (inverse l)) step2
|
||||
step4 = replace {P = \x => x = inverse r <+> inverse l} (semigroupOpIsAssociative (inverse r) (inverse l) (l <+> r <+> inverse (l <+> r))) step3
|
||||
step5 = replace {P = \x => x = inverse r <+> inverse l} (semigroupOpIsAssociative (inverse r <+> inverse l) (l <+> r) (inverse (l <+> r))) step4
|
||||
step6 = replace {P = \x => x <+> inverse (l <+> r) = inverse r <+> inverse l} (semigroupOpIsAssociative (inverse r <+> inverse l) l r) step5
|
||||
step7 = replace {P = \x => x <+> r <+> inverse (l <+> r) = inverse r <+> inverse l} (sym $ semigroupOpIsAssociative (inverse r) (inverse l) l) step6
|
||||
step8 = replace {P = \x => inverse r <+> x <+> r <+> inverse (l <+> r) = inverse r <+> inverse l} (groupInverseIsInverseR l) step7
|
||||
step9 = replace {P = \x => x <+> r <+> inverse (l <+> r) = inverse r <+> inverse l} (monoidNeutralIsNeutralL (inverse r)) step8
|
||||
step10 = replace {P = \x => x <+> inverse (l <+> r) = inverse r <+> inverse l} (groupInverseIsInverseR r) step9
|
||||
step11 = replace {P = \x => x = inverse r <+> inverse l} (monoidNeutralIsNeutralR (inverse (l <+> r))) step10
|
||||
in
|
||||
replace {P = \x => inverse (l <+> r) = x} (abelianGroupOpIsCommutative (inverse r) (inverse l)) step11
|
||||
||| -(x + y) = -x + -y in any verified abelian group.
|
||||
inverseDistributesOverGroupOp : VerifiedAbelianGroup t => (l, r : t) ->
|
||||
inverse (l <+> r) = inverse l <+> inverse r
|
||||
inverseDistributesOverGroupOp l r =
|
||||
rewrite abelianGroupOpIsCommutative (inverse l) (inverse r) in
|
||||
inverseOfSum l r
|
||||
|
||||
||| A proof that anything multiplied by zero yields zero back.
|
||||
multNeutralAbsorbingL : VerifiedRingWithUnity t => (r : t) -> A.neutral <.> r = A.neutral
|
||||
multNeutralAbsorbingL r =
|
||||
let step1 = the (unity <.> r = r) (ringWithUnityIsUnityR r)
|
||||
step2 = replace {P = \x => x <.> r = r} (sym $ monoidNeutralIsNeutralR unity) step1
|
||||
step3 = replace {P = \x => x = r} (ringOpIsDistributiveR neutral unity r) step2
|
||||
step4 = replace {P = \x => neutral <.> r <+> x = r} (ringWithUnityIsUnityR r) step3
|
||||
step5 = cong {f = \x => x <+> inverse r} step4
|
||||
step6 = replace {P = \x => x = r <+> inverse r} (sym $ semigroupOpIsAssociative (neutral <.> r) r (inverse r)) step5
|
||||
step7 = replace {P = \x => neutral <.> r <+> x = x} (groupInverseIsInverseL r) step6
|
||||
in
|
||||
replace {P = \x => x = neutral} (monoidNeutralIsNeutralL (neutral <.> r)) step7
|
||||
||| Anything multiplied by zero yields zero back in a verified ring.
|
||||
multNeutralAbsorbingL : VerifiedRing t => (r : t) ->
|
||||
A.neutral <.> r = A.neutral
|
||||
multNeutralAbsorbingL {t} r =
|
||||
let
|
||||
e = the t neutral
|
||||
ir = inverse r
|
||||
exr = e <.> r
|
||||
iexr = inverse exr
|
||||
in
|
||||
rewrite sym $ monoidNeutralIsNeutralR exr in
|
||||
rewrite sym $ groupInverseIsInverseR exr in
|
||||
rewrite sym $ semigroupOpIsAssociative iexr exr ((iexr <+> exr) <.> r) in
|
||||
rewrite groupInverseIsInverseR exr in
|
||||
rewrite sym $ ringOpIsDistributiveR e e r in
|
||||
rewrite monoidNeutralIsNeutralR e in
|
||||
groupInverseIsInverseR exr
|
||||
|
||||
||| A proof that anything multiplied by zero yields zero back.
|
||||
multNeutralAbsorbingR : VerifiedRingWithUnity t => (l : t) -> l <.> A.neutral = A.neutral
|
||||
multNeutralAbsorbingR l =
|
||||
let step1 = the (l <.> unity = l) (ringWithUnityIsUnityL l)
|
||||
step2 = replace {P = \x => l <.> x = l} (sym $ monoidNeutralIsNeutralR unity) step1
|
||||
step3 = replace {P = \x => x = l} (ringOpIsDistributiveL l neutral unity) step2
|
||||
step4 = replace {P = \x => l <.> neutral <+> x = l} (ringWithUnityIsUnityL l) step3
|
||||
step5 = cong {f = \x => x <+> inverse l} step4
|
||||
step6 = replace {P = \x => x = l <+> inverse l} (sym $ semigroupOpIsAssociative (l <.> neutral) l (inverse l)) step5
|
||||
step7 = replace {P = \x => l <.> neutral <+> x = x} (groupInverseIsInverseL l) step6
|
||||
in
|
||||
replace {P = \x => x = neutral} (monoidNeutralIsNeutralL (l <.> neutral)) step7
|
||||
||| Anything multiplied by zero yields zero back in a verified ring.
|
||||
multNeutralAbsorbingR : VerifiedRing t => (l : t) ->
|
||||
l <.> A.neutral = A.neutral
|
||||
multNeutralAbsorbingR {t} l =
|
||||
let
|
||||
e = the t neutral
|
||||
il = inverse l
|
||||
lxe = l <.> e
|
||||
ilxe = inverse lxe
|
||||
in
|
||||
rewrite sym $ monoidNeutralIsNeutralL lxe in
|
||||
rewrite sym $ groupInverseIsInverseL lxe in
|
||||
rewrite semigroupOpIsAssociative (l <.> (lxe <+> ilxe)) lxe ilxe in
|
||||
rewrite groupInverseIsInverseL lxe in
|
||||
rewrite sym $ ringOpIsDistributiveL l e e in
|
||||
rewrite monoidNeutralIsNeutralL e in
|
||||
groupInverseIsInverseL lxe
|
||||
|
||||
||| A proof that inverse operator can be extracted before multiplication
|
||||
||| Inverse operator can be extracted before multiplication.
|
||||
||| (-x)y = -(xy)
|
||||
multInverseInversesL : VerifiedRingWithUnity t => (l, r : t) -> inverse l <.> r = inverse (l <.> r)
|
||||
multInverseInversesL : VerifiedRing t => (l, r : t) ->
|
||||
inverse l <.> r = inverse (l <.> r)
|
||||
multInverseInversesL l r =
|
||||
let step1 = replace {P = \x => x <.> r = neutral} (sym $ groupInverseIsInverseL l) (multNeutralAbsorbingL r)
|
||||
step2 = replace {P = \x => x = neutral} (ringOpIsDistributiveR l (inverse l) r) step1
|
||||
step3 = cong {f = ((inverse (l <.> r)) <+>)} step2
|
||||
step4 = replace {P = \x => inverse (l <.> r) <+> (l <.> r <+> inverse l <.> r) = x} (monoidNeutralIsNeutralL (inverse (l <.> r))) step3
|
||||
step5 = replace {P = \x => x = inverse (l <.> r)} (semigroupOpIsAssociative (inverse (l <.> r)) (l <.> r) (inverse l <.> r)) step4
|
||||
step6 = replace {P = \x => x <+> inverse l <.> r = inverse (l <.> r)} (groupInverseIsInverseR (l <.> r)) step5
|
||||
in
|
||||
replace {P = \x => x = inverse (l <.> r)} (monoidNeutralIsNeutralR (inverse l <.> r)) step6
|
||||
let
|
||||
il = inverse l
|
||||
lxr = l <.> r
|
||||
ilxr = il <.> r
|
||||
i_lxr = inverse lxr
|
||||
in
|
||||
rewrite sym $ monoidNeutralIsNeutralR ilxr in
|
||||
rewrite sym $ groupInverseIsInverseR lxr in
|
||||
rewrite sym $ semigroupOpIsAssociative i_lxr lxr ilxr in
|
||||
rewrite sym $ ringOpIsDistributiveR l il r in
|
||||
rewrite groupInverseIsInverseL l in
|
||||
rewrite multNeutralAbsorbingL r in
|
||||
monoidNeutralIsNeutralL i_lxr
|
||||
|
||||
||| A proof that inverse operator can be extracted before multiplication
|
||||
||| Inverse operator can be extracted before multiplication.
|
||||
||| x(-y) = -(xy)
|
||||
multInverseInversesR : VerifiedRingWithUnity t => (l, r : t) -> l <.> inverse r = inverse (l <.> r)
|
||||
multInverseInversesR : VerifiedRing t => (l, r : t) ->
|
||||
l <.> inverse r = inverse (l <.> r)
|
||||
multInverseInversesR l r =
|
||||
let step1 = replace {P = \x => l <.> x = neutral} (sym $ groupInverseIsInverseL r) (multNeutralAbsorbingR l)
|
||||
step2 = replace {P = \x => x = neutral} (ringOpIsDistributiveL l r (inverse r)) step1
|
||||
step3 = cong {f = ((inverse (l <.> r)) <+>)} step2
|
||||
step4 = replace {P = \x => inverse (l <.> r) <+> (l <.> r <+> l <.> inverse r) = x} (monoidNeutralIsNeutralL (inverse (l <.> r))) step3
|
||||
step5 = replace {P = \x => x = inverse (l <.> r)} (semigroupOpIsAssociative (inverse (l <.> r)) (l <.> r) (l <.> inverse r)) step4
|
||||
step6 = replace {P = \x => x <+> l <.> inverse r = inverse (l <.> r)} (groupInverseIsInverseR (l <.> r)) step5
|
||||
in
|
||||
replace {P = \x => x = inverse (l <.> r)} (monoidNeutralIsNeutralR (l <.> inverse r)) step6
|
||||
let
|
||||
ir = inverse r
|
||||
lxr = l <.> r
|
||||
lxir = l <.> ir
|
||||
ilxr = inverse lxr
|
||||
in
|
||||
rewrite sym $ monoidNeutralIsNeutralL lxir in
|
||||
rewrite sym $ groupInverseIsInverseL lxr in
|
||||
rewrite semigroupOpIsAssociative lxir lxr ilxr in
|
||||
rewrite sym $ ringOpIsDistributiveL l ir r in
|
||||
rewrite groupInverseIsInverseR r in
|
||||
rewrite multNeutralAbsorbingR l in
|
||||
monoidNeutralIsNeutralR ilxr
|
||||
|
||||
||| A proof that multiplication of inverses is the same as multiplication of original
|
||||
||| elements. (-x)(-y) = xy
|
||||
multNegativeByNegativeIsPositive : VerifiedRingWithUnity t => (l, r : t) -> inverse l <.> inverse r = l <.> r
|
||||
||| Multiplication of inverses is the same as multiplication of
|
||||
||| original elements.
|
||||
||| (-x)(-y) = xy
|
||||
multNegativeByNegativeIsPositive : VerifiedRing t => (l, r : t) ->
|
||||
inverse l <.> inverse r = l <.> r
|
||||
multNegativeByNegativeIsPositive l r =
|
||||
rewrite multInverseInversesR (inverse l) r in
|
||||
rewrite sym $ multInverseInversesL (inverse l) r in
|
||||
|
||||
Loading…
Reference in New Issue
Block a user