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