some algebra
This commit is contained in:
parent
cf26b7c9ec
commit
dbf4b88738
3 changed files with 111 additions and 56 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Reference in a new issue