Proof-Producing Tactics and the Kernel Boundary

Definition 114.1 — Goals and proof states¶

A goal is a pair $g=(\mathrm{\Gamma }\mid G)$, where $\mathrm{\Gamma }\mathsf{ctx}$ and $\mathrm{\Gamma }⊢G\mathsf{type}$. A validation from goals $g_i=({\mathrm{\Gamma }}_i\mid G_i)$, for $1\le i\le n$, to $g=(\mathrm{\Gamma }\mid G)$ is a partial meta-level function $V$ whose domain contains every tuple of kernel proofs of the displayed goals and such that $$({\mathrm{\Gamma }}_i⊢p_i:G_i\text{ for every }i)⟹\mathrm{\Gamma }⊢V(p_1,\dots ,p_n):G.$$ Write each context as a telescope ${\mathrm{\Gamma }}_i=(x_{i1}:A_{i1},\dots ,x_{i{k}_i}:A_{i{k}_i})$. A contextual metavariable for $g_i$ is a fresh declaration $$?m_i:(x_{i1}:A_{i1})\cdots (x_{i{k}_i}:A_{i{k}_i})⊢G_i.$$ Its identity occurrence in ${\mathrm{\Gamma }}_i$ is $?m_i{x}_{i1}\cdots x_{i{k}_i}$. A proof state for $g$ is $$S=(?m_1:g_1,\dots ,?m_n:g_n;V),$$ where the $?m_i$ are pairwise distinct, there is exactly one declaration for each open goal, and $V$ is a validation from those goals to $g$. The state represents the suspended meta-expression $$\lceil S\rceil :=V(?m_1{x}_{11}\cdots x_{1k_1},\dots ,?m_n{x}_{n1}\cdots x_{n{k}_n}).$$ Each argument in this display is formed in its own goal context before the validation abstracts or otherwise assembles it in $\mathrm{\Gamma }$. No metavariable other than the displayed $?m_i$ may occur in $\lceil S\rceil$. The empty state $(;V)$ is successful: its suspended expression is the ordinary kernel term $V()$.

Definition 114.2 — Primitive proof-producing tactics¶

A tactic maps a goal either to failure or to a proof state for that goal. The following primitive tactics are defined when their displayed side conditions hold.

1. $\mathsf{exact}(q)$ on $(\mathrm{\Gamma }\mid G)$ returns the empty state with validation $()\mapsto q$, provided the kernel derives $\mathrm{\Gamma }⊢q:G$.

2. $\mathsf{intro}$ on $(\mathrm{\Gamma }\mid \prod _{x:A}B)$ returns $$(?m:(\mathrm{\Gamma },x:A\mid B);p\mapsto \lambda x.p),$$ where $?m$ is fresh.

3. $\mathsf{split}$ on $(\mathrm{\Gamma }\mid A\times B)$ returns the goals explicitly represented by $$(?m:(\mathrm{\Gamma }\mid A),?n:(\mathrm{\Gamma }\mid B);(p,q)\mapsto (p,q)),$$ where $?m$ and $?n$ are fresh and distinct.

4. $\mathsf{assumption}$ returns $\mathsf{exact}(x)$ for the first declaration $x:G$ in $\mathrm{\Gamma }$, and fails if there is none.

The ordering in the last clause is part of the replayable tactic semantics.

Definition 114.4 — Tactic evaluation¶

Write $T\mathsf{@}g\Downarrow S$ when tactic $T$ succeeds on goal $g$ with proof state $S$, and write $\mathsf{fails}(T,g)$ for failure. The four primitives have exactly the successful results in definition 114.2. Their failure rules are

The first premise means that the kernel rejects the exact judgment; it is not a second typing relation. The two shape failures are syntactic because the primitive success clauses in definition 114.2 match those two outer forms; a front end may normalize a goal before invoking a primitive. For a vector of goals ${\overrightarrow{h}}_i$, write ${\overline{?n}}_i:{\overrightarrow{h}}_i$ for a vector containing one fresh contextual metavariable declaration for each component of ${\overrightarrow{h}}_i$. Metavariable vectors generated by separate premises are chosen disjointly. Given $V$ and $W_1,\dots ,W_n$, define their composite validation by $$V_{\overrightarrow{W}}({\overrightarrow{q}}_1,\dots ,{\overrightarrow{q}}_n):=V(W_1({\overrightarrow{q}}_1),\dots ,W_n({\overrightarrow{q}}_n)).$$ The rules for sequence and left-biased choice are

