Theorem: Nat.ArithPart₁.to_partrec' (Logic/Vorspiel/Arith.lean)

State before:
n : ℕ
f : Vector ℕ n →. ℕ
hf : ArithPart₁ f
⊢ Partrec' f
Tactic:
induction hf
State after:
case zero
n : ℕ
f : Vector ℕ n →. ℕ
n✝ : ℕ
⊢ Partrec' fun x => 0

case one
n : ℕ
f : Vector ℕ n →. ℕ
n✝ : ℕ
⊢ Partrec' fun x => 1

case add
n : ℕ
f : Vector ℕ n →. ℕ
n✝ : ℕ
i✝ j✝ : Fin n✝
⊢ Partrec' ↑fun v => v.get i✝ + v.get j✝

case mul
n : ℕ
f : Vector ℕ n →. ℕ
n✝ : ℕ
i✝ j✝ : Fin n✝
⊢ Partrec' ↑fun v => v.get i✝ * v.get j✝

case proj
n : ℕ
f : Vector ℕ n →. ℕ
n✝ : ℕ
i✝ : Fin n✝
⊢ Partrec' ↑fun v => v.get i✝

case equal
n : ℕ
f : Vector ℕ n →. ℕ
n✝ : ℕ
i✝ j✝ : Fin n✝
⊢ Partrec' ↑fun v => (v.get i✝).isEqNat (v.get j✝)

case lt
n : ℕ
f : Vector ℕ n →. ℕ
n✝ : ℕ
i✝ j✝ : Fin n✝
⊢ Partrec' ↑fun v => (v.get i✝).isLtNat (v.get j✝)

case comp
n : ℕ
f : Vector ℕ n →. ℕ
m✝ n✝ : ℕ
f✝ : Vector ℕ n✝ →. ℕ
g✝ : Fin n✝ → Vector ℕ m✝ →. ℕ
a✝¹ : ArithPart₁ f✝
a✝ : ∀ (i : Fin n✝), ArithPart₁ (g✝ i)
a_ih✝¹ : Partrec' f✝
a_ih✝ : ∀ (i : Fin n✝), Partrec' (g✝ i)
⊢ Partrec' fun v => (mOfFn fun i => g✝ i v) >>= f✝

case rfind
n : ℕ
f : Vector ℕ n →. ℕ
n✝ : ℕ
f✝ : Vector ℕ (n✝ + 1) → ℕ
a✝ : ArithPart₁ ↑f✝
a_ih✝ : Partrec' ↑f✝
⊢ Partrec' fun v => Nat.rfind fun n => Part.some (decide (f✝ (n ::ᵥ v) = 0))

State before:
n : ℕ
f : Vector ℕ n →. ℕ
n✝ : ℕ
⊢ Partrec' fun x => 0
Tactic:
case zero => exact Partrec'.of_part (Partrec.const' 0)
State after:
no goals

State before:
n : ℕ
f : Vector ℕ n →. ℕ
n✝ : ℕ
⊢ Partrec' fun x => 1
Tactic:
case one  => exact Partrec'.of_part (Partrec.const' 1)
State after:
no goals

State before:
n✝ : ℕ
f : Vector ℕ n✝ →. ℕ
n : ℕ
i j : Fin n
⊢ Partrec' ↑fun v => v.get i + v.get j
Tactic:
case add n i j =>
  exact (Partrec'.of_part ((Primrec.nat_add.comp
    (Primrec.vector_get.comp _root_.Primrec.id (_root_.Primrec.const i))
    (Primrec.vector_get.comp _root_.Primrec.id (_root_.Primrec.const j))).to_comp.partrec))
State after:
no goals

State before:
n✝ : ℕ
f : Vector ℕ n✝ →. ℕ
n : ℕ
i j : Fin n
⊢ Partrec' ↑fun v => v.get i * v.get j
Tactic:
case mul n i j =>
  exact (Partrec'.of_part ((Primrec.nat_mul.comp
    (Primrec.vector_get.comp _root_.Primrec.id (_root_.Primrec.const i))
    (Primrec.vector_get.comp _root_.Primrec.id (_root_.Primrec.const j))).to_comp.partrec))
State after:
no goals

