Theorem: LO.FirstOrder.UTerm.bind_primrec_param (Logic/FirstOrder/Computability/Term.lean)

State before:
L : Language
μ : Type v
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
μ₁ : Type u_1
μ₂ : Type u_2
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
σ : Type u_3
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
g : σ → UTerm L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hg : Primrec g
⊢ Primrec fun x => bind (b x) (e x) (g x)
Tactic:
have : Primrec₂ (fun _ p => funcL p.1 p.2 : σ → ((k : ℕ) × L.Func k) × List (UTerm L μ₂) → Option (UTerm L μ₂)) :=
  funcL_primrec.comp₂ (fst.comp₂ Primrec₂.right) (snd.comp₂ Primrec₂.right)
State after:
L : Language
μ : Type v
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
μ₁ : Type u_1
μ₂ : Type u_2
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
σ : Type u_3
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
g : σ → UTerm L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hg : Primrec g
this : Primrec₂ fun x p => funcL p.1 p.2
⊢ Primrec fun x => bind (b x) (e x) (g x)

State before:
L : Language
μ : Type v
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
μ₁ : Type u_1
μ₂ : Type u_2
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
σ : Type u_3
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
g : σ → UTerm L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hg : Primrec g
this : Primrec₂ fun x p => funcL p.1 p.2
⊢ Primrec fun x => bind (b x) (e x) (g x)
Tactic:
have := elim_primrec_param_opt hb he (fun _ _ f v => func f v) this hg
  (by intro _ k f v; simp[funcL])
State after:
L : Language
μ : Type v
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
μ₁ : Type u_1
μ₂ : Type u_2
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
σ : Type u_3
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
g : σ → UTerm L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hg : Primrec g
this✝ : Primrec₂ fun x p => funcL p.1 p.2
this : Primrec fun x => elim (b x) (e x) (fun {k} => (fun x x f v => func f v) x k) (g x)
⊢ Primrec fun x => bind (b x) (e x) (g x)

State before:
L : Language
μ : Type v
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
μ₁ : Type u_1
μ₂ : Type u_2
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
σ : Type u_3
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
g : σ → UTerm L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hg : Primrec g
this✝ : Primrec₂ fun x p => funcL p.1 p.2
this : Primrec fun x => elim (b x) (e x) (fun {k} => (fun x x f v => func f v) x k) (g x)
⊢ Primrec fun x => bind (b x) (e x) (g x)
Tactic:
exact this.of_eq <| by intro x; generalize g x = t; induction t <;> simp[elim, bind, *]
State after:
no goals

State before:
L : Language
μ : Type v
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
μ₁ : Type u_1
μ₂ : Type u_2
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
σ : Type u_3
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
g : σ → UTerm L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hg : Primrec g
this : Primrec₂ fun x p => funcL p.1 p.2
⊢ ∀ (x : σ) {k : ℕ} (f : L.Func k) (v : Fin k → UTerm L μ₂),
    funcL (⟨k, f⟩, List.ofFn v).1 (⟨k, f⟩, List.ofFn v).2 = some ((fun x x f v => func f v) x k f v)
Tactic:
intro _ k f v
State after:
L : Language
μ : Type v
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
μ₁ : Type u_1
μ₂ : Type u_2
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
σ : Type u_3
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
g : σ → UTerm L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hg : Primrec g
this : Primrec₂ fun x p => funcL p.1 p.2
x✝ : σ
k : ℕ
f : L.Func k
v : Fin k → UTerm L μ₂
⊢ funcL (⟨k, f⟩, List.ofFn v).1 (⟨k, f⟩, List.ofFn v).2 = some ((fun x x f v => func f v) x✝ k f v)

State before:
L : Language
μ : Type v
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
μ₁ : Type u_1
μ₂ : Type u_2
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
σ : Type u_3
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
g : σ → UTerm L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hg : Primrec g
this : Primrec₂ fun x p => funcL p.1 p.2
x✝ : σ
k : ℕ
f : L.Func k
v : Fin k → UTerm L μ₂
⊢ funcL (⟨k, f⟩, List.ofFn v).1 (⟨k, f⟩, List.ofFn v).2 = some ((fun x x f v => func f v) x✝ k f v)
Tactic:
simp[funcL]
State after:
no goals

State before:
L : Language
μ : Type v
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
μ₁ : Type u_1
μ₂ : Type u_2
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
σ : Type u_3
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
g : σ → UTerm L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hg : Primrec g
this✝ : Primrec₂ fun x p => funcL p.1 p.2
this : Primrec fun x => elim (b x) (e x) (fun {k} => (fun x x f v => func f v) x k) (g x)
⊢ ∀ (n : σ), elim (b n) (e n) (fun {k} => (fun x x f v => func f v) n k) (g n) = bind (b n) (e n) (g n)
Tactic:
intro x
State after:
L : Language
μ : Type v
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
μ₁ : Type u_1
μ₂ : Type u_2
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
σ : Type u_3
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
g : σ → UTerm L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hg : Primrec g
this✝ : Primrec₂ fun x p => funcL p.1 p.2
this : Primrec fun x => elim (b x) (e x) (fun {k} => (fun x x f v => func f v) x k) (g x)
x : σ
⊢ elim (b x) (e x) (fun {k} => (fun x x f v => func f v) x k) (g x) = bind (b x) (e x) (g x)

State before:
L : Language
μ : Type v
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
μ₁ : Type u_1
μ₂ : Type u_2
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
σ : Type u_3
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
g : σ → UTerm L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hg : Primrec g
this✝ : Primrec₂ fun x p => funcL p.1 p.2
this : Primrec fun x => elim (b x) (e x) (fun {k} => (fun x x f v => func f v) x k) (g x)
x : σ
⊢ elim (b x) (e x) (fun {k} => (fun x x f v => func f v) x k) (g x) = bind (b x) (e x) (g x)
Tactic:
generalize g x = t
State after:
L : Language
μ : Type v
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
μ₁ : Type u_1
μ₂ : Type u_2
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
σ : Type u_3
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
g : σ → UTerm L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hg : Primrec g
this✝ : Primrec₂ fun x p => funcL p.1 p.2
this : Primrec fun x => elim (b x) (e x) (fun {k} => (fun x x f v => func f v) x k) (g x)
x : σ
t : UTerm L μ₁
⊢ elim (b x) (e x) (fun {k} => (fun x x f v => func f v) x k) t = bind (b x) (e x) t

State before:
L : Language
μ : Type v
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
μ₁ : Type u_1
μ₂ : Type u_2
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
σ : Type u_3
inst✝ : Primcodable σ
b : σ → ℕ → UTerm L μ₂
e : σ → μ₁ → UTerm L μ₂
g : σ → UTerm L μ₁
hb : Primrec₂ b
he : Primrec₂ e
hg : Primrec g
this✝ : Primrec₂ fun x p => funcL p.1 p.2
this : Primrec fun x => elim (b x) (e x) (fun {k} => (fun x x f v => func f v) x k) (g x)
x : σ
t : UTerm L μ₁
⊢ elim (b x) (e x) (fun {k} => (fun x x f v => func f v) x k) t = bind (b x) (e x) t
Tactic:
induction t <;> simp[elim, bind, *]
State after:
no goals