The leanmini Language

Running scripts

The runner is the binary mini-lean built from src/main.rs.

cargo run -- examples/identity.leanmini    # run a script file
cargo run                                  # interactive session on stdin
cargo test                                 # the kernel's own test suite

A script is a sequence of lines. The runner processes them from top to bottom and stops at the first error, printing the message and exiting with status 1. Blank lines and lines beginning with # are comments and are skipped.

# This is a comment.
goal forall (P : Sort 0), P -> P

Without a file argument the runner reads the same commands from standard input, one per line, after printing a reminder of the available commands. Errors are reported with the prefix error: and the session continues. The command quit (or exit) ends it. One command differs between the two modes: in a file, an inductive block is the header line followed by its | lines; interactively, the block is closed by a line containing only end.

Terms

A term is written in one of the following forms. A, B, t stand for terms and x for a name.

Application associates to the left and binds tightest: f a b is (f a) b. Arrows associate to the right: A -> B -> C is A -> (B -> C). A forall or fun extends as far to the right as possible, and so does the right-hand side of an arrow, so A -> forall (x : B), C needs no parentheses. A forall or fun used as an argument must be parenthesized, as in Nat.rec1 (fun (_n : Nat) => Nat) m. The arrow A -> B is read as forall (_ : A), B; the name _ is reserved for this purpose and may not be used as a binder in an inductive declaration.

The tokenizer splits on whitespace and on the characters (, ), ,, :, and the two-character symbols -> and =>. A name is a run of letters, digits, _, ', and ., so Nat.succ, List.rec1, and x' are single names. Three Unicode characters are accepted as aliases: → for ->, λ for fun, and ∀ for forall. Any other character is rejected with unexpected character: ....

Names are resolved when the term is parsed, not later.

• A name bound by an enclosing fun or forall, or present in the current goal's context, is a local variable.
• Otherwise, a name declared in the kernel (by inductive, def, axiom, or recursor, or built in) is a constant.
• Otherwise the parse fails with unknown identifier: x. This is also the error you get for a misspelled constructor or for using a hypothesis that has not been introduced yet.

A local shadows a constant of the same name. The parser never guesses types: Sort must be followed by a numeral, and a binder must be written (x : A) with its type.

Declarations

Inductive types

inductive List (A : Sort 1) : Sort 1 where
  | nil
  | cons (head : A) (tail : List A)

The header has the form inductive Name (p : P) ... (index i : J) ... : Sort u where. Each parenthesized binder is a parameter, or an index if it starts with the word index. Parameters must come before indices (parameters must precede indices). The universe after the colon must be a literal Sort u (inductive result must be Sort u), and the line must end with where.

Each following line begins with | and declares one constructor: | ctor (field : T) ... [: Name params indices]. Field types may mention the parameters, the earlier fields, and Name itself. The result type after the optional colon must be Name applied to the parameters, in order and unchanged (constructor parameters must be uniform), followed by one index term per index. If the type has indices, every constructor must give its result type (indexed constructor requires explicit result type); if it has none, the result type may be omitted. The index keyword is not allowed on constructor fields.

inductive Vec (A : Sort 1) (index n : Nat) : Sort 1 where
  | nil : Vec A Nat.zero
  | cons (n : Nat) (head : A) (tail : Vec A n) : Vec A (Nat.succ n)

Constructors are registered under qualified names: the declaration above adds Vec.nil and Vec.cons, and the constructors of List are List.nil and List.cons. Scripts must use the qualified form.

Accepting the declaration runs the four conditions of Chapter 8: the type of Name is a type, each constructor type is a type that ends in Name applied to the parameters, every field that mentions Name is strictly positive, and no field lives in a universe above Sort u when u is at least 1. The messages for failures include non-strictly-positive / unsupported recursive field, field f lives in Sort w, exceeding inductive universe Sort u, and inductive occurrence inside result index. Binder names starting with _ or __ are refused (reserved binder name), because the kernel uses such names for the binders it generates.

On success the runner prints inductive Name registered and the kernel adds the type former, the constructors, the recursor Name.rec0, and, when large elimination is allowed, Name.rec1. A proposition (Sort 0) gets Name.rec1 only if it is a subsingleton, as Chapter 8 explains.

Definitions and axioms

def add : Nat -> Nat -> Nat := fun (m : Nat) => fun (n : Nat) => Nat.rec1 (fun (_n : Nat) => Nat) m (fun (k : Nat) => fun (r : Nat) => Nat.succ r) n
axiom em : forall (P : Sort 0), P -> P

