Chapter 78Core route

Indexed Inductive Families and Dependent Pattern Matching

A list records its elements but not its length. Attaching a natural number to a list repairs the statement of lookup only externally: the type checker still cannot infer from the constructor that the number is zero or a successor. The result index of a constructor must therefore be part of the declaration.

The index is fixed by the constructor

The unindexed schema of definition 28.34 permits a constructor whose recursive arguments have the type being declared. It does not permit the attempted declaration $vnil : Vec (A, 0), vcons : \prod_{n : N} A ⟶ Vec (A, n) ⟶ Vec (A, suc (n)),$ because there is no single unindexed result type to put in the constructor signature. Replacing every occurrence by $\sum_{n : N} Vec (A, n)$ loses the constraint: the tail of a purported successor vector may then carry an unrelated index. Write ${vcons}^{'}$ for the constructor produced by this attempted replacement. If $x s : Vec (A, 5)$ , then the raw package $(suc (0), {vcons}^{'} (a, (5, x s)))$ claims outer index $1$ while its displayed tail has index $5$ . No equation in the unindexed signature relates the two components. The index must occur in the result type of the constructor, not merely in a package around its recursive argument.

An indexed inductive family is generated simultaneously at every index, and each constructor specifies the index of its result. Extend the signature of definition 28.34 by the following vector family.

Definition 78.1 — Vectors ¶

For $A : U_{i}$ , the family $Vec (A, -) : N \to U_{i}$ is formed by

Γ ⊢ A : U_{i}

Γ ⊢ n : N

Γ ⊢ Vec (A, n) : U_{i}

Vec-form

Its constructors have types $vnil : Vec (A, 0), vcons : \prod_{n : N} A ⟶ Vec (A, n) ⟶ Vec (A, suc (n)) .$ For example, the successor constructor has the derivation $\frac{\begin{matrix} Γ ⊢ n : N \\ Γ ⊢ a : A \\ Γ ⊢ x s : Vec (A, n) \end{matrix}}{Γ ⊢ vcons (n, a, x s) : Vec (A, suc (n))} Vec - {intro}_{s} .$ In this derivation Vec-form first forms the result family at $suc (n)$ , and Vec-intro $_{s}$ then assigns the constructor the displayed result type. Its dependent eliminator has the following rule. Put $P_{0} : = P [0 / n, vnil / v]$ and $P_{s} : = P [suc (n) / n, vcons (n, a, x s) / v]$ .

Γ, n : N, v : Vec (A, n) ⊢ P : U_{j}

Γ ⊢ p_{0} : P_{0}

Γ, n : N, a : A, x s : Vec (A, n), q : P [n / n, x s / v] ⊢ p_{s} : P_{s}

Γ ⊢ m : N

Γ ⊢ y s : Vec (A, m)

Γ ⊢ vind (P; p_{0}; p_{s}; m, y s) : P [m / n, y s / v]

Vec-elim

Put $r : = vind (P; p_{0}; p_{s}; n, x s)$ . The two computation rules are $\begin{aligned} vind (P; p_{0}; p_{s}; 0, vnil) & \equiv p_{0}, \\ vind (P; p_{0}; p_{s}; suc (n), vcons (n, a, x s)) & \equiv p_{s} [n / n, a / a, x s / x s, r / q] . \end{aligned}$ We refer to these two constructor equations collectively as Vec-comp. The variables displayed in the motive and successor branch are pairwise distinct and avoid $dom (Γ)$ .

Referenced from 14 locations

The successor branch is the new feature. Its recursive hypothesis concerns $x s : Vec (A, n)$ , while its target concerns a value at index $suc (n)$ . Thus constructor typing performs the index refinement that an unindexed encoding could only postulate.

Construction 78.2 — Head and tail from the eliminator ¶

First use natural-number recursion in the universe to define $h, t : N \to U_{i}$ by $\begin{aligned} h (0) & : = 1, & h (suc (n)) & : = A, \\ t (0) & : = 1, & t (suc (n)) & : = Vec (A, n) . \end{aligned}$ Now put $H (n, v) : = h (n)$ and $T (n, v) : = t (n)$ in the context $n : N, v : Vec (A, n)$ . These are well-formed motives because the recursion defining $h$ and $t$ is completed before weakening them by the dependent variable $v$ ; neither definition eliminates $n$ while retaining a fixed $v$ . The vector eliminator gives $\begin{aligned} {head}^{+} (m, y s) & : = vind (H; ⋆; n . a . x s . q . a; m, y s) : H (m, y s), \\ {tail}^{+} (m, y s) & : = vind (T; ⋆; n . a . x s . q . x s; m, y s) : T (m, y s) . \end{aligned}$ For $y s : Vec (A, suc (n))$ , set $head (y s) : = {head}^{+} (suc (n), y s)$ and $tail (y s) : = {tail}^{+} (suc (n), y s)$ . Their constructor computations are judgmental: $head (vcons (n, a, x s)) \equiv a, tail (vcons (n, a, x s)) \equiv x s .$ No impossible $vnil$ clause was assumed; the eliminator places that clause in the harmless types $1$ and $1$ .

If $m : N$ and $y s : Vec (A, m)$ are variables, then $vind (P; p_{0}; p_{s}; m, y s)$ is neutral: neither constructor computation rule applies. The vector rules contain no uniqueness equation that could reconstruct $y s$ from this stuck eliminator.

Referenced from 6 locations

Finite indices and direct programs

The recursive universe-valued family of construction 29.17 will be written ${Fin}_{LE}$ : it satisfies ${Fin}_{LE} (0) \equiv 0$ and ${Fin}_{LE} (suc (n)) \equiv {Fin}_{LE} (n) + 1$ . An inductive presentation makes the two ways to inhabit a successor size available as constructors. The subscript $LE$ recalls the strict inequality $k < n$ used in the universe-valued definition; $ind$ marks the constructor-generated presentation.

Definition 78.3 — Inductive finite indices ¶

The family ${Fin}_{ind} : N \to U_{0}$ has constructors $fz : \prod_{n : N} {Fin}_{ind} (suc (n)), fs : \prod_{n : N} {Fin}_{ind} (n) \to {Fin}_{ind} (suc (n)) .$ For a motive $Q : \prod_{n : N} {Fin}_{ind} (n) \to U_{j}$ , branches $\begin{aligned} q_{z} & : \prod_{n : N} Q (suc (n), fz (n)), \\ q_{s} & : \prod_{n : N} \prod_{k : {Fin}_{ind} (n)} Q (n, k) \to Q (suc (n), fs (n, k)) \end{aligned}$ determine $find (Q; q_{z}; q_{s}; n, k) : Q (n, k)$ , with judgmental computation on $fz$ and $fs$ . More precisely, elimination is governed by

Γ, n : N, k : {Fin}_{ind} (n) ⊢ Q (n, k) : U_{j}

Γ ⊢ q_{z} : \prod_{n : N} Q (suc (n), fz (n))

Γ ⊢ q_{s} : \prod_{n : N} \prod_{k : {Fin}_{ind} (n)} Q (n, k) \to Q (suc (n), fs (n, k))