State before:
n✝ : ℕ
f : Vector ℕ n✝ →. ℕ
n : ℕ
i : Fin n
⊢ Partrec' ↑fun v => v.get i
Tactic:
case proj n i =>
  exact Partrec'.of_part
    (Primrec.vector_get.comp _root_.Primrec.id (_root_.Primrec.const i)).to_comp.partrec
State after:
no goals

State before:
n✝ : ℕ
f : Vector ℕ n✝ →. ℕ
n : ℕ
i j : Fin n
⊢ Partrec' ↑fun v => (v.get i).isEqNat (v.get j)
Tactic:
case equal n i j =>
  have : Primrec (fun (v : Vector ℕ n) => if v.get i = v.get j then 1 else 0) :=
    Primrec.ite
      (Primrec.eq.comp
        (Primrec.vector_get.comp _root_.Primrec.id (_root_.Primrec.const i))
        (Primrec.vector_get.comp _root_.Primrec.id (_root_.Primrec.const j)))
      (_root_.Primrec.const 1)
      (_root_.Primrec.const 0)
  exact Partrec'.of_part this.to_comp.partrec
State after:
no goals

State before:
n✝ : ℕ
f : Vector ℕ n✝ →. ℕ
n : ℕ
i j : Fin n
⊢ Partrec' ↑fun v => (v.get i).isLtNat (v.get j)
Tactic:
case lt n i j =>
  have : Primrec (fun (v : Vector ℕ n) => if v.get i < v.get j then 1 else 0) :=
    Primrec.ite
      (Primrec.nat_lt.comp
        (Primrec.vector_get.comp _root_.Primrec.id (_root_.Primrec.const i))
        (Primrec.vector_get.comp _root_.Primrec.id (_root_.Primrec.const j)))
      (_root_.Primrec.const 1)
      (_root_.Primrec.const 0)
  exact Partrec'.of_part this.to_comp.partrec
State after:
no goals

State before:
n✝ : ℕ
f✝ : Vector ℕ n✝ →. ℕ
m n : ℕ
f : Vector ℕ n →. ℕ
g : Fin n → Vector ℕ m →. ℕ
a✝¹ : ArithPart₁ f
a✝ : ∀ (i : Fin n), ArithPart₁ (g i)
hf : Partrec' f
hg : ∀ (i : Fin n), Partrec' (g i)
⊢ Partrec' fun v => (mOfFn fun i => g i v) >>= f
Tactic:
case comp m n f g _ _ hf hg =>
  exact Partrec'.comp g hf hg
State after:
no goals

State before:
n : ℕ
f✝ : Vector ℕ n →. ℕ
n✝ : ℕ
f : Vector ℕ (n✝ + 1) → ℕ
a✝ : ArithPart₁ ↑f
hf : Partrec' ↑f
⊢ Partrec' fun v => Nat.rfind fun n => Part.some (decide (f (n ::ᵥ v) = 0))
Tactic:
case rfind f _ hf =>
  exact Partrec'.rfind hf
State after:
no goals

State before:
n : ℕ
f : Vector ℕ n →. ℕ
n✝ : ℕ
⊢ Partrec' fun x => 0
Tactic:
exact Partrec'.of_part (Partrec.const' 0)
State after:
no goals

State before:
n : ℕ
f : Vector ℕ n →. ℕ
n✝ : ℕ
⊢ Partrec' fun x => 1
Tactic:
exact Partrec'.of_part (Partrec.const' 1)
State after:
no goals

State before:
n✝ : ℕ
f : Vector ℕ n✝ →. ℕ
n : ℕ
i j : Fin n
⊢ Partrec' ↑fun v => v.get i + v.get j
Tactic:
exact (Partrec'.of_part ((Primrec.nat_add.comp
  (Primrec.vector_get.comp _root_.Primrec.id (_root_.Primrec.const i))
  (Primrec.vector_get.comp _root_.Primrec.id (_root_.Primrec.const j))).to_comp.partrec))
State after:
no goals

State before:
n✝ : ℕ
f : Vector ℕ n✝ →. ℕ
n : ℕ
i j : Fin n
⊢ Partrec' ↑fun v => v.get i * v.get j
Tactic:
exact (Partrec'.of_part ((Primrec.nat_mul.comp
  (Primrec.vector_get.comp _root_.Primrec.id (_root_.Primrec.const i))
  (Primrec.vector_get.comp _root_.Primrec.id (_root_.Primrec.const j))).to_comp.partrec))