The sequence rule removes the intermediate declarations $?m_i:g_i$: each $W_i$ directly supplies the corresponding argument of $V$. Its result contains exactly the final declarations ${\overline{?n}}_i:{\overrightarrow{h}}_i$, and splits their proof arguments according to the displayed concatenation. If $T$ succeeds on no goals, Tac-Seq has no $U$-premises and returns the same nullary validation.

For repetition, write a state relative to its original goal as $$S=(?m_1:g_1,\dots ,?m_n:g_n;V).$$ Put ordered lexicographically, where $c(g_1)$ counts $\to$ and $\times$ in the conclusion of $g_1$. Thus the empty state is below every nonempty state, including a single atomic goal. Suppose $T\mathsf{@}{g}_1\Downarrow (\overline{?n}:\overrightarrow{h};W)$, where every declaration in $\overline{?n}:\overrightarrow{h}$ is fresh for the declarations retained from $S$. Define A one-step transition on the first goal is then

Define ${\mathsf{stops}}_T(S)$ to hold exactly when $S$ is empty, or its first goal $g_1$ satisfies $\mathsf{fails}(T,g_1)$, or every successful evaluation of $T$ on $g_1$ produces a state whose measure is not below $\mu (S)$. The terminating closure is generated by

Thus Rep-Done is available exactly at a stopping state. For a fresh contextual metavariable $?m:g$, the identity state has suspended expression $?m$ applied to the variables of the context of $g$. Finally, $$\mathsf{repeat}(T)\mathsf{@}g\Downarrow S^{\prime }⟺{\mathsf{Rep}}_T((?m:g;p\mapsto p),S^{\prime }).$$ Thus choice and repetition fix both the returned proof term and its replay trace; the decrease side condition excludes $\mathsf{repeat}(\mathsf{id})$.

Definition 114.6 — Closing a proof state¶

Let $S=(?m_1:g_1,\dots ,?m_n:g_n;V)$, where $g_i=({\mathrm{\Gamma }}_i\mid G_i)$. A meta-substitution $\rho$ closes $S$ when both conditions hold:

1. its domain is exactly $\{?m_1,\dots ,?m_n\}$;

2. for every $i$, its assignment $\rho (?m_i)=q_i$ is a metavariable-free kernel term satisfying ${\mathrm{\Gamma }}_i⊢q_i:G_i$;

Contextual substitution acts on an occurrence by $$(?m_i{u}_1\cdots u_{k_i})[\rho ]:=q_i[u_1/x_{i1},\dots ,u_{k_i}/x_{i{k}_i}],$$ and acts pointwise on a validation application: $$V(t_1,\dots ,t_n)[\rho ]:=V(t_1[\rho ],\dots ,t_n[\rho ]).$$ Thus the empty substitution closes only an empty state; a state with an open goal cannot satisfy closure without a checked proof of that goal.

Definition 114.8 — Case-split certificate¶

For $s:I\overrightarrow{a}\overrightarrow{i}$ and goal $G$, a case-split certificate contains a well-typed motive $$P:(\overrightarrow{j}:\overrightarrow{J})\to I\overrightarrow{a}\overrightarrow{j}\to {\mathcal{U}}_k,P\overrightarrow{i}s\equiv G,$$ where $k$ is the level at which the kernel derives $\mathrm{\Gamma }⊢G:{\mathcal{U}}_k$, and $\overrightarrow{J}$ is the index telescope of $I$ at the parameters $\overrightarrow{a}$; one fresh contextual-metavariable declaration for every constructor goal accepted by the family eliminator; and a validation whose eliminator application consumes exactly those branch-proof arguments. Impossible branches have no declaration and no validation argument, and are omitted only when the kernel derives the corresponding index contradiction.

Definition 114.9 — Replay certificate¶

A replay certificate records the original goal, the ordered primitive calls, every generated contextual-metavariable declaration, every choice branch, every case-split motive, and the final closed proof term. Replay executes the recorded primitive calls without search and then invokes the kernel on the final term.