Γ ⊢ m : N

Γ ⊢ u : {Fin}_{ind} (m)

Γ ⊢ find (Q; q_{z}; q_{s}; m, u) : Q (m, u)

Fin-elim

Writing $r : = find (Q; q_{z}; q_{s}; n, k)$ , its computation equations are $\begin{aligned} find (Q; q_{z}; q_{s}; suc (n), fz (n)) & \equiv q_{z} (n), \\ find (Q; q_{z}; q_{s}; suc (n), fs (n, k)) & \equiv q_{s} (n, k, r) . \end{aligned}$

Referenced from 2 locations

Indexed Inductive Families and Dependent Pattern Matching

Theorem 78.4 — The two finite families agree ¶

For every $n : N$ there are maps $e_{n} : {Fin}_{ind} (n) \to {Fin}_{LE} (n), d_{n} : {Fin}_{LE} (n) \to {Fin}_{ind} (n)$ and identifications $d_{n} (e_{n} (k)) = k$ and $e_{n} (d_{n} (u)) = u$ for all $k$ and $u$ in their respective domains.

Referenced from 3 locations

Indexed Inductive Families and Dependent Pattern Matching

Proof of Theorem 78.4 — The two finite families agree

Proof. Rule Fin-elim defines $e_{suc (n)} (fz (n)) : = inr (⋆), e_{suc (n)} (fs (n, k)) : = inl (e_{n} (k)) .$ Natural-number induction defines $d_{0}$ by empty elimination and $d_{suc (n)} (inr (⋆)) : = fz (n), d_{suc (n)} (inl (u)) : = fs (n, d_{n} (u)) .$ For $d_{n} e_{n}$ , apply finite-index elimination. The $fz$ branch is reflexivity; the $fs$ branch applies $ap$ to $fs (n, -)$ and the recursive hypothesis. For $e_{n} d_{n}$ , apply natural-number induction. Its zero case is empty elimination. In the successor case apply coproduct elimination. The right branch is reflexivity; the left branch applies $ap$ to $inl$ and the induction hypothesis. These are all constructor cases, so the displayed definitions compute judgmentally before the final applications of $ap$ . ◻

After theorem 78.4, write $Fin (n)$ when a construction is invariant under these two inverse maps. The programs below use ${Fin}_{ind}$ because its eliminator exposes the zero and successor positions.

Construction 78.5 — Lookup, map, and append ¶

Finite-index elimination avoids an impossible vector branch. Take $Q (m, k) : = Vec (A, m) \to A .$ The $fz (n)$ method sends $y s : Vec (A, suc (n))$ to $head (y s)$ . The $fs (n, k)$ method sends a recursive map $q : Vec (A, n) \to A$ and $y s : Vec (A, suc (n))$ to $q (tail (y s))$ . Define $lookup (y s, k) : = find (Q; q_{z}; q_{s}; m, k) (y s),$ where $y s : Vec (A, m)$ and $k : {Fin}_{ind} (m)$ . The two finite-index equations followed by the head and tail equations give $\begin{aligned} lookup (vcons (n, a, x s), fz (n)) & \equiv a, \\ lookup (vcons (n, a, x s), fs (n, k)) & \equiv lookup (x s, k) . \end{aligned}$ Thus lookup has no size-zero clause: there is no $k : {Fin}_{ind} (0)$ to eliminate.

For $B : U_{i}$ and $f : A \to B$ , vector elimination with motive $P (n, x s) : = Vec (B, n)$ defines $\begin{aligned} map (f, vnil) & : = vnil, \\ map (f, vcons (n, a, x s)) & : = vcons (n, f (a), map (f, x s)) . \end{aligned}$ To append $x s : Vec (A, m)$ to $y s : Vec (A, n)$ , use the motive $P (m, x s) : = Vec (A, n + m)$ . The fixed length $n$ is written first because the addition of construction 28.23 recurs on its second argument. The equations are $\begin{aligned} append (vnil, y s) & : = y s, \\ append (vcons (m, a, x s), y s) & : = vcons (n + m, a, append (x s, y s)) . \end{aligned}$ The empty branch has the required type because $n + 0 \equiv n$ by the orientation of construction 28.23. The second term has the required type because $n + suc (m) \equiv suc (n + m)$ for that same orientation.

Referenced from 4 locations

Exercise 78.1 ¶

★★☆ For $f : A \to B$ , $x s : Vec (A, n)$ , and $k : {Fin}_{ind} (n)$ , construct an identification $lookup (map (f, x s), k) = f (lookup (x s, k)) .$ Use vector elimination and display both finite-index cases in the successor branch.

Referenced from 3 locations

No confusion and pattern clauses

A constructor pattern refines its index, but it must not silently assert an identity between constructor forms. The required facts are derived from eliminators.

Proposition 78.6 — No confusion used for vectors and finite indices ¶

The following terms are derivable without K.

For $k : {Fin}_{ind} (n)$ , ${Id}_{{Fin}_{ind} (suc (n))} (fz (n), fs (n, k)) \to 0$ .
If $p : {Id}_{{Fin}_{ind} (suc (n))} (fs (n, k), fs (n, l))$ , then there is an identification $k = l$ in ${Fin}_{ind} (n)$ .
If $p : {Id}_{Vec (A, suc (n))} (vcons (n, a, x s), vcons (n, b, y s))$ , then there are identifications $a = b$ in $A$ and $x s = y s$ in $Vec (A, n)$ .

Referenced from 2 locations

Indexed Inductive Families and Dependent Pattern Matching

Proof of Proposition 78.6 — No confusion used for vectors and finite indices

Proof. For (i), finite-index elimination defines $C : {Fin}_{ind} (suc (n)) \to U_{0} .$ Its constructor equations are $C (fz (n)) \equiv 1$ and $C (fs (n, k)) \equiv 0$ . Transporting $⋆ : C (fz (n))$ along $p$ gives an element of $0$ .

For (ii), define a predecessor into ${Fin}_{ind} (n) + 1$ by sending $fz$ to the right summand and $fs (n, r)$ to $inl (r)$ . Applying this map to $p$ gives $inl (k) = inl (l)$ . Choose a default value $k$ and define $q : {Fin}_{ind} (n) + 1 \to {Fin}_{ind} (n)$ by $q (inl (r)) : = r$ and $q (inr (⋆)) : = k$ . Applying ${ap}_{q}$ to the displayed equality gives $k = l$ . For (iii), apply $ap$ to $head$ and $tail$ from construction 78.2. Their constructor computations identify the endpoints with $a, b$ and $x s, y s$ , respectively. ◻

The disjointness proof depends only on the eliminators and identity induction. Judgmental injectivity of raw constructors would require a normalization or term-model theorem; no such stronger assertion is used here.

