Worked Examples

To verify a proof $t$ of a theorem $T$, the kernel calls $\Check(\cdot, t, T)$, which calls $\Infer(\cdot, t)$ and compares the result with $T$. The traces show the recursive calls that $\Infer$ makes, with the typing rule each call corresponds to. Expand or collapse the nodes to follow the recursion.

The identity proof

Let $\Gamma_1 = P : \Sort{0}$ and $\Gamma_2 = \Gamma_1, h : P$. The derivation of the opening example of Chapter 1, with the well-formedness premises omitted, is

The algorithm builds the same derivation from the bottom up. The call $\Infer(\cdot, \tLam{P}{\Sort{0}}{\tLam{h}{P}{h}})$ proceeds as follows.

• $\Infer(\cdot,\; \tLam{P}{\Sort{0}}{\tLam{h}{P}{h}})$ T-Lam
  • $\InferSort(\cdot,\; \Sort{0})$: $\Infer$ returns $\Sort{1}$, so the annotation is a type T-Sort
  • $\Freshen$ leaves $P$ unchanged, since the context is empty
  • $\Infer(\Gamma_1,\; \tLam{h}{P}{h})$ T-Lam
    • $\InferSort(\Gamma_1,\; P)$: $\Infer$ looks up $P$ and returns $\Sort{0}$ T-Var
    • $\Freshen$ leaves $h$ unchanged
    • $\Infer(\Gamma_2,\; h)$ looks up $h$ and returns $P$ T-Var
    • returns $\tPi{h}{P}{P}$
  • returns $\tPi{P}{\Sort{0}}{\tPi{h}{P}{P}}$

Each call that returns a type corresponds to one node of the derivation tree, and no call uses computation. Finally, $\Check$ compares the result with the stated type $\tPi{P}{\Sort{0}}{P \to P}$. The two differ only in the name of one bound variable, because $P \to P$ abbreviates $\tPi{\_}{P}{P}$ and neither $h$ nor $\_$ occurs in the body. So $\IsDefEq$ succeeds and the proof is accepted.

The same run, recorded by the kernel itself. The call view matches the list above; the proof-tree view matches the derivation.

# The same proof, given as a complete term. The kernel infers its type
# and compares it with the goal.
goal forall (P : Sort 0), P -> P
exact fun (P : Sort 0) => fun (h : P) => h
qed

A wrong proof

Suppose a user claims that $t = \tLam{P}{\Sort{0}}{\tLam{h}{P}{P}}$ proves $\tPi{P}{\Sort{0}}{P \to P}$. The body returns the proposition $P$ instead of the proof $h$. The kernel calls $\Check(\cdot, t, \tPi{P}{\Sort{0}}{P \to P})$, which first calls $\Infer$. The calls are the same as above, except that the last one, $\Infer(\Gamma_2, P)$, returns $\Sort{0}$. So $\Infer$ succeeds, with

The term $t$ is well typed, but it does not prove the claimed proposition. When $\Check$ compares the two types, neither reduces further, and renaming bound variables cannot make them equal: the innermost body is $\Sort{0}$ on one side and $P$ on the other. Thus $\IsDefEq$ fails, and $\Check$ reports a type mismatch. (Chapter 11 replays this comparison step by step with the algorithm that $\IsDefEq$ uses.)

The error is found only because the user stated the proposition to be proved. A kernel that only ran $\Infer$ would accept $t$ and silently assign it a different type. This is why goal comes first in every script, and why qed checks against it.

goal forall (P : Sort 0), P -> P
exact fun (P : Sort 0) => fun (h : P) => P
qed

Using a hypothesis: modus ponens

The examples so far never apply a function. Consider checking

which says "if $P$ implies $Q$ and $P$ holds, then $Q$ holds". The four $\lambda$s extend the context to $\Gamma = P : \Sort{0},\; Q : \Sort{0},\; f : P \to Q,\; p : P$ as before. The body $f\;p$ reaches the application case of $\Infer$:

• $\Infer(\Gamma,\; f\;p)$ T-App
  • $\Infer(\Gamma,\; f)$ returns $P \to Q$, that is, $\tPi{\_}{P}{Q}$. $\Whnf$ leaves it unchanged, and it is a $\Pi$ T-Var
  • $\Check(\Gamma,\; p,\; P)$ succeeds, since $p : P$ is in $\Gamma$ T-Var, T-Conv
  • returns $\subst{Q}{\_}{p} = Q$. The name $\_$ does not occur in $Q$, so the substitution does nothing

