Theorem: Primrec.nat_omega_rec_prod (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 σ
inst✝ : DecidableEq α
t : α → ℕ → α
f : α → ℕ → σ
g : α × ℕ → List σ → Option σ
ht : Primrec₂ t
hg : Primrec₂ g
H : ∀ (a : α) (k : ℕ), g (a, k) (List.map (f (t a k)) (List.range k)) = some (f a k)
⊢ Primrec₂ f
Tactic:
have hm : Primrec (fun p => p.2 : α × ℕ → ℕ) := snd
State after:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : DecidableEq α
t : α → ℕ → α
f : α → ℕ → σ
g : α × ℕ → List σ → Option σ
ht : Primrec₂ t
hg : Primrec₂ g
H : ∀ (a : α) (k : ℕ), g (a, k) (List.map (f (t a k)) (List.range k)) = some (f a k)
hm : Primrec fun p => p.2
⊢ Primrec₂ f

State before:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : DecidableEq α
t : α → ℕ → α
f : α → ℕ → σ
g : α × ℕ → List σ → Option σ
ht : Primrec₂ t
hg : Primrec₂ g
H : ∀ (a : α) (k : ℕ), g (a, k) (List.map (f (t a k)) (List.range k)) = some (f a k)
hm : Primrec fun p => p.2
⊢ Primrec₂ f
Tactic:
have hl : Primrec (fun p => (List.range p.2).map fun x => (t p.1 p.2, x) : α × ℕ → List (α × ℕ)) :=
  list_map (list_range.comp snd) (Primrec₂.pair.comp₂ (ht.comp₂ (fst.comp₂ Primrec₂.left) (snd.comp₂ Primrec₂.left)) Primrec₂.right)
State after:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : DecidableEq α
t : α → ℕ → α
f : α → ℕ → σ
g : α × ℕ → List σ → Option σ
ht : Primrec₂ t
hg : Primrec₂ g
H : ∀ (a : α) (k : ℕ), g (a, k) (List.map (f (t a k)) (List.range k)) = some (f a k)
hm : Primrec fun p => p.2
hl : Primrec fun p => List.map (fun x => (t p.1 p.2, x)) (List.range p.2)
⊢ Primrec₂ f

State before:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : DecidableEq α
t : α → ℕ → α
f : α → ℕ → σ
g : α × ℕ → List σ → Option σ
ht : Primrec₂ t
hg : Primrec₂ g
H : ∀ (a : α) (k : ℕ), g (a, k) (List.map (f (t a k)) (List.range k)) = some (f a k)
hm : Primrec fun p => p.2
hl : Primrec fun p => List.map (fun x => (t p.1 p.2, x)) (List.range p.2)
⊢ Primrec₂ f
Tactic:
have := nat_omega_rec' (fun (p : α × ℕ) => f p.1 p.2) hm hl hg (by simp) (by rintro ⟨a, k⟩; simp[Function.comp, H])
State after:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : DecidableEq α
t : α → ℕ → α
f : α → ℕ → σ
g : α × ℕ → List σ → Option σ
ht : Primrec₂ t
hg : Primrec₂ g
H : ∀ (a : α) (k : ℕ), g (a, k) (List.map (f (t a k)) (List.range k)) = some (f a k)
hm : Primrec fun p => p.2
hl : Primrec fun p => List.map (fun x => (t p.1 p.2, x)) (List.range p.2)
this : Primrec fun p => f p.1 p.2
⊢ Primrec₂ f

State before:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : DecidableEq α
t : α → ℕ → α
f : α → ℕ → σ
g : α × ℕ → List σ → Option σ
ht : Primrec₂ t
hg : Primrec₂ g
H : ∀ (a : α) (k : ℕ), g (a, k) (List.map (f (t a k)) (List.range k)) = some (f a k)
hm : Primrec fun p => p.2
hl : Primrec fun p => List.map (fun x => (t p.1 p.2, x)) (List.range p.2)
this : Primrec fun p => f p.1 p.2
⊢ Primrec₂ f
Tactic:
exact to₂ this
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 σ
inst✝ : DecidableEq α
t : α → ℕ → α
f : α → ℕ → σ
g : α × ℕ → List σ → Option σ
ht : Primrec₂ t
hg : Primrec₂ g
H : ∀ (a : α) (k : ℕ), g (a, k) (List.map (f (t a k)) (List.range k)) = some (f a k)
hm : Primrec fun p => p.2
hl : Primrec fun p => List.map (fun x => (t p.1 p.2, x)) (List.range p.2)
⊢ ∀ (b b' : α × ℕ), b' ∈ List.map (fun x => (t b.1 b.2, x)) (List.range b.2) → b'.2 < b.2
Tactic:
simp
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 σ
inst✝ : DecidableEq α
t : α → ℕ → α
f : α → ℕ → σ
g : α × ℕ → List σ → Option σ
ht : Primrec₂ t
hg : Primrec₂ g
H : ∀ (a : α) (k : ℕ), g (a, k) (List.map (f (t a k)) (List.range k)) = some (f a k)
hm : Primrec fun p => p.2
hl : Primrec fun p => List.map (fun x => (t p.1 p.2, x)) (List.range p.2)
⊢ ∀ (b : α × ℕ),
    g b (List.map (fun p => f p.1 p.2) (List.map (fun x => (t b.1 b.2, x)) (List.range b.2))) =
      some ((fun p => f p.1 p.2) b)
Tactic:
rintro ⟨a, k⟩
State after:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : DecidableEq α
t : α → ℕ → α
f : α → ℕ → σ
g : α × ℕ → List σ → Option σ
ht : Primrec₂ t
hg : Primrec₂ g
H : ∀ (a : α) (k : ℕ), g (a, k) (List.map (f (t a k)) (List.range k)) = some (f a k)
hm : Primrec fun p => p.2
hl : Primrec fun p => List.map (fun x => (t p.1 p.2, x)) (List.range p.2)
a : α
k : ℕ
⊢ g (a, k) (List.map (fun p => f p.1 p.2) (List.map (fun x => (t (a, k).1 (a, k).2, x)) (List.range (a, k).2))) =
    some ((fun p => f p.1 p.2) (a, k))

State before:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : DecidableEq α
t : α → ℕ → α
f : α → ℕ → σ
g : α × ℕ → List σ → Option σ
ht : Primrec₂ t
hg : Primrec₂ g
H : ∀ (a : α) (k : ℕ), g (a, k) (List.map (f (t a k)) (List.range k)) = some (f a k)
hm : Primrec fun p => p.2
hl : Primrec fun p => List.map (fun x => (t p.1 p.2, x)) (List.range p.2)
a : α
k : ℕ
⊢ g (a, k) (List.map (fun p => f p.1 p.2) (List.map (fun x => (t (a, k).1 (a, k).2, x)) (List.range (a, k).2))) =
    some ((fun p => f p.1 p.2) (a, k))
Tactic:
simp[Function.comp, H]
State after:
no goals