{-# OPTIONS --guardedness #-}
{-

Exercises for Type Theory at MGS 2023

Tuesday

-}

{-
Important commands
C-c C-l : load / reload
C-C C-n : evaluate term
C-c C-x C-r : kill kill kill

In shed:
C-c C-c : (co-)pattern match
C-c SPC : give
C-C C-r : refine
C-c C-, : current context and type
C-c C-. : current context, type and term so far.
-}
open import tue-lib


{- Part 1 : Recursion via patterns

Define the following functions using pattern matching and structural
recursion on the natural numbers.  -}

-- Define a function even that determines wether its input is even.

! : Bool → Bool
! false = true
! true = false

even :  ℕ → Bool
even zero = true
even (suc x) = ! (even x)

-- tests:
-- even 3 = false
-- even 6 = true

-- Define a function sum that sums the numbers from 0 unil n-1
sum : ℕ → ℕ
sum = {!!}

-- tests
-- sum 2 = 1
-- sum 10 = 45

-- Define a function max that calculates the maximum of 2 numbers
max : ℕ → ℕ → ℕ
max zero n = n
max (suc m) zero = suc m
max (suc m) (suc n) = suc (max m n)

-- tests
-- max 2 3 = 3
-- max 10 1 = 10

-- Define a function fib which calculates the nth item of the
-- Fibonacci sequence: 1,1,2,3,5,8,13
-- (each number is the sum of the two previous ones).
fib : ℕ → ℕ
fib = {!!}

-- tests
-- fib 0 = 1
-- fib 6 = 13

-- Define a function eq that determines wether two numbers
-- are equal.
eq : ℕ → ℕ → Bool
eq = {!!}

-- tests
-- eq 4 3 = false
-- eq 6 6 = true

-- Define a function rem such that rem m n returns the remainder
-- when dividing m by suc n (this way we avoid division by 0).
rem : ℕ → ℕ → ℕ 
rem = {!!}

-- tests
-- rem 5 1 = 1
-- rem 11 2 = 2

-- Define a function div such that div m n returns the result
-- of dividing m by suc n (ignoring the remainder)
div : ℕ → ℕ → ℕ
div = {!!}
-- tests
-- div 5 1 = 2
-- div 11 2 = 3

{- Part 2 : Iterator and recursor

Define all the functions of part 1 but this time only use the 
iterator Itℕ and/or the recursor Rℕ.

Naming convention if the function in part 1 is called f then call it 
f-i if you only use the iterator, but f-r if you use the recusor (and possibly the iterator. 

Test the functions with at least the same test cases.
  -}

{-
f : ℕ → M

f 0 = z
f (suc n) = s (f n)

-}
Itℕ : {M : Set} → M → (M → M) → ℕ → M
Itℕ z s zero = z
Itℕ z s (suc n) = s (Itℕ z s n)

{-
g : ℕ → M

g 0 = z
g (suc n) = s n (g n)

-}

-- reduce Rℕ to Itℕ

Rℕ : {M : Set} → M → (ℕ → M → M) → ℕ → M
Rℕ z s zero = z
Rℕ z s (suc n) = s n (Rℕ z s n)

{-
even :  ℕ → Bool
even zero = true
even (suc x) = ! (even x)
-}
even-i :  ℕ → Bool
even-i = Itℕ true (λ even-x → ! even-x)

{-
max : ℕ → ℕ → ℕ
max zero n = n
max (suc m) zero = suc m
max (suc m) (suc n) = suc (max m n)
-}

max-i : ℕ → ℕ → ℕ
max-i = Rℕ (λ n → n) λ m max-m →
      Rℕ (suc m) λ n _ → suc (max-m n)



{- Part 3 

Conatural numbers. 

-}

{- We defined 

_+∞_ : ℕ∞ → ℕ∞ → ℕ∞
pred∞ (m +∞ n) with pred∞ m
... | nothing = pred∞ n
... | just m' = just (m' +∞ n)
-}

{- Here is some test kit -}

-- map natural numbers to conatural numbers
ℕ→ℕ∞ : ℕ → ℕ∞
ℕ→ℕ∞ zero = zero∞
ℕ→ℕ∞ (suc n) = suc∞ (ℕ→ℕ∞ n)

-- map conatural numbers to natural numbers
-- ℕ∞→ℕ b n : b is the bound, if n>b then the result is nothing
-- in particular ∞ is always mapped to nothing
ℕ∞→ℕ : ℕ → ℕ∞ → Maybe ℕ
ℕ∞→ℕ zero x = nothing
ℕ∞→ℕ (suc b) x with pred∞ x
... | nothing = just zero
... | just x' with ℕ∞→ℕ b x'
...            | just y = just (suc y)
...            | nothing = nothing

-- example
x2+3 = ℕ∞→ℕ 10 ((ℕ→ℕ∞ 2) +∞ (ℕ→ℕ∞ 3))
x∞+3 = ℕ∞→ℕ 100 (∞ +∞ (ℕ→ℕ∞ 3))
-- C-c C-n x2+3
-- C-c C-n x∞+3

{-
_*_ : ℕ → ℕ → ℕ
zero * n = zero
suc m * n = n + (m * n)
-}

--{-# TERMINATING #-}
_*∞_ :  ℕ∞ → ℕ∞ → ℕ∞
pred∞ (m *∞ n) with pred∞ m
... | nothing = nothing
... | just m' with pred∞ n
...           | nothing = nothing
...           | just n' = just (n' +∞ (m' *∞ n))

{- My unit-test -}
x3*5 = ℕ∞→ℕ 100 (ℕ→ℕ∞ 3 *∞ ℕ→ℕ∞ 5)
x∞*5 = ℕ∞→ℕ 100 (∞ *∞ ℕ→ℕ∞ 5)
x3*∞ = ℕ∞→ℕ 100 (ℕ→ℕ∞ 3 *∞ ∞)
{- 15 -}

Co-Itℕ∞ : (M → Maybe M) → M → ℕ∞
pred∞ (Co-Itℕ∞ f m) with f m
... | nothing = nothing
... | just x = just (Co-Itℕ∞ f x)

Co-Rℕ∞ : (M → ℕ∞ ⊎ Maybe M) → M → ℕ∞
pred∞ (Co-Rℕ∞ f x) with f x
... | inj₁ n = pred∞ n
... | inj₂ nothing = nothing
... | inj₂ (just x) = just (Co-Rℕ∞ f x)