reworked and added many more examples

README.md

@@ -1,4 +1,4 @@
-`perga` is a basic proof assistant based on a dependently typed lambda calculus (calculus of constructions). 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 (though lacks a *primitive notion* system for the moment), and a touch less ergonomic.
+`perga` is a basic proof assistant based on a dependently typed lambda calculus (calculus of constructions). 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.
 
 
 # Syntax
@@ -15,7 +15,7 @@ I mostly stick to Coq syntax throughout this file and the examples, as that is w
 
 Definitions work similarly, having abstract syntax as shown below.
 
-    <ident> (<ident> : <type>)* : <type>? := <term>;
+    <ident> (<ident> : <type>)* : <type>? := <term> | axiom;
 
 (The distinction between `<type>` and `<term>` is for emphasis; they are the exact same syntactic category.) Here&rsquo;s a couple definitions of the `const` function from above showing the options with the syntax.
 
@@ -25,6 +25,8 @@ Definitions work similarly, having abstract syntax as shown below.
 
 Type ascriptions are optional. If included, `perga` will check to make sure your definition matches the ascription, and, if so, will remember the way your wrote the type when printing inferred types, which is particularly handy when using abbreviations for complex types. `perga` has no problem inferring the types of top-level definitions, as they are completely determined by the term, but I recommend including ascriptions most of the time, as they serve as a nice piece of documentation, help guide the implementation process, and make sure you are implementing the type you think you are.
 
+If the RHS of a definition is `axiom`, then `perga` will assume that the identifier is an inhabitant of the type ascribed to it (as such when using axioms, a type ascription is required). This allows you to use axioms.
+
 Line comments are `--` like in Haskell, and block comments are `(* *)` like ML (and nest properly). There is no significant whitespace, so you are free to format code as you wish.
 
 
@@ -59,7 +61,16 @@ You can also give `perga` a filename as an argument, in which case it will typec
 
 # Simple Example
 
-A much larger, commented example is located in <./examples/example.pg>. Here is an example file defining Leibniz equality and proving that it is reflexive, symmetric, and transitive.
+There are many very well commented examples in the <./examples/> folder. These include
+
+-   <./examples/logic.pg>, which defines the standard logical operators and proves standard results about them,
+-   <./examples/computation.pg>, which demonstrates using `perga` for computational purposes,
+-   <./examples/algebra.pg>, which defines standard algebraic structures and proves results for them, and
+-   <./examples/peano.pg>, which proves standard arithmetic results from the Peano axioms.
+
+I intend to extend these examples further.
+
+Here is an example file defining Leibniz equality and proving that it is reflexive, symmetric, and transitive.
 
     -- file: equality.pg
     
@@ -109,7 +120,7 @@ Obviously not fully decidable, but I might be able to implement some basic unifi
 
 ### TODO Implicits
 
