Theorem: Primrec.nat_strong_rec' (Logic/Vorspiel/Computability.lean)

State before:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : α → ℕ → σ
g : α × ℕ → List σ → Option σ
hg : Primrec₂ g
H : ∀ (a : α) (n : ℕ), g (a, n) (List.map (f a) (List.range n)) = some (f a n)
⊢ Primrec₂ f
Tactic:
let g' : α → List σ → Option σ := fun a l => g (a, l.length) l
State after:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : α → ℕ → σ
g : α × ℕ → List σ → Option σ
hg : Primrec₂ g
H : ∀ (a : α) (n : ℕ), g (a, n) (List.map (f a) (List.range n)) = some (f a n)
g' : α → List σ → Option σ := fun a l => g (a, l.length) l
⊢ Primrec₂ f

State before:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : α → ℕ → σ
g : α × ℕ → List σ → Option σ
hg : Primrec₂ g
H : ∀ (a : α) (n : ℕ), g (a, n) (List.map (f a) (List.range n)) = some (f a n)
g' : α → List σ → Option σ := fun a l => g (a, l.length) l
⊢ Primrec₂ f
Tactic:
have : Primrec₂ g' := hg.comp₂ (pair fst (list_length.comp snd)) Primrec₂.right
State after:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : α → ℕ → σ
g : α × ℕ → List σ → Option σ
hg : Primrec₂ g
H : ∀ (a : α) (n : ℕ), g (a, n) (List.map (f a) (List.range n)) = some (f a n)
g' : α → List σ → Option σ := fun a l => g (a, l.length) l
this : Primrec₂ g'
⊢ Primrec₂ f

State before:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : α → ℕ → σ
g : α × ℕ → List σ → Option σ
hg : Primrec₂ g
H : ∀ (a : α) (n : ℕ), g (a, n) (List.map (f a) (List.range n)) = some (f a n)
g' : α → List σ → Option σ := fun a l => g (a, l.length) l
this : Primrec₂ g'
⊢ Primrec₂ f
Tactic:
exact nat_strong_rec f this (by simpa [g'] using H)
State after:
no goals

State before:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
f : α → ℕ → σ
g : α × ℕ → List σ → Option σ
hg : Primrec₂ g
H : ∀ (a : α) (n : ℕ), g (a, n) (List.map (f a) (List.range n)) = some (f a n)
g' : α → List σ → Option σ := fun a l => g (a, l.length) l
this : Primrec₂ g'
⊢ ∀ (a : α) (n : ℕ), g' a (List.map (f a) (List.range n)) = some (f a n)
Tactic:
simpa [g'] using H
State after:
no goals