module Functions.Recursive where

Import List


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

_+_: Addition

Definition of addition:


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

infixl 6 _+_

Exercises: pred, _*_, _⊔_, _⊓_ and ⌊_/2⌋

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)

Exercises: even, odd


odd   : ℕ → Bool   -- is odd


even  : ℕ → Bool   -- is even

Mutual definitions

Define even and odd mutually with the mutual keyword!

Exercises: _≡?_, _≤?_


_≡?_  : ℕ → ℕ → 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 the conversion function:


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

from should define the backward function of the following isomorphism between ℕ and ℕ₂ (we prove that from is an isomorphism later):

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

We will see how to define the conversion to the other direction later.

Exercises

Define ℤ and some operations on it (_+_, _-_, _*_)!

Binary trees


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

Exercise: define (recursive) mirroring of binary trees!