#+title: Perga
#+options: toc:nil

=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.

* 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 the usual 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
  λ (α : *) ⇒ λ (β : *) ⇒ λ (x : α) ⇒ λ (y : β) ⇒ x
  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)
#+end_src
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 "\to". 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.

=Let= expressions have syntax shown below.
#+begin_src
  let ( (<ident> (: <type>)? := <expr>) )+ in <expr> end
#+end_src
Below is a more concrete example.
#+begin_src
  let (a : A := (and_elim_l A (and B C) h))
      (bc := (and_elim_r A (and B C) h))
      (b := (and_elim_l B C bc))
      (c := (and_elim_r B C bc))
  in
      and_intro (and A B) C (and_intro A B a b) c
  end
#+end_src
You can also directly bind functions. Here's an example.
#+begin_src
  let (f (A : *) (x : A) : A := x) in
      f x
  end
#+end_src
The syntax for binding functions is just like with definitions.

Definitions and axioms have abstract syntax as shown below.
#+begin_src
  def <ident> (<ident> : <type>)* : <type>? := <term>;
  axiom <ident> (<ident> : <type>)* : <type>;
#+end_src
(The distinction between =<type>= and =<term>= is purely 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, and a more complex example declaring functional extensionality as an axiom (assuming equality has been previously defined having type =eq : Π (A : *) → A → A → *=). Duplicate definitions are not normally allowed and will result in an error.
#+begin_src
  def const := λ (α : *) ⇒ λ (β : *) ⇒ λ (x : α) => λ (y : β) => x;
  def const : ∀ (α β : *), α → β → α := fun (α β : *) (x : α) (y : β) ⇒ x;
  def const (α β : *) (x : α) (y : β) : α := x;

  axiom funext (A B : *) (f g : A → B) : (∀ (x : A), eq B (f x) (g x)) → eq (A → B) f g;
#+end_src
Type ascriptions are optional in both definitions and =let= bindings. 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 =[* *]= somewhat like ML (and nest properly). There is no significant whitespace, so you are free to format code as you wish.

There isn't a proper module system (yet), but you can include other files in a dumb, C preprocessor way by using =@include <filepath>= (NOTE: this unfortunately messes up line numbers in error messages). Filepaths are relative to the current file. Additionally, =@include= automatically keeps track of what has been included, so duplicate inclusions are skipped, meaning no include guards are necessary.

* 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.

Here's an example session showing the capabilities of the repl.
#+begin_src text
  > :l examples/computation.pg
  loading: examples/computation.pg
  > :e
  eight : nat
  eq : ∏ (A : *) . A -> A -> *
  eq_cong : ∏ (A B : *) (x y : A) (f : A -> B) . eq A x y -> eq B (f x) (f y)
  eq_refl : ∏ (A : *) (x : A) . eq A x x
  eq_sym : ∏ (A : *) (x y : A) . eq A x y -> eq A y x
  eq_trans : ∏ (A : *) (x y z : A) . eq A x y -> eq A y z -> eq A x z
  five : nat
  four : nat
  nat : *
  nine : nat
  one : nat
  one_plus_one_is_two : eq nat (plus one one) two
  plus : nat -> nat -> nat
  seven : nat
  six : nat
  suc : nat -> nat
  ten : nat
  three : nat
  times : nat -> nat -> nat
  two : nat
  two_plus_two_is_four : eq nat (plus two two) four
  two_times_five_is_ten : eq nat (times two five) ten
  zero : nat
  > :n plus one one
  λ (A : *) (f : A -> A) (x : A) . f (f x)
  > :n two
  λ (A : *) (f : A -> A) (x : A) . f (f x)
  > :w plus one one
  λ (A : *) (f : A -> A) (x : A) . one A f (one A f x)
  > :w two
  λ (A : *) (f : A -> A) (x : A) . f (one A f x)
#+end_src

You can also give =perga= a filename as an argument, in which case it will typecheck every definition in the file. If you give =perga= multiple filenames, it will process each one in turn, sharing an environment between them. Upon finishing, which should be nearly instantaneous, it will print out all files it processed, and "success!" if it successfully typechecked, and the first error it encountered otherwise.

* Simple Example
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/classical.pg]], which asserts the law of the excluded middle as an axiom, and proves several results that require it,
- [[./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
  
  -- Defining Leibniz equality
  -- Note that we can leave the ascription off
  eq (A : *) (x y : A) := forall (P : A -> *), P x -> P y;

  -- Equality is reflexive, which is easy to prove
  -- Here we give an ascription so that when `perga` reports the type,
  -- it references `eq` rather than inferring the type.
  eq_refl (A : *) (x : A) : eq A x x := fun (P : A -> *) (Hx : P x) => Hx;

  -- Equality is symmetric. This one's a little harder to prove.
  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;

  -- Equality is transitive.
  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);
#+end_src
Running =perga equality.pg= yields the following output.
#+begin_src
  loading: equality.pg
  success!
#+end_src
This means our proofs were accepted.

If we had an error in the proofs, we would get a somewhat useful error message. For example, if we had defined =eq_trans= as shown below, it would be incorrect (missing the =P= after =Hxy=).
#+begin_src
  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 Hx);
#+end_src
Then running =perga equality.pg= yields the following output.
#+begin_src 
  loading: equality.pg
  19:50:
     |
  19 |     fun (P : A -> *) (Hx : P x) => Hyz P (Hxy Hx);
     |                                                  ^
  Cannot unify 'A -> *' with 'P x' when evaluating 'Hxy Hx'
#+end_src
This indicates that, when evaluating =Hxy Hx=, it was expecting something of type =A -> *=, but instead found something of type =P x=. Since =P= is type =A -> *=, we can then realize that we forgot the =P=.