Theorem: Primrec.iterate (Logic/Vorspiel/OmegaRec.lean)

State before:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → α
hf : Primrec f
⊢ Primrec₂ fun x x_1 => f^[x] x_1
Tactic:
have : Primrec₂ (fun s a => s.rec a (fun _ => f) : ℕ → α → α) :=
  to₂ (nat_rec' fst snd (hf.comp₂ (snd.comp₂ Primrec₂.right)))
State after:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → α
hf : Primrec f
this : Primrec₂ fun s a => Nat.rec a (fun x => f) s
⊢ Primrec₂ fun x x_1 => f^[x] x_1

State before:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → α
hf : Primrec f
this : Primrec₂ fun s a => Nat.rec a (fun x => f) s
⊢ Primrec₂ fun x x_1 => f^[x] x_1
Tactic:
exact this.of_eq (fun s a => by
  induction' s with s ih <;> simp[*]; { exact Eq.symm (Function.iterate_succ_apply' f s a) })
State after:
no goals

State before:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → α
hf : Primrec f
this : Primrec₂ fun s a => Nat.rec a (fun x => f) s
s : ℕ
a : α
⊢ Nat.rec a (fun x => f) s = f^[s] a
Tactic:
induction' s with s ih <;> simp[*]
State after:
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → α
hf : Primrec f
this : Primrec₂ fun s a => Nat.rec a (fun x => f) s
a : α
s : ℕ
ih : Nat.rec a (fun x => f) s = f^[s] a
⊢ f (f^[s] a) = f^[s] (f a)

State before:
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → α
hf : Primrec f
this : Primrec₂ fun s a => Nat.rec a (fun x => f) s
a : α
s : ℕ
ih : Nat.rec a (fun x => f) s = f^[s] a
⊢ f (f^[s] a) = f^[s] (f a)
Tactic:
{ exact Eq.symm (Function.iterate_succ_apply' f s a) }
State after:
no goals

State before:
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → α
hf : Primrec f
this : Primrec₂ fun s a => Nat.rec a (fun x => f) s
a : α
s : ℕ
ih : Nat.rec a (fun x => f) s = f^[s] a
⊢ f (f^[s] a) = f^[s] (f a)
Tactic:
exact Eq.symm (Function.iterate_succ_apply' f s a)
State after:
no goals