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!