Proof production, metaprogramming, levels, and generated actions

Tactic validations and replay

A goal is $g=(\mathrm{\Gamma }\mid G)$. A validation from $g_1,\dots ,g_n$ to $g$ is a partial meta-level function $V$ satisfying $$({\mathrm{\Gamma }}_i⊢p_i:G_i\text{ for every }i)⟹\mathrm{\Gamma }⊢V(p_1,\dots ,p_n):G.$$ The primitive validations are Sequencing composes a first validation $V$ with the subgoal validations $W_i$ as $({\overrightarrow{q}}_1,\dots ,{\overrightarrow{q}}_n)\mapsto V(W_1({\overrightarrow{q}}_1),\dots ,W_n({\overrightarrow{q}}_n))$. A successful replay must end by checking $\mathrm{\Gamma }⊢p:G$ for its completed proof term in the unchanged kernel. The tactic semantics has separate success and failure judgments, $T\mathsf{@}g\Downarrow (\overrightarrow{h},V)$ and $\mathsf{fails}(T,g)$. Choice therefore commits to its left branch only on success:

$T\mathsf{@}g\Downarrow (\overrightarrow{h},V)$

$(T\mathsf{orelse}U)\mathsf{@}g\Downarrow (\overrightarrow{h},V)$

$\mathsf{fails}(T,g)$$U\mathsf{@}g\Downarrow (\overrightarrow{h},V)$

$(T\mathsf{orelse}U)\mathsf{@}g\Downarrow (\overrightarrow{h},V)$

$\mathsf{fails}(T,g)$$\mathsf{fails}(U,g)$

$\mathsf{fails}(T\mathsf{orelse}U,g)$

For a state $S=(g_1,\dots ,g_n;V)$, a repeat step evaluates $T$ on $g_1$, composes its validation into $V$, and is admitted only when the lexicographic measure $(c(g_1),n)$ strictly decreases. The closure has Rep-Done exactly when the state is empty, the first tactic application fails, or no successful application decreases the measure, and Rep-More for one decreasing step followed by the closure. Thus $$\mathsf{repeat}(T)\mathsf{@}g\Downarrow (\overrightarrow{h},V)⟺{\mathsf{Rep}}_T((g;p\mapsto p),(\overrightarrow{h};V)).$$

Certified simplification and reflection

A database entry is a typed equality $q:{\mathsf{Id}}_A(\ell ,r)$ oriented only when its well-founded measure decreases after every admitted instantiation. The contextual rewriting judgment is generated by

${\mathsf{root}}_D(t)=(r\rho ,q\rho )$

$\mathsf{Rw}(\mathrm{\Gamma };=;t;r\rho ;q\rho )$

$\mathrm{\Gamma }⊢t:A$$\mathrm{\Gamma }⊢{\mathsf{reflex}}_R:\prod _{x:A}Rxx$

$\mathsf{Rw}(\mathrm{\Gamma };R;t;t;{\mathsf{reflex}}_{R}t)$

$\mathsf{Rw}(\mathrm{\Gamma };R_A\Rightarrow R_B;f;f^{\prime };v_f)$$\mathsf{Rw}(\mathrm{\Gamma };R_A;a;a^{\prime };v_a)$

$\mathsf{Rw}(\mathrm{\Gamma };R_B;fa;f^{\prime }{a}^{\prime };v_{f}a{a}^{\prime }{v}_a)$

$\mathsf{Rw}(\mathrm{\Gamma },x:A,y:A,p:R_{A}xy;R_B;b;b^{\prime };v)$

$\mathsf{Rw}(\mathrm{\Gamma };R_A\Rightarrow R_B;\lambda x.b;\lambda y.b^{\prime };\lambda x.\lambda y.\lambda p.v)$

Here $R_A\Rightarrow R_B$ is the binary respectful relation: its witness maps $x,y,p:R_{A}xy$ to a proof of $R_B(fx)(f^{\prime }y)$. It is not the pointwise unary relation. The substitution rule composes an $R$-certificate with a checked implication into a relation $S$. Reflection reifies a commutative-monoid expression, computes its finite multiplicity map, and accepts the result only after the kernel checks the produced equality proof.

Hygienic and phase-indexed expansion

A raw binder is $a^{\beta }$, and a raw reference $a_{\beta }^{\omega }$ carries both its stable occurrence token $\omega$ and its lexical target token $\beta$. An expanded reference has the form $a^S[o;\mathsf{src}(\omega )]$ or $a^S[o;\mathsf{new}(o_t)]$: $S$ is its finite scope set, $o$ is its resolved origin, and the final marker records copied provenance or a declared constructed target. Transformer output marks every node as substituted or constructed; substituted syntax retains caller scopes, whereas constructed syntax receives a fresh introduction scope. Each free constructed reference declares a target origin, and expansion rejects an unresolved, ambiguous, or provenance-mismatched reference. The source judgment $E_0;\mathrm{\Gamma }{⊢}_n^{\mathsf{src}}r:A$ includes

