Graded Erasure and Extraction

Proof. Matrix multiplication satisfies Here the middle identity says that the $i$-th unit row selects row $i$ of $\mathrm{\Psi }$. If ${\mathrm{\Psi }}^{+}$ is the matrix of the lifted substitution, then $$\begin{array}{}\text{(}101.1\text{)}& (\gamma ,p){\mathrm{\Psi }}^{+}=(\gamma \mathrm{\Psi },p),(\gamma ,p,r){\mathrm{\Psi }}^{++}=(\gamma \mathrm{\Psi },p,r).\end{array}$$ Induct on the displayed usage derivation.

Leaves and subsumption. For U-Universe, U-N, U-Empty, and U-Zero, use $0\mathrm{\Psi }=0$. The U-Var goal is exactly the row premise $e_i\mathrm{\Psi }▸\sigma (i)$. In U-Sub, monotonicity of matrix multiplication sends $\delta \le \gamma$ to $\delta \mathrm{\Psi }\le \gamma \mathrm{\Psi }$, after which U-Sub applies to the induction hypothesis.

Formation and binders. For U-$\mathrm{\Pi }$, the induction hypotheses, with the lifted substitution in the codomain, give $\gamma \mathrm{\Psi }▸A[\sigma ]$ and $\delta \mathrm{\Psi },q▸B[{\sigma }^{+}]$. Rule U-$\mathrm{\Pi }$ gives $$p(\gamma \mathrm{\Psi })+\delta \mathrm{\Psi }=(p\gamma +\delta )\mathrm{\Psi }▸{\mathrm{\Pi }}_p^{q}A[\sigma ]B[{\sigma }^{+}].$$ For U-$\mathrm{\Sigma }$, replace the left side by $\gamma \mathrm{\Psi }+\delta \mathrm{\Psi }=(\gamma +\delta )\mathrm{\Psi }$. For U-Lam, equation 101.1 turns the body induction hypothesis into $\gamma \mathrm{\Psi },p▸t[{\sigma }^{+}]$, and U-Lam removes the last component.

Binary constructors. The application hypotheses rebuild U-App at $$\gamma \mathrm{\Psi }+p(\delta \mathrm{\Psi })=(\gamma +p\delta )\mathrm{\Psi }.$$ The weak-pair calculation is $\gamma \mathrm{\Psi }+\delta \mathrm{\Psi }=(\gamma +\delta )\mathrm{\Psi }$. For a strong pair, U-StrongPair first gives $\gamma \mathrm{\Psi }\wedge \delta \mathrm{\Psi }$. Monotonicity gives $$(\gamma \wedge \delta )\mathrm{\Psi }\le \gamma \mathrm{\Psi },(\gamma \wedge \delta )\mathrm{\Psi }\le \delta \mathrm{\Psi },$$ so the defining property of meet and U-Sub give the required context $(\gamma \wedge \delta )\mathrm{\Psi }$. The U-Fst, U-Snd, and U-Suc cases apply their displayed unary rule to the induction hypothesis.

Eliminators. For U-Prodrec, the three induction hypotheses and equation 101.1 have contexts $\gamma \mathrm{\Psi }$, $\delta \mathrm{\Psi },r,r$, and $\eta \mathrm{\Psi },q$. Rebuilding the rule gives $$r(\gamma \mathrm{\Psi })+\delta \mathrm{\Psi }=(r\gamma +\delta )\mathrm{\Psi }.$$ The predicate $\mathsf{Prodrec}(r)$ is unchanged by substitution. For U-Emptyrec, the term and motive hypotheses rebuild the rule at $p(\gamma \mathrm{\Psi })=(p\gamma )\mathrm{\Psi }$; the predicate $\mathsf{Emptyrec}(p)$ is unchanged.

For U-Natrec, fix a target component $j$. Expanding matrix multiplication gives a finite sum over source rows. Apply NR-Right, equation 101.4, to move each matrix entry into the three branch demands, apply NR-Interchange, equation 101.5, to combine the rows, and apply NR-Mono, equation 101.3, to the induction-hypothesis bounds. Componentwise this proves $${\mathsf{nr}}_{p,r}({\gamma }_z,{\gamma }_s,{\gamma }_n)\mathrm{\Psi }\le {\mathsf{nr}}_{p,r}({\gamma }_z\mathrm{\Psi },{\gamma }_s\mathrm{\Psi },{\gamma }_n\mathrm{\Psi }).$$ Rule U-Natrec resources the substituted term at the right side, and U-Sub changes it to the left side. This exhausts the usage card and proves substitution.

For preservation, induct on the rules of definition 101.5; if the last usage rule is U-Sub, first apply the induction argument above it and then reapply its inequality.

Application and strong sums. For R-App, the reduction induction hypothesis replaces the function premise of U-App; the argument premise and the context $\gamma +p\delta$ do not change. Rule R-$\beta$ is the single-substitution instance $$\gamma ,p▸t,\delta ▸u⟹\gamma +p\delta ▸t[u].$$ For R-Fst and R-Snd, apply the reduction induction hypothesis to the scrutinee and rebuild U-Fst or U-Snd. In the two projection beta cases, inversion of U-StrongPair gives $\gamma ▸t$ and $\delta ▸u$, while the redex has context $\gamma \wedge \delta$. The inequalities $\gamma \wedge \delta \le \gamma$ and $\gamma \wedge \delta \le \delta$, followed by U-Sub, resource the selected component.

Weak sums. Rule R-Prodrec applies the reduction induction hypothesis to its scrutinee and rebuilds U-Prodrec. For R-Prodrec-$\beta$, invert the weak-pair premise to obtain ${\gamma }_1▸t_1$ and ${\gamma }_2▸t_2$, and invert the branch premise to obtain $\delta ,r,r▸u$. Two applications of usage substitution give $$\delta +r{\gamma }_1+r{\gamma }_2▸u[t_1,t_2].$$ Distributivity and commutativity identify this context with $r({\gamma }_1+{\gamma }_2)+\delta$, the demand of the redex.

