Theorem: LO.FirstOrder.Semiterm.Operator.foldr_primrec (Logic/FirstOrder/Computability/Term.lean)

State before:
L : Language
μ : Type v
α : Type u_1
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
k : ℕ
f : Operator L 2
z : Operator L k
⊢ Primrec (f.foldr z)
Tactic:
have : Primrec₂ (fun _ p => f.comp ![p.2, p.1] : List (Operator L k) → Operator L k × Operator L k → Operator L k) :=
  by apply (comp_primrec₂ f).comp₂ (Primrec.snd.comp₂ .right) (Primrec.fst.comp₂ .right)
State after:
L : Language
μ : Type v
α : Type u_1
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
k : ℕ
f : Operator L 2
z : Operator L k
this : Primrec₂ fun x p => f.comp ![p.2, p.1]
⊢ Primrec (f.foldr z)

State before:
L : Language
μ : Type v
α : Type u_1
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
k : ℕ
f : Operator L 2
z : Operator L k
this : Primrec₂ fun x p => f.comp ![p.2, p.1]
⊢ Primrec (f.foldr z)
Tactic:
have := Primrec.list_foldr Primrec.id (.const z) this
State after:
L : Language
μ : Type v
α : Type u_1
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
k : ℕ
f : Operator L 2
z : Operator L k
this✝ : Primrec₂ fun x p => f.comp ![p.2, p.1]
this : Primrec fun a => List.foldr (fun b s => f.comp ![(b, s).2, (b, s).1]) z (id a)
⊢ Primrec (f.foldr z)

State before:
L : Language
μ : Type v
α : Type u_1
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
k : ℕ
f : Operator L 2
z : Operator L k
this✝ : Primrec₂ fun x p => f.comp ![p.2, p.1]
this : Primrec fun a => List.foldr (fun b s => f.comp ![(b, s).2, (b, s).1]) z (id a)
⊢ Primrec (f.foldr z)
Tactic:
exact this.of_eq <| by
  intro l; induction l <;> simp[foldr, *] at*
State after:
no goals

State before:
L : Language
μ : Type v
α : Type u_1
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
k : ℕ
f : Operator L 2
z : Operator L k
⊢ Primrec₂ fun x p => f.comp ![p.2, p.1]
Tactic:
apply (comp_primrec₂ f).comp₂ (Primrec.snd.comp₂ .right) (Primrec.fst.comp₂ .right)
State after:
no goals

State before:
L : Language
μ : Type v
α : Type u_1
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
k : ℕ
f : Operator L 2
z : Operator L k
this✝ : Primrec₂ fun x p => f.comp ![p.2, p.1]
this : Primrec fun a => List.foldr (fun b s => f.comp ![(b, s).2, (b, s).1]) z (id a)
⊢ ∀ (n : List (Operator L k)), List.foldr (fun b s => f.comp ![(b, s).2, (b, s).1]) z (id n) = f.foldr z n
Tactic:
intro l
State after:
L : Language
μ : Type v
α : Type u_1
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
k : ℕ
f : Operator L 2
z : Operator L k
this✝ : Primrec₂ fun x p => f.comp ![p.2, p.1]
this : Primrec fun a => List.foldr (fun b s => f.comp ![(b, s).2, (b, s).1]) z (id a)
l : List (Operator L k)
⊢ List.foldr (fun b s => f.comp ![(b, s).2, (b, s).1]) z (id l) = f.foldr z l

State before:
L : Language
μ : Type v
α : Type u_1
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable μ
inst✝⁴ : (k : ℕ) → Primcodable (L.Func k)
inst✝³ : UniformlyPrimcodable L.Func
σ : Type u_2
μ₁ : Type u_3
μ₂ : Type u_4
inst✝² : Primcodable μ₁
inst✝¹ : Primcodable μ₂
inst✝ : Primcodable σ
k : ℕ
f : Operator L 2
z : Operator L k
this✝ : Primrec₂ fun x p => f.comp ![p.2, p.1]
this : Primrec fun a => List.foldr (fun b s => f.comp ![(b, s).2, (b, s).1]) z (id a)
l : List (Operator L k)
⊢ List.foldr (fun b s => f.comp ![(b, s).2, (b, s).1]) z (id l) = f.foldr z l
Tactic:
induction l <;> simp[foldr, *] at*
State after:
no goals