Chapter 9 - Exercise 10

Let $\mathcal{J}_1, \ldots, J_n$ be judgements such that, listed in this order, they form a derivation. Let

$$ \mathcal{J}_n \; \equiv \;  \Delta_n \; ; \; \Gamma_n \; \vdash \; M_n \; : \; N_n \; \mid \; J_n $$

be the final judgement in this derivation, with $J_n$ its justification in $λD_0$.

Assume that for all $i < j$: if $\mathcal{J}_i \equiv \Delta_i ; \Gamma_i \vdash M_i : N_i$, then we have that $\Delta_i \; ; \; \Gamma_i \; \vdash \; *: \Box$.

(a) Let $J_n$ be a case of the (weak)-rule. Prove that

$$\Delta_n \; ; \; \Gamma_n \; \vdash \;  *: \Box$$

(b) The same if $J_n$ is a case of the (var)-rule.

(c) The same if $J_n$ is a case of the (def)-rule.

(d) The same if $J_n$ is a case of one of the other $λD_0$-rules as given in Figure 9.3.

(a) If $J_n$ is the (weak) rule then it must be the case that

$$ (\textit{weak}) \quad \frac{\Delta_n ; \Gamma_n^{\prime} \vdash M_n:N_n \quad \Delta_n;  \Gamma_n^{\prime} \vdash C:s}{\Delta_n ; \Gamma_n \vdash M_n:N_n} \quad \text{ where } x \notin  \Gamma_n^{\prime} $$

where $\Gamma_n \equiv  \Gamma_n^{\prime}, x:C$, and $s=*$ or $s=\Box$. 

The first premise $\Delta_n ; \Gamma_n^{\prime} \vdash M_n:N_n$ must have been derived before $\mathcal{J}_n$. By the given assumption, this means $\Delta_n ; \Gamma_n^{\prime} \vdash *:\Box$. 

Using the (weak) rule

$$ (\textit{weak}) \quad \frac{\Delta_n ; \Gamma_n^{\prime} \vdash *:\Box \quad \Delta_n;  \Gamma_n^{\prime} \vdash C:s}{\Delta_n ; \Gamma_n \vdash *:\Box} \quad \text{ where } x \notin  \Gamma_n^{\prime} $$

This is the conclusion we desire.

(b) If $J_n$ is the (var) rule then it must be the case that

$$ (\textit{var}) \quad \frac{\Delta_n ; \Gamma_n^{\prime} \vdash N_n:s}{\Delta_n ; \Gamma_n \vdash M_n:N_n} $$

where $\Gamma_n \equiv  \Gamma_n^{\prime}, M_n:N_n$, and $s=*$ or $s=\Box$. 

The premise $\Delta_n ; \Gamma_n^{\prime} \vdash N_n:s$ must have been derived before $\mathcal{J}_n$. By the given assumption, this means $\Delta_n ; \Gamma_n^{\prime} \vdash *:\Box$.

Using the (weak) rule

$$ (\textit{weak}) \quad \frac{\Delta_n ; \Gamma_n^{\prime} \vdash *:\Box \quad \Delta_n;  \Gamma_n^{\prime} \vdash N_n:s}{\Delta_n ; \Gamma_n \vdash *:\Box} \quad \text{ where } x \notin  \Gamma_n^{\prime} $$

This is the conclusion we desire.

(c) If $J_n$ is the (def) rule then it must be the case that

$$ (\textit{def}) \quad \frac{\Delta_n^{\prime};\Gamma_n \vdash M_n:M_n \quad \Delta_n^{\prime} ; \bar{x}:\bar{A} \vdash C:D} {\Delta_n ; \Gamma_n \vdash M_n:N_n} \quad \text{ if } a \notin \Delta $$

where $\Delta_n \equiv \Delta_n^{\prime},\bar{x}:\bar{A} \triangleright a(\bar{x}) := C:D$. 

The first premise $\Delta_n^{\prime};\Gamma_n \vdash M_n:M_n$ must have been derived before $\mathcal{J}_n$. By the given assumption, this means $\Delta_n^{\prime};\Gamma_n \vdash *:\Box$. 

Using the (def) rule

$$ (\textit{def}) \quad \frac{\Delta_n^{\prime};\Gamma_n \vdash *:\Box \quad \Delta_n^{\prime} ; \bar{x}:\bar{A} \vdash C:D} {\Delta_n ; \Gamma_n \vdash *:\Box} \quad \text{ if } a \notin \Delta $$

This is the conclusion we desire.

Note: This exercise is suggesting that correctness is preserved by the $\lambda D_0$ derivation rules.

(d) As an edge case, we'll try the (sort) rule.