-Much, much more useful than [inference](#org84d2ba6), implicit arguments would be amazing. It also seems a lot more complicated, but any system for dealing with implicit arguments is far better than none. Getting rid of stuff like [lines 213-215 of the example file](./examples/example.pg) would be amazing.
+Much, much more useful than [inference](#orgdba513b), implicit arguments would be amazing. It also seems a lot more complicated, but any system for dealing with implicit arguments is far better than none. Getting rid of stuff like [lines 213-215 of the example file](./examples/example.pg) would be amazing.
 
 
 ### TODO Module System
@@ -119,7 +130,7 @@ A proper module system would be wonderful. To me, ML style modules with structur
 
 ### TODO Universes?
 
-Not really all that necessary, especially without [inductive definitions](#orgfd1e388), but could be fun.
+Not really all that necessary, especially without [inductive definitions](#org1f674ce), but could be fun.
 
 
 ### TODO Inductive Definitions
@@ -186,7 +197,7 @@ I&rsquo;m imagining the parser could be chosen based on the file extension or so
 
 ### TODO treesitter parser and/or emacs mode
 
-Really not necessary, especially while the syntax is in a bit of flux, but would eventually be nice. The syntax is simple enough that a treesitter grammar shouldn&rsquo;t be too hard to write. An emacs mode would especially be nice if I ever get end up implementing an [alternate syntax](#org058ce83), to better handle indentation, automatically adjust line numbers, etc.
+Really not necessary, especially while the syntax is in a bit of flux, but would eventually be nice. The syntax is simple enough that a treesitter grammar shouldn&rsquo;t be too hard to write. An emacs mode would especially be nice if I ever get end up implementing an [alternate syntax](#org4dd267a), to better handle indentation, automatically adjust line numbers, etc.
 
 
 ### TODO TUI

README.org

@@ -1,7 +1,7 @@
 #+title: Perga
 #+options: toc:nil
 
-=perga= is a basic proof assistant based on a dependently typed lambda calculus (calculus of constructions). 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 (though lacks a /primitive notion/ system for the moment), and a touch less ergonomic.
+=perga= is a basic proof assistant based on a dependently typed lambda calculus (calculus of constructions). 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.
 
 * Syntax
 The syntax is fairly flexible and should work as you expect. Identifiers can be Unicode as long as =megaparsec= calls them alphanumeric. =λ= and =Π= abstractions can be written in many obvious ways that should be clear from the examples below. Additionally, arrows can be used as an abbreviation for a Π type where the parameter doesn't appear in the body as usual.
@@ -16,7 +16,7 @@ I mostly stick to Coq syntax throughout this file and the examples, as that is w
 
 Definitions work similarly, having abstract syntax as shown below.
 #+begin_src
-  <ident> (<ident> : <type>)* : <type>? := <term>;
+  <ident> (<ident> : <type>)* : <type>? := <term> | axiom;
 #+end_src
 (The distinction between =<type>= and =<term>= is for emphasis; they are the exact same syntactic category.) Here's a couple definitions of the =const= function from above showing the options with the syntax.
 #+begin_src
@@ -26,6 +26,8 @@ Definitions work similarly, having abstract syntax as shown below.
 #+end_src
 Type ascriptions are optional. If included, =perga= will check to make sure your definition matches the ascription, and, if so, will remember the way your wrote the type when printing inferred types, which is particularly handy when using abbreviations for complex types. =perga= has no problem inferring the types of top-level definitions, as they are completely determined by the term, but I recommend including ascriptions most of the time, as they serve as a nice piece of documentation, help guide the implementation process, and make sure you are implementing the type you think you are.
 
+If the RHS of a definition is =axiom=, then =perga= will assume that the identifier is an inhabitant of the type ascribed to it (as such when using axioms, a type ascription is required). This allows you to use axioms.
+
 Line comments are =--= like in Haskell, and block comments are =(* *)= like ML (and nest properly). There is no significant whitespace, so you are free to format code as you wish.
 
 * Usage
@@ -57,7 +59,14 @@ Here's an example session defining Church numerals and doing some computations w
 You can also give =perga= a filename as an argument, in which case it will typecheck every definition in the file. Upon finishing, which should be nearly instantaneous, it will print out all the definitions it parsed along with their types (like you had typed ":e" in the repl) so you can verify that it worked.
 
 * Simple Example
-A much larger, commented example is located in [[./examples/example.pg]]. Here is an example file defining Leibniz equality and proving that it is reflexive, symmetric, and transitive.
+There are many very well commented examples in the [[./examples/]] folder. These include
+- [[./examples/logic.pg]], which defines the standard logical operators and proves standard results about them,
+- [[./examples/computation.pg]], which demonstrates using =perga= for computational purposes,
+- [[./examples/algebra.pg]], which defines standard algebraic structures and proves results for them, and
+- [[./examples/peano.pg]], which proves standard arithmetic results from the Peano axioms.
+I intend to extend these examples further.
+
+Here is an example file defining Leibniz equality and proving that it is reflexive, symmetric, and transitive.
 #+begin_src
   -- file: equality.pg
   

app/Repl.hs

@@ -23,44 +23,44 @@ parseCommand (Just input)
     | ":n " `isPrefixOf` input = Normalize <$> stripPrefix ":n " input
     | otherwise = Just $ Input input
 
-showEnvEntry :: T.Text -> Expr -> String
-showEnvEntry k v = T.unpack k ++ " : " ++ prettyS v
+showEnvEntry :: T.Text -> EnvLine -> String
+showEnvEntry k EL{_ty = t} = T.unpack k ++ " : " ++ prettyS t
 
 dumpEnv :: Env -> InputT IO ()
 dumpEnv = void . M.traverseWithKey ((outputStrLn .) . showEnvEntry)
 
-handleInput :: GlobalState -> String -> InputT IO GlobalState
+handleInput :: Env -> String -> InputT IO Env
 handleInput env input =
     let (res, env') = parseDefEmpty env (T.pack input)
      in case res of
             Left err -> outputStrLn err >> pure env'
             Right () -> pure env'
 
-repl :: IO GlobalState
+repl :: IO Env
 repl = do
     home <- getHomeDirectory
     let basepath = home </> ".cache" </> "perga"
     let filepath = basepath </> "history"
     createDirectoryIfMissing True basepath
-    runInputT (defaultSettings{historyFile = Just filepath}) (loop GS{_defs = M.empty, _types = M.empty})
+    runInputT (defaultSettings{historyFile = Just filepath}) (loop M.empty)
   where
-    loop :: GlobalState -> InputT IO GlobalState
+    loop :: Env -> InputT IO Env
     loop env = do
         minput <- getInputLine "> "
         case parseCommand minput of
             Nothing -> pure env
             Just Quit -> pure env
-            Just DumpEnv -> dumpEnv (_types env) >> loop env
+            Just DumpEnv -> dumpEnv env >> loop env
             Just (TypeQuery input) ->
-                ( case M.lookup (T.pack input) (_types env) of
+                ( case M.lookup (T.pack input) env of
                     Nothing -> outputStrLn (input ++ " unbound")
-                    Just expr -> outputStrLn $ prettyS expr
+                    Just (EL{_ty = t}) -> outputStrLn $ prettyS t
                 )
                     >> loop env
             Just (Normalize input) ->
                 ( case parseExpr env (T.pack input) of
                     Left err -> outputStrLn err
-                    Right expr -> case runReaderT (normalize expr) (_defs env) of
+                    Right expr -> case runReaderT (normalize expr) env of
                         Left err -> outputStrLn $ show err
                         Right result -> outputStrLn $ prettyS result
                 )

examples/algebra.pg

@@ -0,0 +1,137 @@
+-- --------------------------------------------------------------------------------------------------------------
+-- |                                            BASIC LOGIC                                                     |
+-- --------------------------------------------------------------------------------------------------------------
+
+-- first some basic logic, see <examples/logic.pg> for more details on these definitions
+
+false : * := forall (A : *), A;
+false_elim (A : *) (contra : false) : A := contra A;
+
+not (A : *) : * := A -> false;
+not_intro (A : *) (h : A -> false) : not A := h;
+not_elim (A B : *) (a : A) (na : not A) : B := na a B;
+
+and (A B : *) : * := forall (C : *), (A -> B -> C) -> C;
+and_intro (A B : *) (a : A) (b : B) : and A B :=
+    fun (C : *) (H : A -> B -> C) => H a b;
+and_elim_l (A B : *) (ab : and A B) : A :=
+    ab A (fun (a : A) (b : B) => a);
+and_elim_r (A B : *) (ab : and A B) : B :=
+    ab B (fun (a : A) (b : B) => b);
+
+or (A B : *) : * := forall (C : *), (A -> C) -> (B -> C) -> C;
+or_intro_l (A B : *) (a : A) : or A B :=
+    fun (C : *) (ha : A -> C) (hb : B -> C) => ha a;
+or_intro_r (A B : *) (b : B) : or A B :=
+    fun (C : *) (ha : A -> C) (hb : B -> C) => hb b;
+or_elim (A B C : *) (ab : or A B) (ha : A -> C) (hb : B -> C) : C :=
+    ab C ha hb;
+
+eq (A : *) (x y : A) := forall (P : A -> *), P x -> P y;
+eq_refl (A : *) (x : A) : eq A x x := fun (P : A -> *) (Hx : P x) => Hx;
+eq_sym (A : *) (x y : A) (Hxy : eq A x y) : eq A y x := fun (P : A -> *) (Hy : P y) =>
+    Hxy (fun (z : A) => P z -> P x) (fun (Hx : P x) => Hx) Hy;
+eq_trans (A : *) (x y z : A) (Hxy : eq A x y) (Hyz : eq A y z) : eq A x z := fun (P : A -> *) (Hx : P x) =>
+    Hyz P (Hxy P Hx);
+eq_cong (A B : *) (x y : A) (f : A -> B) (H : eq A x y) : eq B (f x) (f y) :=
+  fun (P : B -> *) (Hfx : P (f x)) =>
+      H (fun (a : A) => P (f a)) Hfx;
+
+-- --------------------------------------------------------------------------------------------------------------
+-- |                                        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
+
+-- a unary operation on a set `A` is a function `A -> A`
+unop (A : *) := A -> A;
+
+-- a binary operation on a set `A` is a function `A -> A -> A`
+binop (A : *) := A -> A -> A;
+
+-- a binary operation is associative if ...
+assoc (A : *) (op : binop A) :=
+    forall (a b c : A), eq A (op (op a b) c) (op a (op b c));
+
+-- an element `e : A` is a left identity with respect to binop `op` if `∀ a, e * a = a`
+id_l (A : *) (op : binop A) (e : A) :=
+    forall (a : A), eq A (op e a) a;
+
+-- likewise for right identity
+id_r (A : *) (op : binop 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
+id (A : *) (op : binop A) (e : A) := and (id_l A op e) (id_r A op e);
+
+-- 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
+inv_l (A : *) (op : binop A) (e : A) (a b : A) := eq A (op b a) e;
+
+-- likewise for right inverse
+inv_r (A : *) (op : binop A) (e : A) (a b : A) := eq A (op a b) e;
+
+-- and full-on inverse
+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);
+
+-- --------------------------------------------------------------------------------------------------------------
+-- |                                      ALGEBRAIC STRUCTURES                                                  |
+-- --------------------------------------------------------------------------------------------------------------
+
+-- a set `S` with binary operation `op` is a semigroup if its operation is associative
+semigroup (S : *) (op : binop S) : * := assoc S op;
+
+-- a set `M` with binary operation `op` and element `e` is a monoid 
+monoid (M : *) (op : binop M) (e : M) : * :=
+    and (semigroup M op) (id M op 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
+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);
+
+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);
+
+-- now we can prove that, for any monoid, if `a` is a left identity, then it
+-- must be "the" identity
+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
+
+            -- 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))
+
+            -- now we need to show that `a * e = e`, but this immediately follows from `H`
+            (H e);
+
+-- the analogous result for right identities
+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
+
+            -- 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))
+
+            -- and `e * a = e`
+            (H e);
+  
+
+-- groups are just monoids with inverses
+group (G : *) (op : binop G) (e : G) (i : unop G) : * :=
+    and (monoid G op e)
+        (forall (a : G), inv G op e a (i a));

examples/computation.pg

@@ -0,0 +1,64 @@
+-- without recursion, computation is kind of hard
+-- we can, however, define natural numbers using the Church encoding and do
+-- computation with them
+
+-- the natural number `n` is encoded as the function taking any function
+-- `A -> A` and repeating it `n` times
+nat : * := forall (A : *), (A -> A) -> A -> A;
+
+-- zero is the constant function
+zero : nat := fun (A : *) (f : A -> A) (x : A) => x;
+
+-- `suc n` composes one more `f` than `n`
+suc : nat -> nat := fun (n : nat) (A : *) (f : A -> A) (x : A) => f ((n A f) x);
+
+-- addition can be encoded as usual
+plus : nat -> nat -> nat := fun (n m : nat) (A : *) (f : A -> A) (x : A) => (m A f) (n A f x);
+
+-- likewise for multiplication
+times : nat -> nat -> nat := fun (n m : nat) (A : *) (f : A -> A) (x : A) => (m A (n A f)) x;
+
+-- unforunately, it is impossible to prove induction on Church numerals,
+-- which makes it really hard to prove standard theorems, or do anything really.
+
+-- but we can still do computations with Church numerals
+
+-- first some abbreviations for numbers will be handy
+one   : nat := suc zero;
+two   : nat := suc one;
+three : nat := suc two;
+four  : nat := suc three;
+five  : nat := suc four;
+six   : nat := suc five;
+seven : nat := suc six;
+eight : nat := suc seven;
+nine  : nat := suc eight;
+ten   : nat := suc nine;
+
+-- now we can do a bunch of computations, even at the type level
+-- the way we can do this is by defining equality (see <examples/logic.pg> for
+-- more details on how this works) and proving a bunch of theorems like
+-- `plus one one = two` (how exciting!)
+-- then perga will only accept our proof if `plus one one` and `two` are beta
+-- equivalent
+
+-- first we do need a definition of equality
+eq (A : *) (x y : A) := forall (P : A -> *), P x -> P y;
+eq_refl (A : *) (x : A) : eq A x x := fun (P : A -> *) (Hx : P x) => Hx;
+eq_sym (A : *) (x y : A) (Hxy : eq A x y) : eq A y x := fun (P : A -> *) (Hy : P y) =>
+    Hxy (fun (z : A) => P z -> P x) (fun (Hx : P x) => Hx) Hy;
+eq_trans (A : *) (x y z : A) (Hxy : eq A x y) (Hyz : eq A y z) : eq A x z := fun (P : A -> *) (Hx : P x) =>
+    Hyz P (Hxy P Hx);
+eq_cong (A B : *) (x y : A) (f : A -> B) (H : eq A x y) : eq B (f x) (f y) :=
+  fun (P : B -> *) (Hfx : P (f x)) =>
+      H (fun (a : A) => P (f a)) Hfx;
+
+-- since `plus one one` and `two` are beta-equivalent, `eq_refl nat two` is a
+-- proof that `1 + 1 = 2`
+one_plus_one_is_two : eq nat (plus one one) two := eq_refl nat two;
+
+-- we can likewise compute 2 + 2
+two_plus_two_is_four : eq nat (plus two two) four := eq_refl nat four;
+
+-- even multiplication works
+two_times_five_is_ten : eq nat (times two five) ten := eq_refl nat ten;

examples/logic.pg

@@ -106,6 +106,11 @@ eq_sym (A : *) (x y : A) (Hxy : eq A x y) : eq A y x := fun (P : A -> *) (Hy : P
 eq_trans (A : *) (x y z : A) (Hxy : eq A x y) (Hyz : eq A y z) : eq A x z := fun (P : A -> *) (Hx : P x) =>
     Hyz P (Hxy P Hx);
 
+-- equality is a universal congruence
+eq_cong (A B : *) (x y : A) (f : A -> B) (H : eq A x y) : eq B (f x) (f y) :=
+  fun (P : B -> *) (Hfx : P (f x)) =>
+      H (fun (a : A) => P (f a)) Hfx;
+
 -- --------------------------------------------------------------------------------------------------------------
 
 -- Some logic theorems
@@ -185,71 +190,3 @@ and_distrib_l_or (A B C : *) (h : and A (or B C)) : or (and A B) (and A C) :=
             (and_intro A B (and_elim_l A (or B C) h) b))
         (fun (c : C) => or_intro_r (and A B) (and A C)
             (and_intro A C (and_elim_l A (or B C) h) c));
-
--- --------------------------------------------------------------------------------------------------------------
-
--- very little very basic algebra
-
--- what it means for a set and operation to be a semigroup
-semigroup (M : *) (op : M -> M -> M) : * :=
-    forall (a b c : M), eq M (op (op a b) c) (op a (op b c));
-
--- what it means for a set, operation, and identity element to be a monoid
-monoid (M : *) (op : M -> M -> M) (e : M) : * :=
-    and (semigroup M op)
-        (and (forall (a : M), eq M (op a e) a)
-             (forall (a : M), eq M (op e a) a));
-
--- identity elements in monoids are unique
-monoid_identity_unique
-    (M : *) (op : M -> M -> M) (e : M) (Hmonoid : monoid M op e)
-    (a : M) (H : forall (b : M), eq M (op a b) b) : eq M a e :=
-        eq_trans M a (op a e) e
-            -- a = a * e
-            (eq_sym M (op a e) a
-                (and_elim_l
-                    (forall (a : M), eq M (op a e) a)
-                    (forall (a : M), eq M (op e a) a)
-                    (and_elim_r
-                        (semigroup M op)
-                        (and (forall (a : M), eq M (op a e) a) (forall (a : M), eq M (op e a) a))
-                        Hmonoid) a))
-
-            -- a * e = e
-            (H e);
-  
-
--- what it means for a set, operation, identity element, and inverse map to be a group
-group (G : *) (op : G -> G -> G) (e : G) (inv : G -> G) : * :=
-    and (monoid G op e)
-        (and (forall (a : G), eq G (op a (inv a)) e)
-             (forall (a : G), eq G (op (inv a) a) e));
-
--- --------------------------------------------------------------------------------------------------------------
-
--- Church numerals
-
-nat : * := forall (A : *), (A -> A) -> A -> A;
-
--- zero is the constant function
-zero : nat := fun (A : *) (f : A -> A) (x : A) => x;
-
--- `suc n` composes one more `f` than `n`
-suc : nat -> nat := fun (n : nat) (A : *) (f : A -> A) (x : A) => f ((n A f) x);
-
--- addition as usual
-add : nat -> nat -> nat := fun (n m : nat) (A : *) (f : A -> A) (x : A) => (m A f) (n A f x);
-
--- multiplication as usual
-mul : nat -> nat -> nat := fun (n m : nat) (A : *) (f : A -> A) (x : A) => (m A (n A f)) x;
-
--- unforunately, I believe it is impossible to prove induction on Church numerals,
--- which makes it really hard to prove standard theorems, or do anything really.
-
--- that being said, we still can do computation with Church numerals at the
--- type level, which perga can understand
-one_plus_one_two : eq nat (add (suc zero) (suc zero)) (suc (suc zero)) :=
-    eq_refl nat (suc (suc zero));
-
--- with a primitive notion system, we could stipulate the existence of a type of
--- natural numbers satisfying the Peano axioms, but I haven't implemented that yet.

examples/peano.pg

@@ -0,0 +1,274 @@
+(*
+ * We need some basic logic, so I'm stealing this from <logic.pg>. See that file
+ * for more details on how these work.
+ *)
+
+false : * := forall (A : *), A;
+false_elim (A : *) (contra : false) : A := contra A;
+
+not (A : *) : * := A -> false;
+not_intro (A : *) (h : A -> false) : not A := h;
+not_elim (A B : *) (a : A) (na : not A) : B := na a B;
+
+and (A B : *) : * := forall (C : *), (A -> B -> C) -> C;
+and_intro (A B : *) (a : A) (b : B) : and A B :=
+    fun (C : *) (H : A -> B -> C) => H a b;
+and_elim_l (A B : *) (ab : and A B) : A :=
+    ab A (fun (a : A) (b : B) => a);
+and_elim_r (A B : *) (ab : and A B) : B :=
+    ab B (fun (a : A) (b : B) => b);
+
+or (A B : *) : * := forall (C : *), (A -> C) -> (B -> C) -> C;
+or_intro_l (A B : *) (a : A) : or A B :=
+    fun (C : *) (ha : A -> C) (hb : B -> C) => ha a;
+or_intro_r (A B : *) (b : B) : or A B :=
+    fun (C : *) (ha : A -> C) (hb : B -> C) => hb b;
+or_elim (A B C : *) (ab : or A B) (ha : A -> C) (hb : B -> C) : C :=
+    ab C ha hb;
+
+exists (A : *) (P : A -> *) : * := forall (C : *), (forall (x : A), P x -> C) -> C;
+exists_intro (A : *) (P : A -> *) (a : A) (h : P a) : exists A P :=
+    fun (C : *) (g : forall (x : A), P x -> C) => g a h;
+exists_elim (A B : *) (P : A -> *) (ex_a : exists A P) (h : forall (a : A), P a -> B) : B :=
+    ex_a B h;
+exists_elim_val (A : *) (P : A -> *) (ex_a : exists A P) : A :=
+  exists_elim A A P ex_a (fun (a : A) (_ : P a) => a);
+
+binop (A : *) := A -> A -> A;
+
+-- --------------------------------------------------------------------------------------------------------------
+
+(*
+ * Next we can define equality. This is the same as in <logic.pg>. We get a
+ * couple Peano axioms for free as theorems.
+ *)
+
+-- implies axiom 5
+-- (if `x : nat`, then `y : nat`, since we can only compare objects of the same type)
+eq (A : *) (x y : A) := forall (P : A -> *), P x -> P y;
+
+-- axiom 2 (but as a theorem)
+eq_refl (A : *) (x : A) : eq A x x := fun (P : A -> *) (Hx : P x) => Hx;
+
+-- axiom 3 (but as a theorem)
+eq_sym (A : *) (x y : A) (Hxy : eq A x y) : eq A y x := fun (P : A -> *) (Hy : P y) =>
+    Hxy (fun (z : A) => P z -> P x) (fun (Hx : P x) => Hx) Hy;
+
+-- axiom 4 (but as a theorem)
+eq_trans (A : *) (x y z : A) (Hxy : eq A x y) (Hyz : eq A y z) : eq A x z := fun (P : A -> *) (Hx : P x) =>
+    Hyz P (Hxy P Hx);
+
+-- This isn't an axiom, but is handy. If `x = y`, then `f x = f y`.
+eq_cong (A B : *) (x y : A) (f : A -> B) (H : eq A x y) : eq B (f x) (f y) :=
+  fun (P : B -> *) (Hfx : P (f x)) =>
+      H (fun (a : A) => P (f a)) Hfx;
+
+-- --------------------------------------------------------------------------------------------------------------
+
+(*
+ * Now we can define the Peano axioms. Unlike with equality, perga is not
+ * powerful enough to construct the natural numbers (or at least to prove the
+ * Peano axioms as theorems from a definition constructible in perga). However,
+ * working with axioms is extremely common in math. As such, perga has a system
+ * for doing just that, namely the *axiom* system.
+ *
+ * In a definition, rather than give a value for the term, we can give it the
+ * value `axiom`, in which case a type ascription is mandatory. Perga will then
+ * trust our type ascription, and assume going forward that the identifier we
+ * defined is a value of the asserted type. For example, we will use the axiom
+ * system to assert the existence of a type of natural numbers
+ *)
+
+nat : * := axiom;
+
+(*
+ * As you can imagine, this can be risky. For instance, there's nothing stopping
+ * us from saying
+ *     uh_oh : false := axiom;
+ * or stipulating more subtly contradictory axioms. As such, as in mathematics,
+ * axioms should be used with care.
+ *
+ * There's another problem with axioms, namely that perga cannot do any
+ * computations with axioms. The more you can define within perga natively, the
+ * better, as computations done without axioms can be utilized by perga. For
+ * example, in <computation.pg>, we define the natural numbers as Church
+ * numerals entirely within perga. There, the proof that `1 + 1 = 2` is just
+ * `eq_refl`, since they reduce to the same thing. Here, `1 + 1 = 2` will
+ * require a proof, since perga is unable to do computations with things defined
+ * as axioms.
+ *
+ * With these warnings in place, the Peano axioms are proven to be consistent,
+ * so we should be fine. I'm formalizing the second order axioms given in the
+ * wikipedia article on the Peano axioms
+ * (https://en.wikipedia.org/wiki/Peano_axioms).
+ *)
+
+-- axiom 1: 0 is a natural number
+zero : nat := axiom;
+
+-- axiom 6: For every `n`, `S n` is a natural number.
+suc (n : nat) : nat := axiom;
+
+-- axiom 7: If `S n = S m`, then `n = m`.
+suc_inj : forall (n m : nat), eq nat (suc n) (suc m) -> eq nat n m := axiom;
+
+-- axiom 8: No successor of any natural number is zero.
+suc_nonzero : forall (n : nat), not (eq nat (suc n) zero) := axiom;
+
+-- axiom 9: Induction! For any proposition φ on natural numbers, if φ(0) holds,
+-- and if for every natural number n, φ(n) ⇒ φ(S n), then φ holds for all n.
+nat_ind : forall (φ : nat -> *), φ zero -> (forall (n : nat), φ n -> φ (suc n))
+    -> forall (n : nat), φ n := axiom;
+
+-- --------------------------------------------------------------------------------------------------------------
+
+(*
+ * Now that we have stipulated these axioms, we are free to use them to make
+ * definitions, prove theorems, etc.
+ *
+ * Our first theorem, as a warm up, is to prove that every natural number is
+ * either 0 or the successor of another natural number.
+ *
+ * First, we will make a bunch of abbreviations, since these terms get really
+ * long and complicated really quickly.
+ *)
+
+-- First, the predecessor of `n` is `m` if `n = suc m`.
+pred (n m : nat) : * := eq nat n (suc m);
+
+-- Our claim is a disjunction, whose first option is that `n = 0`.
+szc_l (n : nat) := eq nat n zero;
+
+-- The second option is that `n` has a predecessor.
+szc_r (n : nat) := exists nat (fun (m : nat) => pred n m);
+
+-- So the claim we are trying to prove is that either one of the above options
+-- holds for every `n`.
+szc (n : nat) := or (szc_l n) (szc_r n);
+
+-- And here's our proof!
+suc_or_zero : forall (n : nat), szc n :=
+    -- We will prove this by induction.
+    nat_ind szc
+        -- For the base case, the first option holds, i.e. 0 = 0
+        (or_intro_l (szc_l zero) (szc_r zero) (eq_refl nat zero))
+
+        -- For the inductive case, suppose the theorem holds for `n`.
+        (fun (n : nat) (_ : szc n) => 
+            -- Then the right option holds for `suc n`, since `suc n` is the
+            -- successor of `n`
+            or_intro_r (szc_l (suc n)) (szc_r (suc n))
+                (exists_intro nat (pred (suc n)) n (eq_refl nat (suc n))));
+
+(*
+ * Now we would like to define addition and prove lots of lovely theorems about
+ * addition, but first we need a mechanism for even defining addition in the
+ * first place. The way we will go about this is proving that we can define
+ * functions recursively. In particular, we will prove that for any `A : *`, any
+ * `fzero : A`, and any `fsuc : nat -> A -> A`, there is a unique function
+ * `f : nat -> A` satisfying the following equations:
+ *   (1)    f zero    = fzero
+ *   (2)    f (suc x) = fsuc x (f x)
+ *)
+
+-- Here is equation (1)
+rec_cond_zero (A : *) (fzero : A) (fsuc : nat -> A -> A) (f : nat -> A) :=
+  eq A (f zero) fzero;
+
+-- And here's equation (2)
+rec_cond_suc (A : *) (fzero : A) (fsuc : nat -> A -> A) (f : nat -> A) :=
+  forall (x : nat) (y : A),
+    eq A (f x) y -> eq A (f (suc x)) (fsuc x y);
+
+(*
+ * Our proof strategy is to first define a relation `R` on `nat` such that
+ * `R x y` only holds if `f x = y` for every function `f : nat -> A` satisfying
+ * equations (1) and (2). Then we will prove that `R` is actually total, and use
+ * that to define our recursive function. Then we will show that all function
+ * satisfying equations (1) and (2) have the same outputs, and that this
+ * function actually satisfies the equations, meaning it is uniquely defined.
+ *)
+
+-- Here's the relation.
+rec_rel (A : *) (fzero : A) (fsuc : nat -> A -> A) (n : nat) (x : A) : * :=
+  forall (f : nat -> A),
+    rec_cond_zero A fzero fsuc f ->
+    rec_cond_suc A fzero fsuc f ->
+    eq A (f n) x;
+
+-- Little lemma showing that `R zero fzero`.
+rec_rel_zero (A : *) (fzero : A) (fsuc : nat -> A -> A)
+  : rec_rel A fzero fsuc zero fzero :=
+    fun (f : nat -> A)
+        (Hzero : rec_cond_zero A fzero fsuc f)
+        (Hsuc : rec_cond_suc A fzero fsuc f) =>
+      Hzero;
+
+-- Likewise, we show that if `R x y`, then `R (suc x) (fsuc x y)`.
+rec_rel_suc (A : *) (fzero : A) (fsuc : nat -> A -> A) (x : nat) (y : A)
+  (H : rec_rel A fzero fsuc x y) : rec_rel A fzero fsuc (suc x) (fsuc x y) :=
+    fun (f : nat -> A)
+        (Hzero : rec_cond_zero A fzero fsuc f)
+        (Hsuc : rec_cond_suc A fzero fsuc f) =>
+      Hsuc x y (H f Hzero Hsuc);
+
+-- This is an abbreviation for the statement that `R` is defined on `x`.
+rec_rel_def (A : *) (fzero : A) (fsuc : nat -> A -> A) : nat -> * :=
+  fun (x : nat) => exists A (rec_rel A fzero fsuc x); 
+
+-- Finally, we prove that `R` is total.
+rec_rel_total (A : *) (fzero : A) (fsuc : nat -> A -> A)
+  : forall (x : nat), rec_rel_def A fzero fsuc x :=
+    -- We prove this by induction.
+    nat_ind (rec_rel_def A fzero fsuc)
+
+    -- For our base case, since `R zero fzero` by the earlier lemma, `R` is defined on `zero`.
+    (exists_intro A (rec_rel A fzero fsuc zero) fzero (rec_rel_zero A fzero fsuc))
+
+    -- For the inductive case, let `x : nat` and suppose `R` is defined on `x`.
+    (fun (x : nat) (IH : rec_rel_def A fzero fsuc x) =>
+      -- Then let `y` be such that `R x y`.
+      exists_elim A (exists A (rec_rel A fzero fsuc (suc x))) (rec_rel A fzero fsuc x) IH
+        (fun (y : A) (H : rec_rel A fzero fsuc x y) =>
+          -- Then we claim `R (suc x) (fsuc x y)`.
+          exists_intro A (rec_rel A fzero fsuc (suc x)) (fsuc x y)
+          -- Indeed this follows by the earlier lemma.
+          (rec_rel_suc A fzero fsuc x y H)));
+
+-- With this, we can define a function `nat -> A`.
+rec_def (A : *) (fzero : A) (fsuc : nat -> A -> A) (x : nat) : A :=
+  exists_elim A A (rec_rel A fzero fsuc x)
+    (rec_rel_total A fzero fsuc x)
+    (fun (y : A) (_ : rec_rel A fzero fsuc x y) => y);
+
+-- Now we can prove that for any two functions `f g : nat -> A` satisfying
+-- equations (1) and (2), we must have that `f x = g x` for all `x : nat`.
+rec_def_unique (A : *) (fzero : A) (fsuc : nat -> A -> A) (f g : nat -> A)
+  (Fzero : rec_cond_zero A fzero fsuc f)
+  (Fsuc  : rec_cond_suc  A fzero fsuc f)
+  (Gzero : rec_cond_zero A fzero fsuc g)
+  (Gsuc  : rec_cond_suc  A fzero fsuc g)
+  : forall (x : nat), eq A (f x) (g x) :=
+    -- We prove this by induction.
+    nat_ind (fun (x : nat) => eq A (f x) (g x))
+      -- For the base case, we have
+      --    f zero = fzero    (by (1) for f)
+      --           = g zero   (by (1) for g)
+      (eq_trans A (f zero) fzero (g zero)
+        Fzero
+        (eq_sym A (g zero) fzero Gzero))
+      -- Now suppose `f x = g x`. We want to show that `f (suc x) = g (suc x)`.
+      (fun (x : nat) (IH : eq A (f x) (g x)) =>
+        -- Well, we have
+        --      f (suc x) = fsuc x (f x)    (by (2) for f)
+        --                = fsuc x (g x)    (by the inductive hypothesis)
+        --                = g (suc x)       (by (2) for g)
+        (eq_trans A (f (suc x)) (fsuc x (f x)) (g (suc x))
+          (Fsuc x (f x) (eq_refl A (f x)))
+          (eq_trans A (fsuc x (f x)) (fsuc x (g x)) (g (suc x))
+            (eq_cong A A (f x) (g x) (fun (y : A) => fsuc x y) IH)
+            (eq_sym A (g (suc x)) (fsuc x (g x))
+              (Gsuc x (g x) (eq_refl A (g x)))))));
+
+-- Almost there! We just need to show that `rec_def` actually satisfies the
+-- equations.

lib/Check.hs

@@ -7,7 +7,7 @@ import Control.Monad.Except (MonadError (throwError))
 import Control.Monad.Reader
 import Data.List ((!?))
 import Errors
-import Eval (Env, betaEquiv, envLookup, isSort, subst, whnf)
+import Eval (Env, betaEquiv, envLookupTy, isSort, subst, whnf)
 import Expr (Expr (..), incIndices, occursFree)
 
 type Context = [Expr]
@@ -26,7 +26,8 @@ findType g (Var n x) = do
     (sSort, s) <- findType g t >>= isSort
     unless sSort $ throwError $ NotASort t s
     pure t
-findType g (Free n) = envLookup n >>= findType g
+findType _ (Free n) = envLookupTy n
+findType _ (Axiom n) = envLookupTy n
 findType g e@(App m n) = do
     (a, b) <- findType g m >>= matchPi m
     a' <- findType g n

lib/Errors.hs

@@ -10,6 +10,7 @@ data Error
     | NotASort Expr Expr
     | ExpectedPiType Expr Expr
     | NotEquivalent Expr Expr Expr
+    | PNMissingType Text
     deriving (Eq, Ord)
 
 instance Show Error where
@@ -18,5 +19,6 @@ instance Show Error where
     show (NotASort x t) = "Expected " ++ prettyS x ++ " to have type * or □, instead found " ++ prettyS t
     show (ExpectedPiType x t) = prettyS x ++ " : " ++ prettyS t ++ " is not a function"
     show (NotEquivalent a a' e) = "Cannot unify " ++ prettyS a ++ " with " ++ prettyS a' ++ " when evaluating " ++ prettyS e
+    show (PNMissingType x) = "Primitive Notion " ++ T.unpack x ++ " missing type ascription"
 
 type Result = Either Error

lib/Eval.hs

@@ -9,7 +9,8 @@ import Data.Text (Text)
 import Errors
 import Expr
 
-type Env = M.Map Text Expr
+data EnvLine = EL {_ty :: Expr, _val :: Expr}
+type Env = M.Map Text EnvLine
 
 -- substitute s for k *AND* decrement indices; only use after reducing a redex.
 subst :: Integer -> Expr -> Expr -> Expr
@@ -18,14 +19,18 @@ subst k s (Var n x)
     | n > k = Var (n - 1) x
     | otherwise = Var n x
 subst _ _ (Free s) = Free s
+subst _ _ (Axiom s) = Axiom s
 subst _ _ Star = Star
 subst _ _ Square = Square
 subst k s (App m n) = App (subst k s m) (subst k s n)
 subst k s (Abs x m n) = Abs x (subst k s m) (subst (k + 1) (incIndices s) n)
 subst k s (Pi x m n) = Pi x (subst k s m) (subst (k + 1) (incIndices s) n)
 
-envLookup :: Text -> ReaderT Env Result Expr
-envLookup n = asks (M.lookup n) >>= maybe (throwError $ UnboundVariable n) pure
+envLookupVal :: Text -> ReaderT Env Result Expr
+envLookupVal n = asks ((_val <$>) . M.lookup n) >>= maybe (throwError $ UnboundVariable n) pure
+
+envLookupTy :: Text -> ReaderT Env Result Expr
+envLookupTy n = asks ((_ty <$>) . M.lookup n) >>= maybe (throwError $ UnboundVariable n) pure
 
 -- reduce until β reducts are impossible in head position
 whnf :: Expr -> ReaderT Env Result Expr
@@ -35,7 +40,7 @@ whnf (App m n) = do
     if m == m'
         then pure $ App m n
         else whnf $ App m' n
-whnf (Free n) = envLookup n
+whnf (Free n) = envLookupVal n
 whnf e = pure e
 
 reduce :: Expr -> ReaderT Env Result Expr
@@ -43,7 +48,7 @@ reduce (App (Abs _ _ v) n) = pure $ subst 0 n v
 reduce (App m n) = App <$> reduce m <*> reduce n
 reduce (Abs x t v) = Abs x <$> reduce t <*> reduce v
 reduce (Pi x t v) = Pi x <$> reduce t <*> reduce v
-reduce (Free n) = envLookup n
+reduce (Free n) = envLookupVal n
 reduce e = pure e
 
 normalize :: Expr -> ReaderT Env Result Expr
@@ -70,8 +75,8 @@ betaEquiv e1 e2 = (==) <$> normalize e1 <*> normalize e2
 --         case (e1', e2') of
 --             (Var k1 _, Var k2 _) -> pure $ k1 == k2
 --             (Free n, Free m) -> pure $ n == m
---             (Free n, e) -> envLookup n >>= betaEquiv e
---             (e, Free n) -> envLookup n >>= betaEquiv e
+--             (Free n, e) -> envLookupVal n >>= betaEquiv e
+--             (e, Free n) -> envLookupVal n >>= betaEquiv e
 --             (Star, Star) -> pure True
 --             (Abs _ t1 v1, Abs _ t2 v2) -> (&&) <$> betaEquiv t1 t2 <*> betaEquiv v1 v2 -- i want idiom brackets
 --             (Pi _ t1 v1, Pi _ t2 v2) -> (&&) <$> betaEquiv t1 t2 <*> betaEquiv v1 v2

lib/Expr.hs

@@ -7,6 +7,7 @@ import qualified Data.Text as T
 data Expr where
     Var :: Integer -> Text -> Expr
     Free :: Text -> Expr
+    Axiom :: Text -> Expr
     Star :: Expr
     Square :: Expr
     App :: Expr -> Expr -> Expr
@@ -16,6 +17,8 @@ data Expr where
 
 instance Eq Expr where
     (Var n _) == (Var m _) = n == m
+    (Free s) == (Free t) = s == t
+    (Axiom a) == (Axiom b) = a == b
     Star == Star = True
     Square == Square = True
     (App e1 e2) == (App f1 f2) = e1 == f1 && e2 == f2
@@ -26,6 +29,7 @@ instance Eq Expr where
 occursFree :: Integer -> Expr -> Bool
 occursFree n (Var k _) = n == k
 occursFree _ (Free _) = False
+occursFree _ (Axiom _) = False
 occursFree _ Star = False
 occursFree _ Square = False
 occursFree n (App a b) = on (||) (occursFree n) a b
@@ -37,6 +41,7 @@ shiftIndices d c (Var k x)
     | k >= c = Var (k + d) x
     | otherwise = Var k x
 shiftIndices _ _ (Free s) = Free s
+shiftIndices _ _ (Axiom s) = Axiom s
 shiftIndices _ _ Star = Star
 shiftIndices _ _ Square = Square
 shiftIndices d c (App m n) = App (shiftIndices d c m) (shiftIndices d c n)
@@ -87,6 +92,7 @@ showParamGroup (ids, ty) = parenthesize $ T.unwords ids <> " : " <> pretty ty
 helper :: Integer -> Expr -> Text
 helper _ (Var _ s) = s
 helper _ (Free s) = s
+helper _ (Axiom s) = s
 helper _ Star = "*"
 helper _ Square = "□"
 helper k (App e1 e2) = if k > 3 then parenthesize res else res

lib/Parser.hs

@@ -1,6 +1,6 @@
 {-# LANGUAGE NamedFieldPuns #-}
 
-module Parser (parseProgram, parseDef, parseDefEmpty, GlobalState (..), parseExpr) where
+module Parser (parseProgram, parseDef, parseDefEmpty, parseExpr) where
 
 import Check
 import Control.Monad
@@ -26,10 +26,9 @@ import Text.Megaparsec.Char
 import qualified Text.Megaparsec.Char.Lexer as L
 
 data TypeDef = TD {_ident :: Text, _type :: Expr}
-data DefinitionLine = DL {_td :: TypeDef, _body :: Expr}
+data DefinitionLine = DL {_td :: TypeDef, _body :: Expr} | PN TypeDef
 
-data GlobalState = GS {_defs :: Env, _types :: Env}
-data InnerState = IS {_binds :: [TypeDef], _gs :: GlobalState}
+data InnerState = IS {_binds :: [TypeDef], _env :: Env}
 
 newtype TypeError = TE Error
     deriving (Eq, Ord, Show)
@@ -42,11 +41,8 @@ instance ShowErrorComponent TypeError where
 bindsToIS :: ([TypeDef] -> [TypeDef]) -> InnerState -> InnerState
 bindsToIS f x@(IS{_binds}) = x{_binds = f _binds}
 
-defsToIS :: (Env -> Env) -> InnerState -> InnerState
-defsToIS f x@(IS{_gs = y@GS{_defs}}) = x{_gs = y{_defs = f _defs}}
-
-typesToIS :: (Env -> Env) -> InnerState -> InnerState
-typesToIS f x@(IS{_gs = y@GS{_types}}) = x{_gs = y{_types = f _types}}
+modifyEnv :: (Env -> Env) -> InnerState -> InnerState
+modifyEnv f x@(IS{_env}) = x{_env = f _env}
 
 skipSpace :: Parser ()
 skipSpace =
@@ -72,6 +68,9 @@ pVar = label "variable" $ lexeme $ do
         Just i -> Var (fromIntegral i) var
         Nothing -> Free var
 
+pPN :: Parser ()
+pPN = label "primitive notion" $ lexeme $ defChoice $ "PN" :| ["axiom"]
+
 defChoice :: NE.NonEmpty Text -> Parser ()
 defChoice options = lexeme $ label (T.unpack $ NE.head options) $ void $ choice $ NE.map chunk options
 
@@ -124,11 +123,11 @@ pSquare = lexeme $ Square <$ defChoice ("□" :| ["[]"])
 
 checkAscription :: Text -> Expr -> Maybe Expr -> Parser DefinitionLine
 checkAscription ident value massert = do
-    IS{_gs = GS{_defs, _types}} <- get
-    case (checkType _defs value, massert) of
+    IS{_env} <- get
+    case (checkType _env value, massert) of
         (Left err, _) -> customFailure $ TE err
         (Right ty, Nothing) -> pure DL{_td = TD{_ident = ident, _type = ty}, _body = value}
-        (Right ty, Just assert) -> case checkBeta _defs ty assert of
+        (Right ty, Just assert) -> case checkBeta _env ty assert of
             Left err -> customFailure $ TE err
             Right equiv -> do
                 unless equiv $ customFailure $ TE $ NotEquivalent ty assert value
@@ -136,8 +135,13 @@ checkAscription ident value massert = do
 
 updateStateDefinition :: DefinitionLine -> Parser ()
 updateStateDefinition DL{_td, _body} = do
-    modify $ defsToIS (M.insert (_ident _td) _body)
-    modify $ typesToIS (M.insert (_ident _td) (_type _td))
+    modify $
+        modifyEnv
+            (M.insert (_ident _td) EL{_ty = _type _td, _val = _body})
+updateStateDefinition (PN TD{_type, _ident}) = do
+    modify $
+        modifyEnv
+            (M.insert _ident EL{_ty = _type, _val = Axiom _ident})
 
 pDef :: Parser DefinitionLine
 pDef = lexeme $ label "definition" $ do
@@ -146,10 +150,19 @@ pDef = lexeme $ label "definition" $ do
     params <- pManyParams
     ascription <- fmap (flip (foldr (uncurry Pi)) params) <$> pAscription
     _ <- defChoice $ pure ":="
-    value <- flip (foldr (uncurry Abs)) params <$> pExpr
-    res <- checkAscription ident value ascription
-    _ <- defChoice $ pure ";"
-    pure res
+    choice
+        [ do
+            _ <- pPN
+            _ <- defChoice $ pure ";"
+            case ascription of
+                Just ty -> pure $ PN TD{_ident = ident, _type = ty}
+                Nothing -> customFailure $ TE $ PNMissingType ident
+        , do
+            value <- flip (foldr (uncurry Abs)) params <$> pExpr
+            res <- checkAscription ident value ascription
+            _ <- defChoice $ pure ";"
+            pure res
+        ]
 
 pDefUpdate :: Parser ()
 pDefUpdate = pDef >>= updateStateDefinition
@@ -175,20 +188,20 @@ pAscription :: Parser (Maybe Expr)
 pAscription = lexeme $ optional $ try $ defChoice (pure ":") >> label "type" pExpr
 
 pProgram :: Parser Env
-pProgram = lexeme $ skipSpace >> many pDefUpdate >> _types . _gs <$> get
+pProgram = lexeme $ skipSpace >> many pDefUpdate >> _env <$> get
 
-parseDef :: Text -> State GlobalState (Either String ())
+parseDef :: Text -> State Env (Either String ())
 parseDef input = do
     env <- get
-    let (output, IS{_gs}) = runState (runParserT pDefUpdate "" input) (IS{_binds = [], _gs = env})
-    put _gs
+    let (output, IS{_env}) = runState (runParserT pDefUpdate "" input) (IS{_binds = [], _env = env})
+    put _env
     pure $ first errorBundlePretty output
 
-parseExpr :: GlobalState -> Text -> Either String Expr
-parseExpr env input = first errorBundlePretty $ evalState (runParserT pExpr "" input) IS{_binds = [], _gs = env}
+parseExpr :: Env -> Text -> Either String Expr
+parseExpr env input = first errorBundlePretty $ evalState (runParserT pExpr "" input) IS{_binds = [], _env = env}
 
-parseDefEmpty :: GlobalState -> Text -> (Either String (), GlobalState)
+parseDefEmpty :: Env -> Text -> (Either String (), Env)
 parseDefEmpty env input = runState (parseDef input) env
 
 parseProgram :: Text -> Either String Env
-parseProgram input = first errorBundlePretty $ evalState (runParserT pProgram "" input) IS{_binds = [], _gs = GS{_defs = M.empty, _types = M.empty}}
+parseProgram input = first errorBundlePretty $ evalState (runParserT pProgram "" input) IS{_binds = [], _env = M.empty}