A pattern clause is an equation whose left side is built from variables and constructors. The clauses have coverage when every constructor compatible with the scrutinee index has a branch. A clause is accepted only after coverage and the generated index equations have been checked. Write $T_{pat \to tm} (\vec{p})$ for the ordinary term tuple obtained from a pattern tuple $\vec{p}$ by erasing dots and reading every constructor pattern as the corresponding constructor term. For example, $head (vcons (. n, a, x s)) = a$ contains an inaccessible pattern $. n$ : it records the value forced by unifying the scrutinee index $suc (n)$ with the constructor result index, but it does not split on $n$ .

Construction 78.7 — Compiling head and append ¶

The head clause has one reachable constructor. Give Vec-elim the motive $H$ of construction 78.2; its empty branch is $⋆$ , and its successor branch returns $a$ . Restricting the result to successor indices is exactly $head$ .

The two append clauses are covered by $vnil$ and $vcons$ . Give Vec-elim the motive $P (m, x s) : = Vec (A, n + m)$ , the empty branch $y s$ , and the successor branch $m . a . x s . q . vcons (n + m, a, q)$ . This is the eliminator term of construction 78.5; its two judgmental computations are the two pattern equations. Pattern syntax has therefore introduced no new proof principle in these examples.

Referenced from 5 locations

Case trees without K

Coverage for indexed patterns is not merely a list of constructors. Splitting $x : D (\vec{u})$ against a constructor $c_{i} : Δ_{i} \to D ({\vec{v}}_{i})$ produces the equation list $\vec{u} = {\vec{v}}_{i}$ . A unifier must either solve that list, prove the branch impossible by constructor conflict or a finite occurs check, or refuse the split.

The source argument uses equality of whole telescopes, not a heterogeneous equality hidden in the unifier. We first expose that equality and its eliminator.

Definition 78.8 — Homogeneous telescopic equality ¶

For a telescope $Δ$ , define the telescopic-equality type $\vec{s} \equiv_{Δ} \vec{t}$ recursively: $\begin{aligned} () \equiv_{()} () & : = 1, \\ (s; \vec{s}) \equiv_{x : A; Δ (x)} (t; \vec{t}) & : = \sum_{e : {Id}_{A} (s, t)} e_{*} \vec{s} \equiv_{Δ (t)} \vec{t} . \end{aligned}$ Here $e_{*} \vec{s}$ transports the later components of $\vec{s}$ along $e$ . The expression $\vec{s} \equiv_{Δ} \vec{t}$ is a type internal to the theory. It is distinct from the external judgmental-equality assertion $\vec{s} \equiv \vec{t}$ even though the two notations share a glyph. Reflexivity ${\overset{―}{refl}}_{\vec{s}}$ is defined recursively: at the empty telescope it is $⋆$ , and at $(s; \vec{s})$ it is $({refl}_{s}, {\overset{―}{refl}}_{\vec{s}})$ after the reflexivity transport has computed. For a family $C (\vec{s}, \vec{t}, e) : U_{j}$ , iterated identity induction gives $\begin{aligned} {\overset{―}{J}}_{Δ} (C) : & (\prod_{\vec{s} : Δ} C (\vec{s}, \vec{s}, {\overset{―}{refl}}_{\vec{s}})) \\ \to \prod_{\vec{s}, \vec{t} : Δ} \prod_{e : \vec{s} \equiv_{Δ} \vec{t}} C (\vec{s}, \vec{t}, e) . \end{aligned}$ It satisfies ${\overset{―}{J}}_{Δ} (C, d, \vec{s}, \vec{s}, {\overset{―}{refl}}_{\vec{s}}) \equiv d (\vec{s})$ . The extension step first eliminates the head identity and then invokes $\overset{―}{J}$ on the transported tail. Thus no identity proofs are equated. Telescopic symmetry is the derived map ${\overset{―}{sym}}_{Δ} : \vec{s} \equiv_{Δ} \vec{t} \to \vec{t} \equiv_{Δ} \vec{s},$ obtained by ${\overset{―}{J}}_{Δ}$ with reflexivity clause ${\overset{―}{refl}}_{\vec{s}}$ . Its reflexivity computation is judgmental.

Referenced from 3 locations

Definition 78.9 — Restricted unification ¶

A unification problem is a telescope together with a homogeneous telescopic equality. The restricted transition system has four operations.

Solution: replace a variable $x$ by $t$ when $x \notin FV (t)$ .
Injectivity: replace $c (\vec{s}) = c (\vec{t})$ by the equations $\vec{s} \equiv_{Δ_{c}} \vec{t}$ , where $Δ_{c}$ is the constructor argument telescope.
Conflict: reject $c (\vec{s}) = d (\vec{t})$ when $c \neq d$ .
Cycle: reject $x = c (\vec{t} [x])$ when the displayed occurrence of $x$ lies at a recursive argument position below a constructor. First-order pattern problems produce cycles only at these ${Below}_{D}$ -reachable positions.

There is no transition deleting $t = t$ . Before injectivity is applied to $c (\vec{s}) = c (\vec{t}) : D (\vec{u})$ , the index problem $\vec{u} \equiv_{Ξ} \vec{u}$ must itself have a positive solution. A positive solution records a most general substitution; conflict or cycle is negative; a stuck problem is failure, not coverage.

Referenced from 12 locations

These are the two restrictions imposed in Cockx–Devriese–Piessens, Section 3.1: no deletion, and self-unifiability of indices before constructor injectivity. The first rejects $K (P, p, refl) = p$ for $e : {Id}_{A} (a, a)$ , because matching $e$ with reflexivity generates $a = a$ . Deleting that equation would turn path induction with fixed endpoint into K. The second restriction blocks the same deletion from being concealed by constructor injectivity one level higher. The second restriction has its own boundary. Without it, injectivity would admit the single clause $weakK ({refl}_{{refl}_{a}}) = {refl}_{{refl}_{{refl}_{a}}}$ at the type $\begin{aligned} weakK : & \prod_{e : {Id}_{{Id}_{A} (a, a)} ({refl}_{a}, {refl}_{a})} {Id}_{{Id}_{{Id}_{A} (a, a)} ({refl}_{a}, {refl}_{a})} (e, {refl}_{{refl}_{a}}) . \end{aligned}$ Splitting $e$ compares ${refl}_{a}$ with itself. Injectivity would accept that comparison if it inspected only the constructor heads, and the clause would prove that every loop at ${refl}_{a}$ is reflexivity. The self-unifiability test first asks the restricted unifier to solve the index problem $a = a$ ; deletion is unavailable, so the problem is stuck and the clause is rejected. Thus each restriction blocks a separate route to K.

Definition 78.10 — Basic analysis and recursive hypotheses ¶