$E_0(\beta )=o_s$$\mathrm{\Gamma }(o_s)=A@n$

$E_0;\mathrm{\Gamma }{⊢}_n^{\mathsf{src}}{a}_{\beta }^{\omega }:A$

$\beta \notin \mathrm{dom}{E}_0$$o_s\mathsf{fresh}$$E_0,\beta \mapsto o_s;\mathrm{\Gamma },o_s:A@n{⊢}_n^{\mathsf{src}}r:B$

$E_0;\mathrm{\Gamma }{⊢}_n^{\mathsf{src}}\lambda (a^{\beta }:A).r:A\to B$

$E_0;\mathrm{\Gamma }{⊢}_n^{\mathsf{src}}{r}_1:A\to B$$E_0;\mathrm{\Gamma }{⊢}_n^{\mathsf{src}}{r}_2:A$

$E_0;\mathrm{\Gamma }{⊢}_n^{\mathsf{src}}{r}_1{r}_2:B$

Src-Macro checks only a declared source arity and type together with the argument typings. It does not trust a transformer contract. After expansion, the staged target checker and provenance judgment independently check the output, as required by definition 116.11. The core phase rules are

$\mathrm{\Gamma }{⊢}_{n+1}e:A$

$\mathrm{\Gamma }{⊢}_n\mathsf{quote}(e):\mathsf{Code}(A)$

$\mathrm{\Gamma }{⊢}_{n}e:\mathsf{Code}(A)$

$\mathrm{\Gamma }{⊢}_{n+1}\mathsf{splice}(e):A$

$(x:A@n)\in \mathrm{\Gamma }$

$\mathrm{\Gamma }{⊢}_{n}x:A$

Generated commands expose a scoped declaration and a closed ordinary term; only that term crosses the kernel boundary.

First-class level rules

The principal noncumulative calculus adds

$\mathrm{\Gamma }\mathsf{ctx}$

$\mathrm{\Gamma }⊢\mathsf{Level}:{\mathcal{U}}_0$

$\mathrm{\Gamma }\mathsf{ctx}$

$\mathrm{\Gamma }⊢0:\mathsf{Level}$

$\mathrm{\Gamma }⊢t:\mathsf{Level}$

$\mathrm{\Gamma }⊢t^{+}:\mathsf{Level}$

$\mathrm{\Gamma }⊢t:\mathsf{Level}$$\mathrm{\Gamma }⊢u:\mathsf{Level}$

$\mathrm{\Gamma }⊢t\bigsqcup u:\mathsf{Level}$

$\mathrm{\Gamma }⊢t:\mathsf{Level}$

$\mathrm{\Gamma }⊢{\mathcal{U}}_t:{\mathcal{U}}_{t^{+}}$

Join is associative, commutative, idempotent, and has zero as left identity; successor preserves join and satisfies $t\bigsqcup t^{+}\equiv t^{+}$. Explicit lifts have

$\mathrm{\Gamma }⊢A:{\mathcal{U}}_t$

$\mathrm{\Gamma }⊢{\mathsf{Lift}}_{u}A:{\mathcal{U}}_{t\bigsqcup u}$

$\mathrm{\Gamma }⊢a:A$

$\mathrm{\Gamma }⊢\mathsf{lift}a:{\mathsf{Lift}}_{u}A$

$\mathrm{\Gamma }⊢b:{\mathsf{Lift}}_{u}A$

$\mathrm{\Gamma }⊢\mathsf{lower}b:A$

The beta rule contracts lower after lift; the extensional eta rule identifies two lifted terms when their lowerings are equal.

Sort abstraction and elimination

SortPoly judgments have shape $\mathrm{\Sigma }\mid \mathrm{\Theta }\mid \mathrm{\Gamma }⊢t:A$, with prenex sort and level variables in $\mathrm{\Theta }$. Sort variables have no constraints in the principal system. Every case rule retains the premise $$\mathrm{\Sigma }\mid \mathrm{\Theta }⊢\mathsf{elim}(I,s_P)\mathsf{allowed}.$$ Same-sort elimination is the universal clause

$\mathrm{\Theta }⊢s\mathsf{sort}$$(I\mathsf{declared}\mathsf{at}\mathsf{codomain}\mathsf{sort}s)\in \mathrm{\Sigma }$

$\mathrm{\Sigma }\mid \mathrm{\Theta }⊢\mathsf{elim}(I,s)\mathsf{allowed}$