def name : T := t checks that T is a type and that t : T in the empty context, then adds name with the body t; the kernel unfolds it during reduction ($\delta$-reduction, Chapter 12). The runner prints defined name. A definition must fit on one line, and the first := separates type from body.

axiom name : T adds name : T without a body, after checking that T is a type. It prints added axiom name. Axioms never unfold. Nothing prevents you from assuming something false this way; the kernel checks that the type is well formed, not that it is true.

Names must be new: redeclaring one fails with duplicate declaration: name, and nothing may be declared inside the namespace Name.rec... of an existing inductive type.

Extra recursors

recursor Nat 2

recursor I v generates I.recv for the elimination universe v, if it does not exist yet, and prints generated I.recv. Levels 0 and 1 are generated automatically by inductive; use this command when a motive needs to return a type in Sort 2 or higher. It fails for a proposition that does not allow large elimination (I is not a subsingleton proposition; cannot eliminate into Sort v).

The standard kernel

Every session starts with Nat and Eq already declared, as if the following declarations had been run. The generated binder names begin with __; they are shown here as M and m for readability, and renaming bound variables does not change a type.

Nat      : Sort 1
Nat.zero : Nat
Nat.succ : Nat -> Nat
Nat.rec0 : forall (M : Nat -> Sort 0), M Nat.zero -> (forall (n : Nat), M n -> M (Nat.succ n)) -> forall (x : Nat), M x
Nat.rec1 : forall (M : Nat -> Sort 1), M Nat.zero -> (forall (n : Nat), M n -> M (Nat.succ n)) -> forall (x : Nat), M x

Eq       : forall (A : Sort 1), A -> A -> Sort 0
Eq.refl  : forall (A : Sort 1), forall (a : A), Eq A a a
Eq.rec0  : forall (A : Sort 1), forall (a : A), forall (M : forall (b : A), Eq A a b -> Sort 0), M a (Eq.refl A a) -> forall (b : A), forall (h : Eq A a b), M b h
Eq.rec1  : forall (A : Sort 1), forall (a : A), forall (M : forall (b : A), Eq A a b -> Sort 1), M a (Eq.refl A a) -> forall (b : A), forall (h : Eq A a b), M b h

Nat.rec1 is recursion into types and Nat.rec0 is induction into propositions (Chapter 7). Eq takes its type argument A explicitly, so the equation $a = b$ in $\Nat$ is written Eq Nat a b, and its proof by reflexivity is Eq.refl Nat a (Chapter 9). Because Eq is declared with A : Sort 1, equality is available for types in Sort 1 such as Nat and List Nat, not for propositions.

In general the recursor of an inductive type I into Sort v is named I.recv: List.rec0, List.rec1, Vec.rec1, and so on. Its argument order is parameters, motive, one minor premise per constructor in declaration order, indices, and finally the major premise (Chapter 8).

Proofs

Starting a goal

goal forall (n : Nat), Eq Nat n n

goal T checks that T is a type in the empty context and starts a proof with the single goal ?0 : T. It prints nothing in the command-line runner (the playgrounds print the goal). Any tactic given before a goal fails with start with 'goal <type>'. Starting a new goal abandons an unfinished proof.

After every tactic, the runner prints the remaining goals, each as its number, its hypotheses, and its target after a turnstile:

?3:
  n : Nat
  k : Nat
  ih : Eq Nat (add Nat.zero k) k
  ⊢ Eq Nat (add Nat.zero (Nat.succ k)) (Nat.succ k)

When no goals are left it prints No goals. Run 'qed' to kernel-check. The command show prints the goals without changing anything.

Tactics always act on the first goal. Terms given to tactics are parsed in that goal's context, so hypothesis names are in scope. Chapter 10 explains what each tactic does to the partial proof term; this section states the interface.

Tactics

intro x requires the target to reduce to a forall or an arrow. It adds x : A to the context, where A is the domain, and makes the body the new target. The name must not already be in the context (binder name already in context); otherwise the message is intro expects a Pi/arrow goal.

exact t closes the goal with t, after checking t against the target. A mismatch is reported by the kernel as type mismatch: actual ..., expected ....

apply f infers the type of f and peels off non-dependent arrows until the result is definitionally equal to the target; each peeled domain becomes a new goal, in order. If the type of f already matches the target, apply f behaves like exact f. Dependent binders are refused with dependent apply requires elaboration/unification, and a result that never matches gives apply result does not match the goal.

change T replaces the target by T, which must be a type definitionally equal to it (change expects definitionally equal target). It is used to expose a subterm that only appears after computation, before rw.