Fix $D : Ξ \to U_{i}$ . Abbreviate $R_{k, r} : = Φ_{k, r} \to D ({\vec{v}}_{k, r})$ . Its constructors have the homogeneous telescopic form $\begin{aligned} c_{k} : (\vec{t} : Δ_{k}) & \to (x_{1} : R_{k, 1}) \to \dots \\ \to (x_{n_{k}} : R_{k, n_{k}}) \to D ({\vec{u}}_{k}) . \end{aligned}$ For $P : (\vec{u} : Ξ) \to D (\vec{u}) \to U_{j}$ , basic case analysis has type $\begin{aligned} B_{k} (P) & : = (\vec{t} : Δ_{k}) \to (x_{1} : R_{k, 1}) \to \dots \\ \to (x_{n_{k}} : R_{k, n_{k}}) \to P ({\vec{u}}_{k}, c_{k} \vec{t} x_{1} \dots x_{n_{k}}) . \end{aligned}$ The operation is ${case}_{D} : (\prod_{k} B_{k} (P)) \to \prod_{\vec{u} : Ξ} \prod_{x : D (\vec{u})} P (\vec{u}, x) .$ It computes by selecting $b_{k} (\vec{t}, x_{1}, \dots, x_{n_{k}})$ on the $k$ th constructor. The absent arguments are the recursive hypotheses of the full eliminator.

Define ${Below}_{D} (P, \vec{u}, x)$ by the dependent eliminator with universe-valued motive. Its $k$ th constructor equation is the telescope product $\prod_{r = 1}^{n_{k}} \prod_{ϕ : Φ_{k, r}} {Below}_{D} (P, {\vec{v}}_{k, r}, x_{r} ϕ) \times P ({\vec{v}}_{k, r}, x_{r} ϕ) .$ Thus nullary constructors produce $1$ , and a recursive function argument contributes one pair at each $ϕ : Φ_{k, r}$ . Put $\hat{D} : = \sum_{\vec{u} : Ξ} D (\vec{u}), {Below}_{D} (P, (\vec{u}; x)) : = {Below}_{D} (P, \vec{u}, x) .$ The two-argument form is used only when its second argument is visibly a point of $\hat{D}$ ; otherwise all three arguments are printed. Put ${Step}_{D} (P) : = \prod_{\vec{u} : Ξ} \prod_{x : D (\vec{u})} {Below}_{D} (P, \vec{u}, x) \to P (\vec{u}, x) .$ Given $p : {Step}_{D} (P)$ , the helper ${below}_{D} (P, p) : \prod_{\vec{u} : Ξ} \prod_{x : D (\vec{u})} {Below}_{D} (P, \vec{u}, x)$ is defined by the full eliminator. At recursive argument $x_{r}$ with induction hypothesis $h_{r}$ , its tuple component is $λ ϕ . (h_{r} (ϕ), p ({\vec{v}}_{k, r}, x_{r} ϕ, h_{r} (ϕ))) .$ The associated recursor is ${rec}_{D} : {Step}_{D} (P) \to \prod_{\vec{u} : Ξ} \prod_{x : D (\vec{u})} P (\vec{u}, x) .$ We print the motive $P$ as an explicit bookkeeping parameter, so an application has the form ${rec}_{D} (P, p, \vec{u}, x)$ . It is defined by ${rec}_{D} (P, p, \vec{u}, x) : = p (\vec{u}, x, {below}_{D} (P, p, \vec{u}, x))$ . All displayed constructor equations are judgmental.

Referenced from 3 locations

Indexed Inductive Families and Dependent Pattern Matching

Definition 78.11 — No confusion for an indexed family ¶

Let $\vec{a}, \vec{b} : \hat{D}$ . Define ${NoConfusion}_{D}$ by two applications of basic case analysis. For equal constructor tags it is the homogeneous telescopic equality of all constructor arguments; for distinct tags it is $0$ . Telescopic identity elimination and basic case analysis give $\begin{aligned} {noConf}_{D} (\vec{a}, \vec{b}) & : \vec{a} \equiv_{Ξ; D} \vec{b} \to {NoConfusion}_{D} (\vec{a}, \vec{b}), \\ {noConf}_{D}^{- 1} (\vec{a}, \vec{b}) & : {NoConfusion}_{D} (\vec{a}, \vec{b}) \to \vec{a} \equiv_{Ξ; D} \vec{b} . \end{aligned}$ On the diagonal, the first map returns reflexivity; the inverse transports the argument telescope through the constructor-and-index map and returns reflexivity.

Referenced from 5 locations

Lemma 78.12 — No-confusion retraction ¶

For $\vec{a}, \vec{b} : \hat{D}$ and $e : \vec{a} \equiv_{Ξ; D} \vec{b}$ , ${noConf}_{D}^{- 1} (\vec{a}, \vec{b}, {noConf}_{D} (\vec{a}, \vec{b}, e)) = e;$

Referenced from 3 locations

Indexed Inductive Families and Dependent Pattern Matching

Proof of Lemma 78.12 — No-confusion retraction

Proof. Apply ${\overset{―}{J}}_{Ξ; D}$ to $e$ . Its reflexivity case computes by basic case analysis to reflexivity, which proves the displayed identity without equating arbitrary identity proofs. ◻

Definition 78.13 — Below complements ¶

The acyclicity argument needs a second family elimination; constructor disjointness alone does not supply it. Retain $\hat{D} : = \sum_{\vec{u} : Ξ} D (\vec{u})$ and write a bold argument $\vec{a} = (\vec{u}; a) : \hat{D}$ for an index together with an inhabitant. Define $\begin{aligned} \vec{a} ⊀_{D} \vec{b} & : = {Below}_{D} (λ {\vec{b}}^{'} . \vec{a} \equiv_{Ξ; D} {\vec{b}}^{'} \to 0, \vec{b}), \\ {notBelowEq}_{D} (\vec{a}, \vec{b}) & : = (\vec{a} ⊀_{D} \vec{b}) \times (\vec{a} \equiv_{Ξ; D} \vec{b} \to 0) . \end{aligned}$

Referenced from 2 locations

Indexed Inductive Families and Dependent Pattern Matching

Lemma 78.14 — Acyclicity of recursive descent ¶

For $\vec{a}, \vec{b} : \hat{D}$ there is a term ${noCycle}_{D} : (\vec{a}, \vec{b} : \hat{D}) \to \vec{a} \equiv_{Ξ; D} \vec{b} \to \vec{a} ⊀_{D} \vec{b} .$

Referenced from 3 locations

Indexed Inductive Families and Dependent Pattern Matching

Proof of Lemma 78.14 — Acyclicity of recursive descent

