diff --git a/README.md b/README.md index d6dee73..efa63b0 100644 --- a/README.md +++ b/README.md @@ -1,3 +1,5 @@ +# Perga + `perga` is a basic proof assistant based on a dependently typed lambda calculus (calculus of constructions), but augmented with a simple universe hierarchy (Extended Calculus of Constructions but without Σ-types, though I intend to add them). This implementation is based on the exposition in Nederpelt and Geuvers' *Type Theory and Formal Proof*. Right now it is a perfectly capable higher order logic proof checker, though there is lots of room for improved ergonomics and usability, which I intend to work on. At the moment, `perga` is comparable to Automath in terms of power and ease of use, being slightly more powerful than Automath, and a touch less ergonomic. @@ -16,9 +18,9 @@ fun (A B C : *) (g : → C) (f : A → B) (x : A) : C ⇒ g (f x) fun (S : *) (P Q : S -> *) (H : Π (x : S) , P x -> Q x) (HP : forall (x : S), P x) => fun (x : S) => H x (HP x) ``` -To be perfectly clear, `λ` abstractions can be written with either "λ" or "fun", and are separated from their bodies by either "=>" or "⇒". Binders with the same type can be grouped together, and multiple binders can occur between the "λ" and the "⇒". You can also optionally add the return type after the binders and before the "⇒", though this can always be inferred and so isn't necessary +To be perfectly clear, `λ` abstractions can be written with either `λ` or `fun`, and are separated from their bodies by either `=>` or `⇒`. Binders with the same type can be grouped together, and multiple binders can occur between the `λ` and the `⇒`. You can also optionally add the return type after the binders and before the `⇒`, though this can always be inferred and so isn't necessary -`Π` types can be written with either "Π", "∀", or "forall", and are separated from their bodies with a ",". Arrow types can be written "->" or "→". Like with `λ` abstractions, binders with the same type can be grouped, and multiple binders can occur between the "Π" and the ",". Like with `λ` types, the "return" type can optionally be added after the binders and before the ",", however this is even more useless, as it is nearly always `*`, the type of types. +`Π` types can be written with either `Π`, `∀`, or `forall`, and are separated from their bodies with a `,`. Arrow types can be written `->` or `→`. Like with `λ` abstractions, binders with the same type can be grouped, and multiple binders can occur between the `Π` and the `,`. Like with `λ` types, the "return" type can optionally be added after the binders and before the `,`, however this is even more useless, as it is nearly always `*`, the type of types. The universe hierarchy is very similar to Coq, with `* : □ : □₁ : □₂ : ...`, where `*` is impredicative and the `□ᵢ` are predicative. There is no universe polymorphism, making this rather limited. A lack of inductive types (or even just built-in `Σ`-types and sum types) makes doing logic at any universe level other than `*` extremely limited. For ease of typing, `[]1`, `□1`, `[]₁`, and `□₁` are all the same. @@ -96,7 +98,7 @@ There isn't a proper module system (yet), but you can include other files in a d # Usage -Running `perga` without any arguments drops you into a basic repl. From here, you can type in definitions which `perga` will typecheck. Previous definitions are accessible in future definitions. The usual readline keybindings are available, including navigating history, which is saved between sessions (in `~/.cache/perga/history`). In the repl, you can enter ":q", press C-c, or press C-d to quit. Entering ":e" shows everything that has been defined along with their types. If you want to see the value of an identifier defined in the environment, you can enter ":v ". Entering ":t " prints the type of an expression. Entering ":n " will fully normalize (including unfolding definitions) an expression, while ":w " will reduce it to weak head normal form. Finally ":l " loads a file. +Running `perga` without any arguments drops you into a basic repl. From here, you can type in definitions which `perga` will typecheck. Previous definitions are accessible in future definitions. The usual readline keybindings are available, including navigating history, which is saved between sessions (in `~/.cache/perga/history`). In the repl, you can enter `:q`, press C-c, or press C-d to quit. Entering `:e` shows everything that has been defined along with their types. If you want to see the value of an identifier defined in the environment, you can enter `:v `. Entering `:t ` prints the type of an expression. Entering `:n ` will fully normalize (including unfolding definitions) an expression, while `:w ` will reduce it to weak head normal form. Finally `:l ` loads a file. Here's an example session showing the capabilities of the repl. diff --git a/examples/algebra.pg b/examples/algebra.pg index 708c1fe..d178b49 100644 --- a/examples/algebra.pg +++ b/examples/algebra.pg @@ -8,41 +8,51 @@ -- | BASIC DEFINITIONS | -- -------------------------------------------------------------------------------------------------------------- --- 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 +section BasicDefinitions --- a unary operation on a set `A` is a function `A -> A` -def unop (A : *) := A -> A; + -- 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 --- a binary operation on a set `A` is a function `A -> A -> A` -def binop (A : *) := A -> A -> A; + -- Fix some set A + variable (A : *); --- a binary operation is associative if ... -def assoc (A : *) (op : binop A) := - forall (a b c : A), eq A (op a (op b c)) (op (op a b) c); + -- a unary operation is a function `A -> A` + def unop := A -> A; --- an element `e : A` is a left identity with respect to binop `op` if `∀ a, e * a = a` -def id_l (A : *) (op : binop A) (e : A) := - forall (a : A), eq A (op e a) a; + -- a binary operation is a function `A -> A -> A` + def binop := A -> A -> A; --- likewise for right identity -def id_r (A : *) (op : binop A) (e : A) := - forall (a : A), eq A (op a e) a; + -- fix some binary operation `op` + variable (op : binop); --- an element is an identity element if it is both a left and right identity -def id (A : *) (op : binop A) (e : A) := and (id_l A op e) (id_r A op e); + -- it is associative if ... + def assoc := forall (a b c : A), eq A (op a (op b c)) (op (op a b) c); --- 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 : *) (op : binop A) (e : A) (a b : A) := eq A (op b a) e; + -- fix some element `e` + variable (e : A); --- likewise for right inverse -def inv_r (A : *) (op : binop A) (e : A) (a b : A) := eq A (op a b) e; + -- it is a left identity with respect to binop `op` if `∀ a, e * a = a` + def id_l := forall (a : A), eq A (op e a) a; --- and full-on inverse -def inv (A : *) (op : binop A) (e : A) (a b : A) := and (inv_l A op e a b) (inv_r A op e a b); + -- likewise for right identity + def id_r := forall (a : A), eq A (op a e) a; + + -- an element is an identity element if it is both a left and right identity + def id := and 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 (op b a) e; + + -- likewise for right inverse + def inv_r (a b : A) := eq A (op a b) e; + + -- and full-on inverse + def inv (a b : A) := and (inv_l a b) (inv_r a b); + +end BasicDefinitions -- -------------------------------------------------------------------------------------------------------------- -- | ALGEBRAIC STRUCTURES | @@ -51,109 +61,104 @@ def inv (A : *) (op : binop A) (e : A) (a b : A) := and (inv_l A op e a b) (inv_ -- a set `S` with binary operation `op` is a semigroup if its operation is associative def semigroup (S : *) (op : binop S) : * := assoc S op; --- a set `M` with binary operation `op` and element `e` is a monoid -def monoid (M : *) (op : binop M) (e : M) : * := - and (semigroup M op) (id M op e); +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 (M : *) (op : binop M) (e : M) (Hmonoid : monoid M op e) : 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); + variable (M : *) (op : binop M) (e : M); -def id_rm (M : *) (op : binop M) (e : M) (Hmonoid : monoid M op e) : id_r M op e := - and_elim_r (id_l M op e) (id_r M op e) - (and_elim_r (semigroup M op) (id M op e) Hmonoid); + -- a set `M` with binary operation `op` and element `e` is a monoid + def monoid : * := and (semigroup M op) (id M op e); -def assoc_m (M : *) (op : binop M) (e : M) (Hmonoid : monoid M op e) : assoc M op := - and_elim_l (semigroup M op) (id M op e) Hmonoid; + hypothesis (Hmonoid : monoid); --- 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 - (M : *) (op : binop M) (e : M) (Hmonoid : monoid M op e) - (a : M) (H : id_l M op 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 (op a e) e + -- 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 := + and_elim_l (id_l M op e) (id_r M op e) + (and_elim_r (semigroup M op) (id M op e) Hmonoid); - -- first, `a = a * e`, but we'll use `eq_sym` to flip it around - (eq_sym M (op a e) a - -- now the goal is to show `a * e = a`, which follows immediately from `id_r` - (id_rm M op e Hmonoid a)) + def id_rm : id_r M op e := + and_elim_r (id_l M op e) (id_r M op e) + (and_elim_r (semigroup M op) (id M op e) Hmonoid); - -- now we need to show that `a * e = e`, but this immediately follows from `H` - (H e); + def assoc_m : assoc M op := and_elim_l (semigroup M op) (id M op e) Hmonoid; --- the analogous result for right identities -def monoid_id_r_implies_identity - (M : *) (op : binop M) (e : M) (Hmonoid : monoid M op e) - (a : M) (H : id_r M op a) : eq M a e := - -- this time, we'll show `a = e * a = e` - eq_trans M a (op e a) e + -- 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 op 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 (op a e) e - -- first, `a = e * a` - (eq_sym M (op e a) a - -- this time, it immediately follows from `id_l` - (id_lm M op e Hmonoid a)) + -- first, `a = a * e`, but we'll use `eq_sym` to flip it around + (eq_sym M (op a e) a + -- now the goal is to show `a * e = a`, which follows immediately from `id_r` + (id_rm a)) - -- and `e * a = e` - (H e); - + -- now we need to show that `a * e = e`, but this immediately follows from `H` + (H e); --- groups are just monoids with inverses -def has_inverses (G : *) (op : binop G) (e : G) (i : unop G) : * := - forall (a : G), inv G op e a (i a); + -- the analogous result for right identities + def monoid_id_r_implies_identity (a : M) (H : id_r M op a) : eq M a e := + -- this time, we'll show `a = e * a = e` + eq_trans M a (op e a) e -def group (G : *) (op : binop G) (e : G) (i : unop G) : * := - and (monoid G op e) - (has_inverses G op e i); + -- first, `a = e * a` + (eq_sym M (op e a) a + -- this time, it immediately follows from `id_l` + (id_lm a)) --- more "getters" -def monoid_g (G : *) (op : binop G) (e : G) (i : unop G) (Hgroup : group G op e i) : monoid G op e := - and_elim_l (monoid G op e) (has_inverses G op e i) Hgroup; + -- and `e * a = e` + (H e); -def assoc_g (G : *) (op : binop G) (e : G) (i : unop G) (Hgroup : group G op e i) : assoc G op := - assoc_m G op e (monoid_g G op e i Hgroup); +end Monoid -def id_lg (G : *) (op : binop G) (e : G) (i : unop G) (Hgroup : group G op e i) : id_l G op e := - id_lm G op e (and_elim_l (monoid G op e) (has_inverses G op e i) Hgroup); +section Group -def id_rg (G : *) (op : binop G) (e : G) (i : unop G) (Hgroup : group G op e i) : id_r G op e := - id_rm G op e (and_elim_l (monoid G op e) (has_inverses G op e i) Hgroup); + variable (G : *) (op : binop G) (e : G) (i : unop G); -def inv_g (G : *) (op : binop G) (e : G) (i : unop G) (Hgroup : group G op e i) : forall (a : G), inv G op e a (i a) := - and_elim_r (monoid G op e) (has_inverses G op e i) Hgroup; + -- groups are just monoids with inverses + def has_inverses : * := forall (a : G), inv G op e a (i a); -def inv_lg (G : *) (op : binop G) (e : G) (i : unop G) (Hgroup : group G op e i) (a : G) : inv_l G op e a (i a) := - and_elim_l (inv_l G op e a (i a)) (inv_r G op e a (i a)) (inv_g G op e i Hgroup a); + def group : * := and (monoid G op e) has_inverses; -def inv_rg (G : *) (op : binop G) (e : G) (i : unop G) (Hgroup : group G op e i) (a : G) : inv_r G op e a (i a) := - and_elim_r (inv_l G op e a (i a)) (inv_r G op e a (i a)) (inv_g G op e i Hgroup a); + hypothesis (Hgroup : group); -def left_inv_unique (G : *) (op : binop G) (e : G) (i : unop G) (Hgroup : group G op e i) (a b : G) (h : inv_l G op e a b) : eq G b (i a) := - -- b = b * e - -- = b * (a * a^-1) - -- = (b * a) * a^-1 - -- = e * a^-1 - -- = a^-1 - eq_trans G b (op b e) (i a) - -- b = b * e - (eq_sym G (op b e) b (id_rg G op e i Hgroup b)) - -- b * e = a^-1 - (eq_trans G (op b e) (op b (op a (i a))) (i a) - --b * e = b * (a * a^-1) - (eq_cong G G e (op a (i a)) (op b) - -- e = a * a^-1 - (eq_sym G (op a (i a)) e (inv_rg G op e i Hgroup a))) - -- b * (a * a^-1) = a^-1 - (eq_trans G (op b (op a (i a))) (op (op b a) (i a)) (i a) - -- b * (a * a^-1) = (b * a) * a^-1 - (assoc_g G op e i Hgroup b a (i a)) - -- (b * a) * a^-1 = a^-1 - (eq_trans G (op (op b a) (i a)) (op e (i a)) (i a) - -- (b * a) * a^-1 = e * a^-1 - (eq_cong G G (op b a) e (fun (x : G) => op x (i a)) h) - -- e * a^-1 = a^-1 - (id_lg G op e i Hgroup (i a))))); + -- more "getters" + def monoid_g : monoid G op e := and_elim_l (monoid G op e) has_inverses Hgroup; + def assoc_g : assoc G op := assoc_m G op e monoid_g; + def id_lg : id_l G op e := id_lm G op e (and_elim_l (monoid G op e) has_inverses Hgroup); + def id_rg : id_r G op e := id_rm G op e (and_elim_l (monoid G op e) has_inverses Hgroup); + def inv_g : forall (a : G), inv G op e a (i a) := and_elim_r (monoid G op e) has_inverses Hgroup; + def left_inverse (a b : G) := inv_l G op e a b; + def right_inverse (a b : G) := inv_r G op e a b; + def inv_lg (a : G) : left_inverse a (i a) := and_elim_l (inv_l G op e a (i a)) (inv_r G op e a (i a)) (inv_g a); + def inv_rg (a : G) : right_inverse a (i a) := and_elim_r (inv_l G op e a (i a)) (inv_r G op e a (i a)) (inv_g a); + -- 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) := + -- b = b * e + -- = b * (a * a^-1) + -- = (b * a) * a^-1 + -- = e * a^-1 + -- = a^-1 + eq_trans G b (op b e) (i a) + -- b = b * e + (eq_sym G (op b e) b (id_rg b)) + -- b * e = a^-1 + (eq_trans G (op b e) (op b (op a (i a))) (i a) + --b * e = b * (a * a^-1) + (eq_cong G G e (op a (i a)) (op b) + -- e = a * a^-1 + (eq_sym G (op a (i a)) e (inv_rg a))) + -- b * (a * a^-1) = a^-1 + (eq_trans G (op b (op a (i a))) (op (op 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 (op (op b a) (i a)) (op e (i a)) (i a) + -- (b * a) * a^-1 = e * a^-1 + (eq_cong G G (op b a) e (fun (x : G) => op x (i a)) h) + -- e * a^-1 = a^-1 + (id_lg (i a))))); + +end Group diff --git a/lib/Elaborator.hs b/lib/Elaborator.hs index 05292f8..f79472e 100644 --- a/lib/Elaborator.hs +++ b/lib/Elaborator.hs @@ -47,33 +47,22 @@ sectionVarsL = lens sectionVars setter saveState :: ElabMonad a -> ElabMonad a saveState action = get >>= (action <*) . put -debugIRExpr :: IRExpr -> String -debugIRExpr = E.prettyS . elaborate - -debugIRDef :: IRDef -> String -debugIRDef (Def name (Just ty) body) = "def " ++ toString name ++ " : " ++ debugIRExpr ty ++ " := " ++ debugIRExpr body ++ ";" -debugIRDef (Def name Nothing body) = "def " ++ toString name ++ " := " ++ debugIRExpr body ++ ";" -debugIRDef (Axiom name typ) = "axiom " ++ toString name ++ " : " ++ debugIRExpr typ ++ ";" - -debugIRSectionDef :: IRSectionDef -> String -debugIRSectionDef (Variable name typ) = "variable " ++ toString name ++ " : " ++ debugIRExpr typ ++ ";" -debugIRSectionDef (Section name _) = "section " ++ toString name ++ ";" -debugIRSectionDef (IRDef def) = debugIRDef def - elabSection :: Text -> [IRSectionDef] -> ElabMonad [IRDef] elabSection _name contents = saveState $ concat <$> forM contents elabDef elabProgram :: IRProgram -> [IRDef] elabProgram prog = evalState (elabSection "" prog) (SectionContext [] []) -pushVariable :: Text -> IRExpr -> SectionContext -> SectionContext -pushVariable name ty (SectionContext defs vars) = SectionContext defs ((name, ty) : vars) +pushVariable :: Text -> IRExpr -> ElabMonad () +pushVariable name ty = do + newTy <- traverseBody ty + modify $ over sectionVarsL ((name, newTy) :) pushDefinition :: Text -> [(Text, IRExpr)] -> SectionContext -> SectionContext pushDefinition name defVars (SectionContext defs vars) = SectionContext ((name, defVars) : defs) vars removeName :: Text -> ElabMonad () -removeName name = do +removeName name = do modify $ over sectionDefsL (filter ((/= name) . fst)) modify $ over sectionVarsL (filter ((/= name) . fst)) @@ -167,7 +156,7 @@ elabDef (IRDef (Axiom name ty)) = do modify $ pushDefinition name vars pure [Axiom name (generalizeType ty vars)] elabDef (Section name contents) = saveState $ elabSection name contents -elabDef (Variable name ty) = [] <$ modify' (pushVariable name ty) +elabDef (Variable name ty) = [] <$ pushVariable name ty saveBinders :: State Binders a -> State Binders a saveBinders action = do