Inductive Definitions

Exercises of PFPL, 2nd Edition


# 2.1

Definition of judgment $max(m;n;p)$

```math

\frac {a = b nat} { a \geq b nat } . Rule 1\\
\frac { a \geq b nat } { succ(a) \geq b nat } . Rule 2\\
\frac { a \geq b nat } { max(a;b;a) } . Rule 3\\
\frac { b \geq a nat } { max(a;b;b) } . Rule 4


```

Proof of  mode $ (\forall, \forall, \exists) $

1. For $ \forall a \space nat, \forall b \space nat $, either $ a \geq b $ or $ b \geq a $

Proof:

Some easy to prove Theorem:


1. $ \forall b \space nat , b \geq zero $. - Theorem 1
2. $ \forall a \space nat, b \space nat, if a \geq b, then succ(a) \geq b $. -Theorem 2


If a nat and b nat, then there exists c nat such that max(a;b;c)
Define P1(a nat) as for $\forall b \space nat $ , either $ a \geq b $ or $ b \geq a $

- P1(zero nat) since easy to prove that $ \forall b, b \geq zero $. 
- Suppose P(a nat). We need to prove P1(succ(a) nat).
    - If $ a \geq b$ , then $ succ(a) \geq b $ according to Rule 2
    - If $ b \geq a $
        - If $ b = a $, then $ succ(a) \geq b $ according to Rule 2
        - Otherwise, according to necessity, we have $ b' \geq a, succ(b') = b$. Easy to prove that, $ if a \geq b, then succ(a) \geq b $. So we have $ succ(b') \geq succ(a) $. Or $ b \geq succ(a) $.
        

According to P1(a nat), we have
- If $ a \geq b $, then max(a;b;c) with c = a, exist and unique
- If $ b \geq a $, then max(a;b;c) with c = b, exist and unique



# 2.2

## Existence

- hgt(empty; zero) by Rule (2.11 a). So exist height zero for empty tree
- Suppose hgt(t1; n1), hgt(t2; n2). Then for tree node(t1; t2), exist succ(n) with max(n1;n2;n) according to Rule (2.11 b)


## Uniqueness

- hgt(empty; zero). So for empty tree, height is unique (always zero)
- Suppose tree t3 being node(t1; t2), hgt(t1; n1), hgt(t2; n2) and n1, n2 is unique. max(n1;n2;n). According to necessity of Rule 2.11b, if hgt(t3; n3), with succ(n') = n3, then max(n1;n2;n'). max is unique, so n = n' nat. Therefore, n3 = succ(n) nat. And the height is unique.


# 2.3

```math
\frac {}{Empty \space Tree} \\
\frac {b \space Forest} { node(b) \space Tree} \\
\frac {}{Empty \space Forest} \\
\frac {a \space Tree, b \space Forest}{ cons(a; b) \space Forest}
```


# 2.4
$ hgt_t $ is the height of tree. $ hgt_f $ is the height of forest

```math

\frac {} {hgt_t(Empty \space Tree; zero) } \\
\frac {hgt_f(f \space Forest; n) } {succ(hgt_t(node(f) \space Tree))} \\

\frac {} {hgt_f(Empty \space Forest; zero)} \\
\frac {hgt_t(t \space Tree; n1), hgt_f(f \space Forest; n2), max(n1,n2,n)} {hgt_f(cons(t;f) \space Forest) ; succ(n)}

```

The proof of existence and uniqueness is simple and almost the same as previous questions.

# 2.5

bnat : binary natural number

```math


\frac {} {zero \space bnat} \\
\frac {a \space bnat } {twice(a) \space bnat } \\
\frac {a \space bnat } {twicePlusOne(a) \space bnat }


```

What does "the size of the representation is logarithmic, rather than linear, in the natural number it represents"



# 2.6



```math

\frac {} {succ(zero; twicePlusOne(zero)} \\
\frac {twice(a;b)} {succ(b; twicePlusOne(a)} \\
\frac {twicePlusOne(a;b)} {succ(b; twice(succ(a))} \\

\frac {} {sum(zero; b; b) } \\
\frac {sum(a;b;c)} {sum(a;succ(b); succ(c)}

```