Ground policies may add only their stated clauses, such as singleton elimination from $\mathsf{Prop}$. Monomorphization duplicates each global declaration at all well-formed ground instantiations and deletes only the sort binders; it retains level binders and constraints. The independent subStraTT boundary instead enforces dependency strata:

$\mathrm{\Delta }⊢\mathrm{\Gamma }$

$\mathrm{\Delta };\mathrm{\Gamma }⊢\ast {:}^k\ast$

$\mathrm{\Delta };\mathrm{\Gamma }⊢A{:}^j\ast$$\mathrm{\Delta };\mathrm{\Gamma },x{:}^{j}A⊢B{:}^k\ast$

$\mathrm{\Delta };\mathrm{\Gamma }⊢\prod _{x{:}^{j}A:B}{:}^k\ast$

$\mathrm{\Delta };\mathrm{\Gamma }⊢b{:}^k\prod _{x{:}^{j}A}B$$\mathrm{\Delta };\mathrm{\Gamma }⊢a{:}^{j}A$

$\mathrm{\Delta };\mathrm{\Gamma }⊢ba{:}^{k}B[a/x]$

The bounded SortPoly comparison puts edges ${\mathsf{edge}}_{\mathrm{\Theta }}(s,t)$ in the sort context. Validity requires: every ground path is already generated by ground edges; a reflexive initial ground sort lies below each ground sort incident with a nonground edge; and every dominated sort variable has a reflexive dominant ground sort above every other ground predecessor. Only a valid context admits the dominant ground substitution and the proved preservation, principality, monomorphization, and conditional equiconsistency package.

Coercion paths and insertion

The generated paths contain identities, declared edges, and composition: $${\mathsf{prog}}_{{\mathsf{id}}_A}=\lambda x.x,{\mathsf{prog}}_{q\circ p}=\lambda x.{\mathsf{prog}}_q({\mathsf{prog}}_{p}x).$$ Path coherence requires equal cast programs for every pair of parallel paths. Insertion occurs only at the synthesis-to-checking boundary:

$(x:A)\in \mathrm{\Gamma }$

$\mathrm{\Gamma }⊢x\Rightarrow A⇝x$

$\mathrm{\Gamma }⊢e_1\Rightarrow \prod _{x:A}B⇝t_1$$\mathrm{\Gamma }⊢e_2\Leftarrow A⇝t_2$

$\mathrm{\Gamma }⊢e_1{e}_2\Rightarrow B[t_2/x]⇝t_1{t}_2$

$\mathrm{\Gamma },x:A⊢e\Leftarrow B⇝t$

$\mathrm{\Gamma }⊢\lambda x.e\Leftarrow \prod _{x:A}B⇝\lambda x.t$

$\mathrm{\Gamma }⊢e\Rightarrow A⇝t$$p\in \mathsf{Coe}(A,B)$

$\mathrm{\Gamma }⊢e\Leftarrow B⇝{\mathsf{prog}}_{p}t$

Annotations and pairs retain the syntax-directed rules printed in definition 119.6; no other rule consumes a path. The determinacy proof additionally assumes that target definitional equality is stable under substitution and that dependent products are injective: equality of $\mathrm{\Pi }x:A_1.B_1$ and $\mathrm{\Pi }x:A_2.B_2$ yields equality of the domains and, after context conversion, equality of the codomains. Path coherence alone cannot discharge the Coe-App case.

Generated positive action

Positive descriptions are generated by $\mathbf{1},\mathbf{K}(A),\mathbf{X},\times ,\mathbf{+}$, and dependent sum. Their action is structural: constants are fixed, the parameter clause applies $f$, products act componentwise, sums preserve the injection, and dependent sums preserve their first component. Indexed descriptions replace $\mathbf{X}$ by $\mathbf{X}(j)$ and apply the corresponding family map $f_j$. The judgmental functor equations are $${\mathsf{map}}_F(\mathsf{id})(x)\equiv x,{\mathsf{map}}_F(f)({\mathsf{map}}_F(g)(x))\equiv {\mathsf{map}}_F(f{{\circ }_F}_{F}g)(x).$$ On a neutral $n$, weak-head reduction compacts the second equation to one outer map; the identity equation remains conversion and is not oriented as an expanding reduction. Constructor-headed inputs use only the structural computation equations. Neutral identity and composition are the deliberate definitional-equality delta Desc-Map-Id/Desc-Map-Comp; the latter may be oriented as weak-head reduction only on a neutral argument. Generated action commutes with every well-typed simultaneous substitution, and this substitution lemma proves that constructor computation, the two equality rules, and neutral compaction remain well typed after substitution. Dependent sums act by $(g,f)(x,y)=(g(x),f(x)(y))$; their identity and composition laws reduce by projection and pair computation rather than by the neutral delta.