{-# 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