Eliminator

{-# OPTIONS --safe --without-K #-}
module ag-000K where

open import MLTT.Spartan
open import Naturals.Properties

Eliminator of ℕ

ℕ-elim : ∀ (P : ℕ → 𝓤 ̇) → P 0 → (∀ (n : ℕ) → P n → P (succ n)) → (∀ (n : ℕ) → P n)
ℕ-elim P P0 Ps zero = P0
ℕ-elim P P0 Ps (succ n) = Ps n (ℕ-elim P P0 Ps n)

Define with pattern matching

plus : ℕ → ℕ → ℕ
plus zero b = b
plus (succ a) b = succ (plus a b)

mul : ℕ → ℕ → ℕ
mul zero c = zero
mul (succ a) b = plus b (mul a b)

exp : ℕ → ℕ → ℕ
exp x zero = 1
exp x (succ k) = mul x (exp x k)

Now use the eliminator to define them

plus' : ℕ → ℕ → ℕ
plus' x = ℕ-elim (λ _ → ℕ → ℕ) (λ z → z) (λ x' plus-x' → λ y → succ (plus-x' y)) x

t5 : plus' 1 1 ＝ 2
t5 = refl

p1 : (a b : ℕ) → plus a b ＝ plus' a b
p1 zero b = refl
p1 (succ a) b =
  succ (plus a b)  ＝⟨ ap succ (p1 a b) ⟩
  succ (plus' a b) ＝⟨by-definition⟩
  succ (ℕ-elim (λ _ → ℕ → ℕ) (λ z → z) (λ x' plus-x' → λ y → succ (plus-x' y)) a b)
    ＝⟨by-definition⟩
  plus' (succ a) b ∎

mul' : ℕ → ℕ → ℕ
mul' x = ℕ-elim (λ _ → ℕ → ℕ) (λ z → zero) (λ x' mul-x' → λ y → plus' y (mul-x' y)) x

t7 : mul' 0 1 ＝ 0
t7 = refl
t8 : mul' 1 1 ＝ 1
t8 = refl
t9 : mul' 2 2 ＝ 4
t9 = refl

p2 : (a b : ℕ) → mul a b ＝ mul' a b
p2 zero b = refl
p2 (succ a) zero = p2 a 0
p2 (succ a) (succ b) =
  plus (succ b) (mul a (succ b))   ＝⟨ p1 (succ b) (mul a (succ b)) ⟩
  plus' (succ b) (mul a (succ b))  ＝⟨ ap (plus' (succ b)) (p2 a (succ b)) ⟩
  plus' (succ b) (mul' a (succ b)) ＝⟨by-definition⟩
  mul' (succ a) (succ b) ∎

exp' : ℕ → ℕ → ℕ
exp' x y = ℕ-elim (λ _ → ℕ → ℕ) (λ x → 1) (λ y' exp-y' → λ x → mul' x (exp-y' x)) y x

t10 : exp' 2 0 ＝ 1
t10 = refl
t11 : exp' 2 10 ＝ 1024
t11 = refl

p3 : (a b : ℕ) → exp a b ＝ exp' a b
p3 a zero = refl
p3 zero (succ b) = refl
p3 (succ a) (succ b) =
  exp (succ a) (succ b)           ＝⟨by-definition⟩
  mul (succ a) (exp (succ a) b)   ＝⟨ p2 (succ a) (exp (succ a) b) ⟩
  mul' (succ a) (exp (succ a) b)  ＝⟨ ap (mul' (succ a)) (p3 (succ a) b) ⟩
  mul' (succ a) (exp' (succ a) b) ＝⟨by-definition⟩
  exp' (succ a) (succ b) ∎

Plus commutative yoga

C : commutative plus
C zero zero = refl
C zero (succ b) =
  succ b ＝⟨ ap succ (C 0 b) ⟩
  succ (plus b zero) ∎
C (succ a) zero =
  succ (plus a 0) ＝⟨ ap succ (C a 0) ⟩
  succ (plus 0 a) ＝⟨ refl ⟩
  plus 0 (succ a) ∎
C (succ a) (succ b) =
  succ (plus a (succ b)) ＝⟨ ap succ (C a (succ b)) ⟩
  succ (plus (succ b) a) ＝⟨ ap succ refl ⟩
  succ (succ (plus b a)) ＝⟨ ap (λ x → succ (succ x)) (C b a) ⟩
  succ (succ (plus a b)) ＝⟨ ap succ refl ⟩
  succ (plus (succ a) b) ＝⟨ ap succ (C (succ a) b) ⟩
  succ (plus b (succ a)) ∎

Remind

add1 : ℕ → ℕ
add1 = ℕ-elim (λ _ → ℕ) (succ zero) λ _ n → succ n

t1 : add1 0 ＝ 1
t1 = refl

double' : ℕ → ℕ
double' = ℕ-elim (λ _ → ℕ) zero λ _ mn → succ (succ mn)

t2 : double' 0 ＝ 0
t2 = refl
t3 : double' 1 ＝ 2
t3 = refl
t4 : double' 2 ＝ 4
t4 = refl

Eliminator [ag-000K]

Remind