refactoring of algebra.pg, also fixed minor bug

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 <ident>". Entering ":t <expr>" prints the type of an expression. Entering ":n <expr>" will fully normalize (including unfolding definitions) an expression, while ":w <expr>" will reduce it to weak head normal form. Finally ":l <filepath>" 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 <ident>`. Entering `:t <expr>` prints the type of an expression. Entering `:n <expr>` will fully normalize (including unfolding definitions) an expression, while `:w <expr>` will reduce it to weak head normal form. Finally `:l <filepath>` loads a file.
 
 Here's an example session showing the capabilities of the repl.
 

examples/algebra.pg

@@ -8,41 +8,51 @@
 -- |                                        BASIC DEFINITIONS                                                   |
 -- --------------------------------------------------------------------------------------------------------------
 
+section BasicDefinitions
+
     -- 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 unary operation on a set `A` is a function `A -> A`
+    -- Fix some set A
-def unop (A : *) := A -> A;
+    variable (A : *);
 
--- a binary operation on a set `A` is a function `A -> A -> A`
+    -- a unary operation is a function `A -> A`
-def binop (A : *) := A -> A -> A;
+    def unop := A -> A;
 
--- a binary operation is associative if ...
+    -- a binary operation is a function `A -> A -> A`
-def assoc (A : *) (op : binop A) :=
+    def binop := A -> A -> A;
-    forall (a b c : A), eq A (op a (op b c)) (op (op a b) c);
 
--- an element `e : A` is a left identity with respect to binop `op` if `∀ a, e * a = a`
+    -- fix some binary operation `op`
-def id_l (A : *) (op : binop A) (e : A) :=
+    variable (op : binop);
-    forall (a : A), eq A (op e a) a;
+
+    -- it is associative if ...
+    def assoc := forall (a b c : A), eq A (op a (op b c)) (op (op 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 (op e a) a;
 
     -- likewise for right identity
-def id_r (A : *) (op : binop A) (e : A) :=
+    def id_r := forall (a : A), eq A (op a e) a;
-    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 (A : *) (op : binop A) (e : A) := and (id_l A op e) (id_r A op e);
+    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 : *) (op : binop A) (e : A) (a b : A) := eq A (op b a) e;
+    def inv_l (a b : A) := eq A (op b a) e;
 
     -- likewise for right inverse
-def inv_r (A : *) (op : binop A) (e : A) (a b : A) := eq A (op a b) e;
+    def inv_r (a b : A) := eq A (op a b) e;
 
     -- 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);
+    def inv (a b : A) := and (inv_l a b) (inv_r a b);
+
+end BasicDefinitions
 
 -- --------------------------------------------------------------------------------------------------------------
 -- |                                      ALGEBRAIC STRUCTURES                                                  |
@@ -51,28 +61,30 @@ 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;
 
+section Monoid
+
+    variable (M : *) (op : binop M) (e : M);
+
     -- a set `M` with binary operation `op` and element `e` is a monoid 
-def monoid (M : *) (op : binop M) (e : M) : * :=
+    def monoid : * := and (semigroup M op) (id M op e);
-    and (semigroup M op) (id M op e);
+
+    hypothesis (Hmonoid : 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 :=
+    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);
 
-def id_rm (M : *) (op : binop M) (e : M) (Hmonoid : monoid M op e) : id_r M op e :=
+    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);
 
-def assoc_m (M : *) (op : binop M) (e : M) (Hmonoid : monoid M op e) : assoc M op :=
+    def assoc_m : assoc M op := and_elim_l (semigroup M op) (id M op e) Hmonoid;
-    and_elim_l (semigroup M op) (id M op 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
+    def monoid_id_l_implies_identity (a : M) (H : id_l M op a) : eq M a e :=
-    (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
@@ -80,58 +92,50 @@ def monoid_id_l_implies_identity
                 -- 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))
+                    (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
+    def monoid_id_r_implies_identity (a : M) (H : id_r M op a) : eq M a e :=
-    (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
 
                 -- 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))
+                    (id_lm a))
 
                 -- and `e * a = e`
                 (H e);
 
+end Monoid
+
+section Group
+
+    variable (G : *) (op : binop G) (e : G) (i : unop G);
 
     -- groups are just monoids with inverses
-def has_inverses (G : *) (op : binop G) (e : G) (i : unop G) : * :=
+    def has_inverses : * := forall (a : G), inv G op e a (i a);
-    forall (a : G), inv G op e a (i a);
 
-def group (G : *) (op : binop G) (e : G) (i : unop G) : * :=
+    def group : * := and (monoid G op e) has_inverses;
-    and (monoid G op e)
+
-        (has_inverses G op e i);
+    hypothesis (Hgroup : group);
 
     -- more "getters"
-def monoid_g (G : *) (op : binop G) (e : G) (i : unop G) (Hgroup : group G op e i) : monoid G op e :=
+    def monoid_g : monoid G op e := and_elim_l (monoid G op e) has_inverses Hgroup;
-    and_elim_l (monoid G op e) (has_inverses G op e i) 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);
 
-def assoc_g (G : *) (op : binop G) (e : G) (i : unop G) (Hgroup : group G op e i) : assoc G op :=
+    -- An interesting theorem: left inverses are unique, i.e. if b * a = e, then b = a^-1
-    assoc_m G op e (monoid_g G op e i Hgroup);
+    def left_inv_unique (a b : G) (h : left_inverse a b) : eq G b (i a) :=
-
-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);
-
-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);
-
-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;
-
-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 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);
-
-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
@@ -139,21 +143,22 @@ def left_inv_unique (G : *) (op : binop G) (e : G) (i : unop G) (Hgroup : group
         --   = 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))
+        (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 G op e i Hgroup a)))
+                (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 G op e i Hgroup b a (i a))
+                (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 G op e i Hgroup (i a)))));
+                    (id_lg (i a)))));
 
+end Group

lib/Elaborator.hs

@@ -47,27 +47,16 @@ 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 :: Text -> IRExpr -> ElabMonad ()
-pushVariable name ty (SectionContext defs vars) = SectionContext defs ((name, ty) : vars)
+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
@@ -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