Theorem: Nat.Arith₁.of_primrec (Logic/Vorspiel/Arith.lean)

State before:
n : ℕ
f : Vector ℕ n → ℕ
hf : Primrec' f
⊢ Arith₁ f
Tactic:
induction hf
State after:
case zero
n : ℕ
f : Vector ℕ n → ℕ
⊢ Arith₁ fun x => 0

case succ
n : ℕ
f : Vector ℕ n → ℕ
⊢ Arith₁ fun v => v.head.succ

case get
n : ℕ
f : Vector ℕ n → ℕ
n✝ : ℕ
i✝ : Fin n✝
⊢ Arith₁ fun v => v.get i✝

case comp
n : ℕ
f : Vector ℕ n → ℕ
m✝ n✝ : ℕ
f✝ : Vector ℕ n✝ → ℕ
g✝ : Fin n✝ → Vector ℕ m✝ → ℕ
a✝¹ : Primrec' f✝
a✝ : ∀ (i : Fin n✝), Primrec' (g✝ i)
a_ih✝¹ : Arith₁ f✝
a_ih✝ : ∀ (i : Fin n✝), Arith₁ (g✝ i)
⊢ Arith₁ fun a => f✝ (ofFn fun i => g✝ i a)

case prec
n : ℕ
f : Vector ℕ n → ℕ
n✝ : ℕ
f✝ : Vector ℕ n✝ → ℕ
g✝ : Vector ℕ (n✝ + 2) → ℕ
a✝¹ : Primrec' f✝
a✝ : Primrec' g✝
a_ih✝¹ : Arith₁ f✝
a_ih✝ : Arith₁ g✝
⊢ Arith₁ fun v => rec (f✝ v.tail) (fun y IH => g✝ (y ::ᵥ IH ::ᵥ v.tail)) v.head

State before:
n : ℕ
f : Vector ℕ n → ℕ
⊢ Arith₁ fun x => 0
Tactic:
case zero               => exact zero
State after:
no goals

State before:
n : ℕ
f : Vector ℕ n → ℕ
⊢ Arith₁ fun v => v.head.succ
Tactic:
case succ               => exact (@succ 1 0).of_eq (by simp)
State after:
no goals

State before:
n : ℕ
f : Vector ℕ n → ℕ
n✝ : ℕ
i : Fin n✝
⊢ Arith₁ fun v => v.get i
Tactic:
case get i              => exact proj i
State after:
no goals

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

State before:
n : ℕ
f✝ : Vector ℕ n → ℕ
n✝ : ℕ
f : Vector ℕ n✝ → ℕ
g : Vector ℕ (n✝ + 2) → ℕ
a✝¹ : Primrec' f
a✝ : Primrec' g
hf : Arith₁ f
hg : Arith₁ g
⊢ Arith₁ fun v => rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) v.head
Tactic:
case prec f g _ _ hf hg => exact hf.prec hg
State after:
no goals

State before:
n : ℕ
f : Vector ℕ n → ℕ
⊢ Arith₁ fun x => 0
Tactic:
exact zero
State after:
no goals

State before:
n : ℕ
f : Vector ℕ n → ℕ
⊢ Arith₁ fun v => v.head.succ
Tactic:
exact (@succ 1 0).of_eq (by simp)
State after:
no goals

State before:
n : ℕ
f : Vector ℕ n → ℕ
⊢ ∀ (i : Vector ℕ 1), i.get 0 + 1 = i.head.succ
Tactic:
simp
State after:
no goals

State before:
n : ℕ
f : Vector ℕ n → ℕ
n✝ : ℕ
i : Fin n✝
⊢ Arith₁ fun v => v.get i
Tactic:
exact proj i
State after:
no goals

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

State before:
n : ℕ
f✝ : Vector ℕ n → ℕ
n✝ : ℕ
f : Vector ℕ n✝ → ℕ
g : Vector ℕ (n✝ + 2) → ℕ
a✝¹ : Primrec' f
a✝ : Primrec' g
hf : Arith₁ f
hg : Arith₁ g
⊢ Arith₁ fun v => rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) v.head
Tactic:
exact hf.prec hg
State after:
no goals