From 08ef684418404d8103c553754af10d1b13cc4379 Mon Sep 17 00:00:00 2001 From: William Ball Date: Sun, 22 Dec 2024 13:16:32 -0800 Subject: [PATCH] added changing section variables via '#', reworked `algebra.pg` to use duality --- examples/algebra.pg | 369 ++++++++++++++------------------------------ lib/Elaborator.hs | 3 + lib/IR.hs | 1 + lib/Parser.hs | 5 +- 4 files changed, 122 insertions(+), 256 deletions(-) diff --git a/examples/algebra.pg b/examples/algebra.pg index 80fb1cc..0c47785 100644 --- a/examples/algebra.pg +++ b/examples/algebra.pg @@ -1,291 +1,150 @@ --- -------------------------------------------------------------------------------------------------------------- --- | BASIC LOGIC | --- -------------------------------------------------------------------------------------------------------------- - @include logic.pg --- -------------------------------------------------------------------------------------------------------------- --- | BASIC DEFINITIONS | --- -------------------------------------------------------------------------------------------------------------- +section Magma -section BasicDefinitions +variable (G : ★); +def binop := G → G → G; - -- note we leave off the type ascriptions for most of these, as the type isn't - -- very interesting - -- I'd always strongly recommend including the type ascriptions for theorems +def = := eq G; +infixl 1 =; - -- Fix some set A - variable (A : ★); +variable (* : binop); +infixl 20 *; - -- a unary operation is a function `A → A` - def unop := A → A; +def *> (a b : G) := b * a; +infixl 20 *>; - -- a binary operation is a function `A → A → A` - def binop := A → A → A; - - -- fix some binary operation `*` - variable (* : binop); - infixl 20 *; - - -- it is associative if ... - def assoc := forall (a b c : A), eq A (a * (b * c)) (a * b * c); - - -- fix some element `e` - variable (e : A); - - -- it is a left identity with respect to binop `op` if `∀ a, e * a = a` - def id_l := forall (a : A), eq A (e * a) a; - - -- likewise for right identity - def id_r := forall (a : A), eq A (a * e) a; - - -- an element is an identity element if it is both a left and right identity - def id := id_l ∧ id_r; - - -- b is a left inverse for a if `b * a = e` - -- NOTE: we don't require `e` to be an identity in this definition. - -- this definition is purely for convenience's sake - def inv_l (a b : A) := eq A (b * a) e; - - -- likewise for right inverse - def inv_r (a b : A) := eq A (a * b) e; - - -- and full-on inverse - def inv (a b : A) := inv_l a b ∧ inv_r a b; - -end BasicDefinitions - --- -------------------------------------------------------------------------------------------------------------- --- | ALGEBRAIC STRUCTURES | --- -------------------------------------------------------------------------------------------------------------- - --- 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 +def assoc := forall (a b c : G), a * (b * c) = a * b * c; +hypothesis (Hassoc : assoc); + +def assoc_op (a b c : G) : a *> (b *> c) = a *> b *> c := + eq_sym G (a *> b *> c) (a *> (b *> c)) (Hassoc c b a); section Monoid - -- Let `M` be a set with binary operation `*` and element `e`. - variable (M : ★) (* : binop M) (e : M); - infixl 50 *; - -- a set `M` with binary operation `(*)` and element `e` is a monoid - def monoid : ★ := (semigroup M (*)) ∧ (id M (*) e); +variable (e : G); +def id_l := forall (a : G), e * a = a; +def id_r := forall (a : G), a * e = a; - -- Suppose `(M, *, e)` is a monoid - hypothesis (Hmonoid : monoid); +hypothesis (Hid_l : id_l); +hypothesis (Hid_r : id_r); - -- 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 (*) e := - and_elim_l (id_l M (*) e) (id_r M (*) e) - (and_elim_r (semigroup M (*)) (id M (*) e) Hmonoid); +def id_l_op : forall (a : G), e *> a = a := Hid_r; +def id_r_op : forall (a : G), a *> e = a := Hid_l; - def id_rm : id_r M (*) e := - and_elim_r (id_l M (*) e) (id_r M (*) e) - (and_elim_r (semigroup M (*)) (id M (*) e) Hmonoid); +def left_id_unique (a : G) : #id_l G (*) a → a = e := + fun (H : #id_l G (*) a) => + eq_trans G a (a * e) e + (eq_sym G (a * e) a (Hid_r a)) + (H e); - def assoc_m : assoc M (*) := and_elim_l (semigroup M (*)) (id M (*) e) Hmonoid; - - -- now we can prove that, for any monoid, if `a` is a left identity, then it - -- must be "the" identity - def monoid_id_l_implies_identity (a : M) (H : id_l M (*) a) : eq M a e := - -- WTS a = a * e = e - -- we can use `eq_trans` to glue proofs of `a = a * e` and `a * e = e` together - eq_trans M a (a * e) e - - -- first, `a = a * e`, but we'll use `eq_sym` to flip it around - (eq_sym M (a * e) a - -- now the goal is to show `a * e = a`, which follows immediately from `id_r` - (id_rm a)) - - -- now we need to show that `a * e = e`, but this immediately follows from `H` - (H e); - - -- the analogous result for right identities - def monoid_id_r_implies_identity (a : M) (H : id_r M (*) a) : eq M a e := - -- this time, we'll show `a = e * a = e` - eq_trans M a (e * a) e - - -- first, `a = e * a` - (eq_sym M (e * a) a - -- this time, it immediately follows from `id_l` - (id_lm a)) - - -- and `e * a = e` - (H e); -end Monoid +def right_id_unique (a : G) : #id_r G (*) a → a = e := #left_id_unique G (*>) e Hid_l a; section Group - variable (G : ★) (* : binop G) (e : G) (i : unop G); +variable (i : G → G); +hypothesis (Hinv_l : forall (a : G), i a * a = e); +hypothesis (Hinv_r : forall (a : G), a * i a = e); - infixl 50 *; - - -- groups are just monoids with inverses - def has_inverses : ★ := forall (a : G), inv G (*) e a (i a); - - def group : ★ := (monoid G (*) e) ∧ has_inverses; - - hypothesis (Hgroup : group); - - -- more "getters" - def monoid_g : monoid G (*) e := and_elim_l (monoid G (*) e) has_inverses Hgroup; - def assoc_g : assoc G (*) := assoc_m G (*) e monoid_g; - def id_lg : id_l G (*) e := id_lm G (*) e (and_elim_l (monoid G (*) e) has_inverses Hgroup); - def id_rg : id_r G (*) e := id_rm G (*) e (and_elim_l (monoid G (*) e) has_inverses Hgroup); - def inv_g : forall (a : G), inv G (*) e a (i a) := and_elim_r (monoid G (*) e) has_inverses Hgroup; - def left_inverse (a b : G) := inv_l G (*) e a b; - def right_inverse (a b : G) := inv_r G (*) e a b; - 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) : 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) - (eq_sym G (b * e) b (id_rg b)) +def left_inv_unique (a b : G) (h : b * a = e) : b = i a := + eq_trans G b (b * e) (i a) + (eq_sym G (b * e) b (Hid_r b)) (eq_trans G (b * e) (b * (a * i a)) (i a) (eq_cong G G e (a * i a) ((*) b) - (eq_sym G (a * i a) e (inv_rg a))) + (eq_sym G (a * i a) e (Hinv_r a))) (eq_trans G (b * (a * i a)) (b * a * i a) (i a) - (assoc_g b a (i a)) + (Hassoc b a (i a)) (eq_trans G (b * a * i a) (e * i a) (i a) - (eq_cong G G (b * a) e (fun (x : G) => x * i a) h) - (id_lg (i a))))); + (eq_cong G G (b * a) e ([z : G] z * i a) h) + (Hid_l (i a))))); - -- And so are right inverses - 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) - (eq_sym G (e * b) b (id_lg b)) - (eq_trans G (e * b) (i a * a * b) (i a) - (eq_cong G G e (i a * a) (fun (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)) (i a) - (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 * e) (i a) - (eq_cong G G (a * b) e ((*) (i a)) h) - (id_rg (i a))))); +def right_inv_unique (a b : G) (h : a * b = e) : b = i a := + #left_inv_unique G (*>) assoc_op e Hid_r Hid_l i Hinv_l a b h; - -- (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)); +def inverse_involutive (a : G) : i (i a) = a := + eq_sym G a (i (i a)) (right_inv_unique (i a) a (Hinv_l a)); - -- the classic shoes and socks theorem, namely that (a * b)^-1 = b^-1 * a^-1 - 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) - (let - -- helper function to prove that x * a^-1 = y * a^-1 given x = y - (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 - -- = (a * e) * a^-1 - -- = a * a^-1 - -- = e - eq_trans G (a * b * (i b * i a)) (a * b * i b * i a) e - (assoc_g (a * b) (i b) (i a)) - (eq_trans G (a * b * i b * i a) (a * (b * i b) * i a) e - (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)))) - (eq_trans G (a * (b * i b) * i a) (a * e * i a) e - (eq_cong G G (b * i b) e (fun (x : G) => (a * x * i a)) (inv_rg b)) - (eq_trans G (a * e * i a) (a * i a) e - (under_ai (a * e) a (id_rg a)) - (inv_rg a)))) - end)); +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) + (let + (under_ai (x y : G) (h : x = y) := eq_cong G G x y ([z : G] z * (i a)) h) + in + eq_trans G (a * b * (i b * i a)) (a * b * i b * i a) e + (Hassoc (a * b) (i b) (i a)) + (eq_trans G (a * b * i b * i a) (a * (b * i b) * i a) e + (under_ai (a * b * i b) (a * (b * i b)) (eq_sym G (a * (b * i b)) (a * b * i b) (Hassoc a b (i b)))) + (eq_trans G (a * (b * i b) * i a) (a * e * i a) e + (eq_cong G G (b * i b) e (fun (x : G) => (a * x * i a)) (Hinv_r b)) + (eq_trans G (a * e * i a) (a * i a) e + (under_ai (a * e) a (Hid_r a)) + (Hinv_r 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_l (a b c : G) (h : a * b = a * c) : b = c := + eq_trans G b (e * b) c + (eq_sym G (e * b) b (Hid_l 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 (Hinv_l a))) + (eq_trans G (i a * a * b) (i a * (a * b)) c + (eq_sym G (i a * (a * b)) (i a * a * b) (Hassoc (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 + (Hassoc (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) (Hinv_l a)) + (Hid_l 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 cancel_r (a b c : G) (h : b * a = c * a) : b = c := + #cancel_l G (*>) assoc_op e Hid_r i Hinv_r a b c h; - def abelian : ★ := forall (a b : G), a * b = b * a; +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 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) + (Hassoc (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) (Hinv_l a)) + (eq_trans G (e * b) b (b * a * i a) + (Hid_l b) + (eq_trans G b (b * e) (b * a * i a) + (eq_sym G (b * e) b (Hid_r 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 (Hinv_r a))) + (Hassoc 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 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 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)))))); +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 +end Monoid +end Semigroup +end Magma diff --git a/lib/Elaborator.hs b/lib/Elaborator.hs index 04dbb2e..9d2492f 100644 --- a/lib/Elaborator.hs +++ b/lib/Elaborator.hs @@ -99,6 +99,7 @@ usedVars (I.Var name) = do varDeps <- maybe S.empty (S.singleton . (name,)) <$> lookupVar name defDeps <- maybe S.empty S.fromList <$> lookupDef name pure $ varDeps `S.union` defDeps +usedVars (I.PureVar pvname) = usedVars (I.Var pvname) usedVars I.Star = pure S.empty usedVars (I.Level _) = pure S.empty usedVars (I.App m n) = S.union <$> usedVars m <*> usedVars n @@ -124,6 +125,7 @@ traverseBody (I.Var name) = do case mdeps of Nothing -> pure $ I.Var name Just deps -> pure $ foldl' (\acc newVar -> I.App acc (I.Var $ fst newVar)) (I.Var name) deps +traverseBody (I.PureVar pvname) = pure $ I.PureVar pvname traverseBody I.Star = pure I.Star traverseBody (I.Level k) = pure $ I.Level k traverseBody (I.App m n) = I.App <$> traverseBody m <*> traverseBody n @@ -183,6 +185,7 @@ elaborate ir = evalState (elaborate' ir) [] elaborate' (I.Var n) = do binders <- get pure $ E.Var n . fromIntegral <$> elemIndex n binders ?: E.Free n + elaborate' (I.PureVar pvname) = elaborate' $ I.Var pvname elaborate' I.Star = pure E.Star elaborate' (I.Level level) = pure $ E.Level level elaborate' (I.App m n) = E.App <$> elaborate' m <*> elaborate' n diff --git a/lib/IR.hs b/lib/IR.hs index 6cea276..ae654a0 100644 --- a/lib/IR.hs +++ b/lib/IR.hs @@ -4,6 +4,7 @@ type Param = (Text, IRExpr) data IRExpr = Var {varName :: Text} + | PureVar {pvName :: Text} | Star | Level {level :: Integer} | App diff --git a/lib/Parser.hs b/lib/Parser.hs index 357dc5b..a8eb2f4 100644 --- a/lib/Parser.hs +++ b/lib/Parser.hs @@ -66,6 +66,9 @@ pSymbol = lexeme $ takeWhile1P (Just "symbol") (`elem` symbols) pVar :: Parser IRExpr pVar = label "variable" $ lexeme $ Var <$> pIdentifier +pPureVar :: Parser IRExpr +pPureVar = label "variable" $ lexeme $ symbol "#" >> PureVar <$> pIdentifier + pParamGroup :: Parser [Param] pParamGroup = lexeme $ label "parameter group" $ parens $ do idents <- some $ pIdentifier <|> pSymbol @@ -172,7 +175,7 @@ pOpSection :: Parser IRExpr pOpSection = lexeme $ parens $ Var <$> pSymbol pTerm :: Parser IRExpr -pTerm = lexeme $ label "term" $ choice [pSort, pVar, try pOpSection, parens pIRExpr] +pTerm = lexeme $ label "term" $ choice [pSort, pPureVar, pVar, try pOpSection, parens pIRExpr] pInfix :: Parser IRExpr pInfix = parseWithPrec 0