Naturals and emptiness. For R-Natrec, the reduction induction hypothesis changes ${\gamma }_n▸n$ to ${\gamma }_n▸n^{\prime }$; rebuilding U-Natrec leaves its computed demand unchanged. In R-Nat-Zero, inversion of the zero usage gives ${\gamma }_n\le 0$. Hence NR-Base gives $${\mathsf{nr}}_{p,r}({\gamma }_z,{\gamma }_s,{\gamma }_n)\le {\gamma }_z,$$ and U-Sub changes the base-premise derivation ${\gamma }_z▸z$ to the redex context. In R-Nat-Suc, inversion gives ${\gamma }_n▸n$. Substituting the scrutinee and the recursive call into ${\gamma }_s,p,r▸s$ resources the reduct at $${\gamma }_s+p{\gamma }_n+r{\mathsf{nr}}_{p,r}({\gamma }_z,{\gamma }_s,{\gamma }_n).$$ Rule NR-Step, equation 101.2, places the redex demand below this context, and U-Sub finishes the case. Finally, R-Emptyrec applies the reduction induction hypothesis to the absurd scrutinee and rebuilds U-Emptyrec. For R-Conv, inversion exposes a premise $\mathrm{\Gamma }⊢t⟶u:A$ and an equality $\mathrm{\Gamma }⊢A=B$. The reduction induction hypothesis applied to that premise gives $\gamma ▸u$; usage has no type index, so this is exactly the required conclusion at $B$. These are all rules of definition 101.5, and preservation follows. ◻

Proof. Clause 1 imports the fundamental reducibility results identified in the source’s Section 4.4, printed p. 15. At the displayed signature their type and term consequences are $$\mathrm{\Gamma }⊢A⟹\mathrm{\exists }l.\mathrm{\Gamma }{⊩}_{l}A$$ and, for every derivation $\mathrm{\Gamma }⊢t:A$, reducibility of $t$ at the same candidate. The term component of reducibility supplies a weak-head reduct. Clause 2 is source Theorems 4.1 and 4.2, printed p. 15. The first says that a weak-head normal form admits no nonidentity typed weak-head reduction; the second identifies the endpoints of two typed weak-head reductions from one term.

For clause 3, the source proves soundness of algorithmic conversion by induction on the algorithmic derivation and completeness by mutual induction on declarative type and term equality. Decidability follows by running that conversion procedure on typed inputs; the checking result is restricted to the checkable expressions stated in Section 4.4. All three clauses therefore have exactly the syntax of definition 101.1; no consequence is claimed for identity types, first-class levels, top-level definitions, opacity, or weak units [ADE26]. ◻

Proof. Induct on $\gamma ▸t$. The variable case would imply $0\le 1$, contradicting the well-behaved-zero assumption. Positivity of addition handles applications and weak pairs; positivity of meet handles strong pairs. The abstraction case removes the bound component. For a grade-zero application, the argument is absent from the target, while for a nonzero application the induction hypothesis applies to both subterms. The recursion case uses positivity of the $\mathsf{nr}$ result. These cases cover every extraction clause. ◻

Proof. We use two compatibility claims. First, for every simultaneous substitution $\sigma$, extraction commutes with substitution on retained variables: $$\begin{array}{}\text{(}1\text{)}& (a[\sigma ]{)}^{\bullet }=a^{\bullet }[{\sigma }^{\bullet }].\end{array}$$ For an erased binder, the corresponding component of ${\sigma }^{\bullet }$ is $\circlearrowleft$. Prove (1) by induction on $a$. The variable, binder, application, pair, projection, successor, and recursor clauses follow by the induction hypotheses. In a grade-zero application the argument disappears on both sides. In a grade-zero weak-sum eliminator, lemma 101.10 removes both component variables from the extracted branch, so replacing them by $t_1^{\bullet },t_2^{\bullet }$ or by two copies of $\circlearrowleft$ gives the same target term. Empty elimination extracts to $\circlearrowleft$ on both sides. These are all clauses of definition 101.8.

Second, suppose $\mathrm{\Delta }⊢a⟶b:A$ and the usage derivation for $a$ has total grade zero. Under the two hypotheses of the theorem, $$\begin{array}{}\text{(}2\text{)}& a^{\bullet }{⟶}^{\ast }{b}^{\bullet }.\end{array}$$ Prove (2) by induction on the displayed source-reduction derivation. The R-App, R-Fst, R-Snd, R-Prodrec, and R-Natrec cases apply the induction hypothesis under the matching E-App, E-Fst, E-Snd, E-Prodrec, and E-Natrec context. Rule R-$\beta$ becomes E-$\beta$ when the application grade is nonzero; at grade zero both endpoints are equal by (1). The two strong-pair projection roots become E-Fst-$\beta$ and E-Snd-$\beta$. A weak-pair beta root becomes E-Prodrec-$\beta$ when its scrutinee is retained, and becomes equality by (1) and lemma 101.10 when its grade is zero. The two natural-number roots become E-Nat-Zero and E-Nat-Suc; equation (1) identifies the substituted step branch in the successor case. R-Conv uses the induction hypothesis unchanged because extraction does not inspect the classifier. An empty eliminator at total grade zero would contain a zero-use proof of $\mathrm{\perp }$. If $\mathsf{Emptyrec}(0)$ is available, consistency of $\mathrm{\Delta }$ excludes that derivation; if it is not available, the term is not admitted. Thus no empty-elimination root remains. This exhausts definition 101.5 and proves (2).