-- Mathlib/Computability/Ackermann.lean
theorem exists_lt_ack_of_nat_primrec {f : ℕ → ℕ} (hf : Nat.Primrec f) :
    ∃ m, ∀ n, f n < ack m n

Proof state:
case inr.inl
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m n : ℕ
IH : rec (f m) (fun y IH => g (pair m (pair y IH))) n < ack (a ⊔ b + 9) (m + n)
h₁ : m ≤ pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n)
h₂ : rec (f m) (fun y IH => g (pair m (pair y IH))) n < n
⊢ ack (b + (4 + 4)) n ≤ ack (a ⊔ b + 9) (m + (n + 1))

Tactic:
exact
  ack_le_ack (Nat.add_le_add (le_max_right a b) <| by norm_num)
    ((le_succ n).trans <| self_le_add_left _ _)

Result:
no goals

Proof state:
case right
f : ℕ → ℕ
n : ℕ
⊢ (fun n => (unpair n).2) n ≤ n

Tactic:
exact unpair_right_le n

Result:
no goals

Proof state:
case zero
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m : ℕ
⊢ rec (f m) (fun y IH => g (pair m (pair y IH))) 0 < ack (a ⊔ b + 9) (m + 0)

Tactic:
apply (ha m).trans (ack_strictMono_left m <| (le_max_left a b).trans_lt _)

Result:
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m : ℕ
⊢ a ⊔ b < a ⊔ b + 9

Proof state:
case prec
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
IHf : ∃ m, ∀ (n : ℕ), f n < ack m n
IHg : ∃ m, ∀ (n : ℕ), g n < ack m n
⊢ ∃ m, ∀ (n : ℕ), unpaired (fun z n => rec (f z) (fun y IH => g (pair z (pair y IH))) n) n < ack m n

Tactic:
obtain ⟨a, ha⟩ := IHf

Result:
case prec.intro
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
IHg : ∃ m, ∀ (n : ℕ), g n < ack m n
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
⊢ ∃ m, ∀ (n : ℕ), unpaired (fun z n => rec (f z) (fun y IH => g (pair z (pair y IH))) n) n < ack m n

Proof state:
case inr.inr
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m n : ℕ
IH : rec (f m) (fun y IH => g (pair m (pair y IH))) n < ack (a ⊔ b + 9) (m + n)
h₁ : m ≤ pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n)
h₂ : n ≤ rec (f m) (fun y IH => g (pair m (pair y IH))) n
⊢ ack (b + 4 + 4) (n ⊔ rec (f m) (fun y IH => g (pair m (pair y IH))) n) ≤ ack (a ⊔ b + 9) (m + (n + 1))

Tactic:
rw [max_eq_right h₂]

Result:
case inr.inr
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m n : ℕ
IH : rec (f m) (fun y IH => g (pair m (pair y IH))) n < ack (a ⊔ b + 9) (m + n)
h₁ : m ≤ pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n)
h₂ : n ≤ rec (f m) (fun y IH => g (pair m (pair y IH))) n
⊢ ack (b + 4 + 4) (rec (f m) (fun y IH => g (pair m (pair y IH))) n) ≤ ack (a ⊔ b + 9) (m + (n + 1))

Proof state:
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m n : ℕ
IH : rec (f m) (fun y IH => g (pair m (pair y IH))) n < ack (a ⊔ b + 9) (m + n)
⊢ ack (b + 4) (m ⊔ pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n)) ≤ ack (a ⊔ b + 9) (m + (n + 1))

Tactic:
rcases lt_or_le _ m with h₁ | h₁

Result:
case inl
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m n : ℕ
IH : rec (f m) (fun y IH => g (pair m (pair y IH))) n < ack (a ⊔ b + 9) (m + n)
h₁ : ?m.129969 < m
⊢ ack (b + 4) (m ⊔ pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n)) ≤ ack (a ⊔ b + 9) (m + (n + 1))

case inr
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m n : ℕ
IH : rec (f m) (fun y IH => g (pair m (pair y IH))) n < ack (a ⊔ b + 9) (m + n)
h₁ : m ≤ ?m.129969
⊢ ack (b + 4) (m ⊔ pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n)) ≤ ack (a ⊔ b + 9) (m + (n + 1))

Proof state:
case pair.intro.intro
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
n : ℕ
⊢ f n ⊔ g n ≤ ack a n ⊔ ack b n

Tactic:
exact max_le_max (ha n).le (hb n).le

Result:
no goals

