ch:proof-tactics: ch:proof-tactics · Lectures on Type Theory

Define $apply (f)$ on $(Γ ∣ B)$ to return the one goal $(Γ ∣ A)$ with validation $V (a) = f a$ . If $Γ ⊢ a : A$ , then the variable premise gives $Γ ⊢ f : A \to B$ , and application gives $Γ ⊢ V (a) : B$ . Hence the returned state satisfies the validation invariant.

The states, with their validations to the preceding state, are $\begin{array}{cc} [(\cdot ∣ A \to A \times A)] & id \\ [(x : A ∣ A \times A)] & p \mapsto λ x . p \\ [(x : A ∣ A), (x : A ∣ A)] & (p, q) \mapsto (p, q) \\ [] & () \mapsto (x, x) . \end{array}$ Sequencing partitions the empty final argument list into the two nullary assumption validations and substitutes both returned occurrences of $x$ into the split validation. Substitution of that pair into the intro validation gives the closed term $λ x . (x, x) : A \to A \times A$ .

Let $T_{1} = intro; assumption$ , which returns $p_{1} = λ x . x$ . Let $T_{2}$ be $exact ((λ z : A \to A . z) (λ x : A . x))$ , which returns the beta-distinct raw term $p_{2} = (λ z : A \to A . z) (λ x : A . x)$ . Both kernel-check at $A \to A$ , and $p_{2}$ beta-reduces to $p_{1}$ . Thus $T_{1} orelse T_{2}$ records the intro/assumption trace, whereas the reversed choice records one exact step. Left bias changes the raw proof and trace; validity of the selected branch supplies a kernel proof in either order.