Imports


module Functions.Large where

open import Data.Nat using (ℕ; zero; suc)
open import Data.Empty using (⊥)
open import Data.Unit using (⊤; tt)
open import Data.Sum using (_⊎_; inj₁; inj₂)

Introduction

Function definitions give another possibility to define sets.
We give general design rules on which language construct to use.

Inductive _≤_ definition

The inductive definition of _≤_:


data  _≤_ : ℕ → ℕ → Set where
  z≤n : {n : ℕ} →               zero  ≤ n
  s≤s : {m n : ℕ} →   m ≤ n  →  suc m ≤ suc n

which yields the statements

z≤n : 0 ≤ 0
z≤n : 0 ≤ 1
z≤n : 0 ≤ 2
...
s≤s z≤n : 1 ≤ 1
s≤s z≤n : 1 ≤ 2
s≤s z≤n : 1 ≤ 3
...
s≤s (s≤s z≤n) : 2 ≤ 2
s≤s (s≤s z≤n) : 2 ≤ 3
s≤s (s≤s z≤n) : 2 ≤ 4
...
...

Recursive _≤_ definition

The recursive definition of less-than-or-equal:


_≤′_ : ℕ → ℕ → Set
zero  ≤′ n     = ⊤
suc m ≤′ zero  = ⊥
suc m ≤′ suc n = m ≤′ n

which yields the statements

tt : 0 ≤′ 0
tt : 0 ≤′ 1
tt : 0 ≤′ 2
...
tt : 1 ≤′ 1
tt : 1 ≤′ 2
tt : 1 ≤′ 3
...
tt : 2 ≤′ 2
tt : 2 ≤′ 3
tt : 2 ≤′ 4
...
...

Inductive vs. recursive definitions

_≤_ and _≤′_ have the same type and define exactly the same relations. But:

Inductive definitions are better than recursive definitions with pattern matching.

Explanation

Suppose in a function definition we have n : ℕ, m : ℕ.

Example (we discuss dependent functions like this later):


f : {n m : ℕ} → n ≤ m → n ≤ suc m
f z≤n = z≤n
f (s≤s x) = s≤s (f x)

f′ : {n m : ℕ} → n ≤′ m → n ≤′ suc m
f′ {zero} {m} tt = tt
f′ {suc n} {zero} ()
f′ {suc n} {suc m} x = f′ {n} {m} x

Exercises

Give recursive definitions for _≡_ and _≢_ on natural numbers!

Give mutual recursive definitions for Even and Odd!

Macro-like Set definitions

Macro-like functions don't pattern match on their argument:


_<_ : ℕ → ℕ → Set
n < m = suc n ≤ m

Although we could have an inductive definition of _<_, this definition is better because no conversion functions are needed between _≤_ and _<_.

On the other hand,


Maybe : Set → Set
Maybe A = ⊤ ⊎ A

is possible, but not advised because then we can't distinguish Maybe ⊤ from ⊤ ⊎ ⊤, for example.

General rule:
Macro-like Set definitions are better than inductive definitions if we don't want to distinguish the new type from the base type.

Exercises

Define _>_ and _≥_ on top of _≤_!

Another example


¬ : Set → Set
¬ A = A → ⊥

Another example: recursive Fin

Fin₀ n is isomorphic to Fin n for all n:


Fin₀ : ℕ → Set
Fin₀ zero    = ⊥
Fin₀ (suc n) = ⊤ ⊎ Fin₀ n

Elements:

n    Fin₀ n                             Fin n
------------------------------------------------------------------
0    {                              }   {                      }
1    { inj₁ tt                      }   { zero                 }
2    { inj₁ tt                          { zero
     , inj₂ (inj₁ tt)               }   , suc zero             }
3    { inj₁ tt                          { zero
     , inj₂ (inj₁ tt)                   , suc zero
     , inj₂ (inj₂ (inj₁ tt)         }   , suc (suc zero)       }
4    { inj₁ tt                          { zero
     , inj₂ (inj₁ tt)                   , suc zero
     , inj₂ (inj₂ (inj₁ tt))            , suc (suc zero)
     , inj₂ (inj₂ (inj₂ (inj₁ tt))) }   , suc (suc (suc zero)) }
...

Pattern: