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) We want to prove to prove
$$D_1 ; f : \mathbb{N} → \mathbb{R}, n : \mathbb{N} ⊢ a_1(f,n) : \mathbb{R} $$
We assume that $D_1$ is correct in the empty environment. By exercise 9.7(a) this means the definiens and its type is derivable from the context of the definition.
The context of the definition matches the context of what we want to prove, namely $f : \mathbb{N} → \mathbb{R}, n : \mathbb{N}$. The definition tells us that in this context, $a_1(f,n)$ has type $\mathbb{R}$. This what we want to prove, so we are done.
In effect, what we want to prove is defined to be true by the definition.
