From dbf4b887387b3b3be134addd9e4d2123564d8b4e Mon Sep 17 00:00:00 2001 From: William Ball Date: Fri, 13 Dec 2024 22:45:37 -0800 Subject: [PATCH] some algebra --- examples/algebra.pg | 139 +++++++++++++++++++++++++++++++------------- lib/Expr.hs | 2 +- lib/Parser.hs | 26 ++++----- 3 files changed, 111 insertions(+), 56 deletions(-) diff --git a/examples/algebra.pg b/examples/algebra.pg index 379a83e..80fb1cc 100644 --- a/examples/algebra.pg +++ b/examples/algebra.pg @@ -28,7 +28,7 @@ section BasicDefinitions infixl 20 *; -- it is associative if ... - def assoc := forall (a b c : A), eq A (a * (b * c)) ((a * b) * c); + def assoc := forall (a b c : A), eq A (a * (b * c)) (a * b * c); -- fix some element `e` variable (e : A); @@ -59,11 +59,17 @@ end BasicDefinitions -- | ALGEBRAIC STRUCTURES | -- -------------------------------------------------------------------------------------------------------------- --- a set `S` with binary operation `op` is a semigroup if its operation is associative -def semigroup (S : ★) (op : binop S) : ★ := assoc S op; +-- NOTE: I want to define opposite semigroups, monoids, groups, etc. and prove +-- that they are still semigroups, monoids, etc. in order to get dual results +-- like `cancel_r` after having proved `cancel_l` for free. Unfortunately, this +-- is a bit awkward in perga, at least for now. +section Semigroup + variable (S : ★) (* : binop S); + + def semigroup := assoc S (*); +end Semigroup section Monoid - -- Let `M` be a set with binary operation `*` and element `e`. variable (M : ★) (* : binop M) (e : M); infixl 50 *; @@ -113,7 +119,6 @@ section Monoid -- and `e * a = e` (H e); - end Monoid section Group @@ -140,71 +145,56 @@ section Group def inv_lg (a : G) : left_inverse a (i a) := and_elim_l (inv_l G (*) e a (i a)) (inv_r G (*) e a (i a)) (inv_g a); def inv_rg (a : G) : right_inverse a (i a) := and_elim_r (inv_l G (*) e a (i a)) (inv_r G (*) e a (i a)) (inv_g a); + def = := eq G; + infixl 10 =; + -- An interesting theorem: left inverses are unique, i.e. if b * a = e, then b = a^-1 - def left_inv_unique (a b : G) (h : left_inverse a b) : eq G b (i a) := + def left_inv_unique (a b : G) (h : left_inverse a b) : b = (i a) := -- b = b * e -- = b * (a * a^-1) -- = (b * a) * a^-1 -- = e * a^-1 -- = a^-1 eq_trans G b (b * e) (i a) - -- b = b * e (eq_sym G (b * e) b (id_rg b)) - -- b * e = a^-1 (eq_trans G (b * e) (b * (a * i a)) (i a) - --b * e = b * (a * a^-1) (eq_cong G G e (a * i a) ((*) b) - -- e = a * a^-1 (eq_sym G (a * i a) e (inv_rg a))) - -- b * (a * a^-1) = a^-1 (eq_trans G (b * (a * i a)) (b * a * i a) (i a) - -- b * (a * a^-1) = (b * a) * a^-1 (assoc_g b a (i a)) - -- (b * a) * a^-1 = a^-1 (eq_trans G (b * a * i a) (e * i a) (i a) - -- (b * a) * a^-1 = e * a^-1 (eq_cong G G (b * a) e (fun (x : G) => x * i a) h) - -- e * a^-1 = a^-1 (id_lg (i a))))); -- And so are right inverses - def right_inv_unique (a b : G) (h : right_inverse a b) : eq G b (i a) := + def right_inv_unique (a b : G) (h : right_inverse a b) : b = (i a) := -- b = e * b -- = (a^-1 * a) * b -- = a^-1 * (a * b) -- = a^-1 * e -- = a^-1 eq_trans G b (e * b) (i a) - -- b = e * b (eq_sym G (e * b) b (id_lg b)) - -- e * b = a^-1 (eq_trans G (e * b) (i a * a * b) (i a) - -- e * b = (a^-1 * a) * b (eq_cong G G e (i a * a) (fun (x : G) => x * b) - -- e = (a^-1 * a) (eq_sym G (i a * a) e (inv_lg a))) - - -- (a^-1 * a) * b = a^-1 (eq_trans G (i a * a * b) (i a * (a * b)) (i a) - -- (a^-1 * a) * b = a^-1 * (a * b) (eq_sym G (i a * (a * b)) (i a * a * b) (assoc_g (i a) a b)) - - -- a^-1 * (a * b) = a^-1 (eq_trans G (i a * (a * b)) (i a * e) (i a) - -- a^-1 * (a * b) = a^-1 * e (eq_cong G G (a * b) e ((*) (i a)) h) - - -- a^-1 * e = a^-1 (id_rg (i a))))); + -- (a^-1)^-1 = a + def inverse_involutive (a : G) : i (i a) = a := + eq_sym G a (i (i a)) (right_inv_unique (i a) a (inv_lg 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 (a * b)) (i b * i a) := + def shoes_and_socks (a b : G) : i (a * b) = i b * i a := eq_sym G (i b * i a) (i (a * b)) (right_inv_unique (a * b) (i b * i a) - -- WTS: (a * b) * (b^-1 * a^-1) = e (let -- 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) => z * (i a)) h) + (under_ai (x y : G) (h : x = y) := eq_cong G G x y (fun (z : G) => z * (i a)) h) in -- (a * b) * (b^-1 * a^-1) = ((a * b) * b^-1) * a^-1 -- = (a * (b * b^-1)) * a^-1 @@ -212,25 +202,90 @@ section Group -- = a * a^-1 -- = e eq_trans G (a * b * (i b * i a)) (a * b * i b * i a) e - -- (a * b) * (b^-1 * a^-1) = ((a * b) * b^-1) * a^-1 (assoc_g (a * b) (i b) (i a)) - -- ((a * b) * b^-1) * a^-1 = e (eq_trans G (a * b * i b * i a) (a * (b * i b) * i a) e - -- ((a * b) * b^-1) * a^-1 = (a * (b * b^-1)) * a^-1 (under_ai (a * b * i b) (a * (b * i b)) (eq_sym G (a * (b * i b)) (a * b * i b) (assoc_g a b (i b)))) - - -- (a * (b * b^-1)) * a^-1 = e (eq_trans G (a * (b * i b) * i a) (a * e * i a) e - -- (a * (b * b^-1)) * a^-1 = (a * e) * a^-1 (eq_cong G G (b * i b) e (fun (x : G) => (a * x * i a)) (inv_rg b)) - - -- (a * e) * a^-1 = e (eq_trans G (a * e * i a) (a * i a) e - -- (a * e) * a^-1 = a * a^-1 (under_ai (a * e) a (id_rg a)) - - -- a * a^-1 = e (inv_rg a)))) end)); + def cancel_l (a b c : G) : a * b = a * c → b = c := + fun (h : a * b = a * c) => + eq_trans G b (e * b) c + (eq_sym G (e * b) b (id_lg b)) + (eq_trans G (e * b) (i a * a * b) c + (eq_cong G G e (i a * a) ([x : G] x * b) + (eq_sym G (i a * a) e (inv_lg a))) + (eq_trans G (i a * a * b) (i a * (a * b)) c + (eq_sym G (i a * (a * b)) (i a * a * b) (assoc_g (i a) a b)) + (eq_trans G (i a * (a * b)) (i a * (a * c)) c + (eq_cong G G (a * b) (a * c) ((*) (i a)) h) + (eq_trans G (i a * (a * c)) (i a * a * c) c + (assoc_g (i a) a c) + (eq_trans G (i a * a * c) (e * c) c + (eq_cong G G (i a * a) e ([x : G] x * c) (inv_lg a)) + (id_lg c)))))); + + def cancel_r (a b c : G) : b * a = c * a → b = c := + fun (h : b * a = c * a) => + eq_trans G b (b * e) c + (eq_sym G (b * e) b (id_rg b)) + (eq_trans G (b * e) (b * (a * i a)) c + (eq_cong G G e (a * i a) ((*) b) + (eq_sym G (a * i a) e (inv_rg a))) + (eq_trans G (b * (a * i a)) (b * a * i a) c + (assoc_g b a (i a)) + (eq_trans G (b * a * i a) (c * a * i a) c + (eq_cong G G (b * a) (c * a) ([x : G] x * i a) h) + (eq_trans G (c * a * i a) (c * (a * i a)) c + (eq_sym G (c * (a * i a)) (c * a * i a) (assoc_g c a (i a))) + (eq_trans G (c * (a * i a)) (c * e) c + (eq_cong G G (a * i a) e ((*) c) (inv_rg a)) + (id_rg c)))))); + + def abelian : ★ := forall (a b : G), a * b = b * a; + + def left_right_cancel : (forall (x y z : G), x * y = z * x → y = z) → abelian := + fun (h : forall (x y z : G), x * y = z * x → y = z) (a b : G) => + h (i a) (a * b) (b * a) + (eq_trans G (i a * (a * b)) (i a * a * b) (b * a * i a) + (assoc_g (i a) a b) + (eq_trans G (i a * a * b) (e * b) (b * a * i a) + (eq_cong G G (i a * a) e ([x : G] x * b) (inv_lg a)) + (eq_trans G (e * b) b (b * a * i a) + (id_lg b) + (eq_trans G b (b * e) (b * a * i a) + (eq_sym G (b * e) b (id_rg b)) + (eq_trans G (b * e) (b * (a * i a)) (b * a * i a) + (eq_cong G G e (a * i a) ((*) b) (eq_sym G (a * i a) e (inv_rg a))) + (assoc_g b a (i a))))))); + + def inv_distrib_abelian : (forall (a b : G), i (a * b) = i a * i b) → abelian := + fun (h : forall (a b : G), i (a * b) = i a * i b) (a b : G) => + eq_trans G (a * b) (i (i a) * b) (b * a) + (eq_cong G G a (i (i a)) ([x : G] x * b) (eq_sym G (i (i a)) a (inverse_involutive a))) + (eq_trans G (i (i a) * b) (i (i a) * i (i b)) (b * a) + (eq_cong G G b (i (i b)) ((*) (i (i a))) (eq_sym G (i (i b)) b (inverse_involutive b))) + (eq_trans G (i (i a) * i (i b)) (i (i b * i a)) (b * a) + (eq_sym G (i (i b * i a)) (i (i a) * i (i b)) (shoes_and_socks (i b) (i a))) + (eq_trans G (i (i b * i a)) (i (i b) * i (i a)) (b * a) + (h (i b) (i a)) + (eq_trans G (i (i b) * i (i a)) (b * i (i a)) (b * a) + (eq_cong G G (i (i b)) b ([x : G] x * i (i a)) (inverse_involutive b)) + (eq_cong G G (i (i a)) a ((*) b) (inverse_involutive a)))))); + + def order_two (a : G) : a * a = e → a = i a := right_inv_unique a a; + + def all_order_two_abelian : (forall (a : G), a * a = e) → abelian := + fun (h : forall (a : G), a * a = e) => + inv_distrib_abelian (fun (a b : G) => + (eq_trans G (i (a * b)) (a * b) (i a * i b) + (eq_sym G (a * b) (i (a * b)) (order_two (a * b) (h (a * b)))) + (eq_trans G (a * b) (a * i b) (i a * i b) + (eq_cong G G b (i b) ((*) a) (order_two b (h b))) + (eq_cong G G a (i a) ([x : G] x * i b) (order_two a (h a)))))); + end Group diff --git a/lib/Expr.hs b/lib/Expr.hs index 2a5f1b0..2bb721b 100644 --- a/lib/Expr.hs +++ b/lib/Expr.hs @@ -168,7 +168,7 @@ prettyExpr k expr = case expr of Var s _ -> pretty s Free s -> pretty s Axiom s -> pretty s - Star -> "*" + Star -> "★" Level i | i == 0 -> "□" | otherwise -> "□" <> printLevel i diff --git a/lib/Parser.hs b/lib/Parser.hs index e1366b5..357dc5b 100644 --- a/lib/Parser.hs +++ b/lib/Parser.hs @@ -66,18 +66,18 @@ pSymbol = lexeme $ takeWhile1P (Just "symbol") (`elem` symbols) pVar :: Parser IRExpr pVar = label "variable" $ lexeme $ Var <$> pIdentifier -pParamGroup :: Parser Text -> Parser [Param] -pParamGroup ident = lexeme $ label "parameter group" $ parens $ do - idents <- some ident +pParamGroup :: Parser [Param] +pParamGroup = lexeme $ label "parameter group" $ parens $ do + idents <- some $ pIdentifier <|> pSymbol symbol ":" ty <- pIRExpr pure $ map (,ty) idents -pSomeParams :: Parser Text -> Parser [Param] -pSomeParams ident = lexeme $ concat <$> some (pParamGroup ident) +pSomeParams :: Parser [Param] +pSomeParams = lexeme $ concat <$> some pParamGroup -pManyParams :: Parser Text -> Parser [Param] -pManyParams ident = lexeme $ concat <$> many (pParamGroup ident) +pManyParams :: Parser [Param] +pManyParams = lexeme $ concat <$> many pParamGroup mkAbs :: (Text, IRExpr) -> IRExpr -> IRExpr mkAbs (param, typ) = Abs param typ @@ -88,7 +88,7 @@ mkPi (param, typ) = Pi param typ pLAbs :: Parser IRExpr pLAbs = lexeme $ label "λ-abstraction" $ do _ <- pKeyword "fun" <|> symbol "λ" - params <- pSomeParams pIdentifier + params <- pSomeParams _ <- symbol "=>" <|> symbol "⇒" body <- pIRExpr pure $ foldr mkAbs body params @@ -106,7 +106,7 @@ pALAbs = lexeme $ label "λ-abstraction" $ do pPAbs :: Parser IRExpr pPAbs = lexeme $ label "Π-abstraction" $ do _ <- pKeyword "forall" <|> symbol "∏" <|> symbol "∀" - params <- pSomeParams pIdentifier + params <- pSomeParams symbol "," body <- pIRExpr pure $ foldr mkPi body params @@ -115,7 +115,7 @@ pBinding :: Parser (Text, Maybe IRExpr, IRExpr) pBinding = lexeme $ label "binding" $ do symbol "(" ident <- pIdentifier - params <- pManyParams pIdentifier + params <- pManyParams ascription <- optional pAscription symbol ":=" value <- pIRExpr @@ -212,7 +212,7 @@ pAxiom :: Parser IRDef pAxiom = lexeme $ label "axiom" $ do pKeyword "axiom" ident <- pIdentifier - params <- pManyParams (pIdentifier <|> pSymbol) + params <- pManyParams ascription <- fmap (flip (foldr mkPi) params) pAscription symbol ";" pure $ Axiom ident ascription @@ -220,7 +220,7 @@ pAxiom = lexeme $ label "axiom" $ do pVariable :: Parser [IRSectionDef] pVariable = lexeme $ label "variable declaration" $ do pKeyword "variable" <|> pKeyword "hypothesis" - vars <- pManyParams (pIdentifier <|> pSymbol) + vars <- pManyParams symbol ";" pure $ uncurry Variable <$> vars @@ -228,7 +228,7 @@ pDef :: Parser IRDef pDef = lexeme $ label "definition" $ do pKeyword "def" ident <- pIdentifier <|> pSymbol - params <- pManyParams pIdentifier + params <- pManyParams ascription <- fmap (flip (foldr mkPi) params) <$> optional pAscription symbol ":=" body <- pIRExpr