Proof state:
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m n : ℕ
IH : rec (f m) (fun y IH => g (pair m (pair y IH))) n < ack (a ⊔ b + 9) (m + n)
h₁ : m ≤ pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n)
h₂ : rec (f m) (fun y IH => g (pair m (pair y IH))) n < n
⊢ 4 + 4 ≤ 9

Tactic:
norm_num

Result:
no goals

Proof state:
case succ
f : ℕ → ℕ
n : ℕ
⊢ n.succ < ack 1 n

Tactic:
rw [succ_eq_one_add]

Result:
case succ
f : ℕ → ℕ
n : ℕ
⊢ 1 + n < ack 1 n

Proof state:
case left
f : ℕ → ℕ
⊢ ∃ m, ∀ (n : ℕ), (fun n => (unpair n).1) n < ack m n

Tactic:
refine ⟨0, fun n => ?_⟩

Result:
case left
f : ℕ → ℕ
n : ℕ
⊢ (fun n => (unpair n).1) n < ack 0 n

Proof state:
case inr
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m n : ℕ
IH : rec (f m) (fun y IH => g (pair m (pair y IH))) n < ack (a ⊔ b + 9) (m + n)
h₁ : m ≤ pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n)
⊢ ack (b + 4) (pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n)) ≤ ack (a ⊔ b + 9) (m + (n + 1))

Tactic:
apply (ack_pair_lt _ _ _).le.trans

Result:
case inr
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m n : ℕ
IH : rec (f m) (fun y IH => g (pair m (pair y IH))) n < ack (a ⊔ b + 9) (m + n)
h₁ : m ≤ pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n)
⊢ ack (b + 4 + 4) (n ⊔ rec (f m) (fun y IH => g (pair m (pair y IH))) n) ≤ ack (a ⊔ b + 9) (m + (n + 1))

Proof state:
case succ
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m n : ℕ
IH : rec (f m) (fun y IH => g (pair m (pair y IH))) n < ack (a ⊔ b + 9) (m + n)
⊢ rec (f m) (fun y IH => g (pair m (pair y IH))) (n + 1) < ack (a ⊔ b + 9) (m + (n + 1))

Tactic:
simp only

Result:
case succ
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m n : ℕ
IH : rec (f m) (fun y IH => g (pair m (pair y IH))) n < ack (a ⊔ b + 9) (m + n)
⊢ g (pair m (pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n))) < ack (a ⊔ b + 9) (m + (n + 1))

Proof state:
case left
f : ℕ → ℕ
n : ℕ
⊢ (fun n => (unpair n).1) n < ack 0 n

Tactic:
rw [ack_zero, Nat.lt_succ_iff]

Result:
case left
f : ℕ → ℕ
n : ℕ
⊢ (fun n => (unpair n).1) n ≤ n

Proof state:
f : ℕ → ℕ
hf : Nat.Primrec f
⊢ ∃ m, ∀ (n : ℕ), f n < ack m n

Tactic:
induction' hf with f g hf hg IHf IHg f g hf hg IHf IHg f g hf hg IHf IHg

Result:
case zero
f : ℕ → ℕ
⊢ ∃ m, ∀ (n : ℕ), (fun x => 0) n < ack m n

case succ
f : ℕ → ℕ
⊢ ∃ m, ∀ (n : ℕ), n.succ < ack m n

case left
f : ℕ → ℕ
⊢ ∃ m, ∀ (n : ℕ), (fun n => (unpair n).1) n < ack m n

case right
f : ℕ → ℕ
⊢ ∃ m, ∀ (n : ℕ), (fun n => (unpair n).2) n < ack m n

case pair
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
IHf : ∃ m, ∀ (n : ℕ), f n < ack m n
IHg : ∃ m, ∀ (n : ℕ), g n < ack m n
⊢ ∃ m, ∀ (n : ℕ), (fun n => pair (f n) (g n)) n < ack m n

case comp
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
IHf : ∃ m, ∀ (n : ℕ), f n < ack m n
IHg : ∃ m, ∀ (n : ℕ), g n < ack m n
⊢ ∃ m, ∀ (n : ℕ), (fun n => f (g n)) n < ack m n

case prec
f✝ f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
IHf : ∃ m, ∀ (n : ℕ), f n < ack m n
IHg : ∃ m, ∀ (n : ℕ), g n < ack m n
⊢ ∃ m, ∀ (n : ℕ), unpaired (fun z n => rec (f z) (fun y IH => g (pair z (pair y IH))) n) n < ack m n

Proof state:
case succ
f : ℕ → ℕ
n : ℕ
⊢ 1 + n < ack 1 n

Tactic:
apply add_lt_ack

Result:
no goals