shoes and socks

examples/algebra.pg

@@ -72,7 +72,7 @@ section Monoid
 
     -- some "getters" for `monoid` so we don't have to do a bunch of very verbose
     -- and-eliminations every time we want to use something
-    def id_lm  : id_l M op e :=
+    def id_lm : id_l M op e :=
         and_elim_l (id_l M op e) (id_r M op e)
             (and_elim_r (semigroup M op) (id M op e) Hmonoid);
 
@@ -191,4 +191,46 @@ section Group
                     -- a^-1 * e = a^-1
                     (id_rg (i a)))));
 
+    -- the classic shoes and socks theorem, namely that (a * b)^-1 = b^-1 * a^-1
+    def shoes_and_socks (a b : G) : eq G (i (op a b)) (op (i b) (i a)) :=
+        eq_sym G (op (i b) (i a)) (i (op a b))
+        (right_inv_unique (op a b) (op (i b) (i a))
+        -- WTS: (a * b) * (b^-1 * a^-1) = e
+        (let
+            -- some abbreviations for common terms
+            (ab := op a b)
+            (biai := op (i b) (i a))
+            (ab_bi := op (op a b) (i b))
+            (a_bbi := op a (op b (i b)))
+
+            -- helper function to prove that x * a^-1 = y * a^-1 given x = y
+            (under_ai (x y : G) (h : eq G x y) := eq_cong G G x y (fun (z : G) => op z (i a)) h)
+         in
+            -- (a * b) * (b^-1 * a^-1) = ((a * b) * b^-1) * a^-1
+            --                         = (a * (b * b^-1)) * a^-1
+            --                         = (a * e) * a^-1
+            --                         = a * a^-1
+            --                         = e
+            eq_trans G (op ab biai) (op ab_bi (i a)) e
+            -- (a * b) * (b^-1 * a^-1) = ((a * b) * b^-1) * a^-1
+            (assoc_g ab (i b) (i a))
+            -- ((a * b) * b^-1) * a^-1 = e
+            (eq_trans G (op ab_bi (i a)) (op a_bbi (i a)) e
+                -- ((a * b) * b^-1) * a^-1 = (a * (b * b^-1)) * a^-1
+                (under_ai ab_bi a_bbi (eq_sym G a_bbi ab_bi (assoc_g a b (i b))))
+
+                -- (a * (b * b^-1)) * a^-1 = e
+                (eq_trans G (op a_bbi (i a)) (op (op a e) (i a)) e
+                    -- (a * (b * b^-1)) * a^-1 = (a * e) * a^-1
+                    (eq_cong G G (op b (i b)) e (fun (x : G) => (op (op a x) (i a))) (inv_rg b))
+
+                    -- (a * e) * a^-1 = e
+                    (eq_trans G (op (op a e) (i a)) (op a (i a)) e
+                        -- (a * e) * a^-1 = a * a^-1
+                        (under_ai (op a e) a (id_rg a))
+
+                        -- a * a^-1 = e
+                        (inv_rg a))))
+         end));
+
 end Group

lib/Errors.hs

@@ -17,7 +17,7 @@ data Error
 instance Pretty Error where
     pretty (UnboundVariable x) = "Unbound variable: '" <> pretty x <> "'"
     pretty (NotASort x) = group $ hang 4 ("Term:" <> line <> pretty x) <> line <> "is not a type"
-    pretty (ExpectedPiType x t) = group $ hang 4 ("Term:" <> line <> pretty x) <> hang 4 ("is not a function, instead is type" <> line <> pretty t)
+    pretty (ExpectedPiType x t) = group $ hang 4 ("Term:" <> line <> pretty x) <> line <> hang 4 ("is not a function, instead is type" <> line <> pretty t)
     pretty (NotEquivalent a a' e) =
         group $
             hang 4 ("Cannot unify" <> line <> pretty a)