Theorem: LO.FirstOrder.Semiterm.Operator.numeral_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 σ
inst✝² : Operator.Zero L
inst✝¹ : Operator.One L
inst✝ : Operator.Add L
⊢ Primrec (numeral L)
Tactic:
have : Primrec₂ (fun _ n => Add.add.foldr One.one (List.replicate n One.one) : ℕ → ℕ → Const L) :=
  (foldr_primrec _ _).comp₂ (list_replicate.comp₂ .right (.const _))
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 σ
inst✝² : Operator.Zero L
inst✝¹ : Operator.One L
inst✝ : Operator.Add L
this : Primrec₂ fun x n => op(+).foldr op(1) (List.replicate n op(1))
⊢ Primrec (numeral 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 σ
inst✝² : Operator.Zero L
inst✝¹ : Operator.One L
inst✝ : Operator.Add L
this : Primrec₂ fun x n => op(+).foldr op(1) (List.replicate n op(1))
⊢ Primrec (numeral L)
Tactic:
have := Primrec.nat_casesOn Primrec.id (.const Zero.zero) 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 σ
inst✝² : Operator.Zero L
inst✝¹ : Operator.One L
inst✝ : Operator.Add L
this✝ : Primrec₂ fun x n => op(+).foldr op(1) (List.replicate n op(1))
this : Primrec fun a => Nat.casesOn (id a) op(0) fun n => op(+).foldr op(1) (List.replicate n op(1))
⊢ Primrec (numeral 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 σ
inst✝² : Operator.Zero L
inst✝¹ : Operator.One L
inst✝ : Operator.Add L
this✝ : Primrec₂ fun x n => op(+).foldr op(1) (List.replicate n op(1))
this : Primrec fun a => Nat.casesOn (id a) op(0) fun n => op(+).foldr op(1) (List.replicate n op(1))
⊢ Primrec (numeral L)
Tactic:
exact this.of_eq <| by
  intro n; induction n <;> simp[numeral, *]
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 σ
inst✝² : Operator.Zero L
inst✝¹ : Operator.One L
inst✝ : Operator.Add L
this✝ : Primrec₂ fun x n => op(+).foldr op(1) (List.replicate n op(1))
this : Primrec fun a => Nat.casesOn (id a) op(0) fun n => op(+).foldr op(1) (List.replicate n op(1))
⊢ ∀ (n : ℕ), (Nat.casesOn (id n) op(0) fun n => op(+).foldr op(1) (List.replicate n op(1))) = numeral L n
Tactic:
intro n
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 σ
inst✝² : Operator.Zero L
inst✝¹ : Operator.One L
inst✝ : Operator.Add L
this✝ : Primrec₂ fun x n => op(+).foldr op(1) (List.replicate n op(1))
this : Primrec fun a => Nat.casesOn (id a) op(0) fun n => op(+).foldr op(1) (List.replicate n op(1))
n : ℕ
⊢ (Nat.casesOn (id n) op(0) fun n => op(+).foldr op(1) (List.replicate n op(1))) = numeral L n

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 σ
inst✝² : Operator.Zero L
inst✝¹ : Operator.One L
inst✝ : Operator.Add L
this✝ : Primrec₂ fun x n => op(+).foldr op(1) (List.replicate n op(1))
this : Primrec fun a => Nat.casesOn (id a) op(0) fun n => op(+).foldr op(1) (List.replicate n op(1))
n : ℕ
⊢ (Nat.casesOn (id n) op(0) fun n => op(+).foldr op(1) (List.replicate n op(1))) = numeral L n
Tactic:
induction n <;> simp[numeral, *]
State after:
no goals