If $J_n$ is the (sort) rule then it must be the case that

$$ (\textit{sort}) \quad \emptyset ; \emptyset \vdash *:\Box $$

This is the desired conclusion, with $\Delta = \emptyset, \Gamma = \emptyset$. 

Chapter 9 - Exercise 9

Let $Γ \equiv A : *, B : *, C : *$. Prove, by giving full derivations in $λD_0$:

(a) $\emptyset; \Gamma \; \vdash \; *:\Box$

(b) $\emptyset; \Gamma \; \vdash \; A : *$

(c) $\emptyset; \Gamma \; \vdash \; B : *$

(d) $\emptyset; \Gamma \; \vdash \; C : *$

The following derives all the results (a)-(d) in flag-format.

Chapter 9 - Exercise 8

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.

Chapter 9 - Exercise 7

We call a definition $D$ correct in environment Δ if $\Delta,D; \emptyset ⊢ *: \Box$.

Consider $D_1$ to $D_6$ as in Exercise 9.6.

(a) On what condition can you derive that $D_1$ is correct in environment $\emptyset$?

(b) How do you prove that $D_2$ is correct in environment $D_1$?

(c) The same question for $D_3$ in environment $D_1,D_2$.

We remind ourselves of the (def) rule:

$$ \frac{ \Delta ; \Gamma \; \vdash \; K:L \quad \quad  \Delta; \bar{x}:\bar{A} \; \vdash \; M:N }{ \Delta,  \bar{x}:\bar{A} \triangleright a(\bar{x}) := M:N ; \Gamma \; \vdash \; K:L} \quad \text{ if } a \notin \Delta $$

We also 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) Definition $D_1$ is correct in the empty environment $\emptyset$ if $D_1; \emptyset \vdash *: \Box$.

The (def) rule tells us the premises required to derive this.

$$ \frac{ \emptyset; \emptyset \; \vdash \; *:\Box \quad \quad  \emptyset; f : \mathbb{N} \to \mathbb{R}, \; n : \mathbb{N} \; \vdash \; \sum ^n_{i=0}(f i) : \mathbb{R} }{ \emptyset,  D_1 ; \emptyset \; \vdash \; *:\Box} $$

The first premise is simply the (sort) rule. The second premise requires the definition $D_1$ be well typed, that is, the definiens and its type can be derived from the context of the definition.

So the condition is that $D_1$ is well typed in the empty environment.

(b) Definition $D_2$ is correct in environment $D_1$ if $D_1, D_2 ; \emptyset \vdash *:\Box$. 

The (def) rule tells us the premises required to derive this.

$$ \frac{ D_1; \emptyset \; \vdash \; *:\Box \quad \quad  D_1; f : \mathbb{N} \to \mathbb{R},  d : \mathbb{R} \; \vdash \; \forall _{n:\mathbb{N}}(f (n+1)−f n= d) : *_p }{ D_1,  D_2 ; \emptyset \; \vdash \; *:\Box} $$

The first premise is the requirement that $D_1$ is correct in the empty environment, from part(a) above.

The second premise is the requirement that $D_2$ is well-formed in the environment $D_1$.

(c) Definition $D_3$ is correct in environment $D_1, D_2$ if $D_1, D_2, D_3; \emptyset \vdash *:\Box$. 

The (def) rule tells us the premises required to derive this.

$$ \frac{ D_1, D_2; \emptyset \; \vdash \; *:\Box \quad \quad  D_1, D_2; f : \mathbb{N} \to \mathbb{R}, \; d : \mathbb{R}, \; u : a_2(f,d), \; n : \mathbb{N} \; \vdash \; \texttt{formalprf}_3 : f n= f 0 + n \cdot d }{ D_1,  D_2, D_3 ; \emptyset \; \vdash \; *:\Box} $$

The first premise is the requirement that $D_2$ is correct in the environment $D_1$. 

The second premise is the requirement that $D_3$ is well-formed in the environment $D_1, D_2$.

Chapter 9 - Exercise 6

Consider the following environment $\Delta$ consisting of six definitions, in which we use, for the sake of convenience, some well-known formats such as the $\Sigma$ and infix-notations:

$$ \begin{align} D_1 \; &≡ \; f : \mathbb{N} → \mathbb{R}, \; n : \mathbb{N} \quad \triangleright \quad a_1(f,n) := Σ^n_{i=0}(f i) : \mathbb{R} \\ \\ D_2 \; & ≡ \; f : \mathbb{N} →\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} →\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} →\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} →\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} $$

Assume that $\texttt{formalprf}_3$ to $\texttt{formalprf}_6$ are meta-terms, standing for real proof terms.

