The definition of Ackermann function by double primitive recursion

Ackermann.agda

module Ackermann where

  open import Data.Nat
  open import Relation.Binary.PropositionalEquality

  -- Primitive recursion a la System T, for defining maps ℕ → τ for any type τ.
  primrec : ∀ {τ : Set} → τ → (ℕ → τ → τ) → ℕ → τ
  primrec x f zero = x
  primrec x f (suc m) = f m (primrec x f m)

  -- The standard definition of Ackermann function
  A : ℕ → ℕ → ℕ
  A zero = suc
  A (suc m) 0 = A m 1
  A (suc m) (suc n) = A m (A (suc m) n)

  -- The definition of Ackermann function by double primitive recursion.
  -- Note that the outer recursion maps to τ = ℕ → ℕ, which is not possible
  -- in the usual primitive recursion.
  B : ℕ → ℕ → ℕ
  B = primrec {τ = ℕ → ℕ} suc (λ m a → primrec {τ = ℕ} (a 1) (λ n b → a b))

  -- A and B coincide
  A≡B : ∀ m n → A m n ≡ B m n
  A≡B zero n = refl
  A≡B (suc m) zero = A≡B m 1
  A≡B (suc m) (suc n) = trans (cong (A m) (A≡B (suc m) n)) (trans (A≡B m (B (suc m) n)) refl)