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.

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.

Terms

All of the following example terms correctly parse, and should look familiar if you are used to standard lambda calculus notation or Coq syntax.

λ (α : *) ⇒ λ (β : *) ⇒ λ (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)

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.

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.

let ( (<ident> (: <type>)? := <expr>) )+ in <expr> end

Below is a more concrete example.

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

You can also directly bind functions. Here's an example.

let (f (A : *) (x : A) : A := x) in
    f x
end

The syntax for binding functions is just like with definitions.

Definitions and Axioms

Definitions and axioms have abstract syntax as shown below.

def <ident> (<ident> : <type>)* : <type>? := <term>;
axiom <ident> (<ident> : <type>)* : <type>;

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

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;

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.

Sections

There is a Coq-like section mechanism. You open a section with section <identifier> and close it with end <identifier>. The identifiers used must match. The identifiers don't serve any purpose beyond organization.

section Test
    variable (A B : *);
    def id (x : A) := x;
    def const (x : A) (y : B) := id x;
end Test

def id_full (A : *) (x : A) := id A x;
def const_full (A B : *) (x : A) (y : B) := const A B x y;

In a section, you can add section variables to the context with either variable or hypothesis. The syntax is the same as function parameters, so you can define multiple variables in one line, and can group section variables of the same type. Then, in the section, any definition using the section variables will be automatically generalized over the section variables that they use. Furthermore, any usage of such section variables (like id x in the definition of const above) will automatically apply the necessary section variables.

Nested sections are supported, and work as you would expect.

Comments and preprocessor directives

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.

> :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)

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.

-- file: equality.pg

-- Defining Leibniz equality
-- Note that we can leave the ascription off
def 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.
def 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.
def 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.
def 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);

Running perga equality.pg yields the following output.

loading: equality.pg
success!

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

def 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);

Then running perga equality.pg yields the following output.

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'

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.