fixed beta equivalence check

README.md

@@ -3,7 +3,7 @@
 
 # Syntax
 
-The syntax is fairly flexible and should work as you expect. Identifiers can be Unicode as long as `megaparsec` calls them alphanumeric. `λ` and `\Pi` 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.
+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.
 
 All of the following example terms correctly parse, and should look familiar if you are used to standard lambda calculus notation or Coq syntax.
 
@@ -30,7 +30,7 @@ Line comments are `--` like in Haskell, and block comments are `(* *)` like ML (
 
 # 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 &ldquo;:q&rdquo;, press C-c, or press C-d to quit. Entering &ldquo;:e&rdquo; shows everything that has been defined along with their types. Entering &ldquo;:t <ident>&rdquo; prints the type of a particular identifier.
+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 &ldquo;:q&rdquo;, press C-c, or press C-d to quit. Entering &ldquo;:e&rdquo; shows everything that has been defined along with their types. Entering &ldquo;:t <ident>&rdquo; prints the type of a particular identifier. Entering &ldquo;:n <expr>&rdquo; will fully normalize (including unfolding definitions) an expression.
 
 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 &ldquo;:e&rdquo; in the repl) so you can verify that it worked.
 
@@ -87,7 +87,7 @@ Obviously not fully decidable, but I might be able to implement some basic unifi
 
 ### TODO Implicits
 