(a) Rewrite this environment in flag format.

(b) What is a name used for $a_2$ in the standard literature?

(c) Find the δ-normal form with respect to $\Delta$ of $a_5(λx : \mathbb{N}. 2x,2,u,100)$, where $u$ is an inhabitant of $a_2(λx : \mathbb{N}. 2x,2)$.

(a) The following is the environment in flag format.

(b) $a_2$ defines an arithmetic progression, where $d$ is the common difference.

(c) The definition $D_5$ is

$$  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  $$

This means $a_5(λx : \mathbb{N}. 2x,2,u,100)$ is

$$  a_5(λx : \mathbb{N}. 2x,2,u,100) := \texttt{formalprf}_5 : a_1(λx : \mathbb{N}. 2x,100) = (100 + 1) \cdot (λx : \mathbb{N}. 2x) 0+ \frac{1}{2}\cdot 100 \cdot (100 + 1) \cdot 2  $$

Continuing by unfolding $a_1$,

$$  a_5(λx : \mathbb{N}. 2x,2,u,100) := \texttt{formalprf}_5 :  \sum _{i=0}^{100}((λx : \mathbb{N}. 2x)i) = (100 + 1) \cdot (λx : \mathbb{N}. 2x) 0+ \frac{1}{2}\cdot 100 \cdot (100 + 1) \cdot 2  $$

The above is the δ-normal form. 

Out of interest we can continue to simplify,

$$  a_5(λx : \mathbb{N}. 2x,2,u,100) := \texttt{formalprf}_5 : \sum _{i=0}^{100}(2i) = 10100  $$

That is,

$$ \texttt{formalprf}_5 \; : \; \sum _{i=0}^{100}(2i) = 10100 $$

Chapter 9 - Exercise 5

Check that all instantiations of the parameters of constants defined and used in Exercise 8.2 satisfy the requirements imposed by the (inst)-rule.

The following is the text used in Exercise 8.2.

The following summarises the derivation rules for $\lambda D_0$.

The (inst)-rule ensures that the substituted expressions $\bar{U}$ are derivable in the environment and context $\Delta; \Gamma$.

There are only two instantiations in Exercise 8.2, at line (7) and (8). Let's consider each in turn.

(7) In defining $p_7$, the type $\textit{bounded-from-above}(S,p_6)$ has instantiated

• $V$ as $S$
• $u$ and $p_6$

in that order.

The (inst)-rule requires that we can derive $S:*_s$ in $\Delta; \Gamma$. Indeed, line (5) of the environment establishes $S$ with type $*_s$.

Next, the (inst)-rule requires that we can derive $p_6: V \subseteq \mathbb{R}[V:=S]$ which is $p_6:S \subseteq \mathbb{R}$. Line (6) of the environment establishes $p_6$ with type $S \subseteq \mathbb{R}$. 

And so the instantiations of $\textit{bounded-from-above}(S,p_6)$ satisfy the requirements of the (inst)-rule.

(8) In defining $p_8$, the type $\text{least-upper-bound}(S, p_6, 1)$ has instantiated

• $V$ as $S$
• $u$ as $p_6$
• $s$ as 1

in that order.

The (inst)-rule requires that we can derive $S:*_s$ in $\Delta; \Gamma$. Indeed, line (5) of the environment establishes $S$ with type $*_s$.

Next, the (inst)-rule requires that we can derive $p_6: V \subseteq \mathbb{R}[V:=S]$ which is $p_6:S \subseteq \mathbb{R}$. Line (6) of the environment establishes $p_6$ with type $S \subseteq \mathbb{R}$. 

Finally, the (inst)-rule requires that we can derive $1:\mathbb{R}[V:=S, u:=p_6]$  which is simply $1:\mathbb{R}$. Determining the type of 1 as $\mathbb{R}$ requires no further work.

And so the instantiations of $\textit{least-upper-bound}(S,p_6,1)$ satisfy the requirements of the (inst)-rule.

Chapter 9 - Exercise 4

This question has been updated by the errata.

See Section 9.6. Add the following definition to $(D_1) \ldots  (D4)$:

$$ (D_5) \quad x: \mathbb{Z}, y: \mathbb{Z} \triangleright d(x,y) := (x+ y)^2 $$

Let $\Delta  ≡D_1, \ldots ,D_5$. Give the full δ-reduction diagram of $d(a(u,v),b(w,w))$.

The following diagram illustrates the δ-reduction of $d(a(u,v),b(w,w))$.

(click to enlarge)

The final result is

$$ d(a(u,v), b(w,w)) \; \triangleq \; (u^2 + v^2 + 2 w^2)^2 $$