State after:
no goals

State before:
n✝ : ℕ
f : Vector ℕ n✝ →. ℕ
n : ℕ
i : Fin n
⊢ Partrec' ↑fun v => v.get i
Tactic:
exact Partrec'.of_part
  (Primrec.vector_get.comp _root_.Primrec.id (_root_.Primrec.const i)).to_comp.partrec
State after:
no goals

State before:
n✝ : ℕ
f : Vector ℕ n✝ →. ℕ
n : ℕ
i j : Fin n
⊢ Partrec' ↑fun v => (v.get i).isEqNat (v.get j)
Tactic:
have : Primrec (fun (v : Vector ℕ n) => if v.get i = v.get j then 1 else 0) :=
  Primrec.ite
    (Primrec.eq.comp
      (Primrec.vector_get.comp _root_.Primrec.id (_root_.Primrec.const i))
      (Primrec.vector_get.comp _root_.Primrec.id (_root_.Primrec.const j)))
    (_root_.Primrec.const 1)
    (_root_.Primrec.const 0)
State after:
n✝ : ℕ
f : Vector ℕ n✝ →. ℕ
n : ℕ
i j : Fin n
this : Primrec fun v => if v.get i = v.get j then 1 else 0
⊢ Partrec' ↑fun v => (v.get i).isEqNat (v.get j)

State before:
n✝ : ℕ
f : Vector ℕ n✝ →. ℕ
n : ℕ
i j : Fin n
this : Primrec fun v => if v.get i = v.get j then 1 else 0
⊢ Partrec' ↑fun v => (v.get i).isEqNat (v.get j)
Tactic:
exact Partrec'.of_part this.to_comp.partrec
State after:
no goals

State before:
n✝ : ℕ
f : Vector ℕ n✝ →. ℕ
n : ℕ
i j : Fin n
⊢ Partrec' ↑fun v => (v.get i).isLtNat (v.get j)
Tactic:
have : Primrec (fun (v : Vector ℕ n) => if v.get i < v.get j then 1 else 0) :=
  Primrec.ite
    (Primrec.nat_lt.comp
      (Primrec.vector_get.comp _root_.Primrec.id (_root_.Primrec.const i))
      (Primrec.vector_get.comp _root_.Primrec.id (_root_.Primrec.const j)))
    (_root_.Primrec.const 1)
    (_root_.Primrec.const 0)
State after:
n✝ : ℕ
f : Vector ℕ n✝ →. ℕ
n : ℕ
i j : Fin n
this : Primrec fun v => if v.get i < v.get j then 1 else 0
⊢ Partrec' ↑fun v => (v.get i).isLtNat (v.get j)

State before:
n✝ : ℕ
f : Vector ℕ n✝ →. ℕ
n : ℕ
i j : Fin n
this : Primrec fun v => if v.get i < v.get j then 1 else 0
⊢ Partrec' ↑fun v => (v.get i).isLtNat (v.get j)
Tactic:
exact Partrec'.of_part this.to_comp.partrec
State after:
no goals

State before:
n✝ : ℕ
f✝ : Vector ℕ n✝ →. ℕ
m n : ℕ
f : Vector ℕ n →. ℕ
g : Fin n → Vector ℕ m →. ℕ
a✝¹ : ArithPart₁ f
a✝ : ∀ (i : Fin n), ArithPart₁ (g i)
hf : Partrec' f
hg : ∀ (i : Fin n), Partrec' (g i)
⊢ Partrec' fun v => (mOfFn fun i => g i v) >>= f
Tactic:
exact Partrec'.comp g hf hg
State after:
no goals

State before:
n : ℕ
f✝ : Vector ℕ n →. ℕ
n✝ : ℕ
f : Vector ℕ (n✝ + 1) → ℕ
a✝ : ArithPart₁ ↑f
hf : Partrec' ↑f
⊢ Partrec' fun v => Nat.rfind fun n => Part.some (decide (f (n ::ᵥ v) = 0))
Tactic:
exact Partrec'.rfind hf
State after:
no goals