data _≡_ {A : Set} : A → A → Set where
  refl : {a : A} → a ≡ a

context : {A B : Set} → {a b : A} → (f : A → B) → a ≡ b → f a ≡ f b
context f refl = refl

trans : {A : Set} → {a b c : A} → a ≡ b → b ≡ c → a ≡ c
trans refl refl = refl

data ⊥ : Set where

¬ : Set → Set
¬ A = A → ⊥

_≢_ : {A : Set} → A -> A -> Set
_≢_  a b = ¬ (a ≡ b)

data _∧_ (A B : Set) : Set where
  _∧ᵢ_ : A → B → A ∧ B

infixr 19 _∧_ 
infixr 19 _∧ᵢ_ 

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ
{-# BUILTIN NATURAL ℕ #-}

_+_ : ℕ → ℕ → ℕ
n + 0 = n
n + succ m = succ (n + m)

data _<_ : ℕ → ℕ → Set where
  z<sn : (n : ℕ) → 0 < succ n
  s<s : (n m : ℕ) → n < m → succ n < succ m

data _≤_ : ℕ → ℕ → Set where
  z≤n : ∀ (n : ℕ) -> 0 ≤ n
  s≤s : ∀ (n m : ℕ) -> n ≤ m -> succ n ≤ succ m

-- Task 2
data ℤ : Set where
  pos : ℕ → ℤ
  negsucc : ℕ → ℤ -- -n - 1 alternatively - (n + 1)

recN : {A : Set} → ℕ → A → (ℕ → A → A) → A
recN 0     d e = d
recN (succ x) d e = e x (recN x d e)

addℕ : ℕ → ℕ → ℕ
addℕ n m = recN m n (λ _ x → succ x)

prfadd : (n m : ℕ) → (n + m) ≡ (addℕ n m)
prfadd n 0 = refl
prfadd n (succ m) = context succ (prfadd n m)

-- Task 3
zrec : {A : Set} → ℤ → (ℕ → A) → (ℕ → A) → A
zrec (pos     n) f _ = f n
zrec (negsucc n) _ g = g n

addOne : ℤ → ℤ
addOne a = zrec a (λ x → pos (succ x)) (λ x → recN x (pos x) (λ n _ → negsucc n))

subOne : ℤ → ℤ
subOne a = zrec a (λ x → recN x (negsucc x) (λ n _ → pos n)) (λ x → negsucc (succ x))

prfℤ₁ : (z : ℤ) → subOne (addOne z) ≡ z
prfℤ₁ (pos x) = refl
prfℤ₁ (negsucc 0) = refl
prfℤ₁ (negsucc (succ x)) = refl

prfℤ₂ : (z : ℤ) → addOne (subOne z) ≡ z
prfℤ₂ (pos 0) = refl
prfℤ₂ (pos (succ x)) = refl
prfℤ₂ (negsucc x) = refl

-- Task 4

data Vec (A : Set) : ℕ → Set where
  nil : Vec A 0
  _,_ : {n : ℕ} → Vec A n → (a : A) → Vec A (succ n)

infixl 20 _,_

index : {A : Set} {n : ℕ} → Vec A n → (i : ℕ) → (0 ≤ i ∧ i < n) → A
index (xs , a) 0 (z≤n n ∧ᵢ z<sn n₁) = a
index (xs , a) (succ i) (z≤n n ∧ᵢ s<s i m i<m) = index xs i (z≤n i ∧ᵢ i<m)
  
data PRF : ℕ → Set where
  zero : PRF 0
  succ : PRF 1
  proj : {n : ℕ}   → (i : ℕ)     → 0 ≤ i ∧ i < n        → PRF n
  comp : {n m : ℕ} → (f : PRF m) → (gs : Vec (PRF n) m) → PRF n
  rec  : {n : ℕ}   → (f : PRF n) → (g : PRF (succ (succ n))) → PRF (succ n)

⟦_⟧ : {n : ℕ} → PRF n → (Vec ℕ n) → ℕ
⟦ zero ⟧        nil         = 0
⟦ succ ⟧       (nil , n)    = succ n
⟦ proj i prf ⟧  ρ           = index ρ i prf
⟦ rec f g ⟧    (ρ , 0)      = ⟦ f ⟧ ρ
⟦ rec f g ⟧    (ρ , succ n) = ⟦ g ⟧ ((ρ , n , ⟦ rec f g ⟧ (ρ , n)))
⟦ comp f gs ⟧   ρ           = ⟦ f ⟧ (⟦ gs ⟧* ρ)
  where
    ⟦_⟧* : {n m : ℕ} → Vec (PRF m) n → (Vec ℕ m) → Vec ℕ n
    ⟦ nil ⟧*    ρ = nil
    ⟦ fs , f ⟧* ρ =  (⟦ fs ⟧* ρ , ⟦ f ⟧ ρ)


addProg : PRF 2
addProg =
  rec
    (proj 0 (z≤n 0 ∧ᵢ z<sn 0))
    (comp succ (nil , proj 0 (z≤n 0 ∧ᵢ z<sn 2)))

add : ℕ → ℕ → ℕ
add n m = ⟦ addProg ⟧ (nil , n , m)

prfProg : (n m : ℕ) → (add n m) ≡ (n + m)
prfProg n 0 = refl
prfProg n (succ m) = context succ (prfProg n m)

prfProg2 : (n m : ℕ) → (add n m) ≡ (addℕ n m)
prfProg2 n m = trans (prfProg n m) (prfadd n m)