-Much, much more useful than [inference](#org79d490c), 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](#org6d7253e), 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
@@ -97,7 +97,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](#org357916d), but could be fun.
+Not really all that necessary, especially without [inductive definitions](#org89fc2b3), but could be fun.
 
 
 ### TODO Inductive Definitions
@@ -113,6 +113,11 @@ This is definitely a stretch goal. It would be cool though, and would turn this
 Right now, everything defaults to one line, which can be a problem with how large the proof terms get. Probably want to use [prettyprinter](https://hackage.haskell.org/package/prettyprinter) to be able to nicely handle indentation and line breaks.
 
 
+### TODO Smarter normalization/beta-equivalence checking
+
+I had what I thought was a smarter way to check for β-equivalence than just fully normalizing both terms and checking if they are the same, but it turned out to be a little wrong, which isn&rsquo;t too surprising since I just made it up. It&rsquo;s probably salvageable, but I&rsquo;d also like to look into other forms of normalization and checking for β-equivalence.
+
+
 ### TODO Better repl
 
 The repl is decent, but implementing something like [this](https://abhinavsarkar.net/posts/repling-with-haskeline/) would be awesome. I&rsquo;d also at least like to add a new command `":l <filename>"` to load the definitions from a file.
@@ -159,7 +164,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](#orgf503794), 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](#orgf8270fd), to better handle indentation, automatically adjust line numbers, etc.
 
 
 ### TODO TUI

README.org

@@ -4,7 +4,7 @@
 =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.
 
 * Syntax
-The syntax is fairly flexible and should work as you expect. Identifiers can be Unicode as long as =megaparsec= calls them alphanumeric. =λ= and =\Pi= 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.
+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.
 
 All of the following example terms correctly parse, and should look familiar if you are used to standard lambda calculus notation or Coq syntax.
 #+begin_src
@@ -29,7 +29,7 @@ Type ascriptions are optional. If included, =perga= will check to make sure your
 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
-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. Entering ":t <ident>" prints the type of a particular identifier.
+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. Entering ":t <ident>" prints the type of a particular identifier. Entering ":n <expr>" will fully normalize (including unfolding definitions) an expression.
 
 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.
 
@@ -92,6 +92,9 @@ This is definitely a stretch goal. It would be cool though, and would turn this
 *** TODO Prettier pretty printing
 Right now, everything defaults to one line, which can be a problem with how large the proof terms get. Probably want to use [[https://hackage.haskell.org/package/prettyprinter][prettyprinter]] to be able to nicely handle indentation and line breaks.
 
+*** TODO Smarter normalization/beta-equivalence checking
+I had what I thought was a smarter way to check for β-equivalence than just fully normalizing both terms and checking if they are the same, but it turned out to be a little wrong, which isn't too surprising since I just made it up. It's probably salvageable, but I'd also like to look into other forms of normalization and checking for β-equivalence.
+
 *** TODO Better repl
 The repl is decent, but implementing something like [[https://abhinavsarkar.net/posts/repling-with-haskeline/][this]] would be awesome. I'd also at least like to add a new command =":l <filename>"= to load the definitions from a file.
 

app/Repl.hs

@@ -1,7 +1,8 @@
 module Repl (repl, showEnvEntry) where
 
+import Control.Monad.Reader
 import Data.Functor (void)
-import Data.List (isPrefixOf)
+import Data.List (isPrefixOf, stripPrefix)
 import qualified Data.Map as M
 import qualified Data.Text as T
 import Eval
@@ -11,16 +12,15 @@ import System.Console.Haskeline
 import System.Directory (createDirectoryIfMissing, getHomeDirectory)
 import System.FilePath ((</>))
 
-data ReplCommand = Quit | DumpEnv | TypeQuery String | Input String deriving (Show)
+data ReplCommand = Quit | DumpEnv | TypeQuery String | Normalize String | Input String deriving (Show)
 
 parseCommand :: Maybe String -> Maybe ReplCommand
 parseCommand Nothing = Nothing
 parseCommand (Just ":q") = Just Quit
 parseCommand (Just ":e") = Just DumpEnv
 parseCommand (Just input)
-    | ":t" `isPrefixOf` input = case words input of
+    | ":t " `isPrefixOf` input = TypeQuery <$> stripPrefix ":t " input
-        [":t", rest] -> Just $ TypeQuery rest
+    | ":n " `isPrefixOf` input = Normalize <$> stripPrefix ":n " input
-        _ -> Nothing
     | otherwise = Just $ Input input
 
 showEnvEntry :: T.Text -> Expr -> String
@@ -57,6 +57,14 @@ repl = do
                     Just expr -> outputStrLn $ prettyS expr
                 )
                     >> 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
+                        Left err -> outputStrLn $ show err
+                        Right result -> outputStrLn $ prettyS result
+                )
+                    >> loop env
             Just (Input input) -> do
                 env' <- handleInput env input
                 loop env'

examples/example.pg

@@ -246,5 +246,10 @@ mul : nat -> nat -> nat := fun (n m : nat) (A : *) (f : A -> A) (x : A) => (m A
 -- 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.

lib/Eval.hs

@@ -38,21 +38,44 @@ whnf (App m n) = do
 whnf (Free n) = envLookup n
 whnf e = pure e
 
+reduce :: Expr -> ReaderT Env Result Expr
+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 e = pure e
+
+normalize :: Expr -> ReaderT Env Result Expr
+normalize e = do
+    e' <- reduce e
+    if e == e'
+        then pure e
+        else normalize e'
+
+-- naive beta equivalence check
 betaEquiv :: Expr -> Expr -> ReaderT Env Result Bool
-betaEquiv e1 e2
+betaEquiv e1 e2 = (==) <$> normalize e1 <*> normalize e2
-    | e1 == e2 = pure True
+
-    | otherwise = do
+-- this slightly smarter beta equivalence check is a little buggy,
-        e1' <- whnf e1
+-- failing to notice that `add one one` and `two` are beta equivalent in the
-        e2' <- whnf e2
+-- example file
-        case (e1', e2') of
+
-            (Var k1 _, Var k2 _) -> pure $ k1 == k2
+-- betaEquiv :: Expr -> Expr -> ReaderT Env Result Bool
-            (Free n, Free m) -> pure $ n == m
+-- betaEquiv e1 e2
-            (Free n, e) -> envLookup n >>= betaEquiv e
+--     | e1 == e2 = pure True
-            (e, Free n) -> envLookup n >>= betaEquiv e
+--     | otherwise = do
-            (Star, Star) -> pure True
+--         e1' <- whnf e1
-            (Abs _ t1 v1, Abs _ t2 v2) -> (&&) <$> betaEquiv t1 t2 <*> betaEquiv v1 v2 -- i want idiom brackets
+--         e2' <- whnf e2
-            (Pi _ t1 v1, Pi _ t2 v2) -> (&&) <$> betaEquiv t1 t2 <*> betaEquiv v1 v2
+--         case (e1', e2') of
-            _ -> pure False -- remaining cases impossible or false
+--             (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
+--             (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
+--             _ -> pure False -- remaining cases impossible or false
 
 checkBeta :: Env -> Expr -> Expr -> Result Bool
 checkBeta env e1 e2 = runReaderT (betaEquiv e1 e2) env
@@ -63,4 +86,4 @@ isSortPure Square = True
 isSortPure _ = False
 
 isSort :: Expr -> ReaderT Env Result (Bool, Expr)
-isSort s = (,s) . isSortPure <$> whnf s
+isSort s = (,s) . isSortPure <$> normalize s

lib/Parser.hs

@@ -1,6 +1,6 @@
 {-# LANGUAGE NamedFieldPuns #-}
 
-module Parser (parseProgram, parseDef, parseDefEmpty, GlobalState (..)) where
+module Parser (parseProgram, parseDef, parseDefEmpty, GlobalState (..), parseExpr) where
 
 import Check
 import Control.Monad
@@ -184,6 +184,9 @@ parseDef input = do
     put _gs
     pure $ first errorBundlePretty output
 
+parseExpr :: GlobalState -> Text -> Either String Expr
+parseExpr env input = first errorBundlePretty $ evalState (runParserT pExpr "" input) IS{_binds = [], _gs = env}
+
 parseDefEmpty :: GlobalState -> Text -> (Either String (), GlobalState)
 parseDefEmpty env input = runState (parseDef input) env