Proof. Telescopic identity elimination reduces it to $(\vec{a} : \hat{D}) \to \vec{a} ⊀_{D} \vec{a}$ . In the $c_{i}$ method of the first family eliminator, fix a recursive child $x_{j} ϕ$ and define the complete child ${\vec{x}}_{j, ϕ} : = ({\vec{v}}_{i, j}; x_{j} ϕ) : \hat{D}$ . Define the auxiliary family $\begin{aligned} {Step}_{i, j} (\vec{t}, \vec{x}, ϕ, \vec{b}) : = & ({\vec{x}}_{j, ϕ} ⊀_{D} \vec{b}) \\ \to {notBelowEq}_{D} (({\vec{u}}_{i}; c_{i} \vec{t} \vec{x}), \vec{b}) . \end{aligned}$ The second family eliminator, now on $\vec{b}$ , constructs ${step}_{i, j} : (\vec{t}, \vec{x}, ϕ, \vec{b}) \to {Step}_{i, j} (\vec{t}, \vec{x}, ϕ, \vec{b}) .$ To display its method, let $\vec{b} = ({\vec{u}}_{p}; c_{p} {\vec{t}}^{'} {\vec{x}}^{'})$ , let $h_{q}^{'} ϕ^{'}$ be the second eliminator’s hypothesis for the complete child ${\vec{x}}_{q, ϕ^{'}}^{'} : = ({\vec{v}}_{p, q}; x_{q}^{'} ϕ^{'})$ , and assume $H : {\vec{x}}_{j, ϕ} ⊀_{D} ({\vec{u}}_{p}; c_{p} {\vec{t}}^{'} {\vec{x}}^{'}) .$ Unfolding $H$ gives, for every $q, ϕ^{'}$ , the component $H_{q} (ϕ^{'}) : {notBelowEq}_{D} ({\vec{x}}_{j, ϕ}, {\vec{x}}_{q, ϕ^{'}}^{'}) .$ The method returns $(α, β)$ , where $\begin{aligned} α & : ({\vec{u}}_{i}; c_{i} \vec{t} \vec{x}) ⊀_{D} ({\vec{u}}_{p}; c_{p} {\vec{t}}^{'} {\vec{x}}^{'}), \\ α_{q} (ϕ^{'}) & : = h_{q}^{'} (ϕ^{'}) ({pr}_{1} (H_{q} ϕ^{'})), \\ β & : ({\vec{u}}_{i}; c_{i} \vec{t} \vec{x}) \equiv_{Ξ; D} ({\vec{u}}_{p}; c_{p} {\vec{t}}^{'} {\vec{x}}^{'}) \to 0 . \end{aligned}$ For $β$ , suppose $e$ is such an equality. If $i \neq p$ , ${noConf}_{D} (e) : 0$ . If $i = p$ , no confusion exposes the homogeneous equality of the argument telescopes. Its $j$ th recursive component transports $H_{j} ϕ$ to ${notBelowEq}_{D} ({\vec{x}}_{j, ϕ}, {\vec{x}}_{j, ϕ})$ ; the second projection applied to $refl$ is in $0$ . These are the two components of the source construction: the parent is not below the descendant, and the parent is not the descendant.

Finally the $c_{i}$ method of the first eliminator is $λ \vec{t} . \vec{x} . \vec{h} . (λ ϕ . {step}_{i, 1} (\vec{t}, \vec{x}, ϕ, {\vec{x}}_{1, ϕ}, h_{1} ϕ), \dots, λ ϕ . {step}_{i, n_{i}} (\vec{t}, \vec{x}, ϕ, {\vec{x}}_{n_{i}, ϕ}, h_{n_{i}} ϕ)) .$ It has exactly the telescope product required by ${Below}_{D}$ . The first eliminator computes to this tuple, and $\overset{―}{J}$ computes at reflexivity. Thus the resulting ${noCycle}_{D}$ is obtained from two ordinary eliminations and $\overset{―}{J}$ ; it assumes neither K nor judgmental constructor injectivity. ◻

Definition 78.15 — Valid case tree ¶

A case tree for $f : (\vec{t} : Δ) \to T$ is a finite tree. A leaf contains a body of its specialized type. A split selects $x : D (\vec{u})$ and has the branches obtained by restricted unification with constructor result indices; negative branches have no subtree. A recursive leaf may call $f$ only on a proper recursive field of one fixed datatype argument. The tree is valid when every split has only positive or negative solutions, all specialized leaves typecheck, constructor branches cover the selected family, and calls have the stated structural decrease. The translation uses ${case}_{D}$ , ${Below}_{D}$ , ${rec}_{D}$ , no confusion, and acyclicity from definition 78.10, definition 78.11, lemma 78.14.

Referenced from 3 locations

Lemma 78.16 — Proof-relevant specialization ¶

Let a positive restricted solution of $\vec{u} \equiv_{Ξ} \vec{v}$ in $Δ$ be represented by a telescope map $σ : Δ^{'} \to Δ$ . For every $T : (\vec{t} : Δ) \to \vec{u} (\vec{t}) \equiv_{Ξ} \vec{v} (\vec{t}) \to U_{j}$ and $m : (\vec{z} : Δ^{'}) \to T (σ \vec{z}, \overset{―}{refl})$ there is $s : (\vec{t} : Δ) \to (e : \vec{u} (\vec{t}) \equiv_{Ξ} \vec{v} (\vec{t})) \to T (\vec{t}, e)$ such that $s (σ \vec{z}, \overset{―}{refl}) ⟶^{*} m (\vec{z}) .$ A negative solution yields a term of the same target for arbitrary $T$ .

Referenced from 4 locations

Indexed Inductive Families and Dependent Pattern Matching

Proof of Lemma 78.16 — Proof-relevant specialization

