Merge pull request #4820 from nickdrozd/reverse

More proofs, simpler proofs
idris-lang · Mar 14, 2020 · 93cfe98 · 93cfe98
2 parents 853e453 + 8684dae
commit 93cfe98
Show file tree

Hide file tree

Showing 7 changed files with 267 additions and 178 deletions.
diff --git a/docs/reference/misc.rst b/docs/reference/misc.rst
@@ -115,11 +115,11 @@ Here is an example:
     import Syntax.PreorderReasoning
     multThree : (a, b, c : Nat) -> a * b * c = c * a * b
     multThree a b c =
-      (a * b * c) ={ sym (multAssociative a b c) }=
-      (a * (b * c)) ={ cong (multCommutative b c) }=
-      (a * (c * b)) ={ multAssociative a c b }=
-      (a * c * b) ={ cong {f = (* b)} (multCommutative a c) }=
-      (c * a * b) QED
+      (a * b * c)	={ sym (multAssociative a b c) }=
+      (a * (b * c))	={ cong (multCommutative b c) }=
+      (a * (c * b))	={ multAssociative a c b }=
+      (a * c * b)	={ cong {f = (* b)} (multCommutative a c) }=
+      (c * a * b)	QED
 
 Note that the parentheses are required -- only a simple expression can
 be on the left of ``={ }=`` or ``QED``. Also, when using preorder

diff --git a/libs/base/Control/Isomorphism.idr b/libs/base/Control/Isomorphism.idr
@@ -17,21 +17,22 @@ record Iso a b where
 
 -- Isomorphism properties
 
-||| Isomorphism is Reflexive
+||| Isomorphism is reflexive
 isoRefl : Iso a a
-isoRefl = MkIso id id (\x => Refl) (\x => Refl)
+isoRefl = MkIso id id (\_ => Refl) (\_ => Refl)
 
 ||| Isomorphism is transitive
 isoTrans : Iso a b -> Iso b c -> Iso a c
 isoTrans (MkIso to from toFrom fromTo) (MkIso to' from' toFrom' fromTo') =
