Problem 3 - Structural Induction

Let us define a set $\boldsymbol{L}$ of terms inductively as follows ( $\mathbb{N}$ is the set of natural numbers):

$$nil \in \boldsymbol{L},$$

$$\forall L \in \boldsymbol{L}. \forall N \in \mathbb{N}.(cons(N,L) \in \boldsymbol{L}).$$

Answer the following questions.

1.

Prove that there is exactly one total function $app \in \boldsymbol{L}\times \boldsymbol{L} \rightarrow \boldsymbol{L}$ that satisfies the following equations:

$$\forall L \in \boldsymbol{L}.(app(nil,L) = L),$$

$$\forall L_1, L_2 \in \boldsymbol{L}. \forall N \in \mathbb{N}.(app(cons(N,L_1),L_2) = cons(N, app(L_1, L_2))).$$

2.

Prove that the above function $app$ satisfies

$$\forall L_1, L_2, L_3 \in \boldsymbol{L}.(app(L_1,app(L_2,L_3))=app(app(L_1, L_2), L_3)).$$

1.

Let us suppose that we have two applications $app_1$ and $app_2$ described as above. We want to show that $\forall L_1,L_2 \in \boldsymbol{L}, app_1(L_1) = app_2(L_2)$

• If $L_1 = L_2 = nil$, then $app_1(L_1,L_2)=app_1(nil,nil) = nil$ and $app_2(L_1,L_2)=app_2(nil,nil) = nil$. Thus $app_1(L_1,L_2) = app_2(L_1,L_2)$.
• If $L_1=nil$ and $L_2\neq nil$, then $app_1(L_1,L_2) = L_2$ and $app_2(L_1,L_2) = L_2$. Thus $app_1(L_1,L_2) = app_2(L_1,L_2)$.
• If $L_1\neq nil$ and $L_2$ is either $nil$ or not. We first suppose that $lgh(L_1)=1$. Then $app_1(L_1,L_2) = cons(N_1,app_1(nil,L_2)) = cons(N_1,app_2(nil,L_2)) = app_2(L_1,L_2)$ as seen above. Let us suppose that this is true for $lgh(L_1)=k$. Then, let's choose $L_1$ so that $lgh(L_1)=k+1$. Then we have $app_1(L_1,L_2) = cons(N_{k+1}, app_1(L_1^{k},L_2))$. By the inductive hypothesis, we have $app_1(L_1^k,L_2) = app_2(L_1^k,L_2)$. Then, it means that $app_1(L_1,L_2) = cons(N_{k+1}, app_1(L_1^{k},L_2))= cons(N_{k+1}, app_2(L_1^k,L_2)) = app_2(L_1,L_2)$. Therefore the property is proven for all the kinds of couple $L_1,L_2$ that can occur.

2.

We shall prove the property inductively on the length of $L_1$. Let us first suppose that $L_1=nil$. Then, we have:
$app(nil, app(L_2,L_3)) = app(L_2,L_3)$ (according to the definition of $app$)
$app(app(nil,L_2), L_3) = app(L_2,L_3)$ (since $app(nil,L_2)=L_2$)
Thus, the property is true for $lgh(L_1) = 0$. Let us now suppose that the property is also true for $lgh(L_1)=k$. Does it hold for $lgh(L_1)=k+1$?
$app(L_1, app(L_2, L_3))$
$=app(cons(N_1',L_1'),app(L_2,L_3))$ with $L_1 = N_1'L_1'$
$=cons(N_1',app(L_1',app(L_2,L_3)))$ by the definition of $app$
$=cons(N_1',app(app(L_1',L_2),L_3))$ by the inductive hypothesis
$=app(cons(N_1',app(L_1',L_2)),L_3)$ by the definition of $app$
$=app(app(cons(N_1',L_1'),L_2),L_3)$ by the definition of $app$
$=app(app(L_1,L_2),L_3)$ by the definition of $cons$
We have shown the proof by induction.