Theorem: Primrec.nat_strong_rec'2' (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 : ∀ (n m : ℕ), g (n, m) (List.map (fun i => f i.unpair.1 i.unpair.2) (List.range (n.pair m))) = some (f n m)
⊢ Primrec₂ f
Tactic:
have : Primrec₂ (fun p => g p.2 : Unit × (ℕ × ℕ) → List σ → Option σ) := hg.comp (snd.comp fst) snd
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 : ∀ (n m : ℕ), g (n, m) (List.map (fun i => f i.unpair.1 i.unpair.2) (List.range (n.pair m))) = some (f n m)
this : Primrec₂ fun p => g p.2
⊢ 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 : ∀ (n m : ℕ), g (n, m) (List.map (fun i => f i.unpair.1 i.unpair.2) (List.range (n.pair m))) = some (f n m)
this : Primrec₂ fun p => g p.2
⊢ Primrec₂ f
Tactic:
have := nat_strong_rec'2 (fun _ i => f i.1 i.2 : Unit → ℕ × ℕ → σ) this (by simpa using H)
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 : ∀ (n m : ℕ), g (n, m) (List.map (fun i => f i.unpair.1 i.unpair.2) (List.range (n.pair m))) = some (f n m)
this✝ : Primrec₂ fun p => g p.2
this : Primrec₂ fun x i => f i.1 i.2
⊢ 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 : ∀ (n m : ℕ), g (n, m) (List.map (fun i => f i.unpair.1 i.unpair.2) (List.range (n.pair m))) = some (f n m)
this✝ : Primrec₂ fun p => g p.2
this : Primrec₂ fun x i => f i.1 i.2
⊢ Primrec₂ f
Tactic:
have : Primrec₂ (fun n m => (fun _ i => f i.1 i.2 : Unit → ℕ × ℕ → σ) () (n, m)) := this.comp (const ()) Primrec.id
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 : ∀ (n m : ℕ), g (n, m) (List.map (fun i => f i.unpair.1 i.unpair.2) (List.range (n.pair m))) = some (f n m)
this✝¹ : Primrec₂ fun p => g p.2
this✝ : Primrec₂ fun x i => f i.1 i.2
this : Primrec₂ fun n m => (fun x i => f i.1 i.2) () (n, m)
⊢ 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 : ∀ (n m : ℕ), g (n, m) (List.map (fun i => f i.unpair.1 i.unpair.2) (List.range (n.pair m))) = some (f n m)
this✝¹ : Primrec₂ fun p => g p.2
this✝ : Primrec₂ fun x i => f i.1 i.2
this : Primrec₂ fun n m => (fun x i => f i.1 i.2) () (n, m)
⊢ Primrec₂ f
Tactic:
exact this.of_eq (by simp)
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 : ∀ (n m : ℕ), g (n, m) (List.map (fun i => f i.unpair.1 i.unpair.2) (List.range (n.pair m))) = some (f n m)
this : Primrec₂ fun p => g p.2
⊢ ∀ (a : Unit) (n m : ℕ),
    g (a, n, m).2 (List.map (fun i => (fun x i => f i.1 i.2) a i.unpair) (List.range (n.pair m))) =
      some ((fun x i => f i.1 i.2) a (n, m))
Tactic:
simpa 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 : ∀ (n m : ℕ), g (n, m) (List.map (fun i => f i.unpair.1 i.unpair.2) (List.range (n.pair m))) = some (f n m)
this✝¹ : Primrec₂ fun p => g p.2
this✝ : Primrec₂ fun x i => f i.1 i.2
this : Primrec₂ fun n m => (fun x i => f i.1 i.2) () (n, m)
⊢ ∀ (a b : ℕ), (fun x i => f i.1 i.2) () (a, b) = f a b
Tactic:
simp
State after:
no goals