rfl requires the target to reduce to Eq A a b (rfl expects Eq A lhs rhs) with a and b definitionally equal (rfl: sides are not definitionally equal), and closes it with Eq.refl A a.

rw h requires h to have a type that reduces to Eq A a b (rw expects proof of equality). It replaces every occurrence of a in the target by b and leaves the rewritten target as the new goal. Occurrences are found syntactically, up to the names of bound variables; a term that is only equal after computation is not found, which gives rw: no syntactic occurrence of lhs in goal; use change first. Unlike Lean's rw, it does not try rfl afterwards, so a goal of the form Eq A x x must still be closed explicitly. If abstracting a produces an ill-typed motive, the kernel's type error is reported before the proof state changes.

induction x requires x to be a hypothesis whose type reduces to an inductive type without indices, and no later hypothesis may mention x (induction: revert dependent hypotheses first). It creates one goal per constructor, in declaration order. Each goal's context gains the constructor's fields, under their declared names, and one induction hypothesis per recursive field, named ih (with primes appended if ih is taken). The field named n of Nat.succ is renamed to k when n is already in use, which is why the goals of the examples below mention k and ih. The recursor used is I.recv, where v is the universe of the target; if that recursor does not exist, the message is no elimination recursor at target universe. Indexed families are not supported (indexed induction requires motive/index elaboration (not implemented)).

qed fails if goals remain (N goals remain). Otherwise it assembles the proof term from the tactic steps, sends it to the kernel to be checked against the original goal, prints QED. Kernel checked proof: followed by the term, and ends the proof. This final check is the only step that the soundness of the system depends on.

Any other line gives unknown command: ....

Errors from the kernel

Some messages come from the kernel rather than from the tactic layer, and can appear under any command.

The example scripts

Every script of the examples/ directory follows, as a playground. Each one has been checked by the kernel; edit it and press run to see what changes.

identity.leanmini

# The polymorphic identity on propositions: for every P, P -> P.
goal forall (P : Sort 0), P -> P
intro P
intro p
exact p
qed

nat-reflexivity.leanmini

# Every natural number equals itself, proved by induction on Nat.
# Each case closes by rfl because both sides are syntactically the same.
goal forall (n : Nat), Eq Nat n n
intro n
induction n
rfl
rfl
qed

zero-add.leanmini

# Addition by recursion on the second argument:
#   add m zero     = m
#   add m (succ k) = succ (add m k)
def add : Nat -> Nat -> Nat := fun (m : Nat) => fun (n : Nat) => Nat.rec1 (fun (_n : Nat) => Nat) m (fun (k : Nat) => fun (r : Nat) => Nat.succ r) n

# add zero n = n is not definitional, so it needs induction on n.
goal forall (n : Nat), Eq Nat (add Nat.zero n) n
intro n
induction n
# Base case: add zero zero reduces to zero.
rfl
# Step case: unfold add zero (succ k) to succ (add zero k), then use ih.
change Eq Nat (Nat.succ (add Nat.zero k)) (Nat.succ k)
rw ih
rfl
qed

generic-list.leanmini

# A user-declared polymorphic list. Declaring it generates List.rec0, List.rec1, ...
inductive List (A : Sort 1) : Sort 1 where
  | nil
  | cons (head : A) (tail : List A)

# induction works for any non-indexed inductive, not only Nat.
goal forall (xs : List Nat), Eq (List Nat) xs xs
intro xs
induction xs
rfl
rfl
qed

generic-vec.leanmini

# Length-indexed vectors. The index n varies between constructors,
# so it is declared with the `index` keyword in the header.
inductive Vec (A : Sort 1) (index n : Nat) : Sort 1 where
  | nil : Vec A Nat.zero
  | cons (n : Nat) (head : A) (tail : Vec A n) : Vec A (Nat.succ n)

# Constructors take the parameter A explicitly.
def one : Vec Nat (Nat.succ Nat.zero) := Vec.cons Nat Nat.zero Nat.zero (Vec.nil Nat)

# The tactic `induction` does not support indexed families yet,
# but the kernel still checks terms that use Vec directly.
goal Eq (Vec Nat (Nat.succ Nat.zero)) one (Vec.cons Nat Nat.zero Nat.zero (Vec.nil Nat))
rfl
qed

What is missing compared with Lean 4

leanmini is a vehicle for understanding the kernel, not a proof assistant. The table lists what Lean's front end does for you and this language does not.

The last row has a practical consequence: a qed prints the proof term and discards it. To reuse a result, state it as a def with the term written out, or as an axiom.