See Exercises 9.6 and 9.7.
(a) Let $\Delta^{′} ≡ D_1, \ldots ,D_5$. Assume that $D_6$ is correct in environment $\Delta^{′}$ and
$$\Delta^{′} ; ∅ ⊢ (a_1(λx : \mathbb{N} . x, 100) = (λx : \mathbb{N} . x)5050) : *_p$$
Derive:
$$ \Delta ; ∅ ⊢ \texttt{formalprf}_6 : a_1(λx : \mathbb{N} . x, 100) = (λx : \mathbb{N} . x)5050 $$
(b) Assume that the conditions mentioned in Exercise 9.7(a) have been satisfied. What is the fastest manner to prove
$$D_1 ; f : \mathbb{N} → \mathbb{R}, n : \mathbb{N} ⊢ a_1(f,n) : \mathbb{R} $$
We remind ourselves of definitions $D_1$ to $D_6$:
$$\begin{align*} D_1 \; &≡ \; f : \mathbb{N} \to \mathbb{R}, \; n : \mathbb{N} \quad \triangleright \quad a_1(f,n) := \sum ^n_{i=0}(f i) : \mathbb{R} \\ \\ D_2 \; & ≡ \; f : \mathbb{N} \to \mathbb{R}, \; d : \mathbb{R} \quad \triangleright \quad a_2(f,d) := \forall _{n:\mathbb{N}}(f (n+1)−f n= d) : *_p \\ \\ D_3 \; & ≡ \; f : \mathbb{N} \to \mathbb{R}, \; d : \mathbb{R}, \; u : a_2(f,d), \; n : \mathbb{N} \quad \triangleright \\ & a_3(f,d,u,n) := \texttt{formalprf}_3 : f n= f 0 + n \cdot d \\ \\ D_4 \; & ≡ \; f : \mathbb{N} \to \mathbb{R}, \; d : \mathbb{R}, \; u : a_2(f,d), \; n : \mathbb{N} \quad \triangleright \\ & a_4(f,d,u,n) := \texttt{formalprf}_4 : a_1(f, n) = \frac{1}{2} \cdot (n+1) \cdot (f 0 + f n) \\ \\ D_5 \; & ≡ \; f : \mathbb{N} \to \mathbb{R}, \; d : \mathbb{R}, \; u : a_2(f,d), \; n : \mathbb{N} \quad \triangleright \\ & a_5(f,d,u,n) := \texttt{formalprf}_5 : a_1(f,n) = (n+1) \cdot f 0+ \frac{1}{2}\cdot n \cdot (n+1) \cdot d \\ \\ D_6 \; & ≡ \; \emptyset \quad \triangleright \quad a_6 := \texttt{formalprf}_6 : \sum^{100}_{ i=0} (i) = 5050 \end{align*}$$
(a) We're given $D_6$ is correct in environment $\Delta^{′}$. This means
$$\Delta^{\prime}, \emptyset \; \triangleright \; a_6 := \texttt{formalprf}_6 : \sum^{100}_{ I=0} (i) = 5050 \; ; \; \emptyset \; \vdash \; * : \Box $$
We're also given
$$\Delta^{′} ; ∅ ⊢ (a_1(λx : \mathbb{N} . x, 100) = (λx : \mathbb{N} . x)5050) : *_p$$
And we want to derive
$$ \Delta ; ∅ ⊢ \texttt{formalprf}_6 : a_1(λx : \mathbb{N} . x, 100) = (λx : \mathbb{N} . x)5050 $$
Let's consider the (inst) rule. The conclusion is a judgement $\Delta; \Gamma \vdash a(\bar{U}):N[\bar{x} := \bar{U}]$. Here the constant $a$ is $\texttt{formalprf}_6$ with no parameter list. The type $N$ is $\sum^{100}_{ i=0} (i) = 5050$. Noting that $\Gamma = \emptyset$, this gives us
$$ (\textit{inst}) \quad \frac{\Delta ; \emptyset \vdash *:\Box }{\Delta; \emptyset \vdash \texttt{formalprf}_6 : \sum^{100}_{ i=0} (i) = 5050} \tag{i} $$
where $\Delta = \Delta^{\prime}, D_6$. The first premise is true because we're given that $D_6$ is correct in the environment $\Delta^{\prime}$. There is no second premise as there are no parameters to the defined constant $\texttt{formalprf}_6$.
Next we want to show that $\sum^{100}_{ i=0} (i) = 5050$ is $βδ$-equivalent to $a_1(λx : \mathbb{N} . x, 100) = (λx : \mathbb{N} . x)5050$.
$$ a_1(λx : \mathbb{N} . x, 100) = (λx : \mathbb{N} . x)5050 \quad \triangleq _ \beta \quad \sum ^{100}_{i=0}( i) = (λx : \mathbb{N} . x)5050 \quad \triangleq _ \beta \quad \sum ^{100}_{i=0}(i) = 5050 $$
That is,
$$ a_1(λx : \mathbb{N} . x, 100) = (λx : \mathbb{N} . x)5050 \quad \triangleq_\beta \quad \sum ^n_{i=0}(f i) = 5050 \tag{ii} $$
We need the (def) rule to build the required second premise for the (conv) rule.
$$ (\textit{def}) \quad \frac{ \Delta^{\prime};\emptyset \vdash (a_1(λx : \mathbb{N} . x, 100) = (λx : \mathbb{N} . x)5050) : *_p \quad \quad \Delta^{\prime};\emptyset \vdash \texttt{formalprf}_6 : \sum^{100}_{ i=0} (i) = 5050 }{ \Delta ; \emptyset ⊢ (a_1(λx : \mathbb{N} . x, 100) = (λx : \mathbb{N} . x)5050) : *_p} \tag{iii}$$
where $\Delta = \Delta^{\prime}, D_6$. The second premise is intuitively true, but can be justified by another application of the (inst) rule as follows:
$$ (\textit{inst}) \quad \frac{\Delta^{\prime} ; \emptyset \vdash *:\Box }{\Delta^{\prime}; \emptyset \vdash \texttt{formalprf}_6 : \sum^{100}_{ i=0} (i) = 5050} $$
There is no second premise as there are no parameters to the defined constant $\texttt{formalprf}_6$.
We can now use the (conv) rule using result (ii), and result (iii) as the second premise.
$$ (\textit{conv}) \quad \frac{ \Delta; \emptyset \vdash \texttt{formalprf}_6 : \sum^{100}_{ i=0} (i) = 5050 \quad \quad \Delta ; ∅ ⊢ (a_1(λx : \mathbb{N} . x, 100) = (λx : \mathbb{N} . x)5050) : *_p } {\Delta ; ∅ ⊢ \texttt{formalprf}_6 : a_1(λx : \mathbb{N} . x, 100) = (λx : \mathbb{N} . x)5050}$$
We have derived the required conclusion.
$$\Delta ; ∅ ⊢ \texttt{formalprf}_6 : a_1(λx : \mathbb{N} . x, 100) = (λx : \mathbb{N} . x)5050 \tag*{$\Box$}$$
(b) TODO