Proof. The internal transition terms must retain the proof argument. For a constructor $c$ whose result indices have already self-unified, injectivity uses the term $\begin{aligned} {injectivity}_{c}^{'} : & (Φ : (e : (\vec{u}; c \vec{s}) \equiv_{Ξ; D} (\vec{u}; c \vec{t})) \to U_{j}) \\ \to ((q : \vec{s} \equiv_{Δ_{c}} \vec{t}) \to Φ ({noConf}_{D}^{- 1} (\vec{u}; c \vec{s}, \vec{u}; c \vec{t}, q))) \\ \to (e : {Id}_{D (\vec{u})} (c \vec{s}, c \vec{t})) \to Φ ({\overset{―}{refl}}_{\vec{u}}; e) . \end{aligned}$ It applies ${noConf}_{D}$ and then the supplied method. Its reflexivity calculation uses ${noConf}_{D}^{- 1} {noConf}_{D} = id$ , so it preserves the actual equality proof. The conflict transition and cycle transition both retain the proof parameter: ${conflict}^{'}$ and ${cycle}^{'}$ have targets $(e : \vec{a} \equiv_{Ξ; D} \vec{b}) \to Φ (e)$ : the former eliminates ${noConf}_{D} (e) : 0$ , and the latter eliminates ${noCycle}_{D} (\vec{a}, \vec{b}, e)$ at the offending descendant. These are proof-dependent transition terms, not conversions of equalities to mere constraints.

A solution step, possibly after a dependency-preserving permutation of its telescope, is $\overset{―}{J}$ with the solved variable generalized. Its reflexivity branch is $m$ . There is no deletion step. Inductively a positive run therefore has telescopes $Δ_{0} = Δ, \dots, Δ_{n} = Δ^{'}$ and maps $τ_{r} : Δ_{r} \to Δ_{r - 1}$ with $σ = τ_{1} \circ \dots \circ τ_{n} .$ Only solution/permutation and ${injectivity}^{'}$ occur on such a run. Write (J) for the reflexivity equation of $\overset{―}{J}$ and (N) for the no-confusion retraction of lemma 78.12. If $s_{r}$ is its $r$ th internal transition term, then $\begin{aligned} s (σ \vec{z}, \overset{―}{refl}) & = s_{1} (s_{2} (\dots s_{n} (m) \dots)) (τ_{1} (\dots τ_{n} \vec{z} \dots), \overset{―}{refl}) \\ \overset{(J), (N)}{⟶^{*}} s_{2} (\dots s_{n} (m) \dots) (τ_{2} (\dots τ_{n} \vec{z} \dots), \overset{―}{refl}) \\ \overset{(J), (N)}{⟶^{*}} \dots \overset{(J), (N)}{⟶^{*}} m (\vec{z}) . \end{aligned}$ This proves (78.4) without proof irrelevance. ◻

Lemma 78.17 — One case-tree split is eliminable ¶

Suppose a valid node in context $Θ$ splits $x : D (\vec{u})$ and has goal $T$ . If every positive constructor branch has an eliminator-only term at its exact specialized type, then the node has an eliminator-only term of type $T$ . On $x \equiv c_{k} \vec{y}$ , it reduces to the $k$ th branch specialized by that branch’s telescope map.

Referenced from 2 locations

Indexed Inductive Families and Dependent Pattern Matching

Proof of Lemma 78.17 — One case-tree split is eliminable

Proof. Use basic case analysis with the proof-dependent motive $Q (\vec{w}, z) : = (\vec{t} : Θ) \to (\vec{u} (\vec{t}); x (\vec{t})) \equiv_{Ξ; D} (\vec{w}; z) \to T (\vec{t}) .$ The $c_{k}$ branch has target $(\vec{t} : Θ) \to (\vec{u} (\vec{t}); x (\vec{t})) \equiv_{Ξ; D} ({\vec{v}}_{k} (\vec{y}); c_{k} \vec{y}) \to T (\vec{t}) .$ For a positive unifier this is the specializer target in lemma 78.16; insert the translated subtree as $m$ . For a negative unifier, insert its empty eliminator. Apply the resulting ${case}_{D}$ term to $(\vec{u}; x)$ and ${\overset{―}{refl}}_{(\vec{u}; x)}$ . On $c_{k} \vec{y}$ , the basic-case equation and then (78.4) contract to the specialized $k$ th subtree. Replacing (78.7) by a motive that forgets the equality proof would silently assume proof irrelevance. ◻

Definition 78.18 — Root contraction of a case tree ¶

Let $C$ be a valid case tree for $f : (\vec{t} : Δ) \to T$ . The predicate ${CT}_{C} (\vec{t}, u)$ holds if and only if there are a leaf $f {\vec{p}}_{i} = e_{i}$ of $C$ and a well-typed substitution $θ$ for its pattern variables such that the following three conditions hold.

$\vec{t} \equiv T_{pat \to tm} ({\vec{p}}_{i}) [θ]$ ;
starting at the root, constructor selection and the positive restricted unifier at each split follow the unique path to that leaf;
$u$ is the literal instance $e_{i} [θ]$ , with recursive occurrences of $f$ left unchanged.

This predicate defines root contraction only. Compatible closure, when needed, is the ordinary compatible closure of these contractions.

Referenced from 6 locations

Theorem 78.19 — Elimination of valid dependent case trees ¶

Work in intensional dependent type theory with homogeneous identity types but without K. If $f : (\vec{t} : Δ) \to T$ is given by a valid case tree $C$ obeying definition 78.9, there is an eliminator-only $f^{'} : (\vec{t} : Δ) \to T$ . Write $e [f^{'} / f]$ for replacement of recursive occurrences. If ${CT}_{C} (\vec{t}, u)$ , then $f^{'} \vec{t} \equiv u [f^{'} / f] .$

Referenced from 7 locations

Proof of Theorem 78.19 — Elimination of valid dependent case trees

