ch:dependent-refinement: ch:dependent-refinement

The first product comparison uses the client domain $P$ : $\frac{\begin{matrix} P <: I \\ x : P ⊢ Q_{0} (x) <: Q_{1} (x) \end{matrix}}{(x : I) \to Q_{0} (x) <: (x : P) \to Q_{1} (x)} Π - Sub .$ The second uses reflexivity of the same domain: $\frac{\begin{matrix} P <: P \\ x : P ⊢ Q_{1} (x) <: Q_{2} (x) \end{matrix}}{(x : P) \to Q_{1} (x) <: (x : P) \to Q_{2} (x)} Π - Sub .$ Transitivity gives the required comparison. Reversing only the domain premise would let a function defined merely on positive integers $P$ be used at a type whose domain is all integers $I$ , because $P <: I$ . A client may then pass $- 1 : I$ . The provider has no premise that permits its body to use $- 1$ as an element of $P$ ; the reversed rule is therefore not substitution safe.

The source predicate $1 \leq ν$ entails $0 \leq ν$ , so R-Base-Sub derives $R_{2} <: R_{1}$ . Under $x : R_{1}$ , give an occurrence of $x$ its singleton refinement $X_{x} = {ν : Int ∣ ν = x}$ . Then $λ u : X_{x} . u : Π_{u : X_{x}} {ν : Int ∣ 0 \leq ν - x},$ because the equality edges $x \overset{0}{\to} ν$ and $ν \overset{0}{\to} x$ certify $x - ν \leq 0$ . Narrowing replaces the assumption edge for $R_{1}$ , $x \overset{0}{\to} 0$ , by the stronger edge $x \overset{- 1}{\to} 0$ for $R_{2}$ . The result entailment still uses the two equality edges; the new bound edge is available but is not needed by the zero-weight path $ν \to x$ .

The subtype premise is what permits every old use of $0 \leq x$ . If a replacement declaration is admitted without that premise, take its unconstrained value to be $x = - 1$ . It satisfies the replacement’s empty predicate but falsifies $0 \leq x$ , so any old derivation using the $R_{1}$ assumption can no longer be rebuilt. Thus arbitrary context replacement is not narrowing.

The upcast to an unknown index retains the vector constructor and its index tag. Hence the nil calculation is $cast [Vec A 0 \Leftarrow Vec A ?] (cast [Vec A ? \Leftarrow Vec A 0] (nil A)) ⟶^{*} nil A .$ For the cons value, the retained constructor announces successor index $suc 0$ . The downcast demands index $0$ , so its constructor/index test fails and the term reduces to ${err}_{Vec A 0}$ . The first equation is the projection after the embedding of a run-time representation. It compares constructor tags and returns data; it neither compares nor erases two proof terms, so it is not proof irrelevance.

From $F : Π_{x : A_{1}} B_{1}$ , $N : A_{2}$ , and $A_{2} <: A_{1}$ , subsumption first gives $N : A_{1}$ . Rule $Π$ -E therefore derives $F N : B_{1} [N / x]$ . The codomain premise is checked before substitution in the client context $Γ, x : A_{2} ⊢ B_{1} <: B_{2} .$ Substitution of the already typed argument gives $Γ ⊢ B_{1} [N / x] <: B_{2} [N / x] .$ A final subsumption step yields $F N : B_{2} [N / x]$ . Thus the smaller-domain context occurs in the premise, and $[N / x]$ occurs only after the application and codomain comparison have both been established.

Use a two-element type interpretation $0 < 1$ . Let $P <: I$ , take $B_{1} (x) = 1$ and $B_{2} (x) = 0$ for every $x : P$ , and consider $Π_{x : I} B_{1} (x) and Π_{x : P} B_{2} (x) .$ Both products are well formed, and the domain premise $P <: I$ has the required contravariant orientation. The codomain premise would be $1 <: 0$ under $x : P$ , which is false in the interpretation. Therefore the product subtype judgment is not derivable. The same construction with any proper domain inclusion and constant top/bottom codomain families gives the requested pair; dependence does not make the codomain check optional.

Write $L = len (a)$ . The parameter refinement $0 - i \leq 0$ contributes $i \overset{0}{\to} 0$ . The then-branch test $i - L \leq - 1$ contributes $L \overset{- 1}{\to} i$ . The goal is the latter constraint itself, so the one-edge path $L \overset{- 1}{\to} i$ is a shortest-path certificate of weight $- 1$ . After deleting the branch assumption, set $L = 0$ and $i = 0$ . The parameter constraint holds, but the goal becomes $0 \leq - 1$ , which is false. No certificate can be reconstructed from the remaining graph.

Prove the two statements simultaneously: $\begin{aligned} {check}_{n} ({forget}_{n} (v)) & = some (v), \\ {check}_{n} (l) = some (v) & ⟹ {forget}_{n} (v) = l . \end{aligned}$ For $n = 0$ , a vector is $nil$ ; forgetting gives the empty list, and the zero checker returns $some (nil)$ . Conversely, the zero checker can return a vector only on the empty list, so the forgotten result is that list.

For $n = suc m$ , write $v = cons (a, w)$ . The head calculation is the reflexive equality $a = a$ . The recursive tail equation is ${check}_{m} ({forget}_{m} (w)) = some (w),$ by the induction hypothesis. The successor checker combines these two facts and returns $some (cons (a, w))$ . Conversely, if ${check}_{suc m} (a :: l) = some (cons (b, w))$ , its head test gives $a = b$ , while its recursive call gives ${check}_{m} (l) = some (w)$ . The second induction hypothesis gives ${forget}_{m} (w) = l$ ; congruence of list cons with the head equality yields ${forget}_{suc m} (cons (b, w)) = a :: l$ . These are all vector and list shapes accepted by the indexed checker.