If the user had written $f\;f$ instead, the second step would call $\Check(\Gamma, f, P)$, which fails because $P \to Q$ is not $P$: a function cannot be fed to itself here. Try it: change f p to f f below.

goal forall (P : Sort 0), forall (Q : Sort 0), (P -> Q) -> P -> Q
exact fun (P : Sort 0) => fun (Q : Sort 0) => fun (f : P -> Q) => fun (p : P) => f p
qed

Instantiating a universal statement

In a dependent application the substitution in T-App does real work. Let $\mathit{id} = \tLam{P}{\Sort{0}}{\tLam{h}{P}{h}}$ be the proof from the first example, and let $\Gamma = Q : \Sort{0}$. Then $\Infer(\Gamma, \mathit{id}\;Q)$:

• $\Infer(\Gamma,\; \mathit{id}\;Q)$ T-App
  • $\Infer(\Gamma,\; \mathit{id})$ returns $\tPi{P}{\Sort{0}}{\tPi{h}{P}{P}}$, already a $\Pi$ T-Lam
  • $\Check(\Gamma,\; Q,\; \Sort{0})$ succeeds T-Var
  • returns $\subst{(\tPi{h}{P}{P})}{P}{Q} = \tPi{h}{Q}{Q}$, that is, $Q \to Q$

Logically, this is $\forall$-elimination: from "every proposition implies itself" we obtain "$Q$ implies $Q$". The type of the result depends on the value of the argument $Q$, which is what the dependent $\Pi$-type expresses and why T-App substitutes. In the explorer, $\mathit{id}$ is a defined constant and $Q$ comes from the context; the note on the T-App node records the substitution.

def id : forall (P : Sort 0), P -> P := fun (P : Sort 0) => fun (h : P) => h

Conversion

Recall $\mathit{Id} = \tLam{X}{\Sort{0}}{X}$ from Chapter 3. The core system has no definitions, so $\mathit{Id}\;P$ is shorthand for the term $(\tLam{X}{\Sort{0}}{X})\;P$. Consider checking

$\Infer$ first checks that the annotation $\mathit{Id}\;P$ is a type. $\InferSort(\Gamma_1, \mathit{Id}\;P)$ reaches the application case of $\Infer$: the function $\tLam{X}{\Sort{0}}{X}$ has type $\tPi{X}{\Sort{0}}{\Sort{0}}$, the argument $P$ passes $\Check(\Gamma_1, P, \Sort{0})$, and the result is $\subst{\Sort{0}}{X}{P} = \Sort{0}$. So $\mathit{Id}\;P$ is a type, and a proposition. The body $h$ then has type $\mathit{Id}\;P$, so

Renaming bound variables alone does not turn this into $\tPi{P}{\Sort{0}}{P \to P}$. But $\IsDefEq$ computes both sides before comparing them, and $\mathit{Id}\;P \betared P$, so the inferred type becomes $\tPi{P}{\Sort{0}}{\tPi{h}{P}{P}}$ and the comparison succeeds as in the first example. In the typing rules, this step is a single use of T-Conv at the root of the derivation:

The algorithm never decides where to apply T-Conv. As described in Chapter 5, conversion is hidden in the call to $\IsDefEq$, which runs only where two types are compared.

The live derivation shows where the computation happens: the annotation $\mathit{Id}\;P$ is checked by T-App, and the inferred type still contains $\mathit{Id}\;P$ until $\Check$ compares it with the goal.

# The annotation of h is (fun (X : Sort 0) => X) P, which computes to P.
goal forall (P : Sort 0), P -> P
exact fun (P : Sort 0) => fun (h : (fun (X : Sort 0) => X) P) => h
qed

Exercises

Running $\Infer$ on these by hand, as in the examples above, is a good check of one's understanding of the algorithm. Each can also be tried in a playground.

goal forall (P : Sort 0), forall (Q : Sort 0), forall (R : Sort 0), (P -> Q) -> (Q -> R) -> P -> R
exact fun (P : Sort 0) => fun (Q : Sort 0) => fun (R : Sort 0) => fun (f : P -> Q) => fun (g : Q -> R) => fun (p : P) => g (f p)
qed