Proof. Let $t_{j} : D (\vec{v})$ be the designated structural argument. On a complete family argument $\vec{x}$ use the motive $P (\vec{x}) : = (\vec{t} : Δ) \to \vec{x} \equiv_{Ξ; D} (\vec{v} (\vec{t}); t_{j} (\vec{t})) \to T (\vec{t}) .$ Suppose for the moment that $m : (\vec{t} : Δ) \to {Below}_{D} (P, \vec{v} (\vec{t}), t_{j} (\vec{t})) \to T (\vec{t}) .$ Its recursor step is the proof-dependent wrapper $\begin{aligned} m_{s} (\vec{x}, H, \vec{t}, e) : = & {\overset{―}{J}}_{Ξ; D} (λ \vec{y} . e^{'} . {Below}_{D} (P, \vec{y}) \to T (\vec{t})) \\ (m \vec{t}, (\vec{v} (\vec{t}); t_{j} (\vec{t})), \vec{x}, {\overset{―}{sym}}_{Ξ; D} (e), H) . \end{aligned}$ Consequently $m_{s} ((\vec{v}; t_{j}), H, \vec{t}, \overset{―}{refl}) ⟶^{*} m \vec{t} H$ . Define $f^{'} (\vec{t}) : = {rec}_{D} (P, m_{s}, \vec{v} (\vec{t}), t_{j} (\vec{t})) (\vec{t}, \overset{―}{refl}) .$ Write (R) for the defining equation of ${rec}_{D}$ and (J) for the reflexivity equation of $\overset{―}{J}$ . The head calculation is $\begin{aligned} f^{'} (\vec{t}) & \overset{(R)}{⟶^{*}} m_{s} ((\vec{v}; t_{j}), {below}_{D} (P, m_{s}, \vec{v}, t_{j}), \vec{t}, \overset{―}{refl}) \\ \overset{(J)}{⟶^{*}} m \vec{t} {below}_{D} (P, m_{s}, \vec{v}, t_{j}) . \end{aligned}$

It remains to construct $m$ , by induction on the case tree. At a node whose patterns have variables $Θ$ and induce $τ : Θ \to Δ$ , retain the strengthened target $m_{τ} : (\vec{z} : Θ) \to {Below}_{D} (P, (\vec{v}; t_{j}) (τ \vec{z})) \to T (τ \vec{z}) .$ Suppose the node splits $Θ = Θ_{1}, (y : D^{'} ({\vec{v}}_{y})), Θ_{2}$ . For a constructor $c : (\vec{s} : Δ_{c}) \to D^{'} ({\vec{u}}_{c})$ , basic case analysis requires the method $\begin{aligned} m_{c} : (\vec{s} : Δ_{c}) & \to (\vec{z} : Θ) \to ({\vec{u}}_{c} (\vec{s}); c \vec{s}) \equiv_{Ξ; D} ({\vec{v}}_{y} (\vec{z}); y (\vec{z})) \\ \to {Below}_{D} (P, (\vec{v}; t_{j}) (τ \vec{z})) \to T (τ \vec{z}) . \end{aligned}$ This is the proof-dependent target to which the transition terms above apply. A negative unification run supplies it by ${conflict}^{'}$ or ${cycle}^{'}$ . A positive run has a most general unifier (MGU) $σ : Θ^{'} \to Δ_{c}; Θ$ . Write $σ_{Θ} : = {pr}_{Θ} \circ σ$ for its projection to the original node variables. The subtree induction hypothesis is $m_{c}^{'} : ({\vec{z}}^{'} : Θ^{'}) \to {Below}_{D} (P, (\vec{v}; t_{j}) (τ σ_{Θ} {\vec{z}}^{'})) \to T (τ σ_{Θ} {\vec{z}}^{'}) .$ The specializer of lemma 78.16, instantiated with the remaining ${Below}_{D}$ argument in its motive, turns $m_{c}^{'}$ into (78.13).

The computation is not hidden in an MGU assertion. When the selected value is $c \vec{s}$ , the equations are satisfied, so the syntactic first-order MGU computes ${\vec{z}}^{'} : Θ^{'}$ with the literal substitution identity $σ {\vec{z}}^{'} \equiv (\vec{s}; {\vec{z}}_{1}; c \vec{s}; {\vec{z}}_{2}),$ where $({\vec{z}}_{1}, c \vec{s}, {\vec{z}}_{2})$ has the original valid telescope order. The factorization may permute independent declarations while finding ${\vec{z}}^{'}$ , but that permutation is reflected in the displayed literal identity and drops no dependent declaration. Write (B) for basic-case computation, (M) for this literal identity, and (S) for (78.4). Then $\begin{aligned} m_{τ} ({\vec{z}}_{1}; c \vec{s}; {\vec{z}}_{2}, H) & \overset{(B)}{⟶^{*}} m_{c} (\vec{s}, {\vec{z}}_{1}; c \vec{s}; {\vec{z}}_{2}, \overset{―}{refl}, H) \\ \overset{(M)}{\equiv} m_{c} (σ {\vec{z}}^{'}, \overset{―}{refl}, H) \overset{(S)}{⟶^{*}} m_{c}^{'} ({\vec{z}}^{'}, H) . \end{aligned}$ The last reduction is (78.6). This is why the factorization must preserve the telescope dependencies, not merely pass an occurs check. An empty node has only negative methods and no subtree.

At a leaf with body $e_{i} : T τ$ , replace each structurally recursive call $f \vec{r}$ by the projection supplied by $H$ . If $r_{j}$ is the named proper recursive child, that projection has type $π_{H} : (\vec{r} : Δ) \to (\vec{w}; r_{j}) \equiv_{Ξ; D} (\vec{v}; t_{j}) \to T (\vec{r}) .$ On the canonical below-package it calculates, using (R) and (J), $\begin{aligned} π_{{below}_{D} (P, m_{s}, \vec{v}, t_{j})} (\vec{r}, \overset{―}{refl}) \\ \overset{(R)}{⟶^{*}} m_{s} ((\vec{w}; r_{j}), {below}_{D} (P, m_{s}, \vec{w}, r_{j}), \vec{r}, \overset{―}{refl}) \\ \overset{(J)}{⟶^{*}} m \vec{r} {below}_{D} (P, m_{s}, \vec{w}, r_{j}) \overset{(78.10)}{\equiv} f^{'} (\vec{r}) . \end{aligned}$ Thus the translated leaf $e_{i}^{'}$ is judgmentally equal to $e_{i} [f^{'} / f]$ when its $H$ argument is canonical.

For a source clause $f {\vec{p}}_{i} = e_{i}$ , combine (78.11), the node calculations (78.15), and (78.16): Write (H) for (78.11), (N) for (78.15), and (L) for (78.16). Then $\begin{aligned} f^{'} (T_{pat \to tm} ({\vec{p}}_{i})) & \overset{(H)}{⟶^{*}} m T_{pat \to tm} ({\vec{p}}_{i}) ({below}_{D} (P, m_{s}, T_{pat \to tm} (\vec{v}; p_{i, j}))) \\ \overset{(N)}{⟶^{*}} e_{i}^{'} [H \mapsto {below}_{D} (P, m_{s}, T_{pat \to tm} (\vec{v}; p_{i, j}))] \\ \overset{(L)}{\equiv} e_{i} [f^{'} / f] . \end{aligned}$ By definition 78.18, every ${CT}_{C} (\vec{t}, u)$ selects one such leaf and substitution. Substitution into the displayed calculation gives $f^{'} \vec{t} \equiv u [f^{'} / f]$ . No transition deletes a reflexive equation, and every use of equality is through its proof-dependent motive, so K is absent. ◻

This is a source-bounded reconstruction of Cockx–Devriese–Piessens, Theorem 1 [CDP16]. It retains the theorem’s homogeneous telescopic equality, dependency-preserving unifier factorization, proof-dependent internal transitions, basic case analysis, and ${Below}_{D}$ recursion; only notation is normalized to the book. The specialization proof has no deletion case, and its injectivity case begins with the index self-unifier.

Example 78.20 — The identity family ¶

Fix $a : A$ . The single clause $J (P, p, . a, refl) = p$ has input $b : A, e : {Id}_{A} (a, b)$ . Splitting on $e$ generates $b = a$ . Solution replaces $b$ by $a$ without deleting a reflexive equation. The translated term is based identity induction, and on $refl$ both the case clause and the translated $J$ term reduce to $p$ . If the input instead fixes $e : {Id}_{A} (a, a)$ , the generated problem is $a = a$ ; restricted unification is stuck, so the K case tree is invalid.

Referenced from 2 locations

Indexed Inductive Families and Dependent Pattern Matching

Two larger indexed signatures

The eliminator discipline scales beyond a family whose constructors merely fix an index. It does not license theorem transfer from one larger signature mechanism to another. This section freezes two bounded rule cards: inductive–recursive signatures, where a datatype and a decoding function are generated together, and induction–induction, where a type and a family over it are generated together. We calculate their rules and stop there.

Inductive–recursive and indexed inductive–recursive signatures. Fix $O : U_{j}$ . The selected IR signature codes are generated by $ι (o), σ (A, S), δ (A, S),$ where $o : O$ , $A : U_{i}$ , $S : A \to {Sig}_{i} (O)$ in the $σ$ case, and $S : (A \to O) \to {Sig}_{i} (O)$ in the $δ$ case. Given $R : U_{i}$ and $e : R \to O$ , define the constructor fields $E_{S} (R, e)$ and decoded output $F_{S}$ by $\begin{aligned} E_{ι (o)} (R, e) & : = 1, & F_{ι (o)} (⋆) & : = o, \\ E_{σ (A, S)} (R, e) & : = \sum_{a : A} E_{S (a)} (R, e), & F_{σ (A, S)} (a, x) & : = F_{S (a)} (x), \\ E_{δ (A, S)} (R, e) & : = \sum_{f : A \to R} E_{S (e \circ f)} (R, e), & F_{δ (A, S)} (f, x) & : = F_{S (e \circ f)} (x) . \end{aligned}$ The generated type and decoder have the rules $IR (S) : U_{i}, El : IR (S) \to O, intro : E_{S} (IR (S), El) \to IR (S),$ with recursive decoding equation $El (intro (x)) \equiv F_{S} (x) .$ For $P : IR (S) \to U_{k}$ , let ${IH}_{S} (P, x)$ contain one $P (f (a))$ for every recursive field $f : A \to IR (S)$ in a $δ$ node and recurse through the residual signature. Then $\begin{aligned} {elim}_{IR} : & (P : IR (S) \to U_{k}) \\ \to ((x : E_{S} (IR (S), El)) \to {IH}_{S} (P, x) \to P (intro (x))) \\ \to (z : IR (S)) \to P (z), \end{aligned}$ and ${elim}_{IR} (P, m, intro (x)) \equiv m (x, {mapIH}_{S} ({elim}_{IR} (P, m), x)) .$ A $δ$ field is genuinely recursive: its decoded function $El \circ f$ selects the continuation signature, and the method receives the recursively computed values for every $f (a)$ .

For indexed IR, fix $I : U_{k}$ and $O : I \to U_{j}$ . A $δ$ code now also carries $ix : A \to I$ and continuation $S : ((a : A) \to O (ix (a))) \to {Sig}_{i} (I, O)$ . The generated objects are $\begin{aligned} IIR (S) & : I \to U_{max (i, k)}, \\ El & : IIR (S) (u) \to O (u), \\ intro & : E_{S} (IIR (S), El, u) \to IIR (S) (u), \end{aligned}$ again with $El (intro (x)) \equiv F_{S} (x)$ . For the vector signature, the cons branch chooses $n : N$ , stores $a : A$ , takes one recursive field at index $n$ , and returns index $suc (n)$ . Its derived constructor and recursive-decoding calculation are $\begin{aligned} cons & : (n : N) \to A \to IIR (S) (n) \to IIR (S) (suc (n)), \\ El (cons (n, a, a s)) & \equiv F_{S_{cons}} (n, a, a s) . \end{aligned}$ The indexed eliminator has motives $P : (u : I) \to IIR (S) (u) \to U_{l}$ ; its cons computation passes the induction hypothesis $P (n, a s)$ to the cons method. These are precisely the formation, introduction, recursive-decoding, elimination, and computation rules used here from Kovács’s signatures [Kov26]. His canonicity construction is not imported.

A context/type induction–induction card. The small simultaneous signature has $\begin{aligned} Con & : U, & Ty & : Con \to U, \\ ϵ & : Con, & ext & : (Γ : Con) \to Ty (Γ) \to Con, \\ U & : (Γ : Con) \to Ty (Γ), & El & : (Γ : Con) \to Ty (ext (Γ, U (Γ))) . \end{aligned}$ Its dependent eliminator requires two motives, because the motive for types is indexed by the already computed context result: $C : (Γ : Con) \to U, T : (Γ : Con) \to C (Γ) \to Ty (Γ) \to U .$ The four methods are $\begin{aligned} e & : C (ϵ), \\ x & : (c : C (Γ)) \to T (Γ, c, A) \to C (ext (Γ, A)), \\ u & : (c : C (Γ)) \to T (Γ, c, U (Γ)), \\ q & : (c : C (Γ)) \to T (ext (Γ, U (Γ)), x (c, u (c)), El (Γ)) . \end{aligned}$ They produce simultaneous eliminators $elimCon (Γ) : C (Γ), elimTy (A) : T (Γ, elimCon (Γ), A),$ with computations $\begin{aligned} elimCon (ϵ) & \equiv e, \\ elimCon (ext (Γ, A)) & \equiv x (elimCon (Γ), elimTy (A)), \\ elimTy (U (Γ)) & \equiv u (elimCon (Γ)), \\ elimTy (El (Γ)) & \equiv q (elimCon (Γ)) . \end{aligned}$ The final equation is well typed because the $C$ -result for the extended context computes by the preceding equation. This is the bounded context/type example of Lafont, Kaposi, and Kovács [KKL20]. We claim neither their reduction to ordinary induction nor initiality, extensional reduction, gluing, quotient, or path constructors.

Exercise 78.2 ¶

★★☆ Expand one $δ$ case in the IR eliminator. Show where $El \circ f$ selects the continuation signature, and calculate the induction-hypothesis component for one chosen $a : A$ .

Referenced from 3 locations

Exercise 78.3 ¶

★★☆ Type the method $q$ in the context/type card. Use the computation for $elimCon (ext (Γ, U (Γ)))$ to verify the classifier of the last displayed equation.

Referenced from 3 locations

Exercise 78.4 ¶

★★☆ Run definition 78.9 on the two problems $x = suc (y)$ and $suc (x) = suc (x)$ . Give the transition sequence for the first and identify the exact point at which the second fails. Explain why adding deletion would admit the second problem.

Referenced from 3 locations

Exercise 78.5 ¶

★★☆ Construct $last : \prod_{n : N} Vec (A, suc (n)) \to A$ from Vec-elim. State its value on a one-element vector and on a vector whose tail is nonempty, and justify both equations from Vec-comp.

Referenced from 4 locations

Exercise 78.6 ¶

★★☆ Give constructor clauses for $last$ from exercise 78.5. Build their valid case tree, including the dot pattern forced by the successor index, and apply theorem 78.19. Display the eliminator-only term and verify its one-element and nonempty-tail equations from definition 78.18. (Half a page.)

Referenced from 3 locations

Suggested first pass.

Begin with exercise 78.7.

Exercise 78.7 ¶

★★☆ Reconstruct the eliminator term for append from construction 78.7. Prove by vector elimination that appending $vnil$ on the right yields the input after the required transport. More precisely, first construct $l_{m} : {Id}_{N} (0 + m, m)$ by natural-number induction, and then construct ${tr}_{l_{m}}^{k . Vec (A, k)} (append (x s, vnil)) = x s (x s : Vec (A, m)) .$ State why the equality is not judgmental for a neutral vector.

Referenced from 4 locations

Exercise 78.8 — Executable dependent DSL ¶

★★★ Practical project.indexed-format-parser Implement in Kappa a format-indexed parser for fixed-width unsigned decimal fields. A format contains field widths as an indexed vector; a typed intermediate form pairs each parsed field with evidence that its digit count is the constructor-determined width. Maintain this index invariant through parsing and printing. On the format $[2, 1, 3]$ , the program must parse $427105$ as $[42, 7, 105]$ and print the same six-character string. It must reject $42715$ before constructing the typed intermediate form, naming the final field’s expected width $3$ and actual width $2$ . The acceptance test compares these exact success and rejection results.

Referenced from 4 locations

Sources. The no-K case-tree criterion, its two restricted-unification conditions, and the eliminator translation follow Cockx, Devriese, and Piessens, Eliminating Dependent Pattern Matching without K, Theorem 1 and Section 3.1 [CDP16]. The chapter has restated the theorem at its case-tree signature and proved the identity-family witness locally; it has not assumed Agda’s K axiom or a completeness theorem for unrestricted dependent unification. The IR/IIR rule card is restricted to the signature, introduction, decoding, elimination, and computation rules on pp. 4–8 of Kovács [Kov26]; its canonicity theorem is outside this chapter. The context/type induction–induction card reproduces the signature and general eliminator calculation on pp. 2–3 of Lafont, Kaposi, and Kovács [KKL20]; their reduction and uniqueness results are likewise not transferred.