SICP Exercise 1.10.

Ackerman.agda

module Ackerman where

open import Data.Empty
open import Data.Nat
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

A : ℕ → ℕ → ℕ
A _       0       = 0
A 0       y       = 2 * y
A _       1       = 2
A (suc x) (suc y) = A x (A (suc x) y)

infixl 8 _^_

_^_ : ℕ → ℕ → ℕ
_ ^ 0       = 1
b ^ (suc n) = b * b ^ n

2^-not-zero : ∀ {n} → 2 ^ n ≡ 0 → ⊥
2^-not-zero {zero} ()
2^-not-zero {suc n} eq = 2^-not-zero {n} (ex {2 ^ n} eq)
  where ex : ∀ {n} → 2 * n ≡ 0 → n ≡ 0
        ex {zero} eq = refl
        ex {suc n} ()

f : ∀ {n} → A 0 n ≡ 2 * n
f {0}     = refl
f {suc n} = refl

suc-not-zero : ∀ {n} → suc n ≢ 0
suc-not-zero ()

g' : A 1 0 ≡ 0
g' = refl

g : ∀ {n} → n ≢ 0 → A 1 n ≡ 2 ^ n
g {zero} neq with neq refl
... | ()
g {suc zero}    _ = refl
g {suc (suc n)} _ = begin
  A 1 (suc (suc n)) ≡⟨ refl ⟩
  A 0 (A 1 (suc n)) ≡⟨ cong (λ x → A 0 x) (g {suc n} suc-not-zero) ⟩
  A 0 (2 ^ (suc n)) ≡⟨ f {2 ^ (suc n)} ⟩
  2 * (2 ^ (suc n)) ≡⟨ refl ⟩
  2 ^ (suc (suc n))
  ∎

_⇈_ : ℕ → ℕ → ℕ
_ ⇈ 0       = 1
a ⇈ (suc n) = a ^ (a ⇈ n)

h' : A 2 0 ≡ 0
h' = refl

h : ∀ {n} → n ≢ 0 → A 2 n ≡ 2 ⇈ n
h {zero} neq with neq refl
... | ()
h {suc zero} _      = refl
h {suc (suc n)} neq = begin
  A 2 (suc (suc n)) ≡⟨ refl ⟩
  A 1 (A 2 (suc n)) ≡⟨ cong (λ x → A 1 x) (h {suc n} suc-not-zero) ⟩
  A 1 (2 ⇈ (suc n)) ≡⟨ g {2 ⇈ (suc n)} (lem {suc n})⟩
  2 ^ (2 ⇈ (suc n)) ≡⟨ refl ⟩
  2 ⇈ (suc (suc n))
  ∎
  where lem : ∀ {n} → 2 ⇈ n ≡ 0 → ⊥
        lem {0} ()
        lem {suc n} eq = 2^-not-zero {2 ⇈ n} eq