module Sets.Recursive where open import Sets.Enumerated using (Bool; true; false)

The effect of this `open import`

declaration is the same as if we copied the definition of `Bool`

type here. Note that we enumerated the constructors of `Bool`

too.

More about import declarations come later.

We are looking for a representation natural numbers. The simplest choice is the *Peano representation* which corresponds to the unary numeral system:

term | interpretation in decimal form |
---|---|

`zero` |
0 |

`suc zero` |
1 |

`suc (suc zero)` |
2 |

`suc (suc (suc zero))` |
3 |

... | ... |

`ℕ`

In Agda the definition

data ℕ : Set where zero : ℕ suc : ℕ → ℕ

yields the infinite set of judgements

```
ℕ : Set
zero : ℕ
suc zero : ℕ
suc (suc zero) : ℕ
suc (suc (suc zero)) : ℕ
...
```

With the Emacs command C-`c`

C-`d`

one can get Agda to type-check a given expression (`d`

stands for 'deduce').

Example: Hit C-`c`

C-`d`

and enter `suc (suc zero)`

.

Exercise: Try to type-check the following expressions:

`suc zero`

`suc (zero)`

`(suc) zero`

`zero suc`

`(suc suc) zero`

`suc`

`ℕ`

data ℕ⁺ : Set where one : ℕ⁺ double : ℕ⁺ → ℕ⁺ double+1 : ℕ⁺ → ℕ⁺

yields (without ordering)

```
ℕ⁺ : Set
one : ℕ⁺
double one : ℕ⁺
double+1 one : ℕ⁺
double (double one) : ℕ⁺
double+1 (double one) : ℕ⁺
double (double+1 one) : ℕ⁺
double+1 (double+1 one) : ℕ⁺
double (double (double one)) : ℕ⁺
...
```

And

data ℕ₂ : Set where zero : ℕ₂ id : ℕ⁺ → ℕ₂

yields

```
ℕ₂ : Set
zero : ℕ₂
id one : ℕ₂
id (double one) : ℕ₂
id (double+1 one) : ℕ₂
id (double (double one)) : ℕ₂
id (double+1 (double one)) : ℕ₂
...
```

Soon we will prove in Agda that `ℕ`

and `ℕ₂`

are isomorphic with the following relation:

ℕ |
ℕ₂ |
---|---|

`zero` |
`zero` |

`suc zero` |
`id one` |

`suc (suc zero)` |
`id (double one)` |

`suc (suc (suc zero))` |
`id (double+1 one)` |

... | ... |

*Exercise:* How 9 is represented in `ℕ₂`

? Type-check the expression!

*Question*: why didn't we use one `data`

definition with 4 constructors `zero`

, `one`

, `double`

, `double+1`

?

Each representation has its merit.

*Exercise:* Guess which representation (`ℕ`

or `ℕ₂`

) is better for the following tasks!

- Computing
`n * 2`

. - Computing
`⌊n / 2⌋`

. - Deciding whether the number is odd.
- Computing
`n + m`

. - Computing
`n * m`

. - Proving that
`n + m`

=`m + n`

for all`m`

and`n`

. - Storing the number.

A good strategy is to choose the right representation for each task and convert values between different representations.

- Define
`ℤ`

!

(Several solutions are possible.)

data BinTree : Set where leaf : BinTree node : BinTree → BinTree → BinTree

yields

```
BinTree : Set
leaf : BinTree
node leaf leaf : BinTree
node (node leaf leaf) leaf : BinTree
node leaf (node leaf leaf) : BinTree
node (node leaf leaf) (node leaf leaf) : BinTree
...
```

`BinTree`

elements are good for representing binary trees (just the shapes without data).

*Exercise:* define binary trees according to the following shapes!

- Define binary trees
- with natural number data attached to the leafs
- with natural number data attached to the nodes
- with Booleans in the nodes and natural numbers in the leafs

- Define the lists (finite sequences) of natural numbers.
- Define the non-empty lists of natural numbers.