nested-recursion == recursion with accumulator for all arguments

NumTest.agda

-- The trick for proving that nested-recursion == recursion with accumulator for all arguments (in Agda).
-- Example for Nat. Should be generalizable.

module NumTest where

import Level

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

≡-sym : ∀ {α} {τ : Set α} {a b : τ} → a ≡ b → b ≡ a
≡-sym refl = refl

_~_ : ∀ {α} {τ : Set α} {a b c : τ} → a ≡ b → b ≡ c → a ≡ b
refl ~ refl = refl

_~1_ : ∀ {α} {τ : Set α} {a b b' : τ} → b ≡ a → b ≡ b' → b' ≡ a
refl ~1 refl = refl

_~2_ : ∀ {α} {τ : Set α} {a b b' : τ} → a ≡ b → b ≡ b' → a ≡ b'
refl ~2 refl = refl

cong : ∀ {α β} {A : Set α} {B : Set β} (f : A → B) {x y} → x ≡ y → f x ≡ f y
cong f refl = refl

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

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

_x_ : ℕ → ℕ → ℕ
zero x m = m
(succ n) x m = n x (succ m)

infix 10 _≡_
infix 20 _+_
infix 20 _x_

one = succ zero

temp : ∀ n m → n x succ m ≡ succ (n x m)
temp zero m = refl
temp (succ n) m = temp n (succ m) ~1 refl

samee : ∀ n m → (n + m) ≡ (n x m)
samee zero m = refl
samee (succ n) m = cong succ (samee n m) ~2 ≡-sym (temp n m)