-  MkIso (\x => to' (to x))
-        (\y => from (from' y))
-        (\y => (to' (to (from (from' y))))  ={ cong (toFrom (from' y)) }=
-               (to' (from' y))              ={ toFrom' y               }=
-               y                            QED)
-        (\x => (from (from' (to' (to x))))  ={ cong (fromTo' (to x)) }=
-               (from (to x))                ={ fromTo x              }=
-               x                            QED)
+  MkIso xto xfrom xtoFrom xfromTo where
+    xto : a -> c
+    xto = to' . to
+    xfrom : c -> a
+    xfrom = from . from'
+    xtoFrom : (z : c) -> xto (xfrom z) = z
+    xtoFrom z = rewrite toFrom $ from' z in toFrom' z
+    xfromTo : (x : a) -> xfrom (xto x) = x
+    xfromTo x = rewrite fromTo' (to x) in fromTo x
 
 Category Iso where
   id = isoRefl
@@ -99,8 +100,7 @@ eitherBotRight = isoTrans eitherComm eitherBotLeft
 
 ||| Isomorphism is a congruence with regards to disjunction
 eitherCong : Iso a a' -> Iso b b' -> Iso (Either a b) (Either a' b')
-eitherCong {a = a} {a' = a'} {b = b} {b' = b'}
-           (MkIso to from toFrom fromTo)
+eitherCong (MkIso to from toFrom fromTo)
            (MkIso to' from' toFrom' fromTo') =
   MkIso (eitherMap to to') (eitherMap from from') ok1 ok2
     where eitherMap : (c -> c') -> (d -> d') -> Either c d -> Either c' d'
@@ -143,9 +143,7 @@ pairAssoc = MkIso to from ok1 ok2
 
 ||| Conjunction with truth is a no-op
 pairUnitRight : Iso (a, ()) a
-pairUnitRight = MkIso fst (\x => (x, ())) (\x => Refl) ok
-  where ok : (x : (a, ())) -> (fst x, ()) = x
-        ok (x, ()) = Refl
+pairUnitRight = MkIso fst (\x => (x, ())) (\_ => Refl) (\(_, ()) => Refl)
 
 ||| Conjunction with truth is a no-op
 pairUnitLeft : Iso ((), a) a
@@ -161,8 +159,7 @@ pairBotRight = isoTrans pairComm pairBotLeft
 
 ||| Isomorphism is a congruence with regards to conjunction
 pairCong : Iso a a' -> Iso b b' -> Iso (a, b) (a', b')
-pairCong {a = a} {a' = a'} {b = b} {b' = b'}
-         (MkIso to from toFrom fromTo)
+pairCong (MkIso to from toFrom fromTo)
          (MkIso to' from' toFrom' fromTo') =
   MkIso to'' from'' iso1 iso2
     where to'' : (a, b) -> (a', b')
@@ -205,7 +202,7 @@ distribLeft = MkIso to from toFrom fromTo
 
 ||| Products distribute over sums
 distribRight : Iso (a, Either b c) (Either (a, b) (a, c))
-distribRight {a} {b} {c} = (pairComm `isoTrans` distribLeft) `isoTrans` eitherCong pairComm pairComm
+distribRight = (pairComm `isoTrans` distribLeft) `isoTrans` eitherCong pairComm pairComm
 
 
 -- Enable preorder reasoning syntax over isomorphisms
@@ -222,7 +219,7 @@ step a iso1 iso2 = isoTrans iso1 iso2
 -- Isomorphisms over Maybe
 ||| Isomorphism is a congruence with respect to Maybe
 maybeCong : Iso a b -> Iso (Maybe a) (Maybe b)
-maybeCong {a} {b} (MkIso to from toFrom fromTo) = MkIso (map to) (map from) ok1 ok2
+maybeCong (MkIso to from toFrom fromTo) = MkIso (map to) (map from) ok1 ok2
   where ok1 : (y : Maybe b) -> map to (map from y) = y
         ok1 Nothing = Refl
         ok1 (Just x) = (Just (to (from x))) ={ cong (toFrom x) }= (Just x) QED
@@ -253,7 +250,7 @@ maybeVoidUnit = (Maybe Void)     ={ maybeEither   }=
                 ()              QED
 
 eitherMaybeLeftMaybe : Iso (Either (Maybe a) b) (Maybe (Either a b))
-eitherMaybeLeftMaybe {a} {b} =
+eitherMaybeLeftMaybe =
   (Either (Maybe a) b)     ={ eitherCongLeft maybeEither }=
   (Either (Either a ()) b) ={ eitherAssoc                }=
   (Either a (Either () b)) ={ eitherCongRight eitherComm }=
@@ -263,7 +260,7 @@ eitherMaybeLeftMaybe {a} {b} =
 
 
 eitherMaybeRightMaybe : Iso (Either a (Maybe b)) (Maybe (Either a b))
-eitherMaybeRightMaybe {a} {b} =
+eitherMaybeRightMaybe =
   (Either a (Maybe b)) ={ eitherComm           }=
   (Either (Maybe b) a) ={ eitherMaybeLeftMaybe }=
   (Maybe (Either b a)) ={ maybeCong eitherComm }=
@@ -288,8 +285,8 @@ maybeIsoS = MkIso forth back fb bf
         fb (FS x) = Refl
 
 finZeroBot : Iso (Fin 0) Void
-finZeroBot = MkIso (\x => void (uninhabited x))
-                   (\x => void x)
+finZeroBot = MkIso (void . uninhabited)
+                   void
                    (\x => void x)
                    (\x => void (uninhabited x))
 

diff --git a/libs/contrib/Control/Algebra/Laws.idr b/libs/contrib/Control/Algebra/Laws.idr
@@ -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