```
module Functions.Recursive where```

# Import list

```
open import Data.Bool using (Bool; true; false)
open import Data.Nat using (ℕ; suc; zero)```

Functions can be recursive as well, which is essential for working on sets that were defined recursively. In this case, a common approach is to define an alternative for each of the constructors and when the constructor is recursive then the function itself shall also be probably recursive.

# `_+_`: Addition

Consider the previous definition of the `ℕ` type, where we had the following constructors with the following types:

`zero : ℕ`
`suc : ℕ → ℕ`

Note that this was done along the lines of the mathematical definition of the Peano arithmetic. Consider also the definion of how to calculate the sum of two natural numbers with this representation:

$\begin{array}{ccc}\hfill 0+n& \hfill =\hfill & n\hfill \\ \hfill \left(1+m\right)+n& \hfill =\hfill & 1+\left(m+n\right)\hfill \end{array}$

Now consider the same definition in Agda:

```
_+_ : ℕ → ℕ → ℕ
zero  + n = n
suc m + n = suc (m + n)

infixl 6 _+_```

## Exercises

Define the following functions:

``````pred  : ℕ → ℕ      -- predecessor (pred 0 = 0)

infixl 6 _∸_
_∸_   : ℕ → ℕ → ℕ  -- subtraction (0 ∸ n = n)

infixl 7 _*_
_*_   : ℕ → ℕ → ℕ  -- multiplication

infixl 6 _⊔_
_⊔_   : ℕ → ℕ → ℕ  -- maximum

infixl 7 _⊓_
_⊓_   : ℕ → ℕ → ℕ  -- minimum

⌊_/2⌋ : ℕ → ℕ      -- half (⌊ 1 /2⌋ = 0)

odd   : ℕ → Bool   -- is odd

even  : ℕ → Bool   -- is even``````

# Mutual definitions

It is possible to define functions mutually, like we did for sets. As an example, consider the mutual definition of the `even` and `odd` functions:

``````odd : ℕ → Bool

even : ℕ → Bool
even zero    = true
even (suc n) = odd n

odd zero    = false
odd (suc n) = even n``````

## Exercises

Define the following functions mutually:

```
_≡?_  : ℕ → ℕ → Bool  -- is equal
_≤?_  : ℕ → ℕ → Bool  -- is less than or equal```

# Binary representation of `ℕ`

Import the binary representation of natural numbers:

```
open import Sets.Recursive using (ℕ⁺; one; double; double+1; ℕ₂; zero; id)```

## Exercise

Define a conversion function of the following type:

```
from : ℕ₂ → ℕ  -- hint: use _*_```

Note that the `from` function shall define a reverse function of the following isomorphism between `ℕ` and `ℕ₂` (later we will prove that `from` is an isomorphism):

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

Later we will see how to define the same conversion in the other direction.

## Exercises

Define `ℤ` and some operations on it (such as `_+_`, `_-_`, `_*_`).

# Binary trees

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

## Exercise

Define (recursive) mirroring of binary trees, that is a function with the following type:

`mirror : BinTree → BinTree`