internlm/Lean-Github huggingface dataset:
Theorem: Nat.Arith₁.ball
Proof state before:
n : ℕ
p : Vector ℕ n → ℕ → ℕ
hp : Arith₁ fun v => p v.tail v.head
i : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (p v.tail v.head).inv.or ((v.get i.succ).isLeNat v.head)
hF : Arith₁ F
this✝ : Arith₁ fun v => v.head.isEqNat (v.get i.succ)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isEqNat (v.get i)) v) (rfind fun n_1 => Part.some (decide (0 < F (n_1 ::ᵥ v))))
v : Vector ℕ n
H : ¬∀ m < v.get i, 0 < p v m
x : ℕ
hx : x < v.get i
hpx : p v x = 0
hlx : ∀ y < x, p v y ≠ 0
⊢ ∀ {m : ℕ}, m < x → false = (decide (p v m = 0) || decide (v.get i ≤ m))
Tactic:
intro m hm
Proof state after:
n : ℕ
p : Vector ℕ n → ℕ → ℕ
hp : Arith₁ fun v => p v.tail v.head
i : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (p v.tail v.head).inv.or ((v.get i.succ).isLeNat v.head)
hF : Arith₁ F
this✝ : Arith₁ fun v => v.head.isEqNat (v.get i.succ)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isEqNat (v.get i)) v) (rfind fun n_1 => Part.some (decide (0 < F (n_1 ::ᵥ v))))
v : Vector ℕ n
H : ¬∀ m < v.get i, 0 < p v m
x : ℕ
hx : x < v.get i
hpx : p v x = 0
hlx : ∀ y < x, p v y ≠ 0
m : ℕ
hm : m < x
⊢ false = (decide (p v m = 0) || decide (v.get i ≤ m))
Theorem: Nat.Arith₁.ball
Proof state before:
n : ℕ
p : Vector ℕ n → ℕ → ℕ
hp : Arith₁ fun v => p v.tail v.head
i : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (p v.tail v.head).inv.or ((v.get i.succ).isLeNat v.head)
hF : Arith₁ F
this✝ : Arith₁ fun v => v.head.isEqNat (v.get i.succ)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isEqNat (v.get i)) v) (rfind fun n_1 => Part.some (decide (0 < F (n_1 ::ᵥ v))))
v : Vector ℕ n
H : ¬∀ m < v.get i, 0 < p v m
x : ℕ
hx : x < v.get i
hpx : p v x = 0
hlx : ∀ y < x, p v y ≠ 0
m : ℕ
hm : m < x
⊢ false = (decide (p v m = 0) || decide (v.get i ≤ m))
Tactic:
symm
Proof state after:
n : ℕ
p : Vector ℕ n → ℕ → ℕ
hp : Arith₁ fun v => p v.tail v.head
i : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (p v.tail v.head).inv.or ((v.get i.succ).isLeNat v.head)
hF : Arith₁ F
this✝ : Arith₁ fun v => v.head.isEqNat (v.get i.succ)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isEqNat (v.get i)) v) (rfind fun n_1 => Part.some (decide (0 < F (n_1 ::ᵥ v))))
v : Vector ℕ n
H : ¬∀ m < v.get i, 0 < p v m
x : ℕ
hx : x < v.get i
hpx : p v x = 0
hlx : ∀ y < x, p v y ≠ 0
m : ℕ
hm : m < x
⊢ (decide (p v m = 0) || decide (v.get i ≤ m)) = false
Theorem: Nat.Arith₁.ball
Proof state before:
n : ℕ
p : Vector ℕ n → ℕ → ℕ
hp : Arith₁ fun v => p v.tail v.head
i : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (p v.tail v.head).inv.or ((v.get i.succ).isLeNat v.head)
hF : Arith₁ F
this✝ : Arith₁ fun v => v.head.isEqNat (v.get i.succ)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isEqNat (v.get i)) v) (rfind fun n_1 => Part.some (decide (0 < F (n_1 ::ᵥ v))))
v : Vector ℕ n
H : ¬∀ m < v.get i, 0 < p v m
x : ℕ
hx : x < v.get i
hpx : p v x = 0
hlx : ∀ y < x, p v y ≠ 0
m : ℕ
hm : m < x
⊢ (decide (p v m = 0) || decide (v.get i ≤ m)) = false
Tactic:
simp[hlx m hm, lt_trans hm hx]
Proof state after:
no goals
Theorem: Nat.Arith₁.ball
Proof state before:
n : ℕ
p : Vector ℕ n → ℕ → ℕ
hp : Arith₁ fun v => p v.tail v.head
i : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (p v.tail v.head).inv.or ((v.get i.succ).isLeNat v.head)
hF : Arith₁ F
this✝ : Arith₁ fun v => v.head.isEqNat (v.get i.succ)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isEqNat (v.get i)) v) (rfind fun n_1 => Part.some (decide (0 < F (n_1 ::ᵥ v))))
v : Vector ℕ n
H : ¬∀ m < v.get i, 0 < p v m
x : ℕ
hx : x < v.get i
hpx : p v x = 0
hlx : ∀ y < x, p v y ≠ 0
⊢ x.isEqNat (v.get i) = (v.get i).ball (p v)
Tactic:
have : isEqNat x (v.get i) = 0 := by simp[isEqNat, imp_false]; exact ne_of_lt hx
Proof state after:
n : ℕ
p : Vector ℕ n → ℕ → ℕ
hp : Arith₁ fun v => p v.tail v.head
i : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (p v.tail v.head).inv.or ((v.get i.succ).isLeNat v.head)
hF : Arith₁ F
this✝¹ : Arith₁ fun v => v.head.isEqNat (v.get i.succ)
this✝ :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isEqNat (v.get i)) v) (rfind fun n_1 => Part.some (decide (0 < F (n_1 ::ᵥ v))))
v : Vector ℕ n
H : ¬∀ m < v.get i, 0 < p v m
x : ℕ
hx : x < v.get i
hpx : p v x = 0
hlx : ∀ y < x, p v y ≠ 0
this : x.isEqNat (v.get i) = 0
⊢ x.isEqNat (v.get i) = (v.get i).ball (p v)
Theorem: Nat.Arith₁.ball
Proof state before:
n : ℕ
p : Vector ℕ n → ℕ → ℕ
hp : Arith₁ fun v => p v.tail v.head
i : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (p v.tail v.head).inv.or ((v.get i.succ).isLeNat v.head)
hF : Arith₁ F
this✝¹ : Arith₁ fun v => v.head.isEqNat (v.get i.succ)
this✝ :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isEqNat (v.get i)) v) (rfind fun n_1 => Part.some (decide (0 < F (n_1 ::ᵥ v))))
v : Vector ℕ n
H : ¬∀ m < v.get i, 0 < p v m
x : ℕ
hx : x < v.get i
hpx : p v x = 0
hlx : ∀ y < x, p v y ≠ 0
this : x.isEqNat (v.get i) = 0
⊢ x.isEqNat (v.get i) = (v.get i).ball (p v)
Tactic:
simp[this]
Proof state after:
n : ℕ
p : Vector ℕ n → ℕ → ℕ
hp : Arith₁ fun v => p v.tail v.head
i : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (p v.tail v.head).inv.or ((v.get i.succ).isLeNat v.head)
hF : Arith₁ F
this✝¹ : Arith₁ fun v => v.head.isEqNat (v.get i.succ)
this✝ :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isEqNat (v.get i)) v) (rfind fun n_1 => Part.some (decide (0 < F (n_1 ::ᵥ v))))
v : Vector ℕ n
H : ¬∀ m < v.get i, 0 < p v m
x : ℕ
hx : x < v.get i
hpx : p v x = 0
hlx : ∀ y < x, p v y ≠ 0
this : x.isEqNat (v.get i) = 0
⊢ 0 = (v.get i).ball (p v)
Theorem: Nat.Arith₁.ball
Proof state before:
n : ℕ
p : Vector ℕ n → ℕ → ℕ
hp : Arith₁ fun v => p v.tail v.head
i : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (p v.tail v.head).inv.or ((v.get i.succ).isLeNat v.head)
hF : Arith₁ F
this✝¹ : Arith₁ fun v => v.head.isEqNat (v.get i.succ)
this✝ :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isEqNat (v.get i)) v) (rfind fun n_1 => Part.some (decide (0 < F (n_1 ::ᵥ v))))
v : Vector ℕ n
H : ¬∀ m < v.get i, 0 < p v m
x : ℕ
hx : x < v.get i
hpx : p v x = 0
hlx : ∀ y < x, p v y ≠ 0
this : x.isEqNat (v.get i) = 0
⊢ 0 = (v.get i).ball (p v)
Tactic:
symm
Proof state after:
n : ℕ
p : Vector ℕ n → ℕ → ℕ
hp : Arith₁ fun v => p v.tail v.head
i : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (p v.tail v.head).inv.or ((v.get i.succ).isLeNat v.head)
hF : Arith₁ F
this✝¹ : Arith₁ fun v => v.head.isEqNat (v.get i.succ)
this✝ :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isEqNat (v.get i)) v) (rfind fun n_1 => Part.some (decide (0 < F (n_1 ::ᵥ v))))
v : Vector ℕ n
H : ¬∀ m < v.get i, 0 < p v m
x : ℕ
hx : x < v.get i
hpx : p v x = 0
hlx : ∀ y < x, p v y ≠ 0
this : x.isEqNat (v.get i) = 0
⊢ (v.get i).ball (p v) = 0
Theorem: Nat.Arith₁.ball
Proof state before:
n : ℕ
p : Vector ℕ n → ℕ → ℕ
hp : Arith₁ fun v => p v.tail v.head
i : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (p v.tail v.head).inv.or ((v.get i.succ).isLeNat v.head)
hF : Arith₁ F
this✝¹ : Arith₁ fun v => v.head.isEqNat (v.get i.succ)
this✝ :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isEqNat (v.get i)) v) (rfind fun n_1 => Part.some (decide (0 < F (n_1 ::ᵥ v))))
v : Vector ℕ n
H : ¬∀ m < v.get i, 0 < p v m
x : ℕ
hx : x < v.get i
hpx : p v x = 0
hlx : ∀ y < x, p v y ≠ 0
this : x.isEqNat (v.get i) = 0
⊢ (v.get i).ball (p v) = 0
Tactic:
simp
Proof state after:
n : ℕ
p : Vector ℕ n → ℕ → ℕ
hp : Arith₁ fun v => p v.tail v.head
i : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (p v.tail v.head).inv.or ((v.get i.succ).isLeNat v.head)
hF : Arith₁ F
this✝¹ : Arith₁ fun v => v.head.isEqNat (v.get i.succ)
this✝ :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isEqNat (v.get i)) v) (rfind fun n_1 => Part.some (decide (0 < F (n_1 ::ᵥ v))))
v : Vector ℕ n
H : ¬∀ m < v.get i, 0 < p v m
x : ℕ
hx : x < v.get i
hpx : p v x = 0
hlx : ∀ y < x, p v y ≠ 0
this : x.isEqNat (v.get i) = 0
⊢ ∃ m < v.get i, p v m = 0
Theorem: Nat.Arith₁.ball
Proof state before:
n : ℕ
p : Vector ℕ n → ℕ → ℕ
hp : Arith₁ fun v => p v.tail v.head
i : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (p v.tail v.head).inv.or ((v.get i.succ).isLeNat v.head)
hF : Arith₁ F
this✝¹ : Arith₁ fun v => v.head.isEqNat (v.get i.succ)
this✝ :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isEqNat (v.get i)) v) (rfind fun n_1 => Part.some (decide (0 < F (n_1 ::ᵥ v))))
v : Vector ℕ n
H : ¬∀ m < v.get i, 0 < p v m
x : ℕ
hx : x < v.get i
hpx : p v x = 0
hlx : ∀ y < x, p v y ≠ 0
this : x.isEqNat (v.get i) = 0
⊢ ∃ m < v.get i, p v m = 0
Tactic:
exact ⟨x, hx, hpx⟩
Proof state after:
no goals
Theorem: Nat.Arith₁.ball
Proof state before:
n : ℕ
p : Vector ℕ n → ℕ → ℕ
hp : Arith₁ fun v => p v.tail v.head
i : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (p v.tail v.head).inv.or ((v.get i.succ).isLeNat v.head)
hF : Arith₁ F
this✝ : Arith₁ fun v => v.head.isEqNat (v.get i.succ)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isEqNat (v.get i)) v) (rfind fun n_1 => Part.some (decide (0 < F (n_1 ::ᵥ v))))
v : Vector ℕ n
H : ¬∀ m < v.get i, 0 < p v m
x : ℕ
hx : x < v.get i
hpx : p v x = 0
hlx : ∀ y < x, p v y ≠ 0
⊢ x.isEqNat (v.get i) = 0
Tactic:
simp[isEqNat, imp_false]
Proof state after:
n : ℕ
p : Vector ℕ n → ℕ → ℕ
hp : Arith₁ fun v => p v.tail v.head
i : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (p v.tail v.head).inv.or ((v.get i.succ).isLeNat v.head)
hF : Arith₁ F
this✝ : Arith₁ fun v => v.head.isEqNat (v.get i.succ)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isEqNat (v.get i)) v) (rfind fun n_1 => Part.some (decide (0 < F (n_1 ::ᵥ v))))
v : Vector ℕ n
H : ¬∀ m < v.get i, 0 < p v m
x : ℕ
hx : x < v.get i
hpx : p v x = 0
hlx : ∀ y < x, p v y ≠ 0
⊢ ¬x = v.get i
Theorem: Nat.Arith₁.ball
Proof state before:
n : ℕ
p : Vector ℕ n → ℕ → ℕ
hp : Arith₁ fun v => p v.tail v.head
i : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (p v.tail v.head).inv.or ((v.get i.succ).isLeNat v.head)
hF : Arith₁ F
this✝ : Arith₁ fun v => v.head.isEqNat (v.get i.succ)
this :
  ArithPart₁ fun v =>
    Part.map ((fun v x => x.isEqNat (v.get i)) v) (rfind fun n_1 => Part.some (decide (0 < F (n_1 ::ᵥ v))))
v : Vector ℕ n
H : ¬∀ m < v.get i, 0 < p v m
x : ℕ
hx : x < v.get i
hpx : p v x = 0
hlx : ∀ y < x, p v y ≠ 0
⊢ ¬x = v.get i
Tactic:
exact ne_of_lt hx
Proof state after:
no goals
Theorem: Nat.Arith₁.beta_unbeta_recSequence_eq
Proof state before:
n : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ (n + 2) → ℕ
z : ℕ
v : Vector ℕ n
m : ℕ
hm : m < z + 1
⊢ (unbeta (recSequence f g z v)).beta m = rec (f v) (fun y IH => g (y ::ᵥ IH ::ᵥ v)) m
Tactic:
have := Nat.beta_unbeta_coe (recSequence f g z v) ⟨m, by simp[recSequence, hm]⟩
Proof state after:
n : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ (n + 2) → ℕ
z : ℕ
v : Vector ℕ n
m : ℕ
hm : m < z + 1
this : (unbeta (recSequence f g z v)).beta ↑⟨m, ⋯⟩ = (recSequence f g z v).get ⟨m, ⋯⟩
⊢ (unbeta (recSequence f g z v)).beta m = rec (f v) (fun y IH => g (y ::ᵥ IH ::ᵥ v)) m
Theorem: Nat.Arith₁.beta_unbeta_recSequence_eq
Proof state before:
n : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ (n + 2) → ℕ
z : ℕ
v : Vector ℕ n
m : ℕ
hm : m < z + 1
this : (unbeta (recSequence f g z v)).beta ↑⟨m, ⋯⟩ = (recSequence f g z v).get ⟨m, ⋯⟩
⊢ (unbeta (recSequence f g z v)).beta m = rec (f v) (fun y IH => g (y ::ᵥ IH ::ᵥ v)) m
Tactic:
simp at this
Proof state after:
n : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ (n + 2) → ℕ
z : ℕ
v : Vector ℕ n
m : ℕ
hm : m < z + 1
this : (unbeta (recSequence f g z v)).beta m = (recSequence f g z v).get ⟨m, ⋯⟩
⊢ (unbeta (recSequence f g z v)).beta m = rec (f v) (fun y IH => g (y ::ᵥ IH ::ᵥ v)) m
Theorem: Nat.Arith₁.beta_unbeta_recSequence_eq
Proof state before:
n : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ (n + 2) → ℕ
z : ℕ
v : Vector ℕ n
m : ℕ
hm : m < z + 1
this : (unbeta (recSequence f g z v)).beta m = (recSequence f g z v).get ⟨m, ⋯⟩
⊢ (unbeta (recSequence f g z v)).beta m = rec (f v) (fun y IH => g (y ::ᵥ IH ::ᵥ v)) m
Tactic:
rw[this]
Proof state after:
n : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ (n + 2) → ℕ
z : ℕ
v : Vector ℕ n
m : ℕ
hm : m < z + 1
this : (unbeta (recSequence f g z v)).beta m = (recSequence f g z v).get ⟨m, ⋯⟩
⊢ (recSequence f g z v).get ⟨m, ⋯⟩ = rec (f v) (fun y IH => g (y ::ᵥ IH ::ᵥ v)) m
Theorem: Nat.Arith₁.beta_unbeta_recSequence_eq
Proof state before:
n : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ (n + 2) → ℕ
z : ℕ
v : Vector ℕ n
m : ℕ
hm : m < z + 1
this : (unbeta (recSequence f g z v)).beta m = (recSequence f g z v).get ⟨m, ⋯⟩
⊢ (recSequence f g z v).get ⟨m, ⋯⟩ = rec (f v) (fun y IH => g (y ::ᵥ IH ::ᵥ v)) m
Tactic:
simp[recSequence]
Proof state after:
no goals
Theorem: Nat.Arith₁.beta_unbeta_recSequence_eq
Proof state before:
n : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ (n + 2) → ℕ
z : ℕ
v : Vector ℕ n
m : ℕ
hm : m < z + 1
⊢ m < (recSequence f g z v).length
Tactic:
simp[recSequence, hm]
Proof state after:
no goals
Theorem: Nat.Arith₁.beta_unbeta_recSequence_zero
Proof state before:
n : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ (n + 2) → ℕ
z : ℕ
v : Vector ℕ n
⊢ (unbeta (recSequence f g z v)).beta 0 = f v
Tactic:
simpa using beta_unbeta_recSequence_eq f g z v 0 (inv_iff_ne_zero.mp rfl)
Proof state after:
no goals
Theorem: Nat.Arith₁.beta_unbeta_recSequence_succ
Proof state before:
n : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ (n + 2) → ℕ
z : ℕ
v : Vector ℕ n
m : ℕ
hm : m < z
⊢ (unbeta (recSequence f g z v)).beta (m + 1) = g (m ::ᵥ (unbeta (recSequence f g z v)).beta m ::ᵥ v)
Tactic:
rw [beta_unbeta_recSequence_eq f g z v m (Nat.lt_add_right 1 hm),
  beta_unbeta_recSequence_eq f g z v (m + 1) (Nat.add_lt_add_right hm 1)]
Proof state after:
no goals
Theorem: Nat.Arith₁.beta_eq_rec
Proof state before:
n m : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ (n + 2) → ℕ
z : ℕ
v : Vector ℕ n
h0 : z.beta 0 = f v
hs : ∀ i < m, z.beta (i + 1) = g (i ::ᵥ z.beta i ::ᵥ v)
⊢ z.beta m = rec (f v) (fun y IH => g (y ::ᵥ IH ::ᵥ v)) m
Tactic:
induction' m with m ih <;> simp[h0]
Proof state after:
case succ
n : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ (n + 2) → ℕ
z : ℕ
v : Vector ℕ n
h0 : z.beta 0 = f v
m : ℕ
ih : (∀ i < m, z.beta (i + 1) = g (i ::ᵥ z.beta i ::ᵥ v)) → z.beta m = rec (f v) (fun y IH => g (y ::ᵥ IH ::ᵥ v)) m
hs : ∀ i < m + 1, z.beta (i + 1) = g (i ::ᵥ z.beta i ::ᵥ v)
⊢ z.beta (m + 1) = g (m ::ᵥ rec (f v) (fun y IH => g (y ::ᵥ IH ::ᵥ v)) m ::ᵥ v)
Theorem: Nat.Arith₁.beta_eq_rec
Proof state before:
case succ
n : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ (n + 2) → ℕ
z : ℕ
v : Vector ℕ n
h0 : z.beta 0 = f v
m : ℕ
ih : (∀ i < m, z.beta (i + 1) = g (i ::ᵥ z.beta i ::ᵥ v)) → z.beta m = rec (f v) (fun y IH => g (y ::ᵥ IH ::ᵥ v)) m
hs : ∀ i < m + 1, z.beta (i + 1) = g (i ::ᵥ z.beta i ::ᵥ v)
⊢ z.beta (m + 1) = g (m ::ᵥ rec (f v) (fun y IH => g (y ::ᵥ IH ::ᵥ v)) m ::ᵥ v)
Tactic:
rw[hs m (lt.base m), ←ih (fun i hi => hs i (lt.step hi))]
Proof state after:
no goals
Theorem: Nat.Arith₁.prec
Proof state before:
n : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ (n + 2) → ℕ
hf : Arith₁ f
hg : Arith₁ g
⊢ Arith₁ fun v => rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) v.head
Tactic:
let F : Vector ℕ (n + 2) → ℕ := fun v =>
  (isEqNat (Nat.beta v.head 0) (f v.tail.tail)).and
  (Nat.ball v.tail.head $ fun i => isEqNat (Nat.beta v.head (i + 1)) (g (i ::ᵥ Nat.beta v.head i ::ᵥ v.tail.tail)))
Proof state after:
n : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ (n + 2) → ℕ
hf : Arith₁ f
hg : Arith₁ g
F : Vector ℕ (n + 2) → ℕ :=
  fun v =>
    ((v.head.beta 0).isEqNat (f v.tail.tail)).and
      (v.tail.head.ball fun i => (v.head.beta (i + 1)).isEqNat (g (i ::ᵥ v.head.beta i ::ᵥ v.tail.tail)))
⊢ Arith₁ fun v => rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) v.head
Theorem: Nat.Arith₁.prec
Proof state before:
n : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ (n + 2) → ℕ
hf : Arith₁ f
hg : Arith₁ g
F : Vector ℕ (n + 2) → ℕ :=
  fun v =>
    ((v.head.beta 0).isEqNat (f v.tail.tail)).and
      (v.tail.head.ball fun i => (v.head.beta (i + 1)).isEqNat (g (i ::ᵥ v.head.beta i ::ᵥ v.tail.tail)))
⊢ Arith₁ fun v => rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) v.head
Tactic:
have hp : @Arith₁ (n + 3) (fun v =>
  isEqNat (Nat.beta v.tail.head (v.head + 1))
  (g (v.head ::ᵥ Nat.beta v.tail.head v.head ::ᵥ v.tail.tail.tail))) :=
  (equal 0 1).comp₂ _
    ((beta 0 1).comp₂ _ head.tail ((succ 0).comp₁ _ head))
    (hg.comp' $ head.cons $ ((beta 0 1).comp₂ _ head.tail head).cons $ by intro i; simp; exact proj _)
Proof state after:
n : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ (n + 2) → ℕ
hf : Arith₁ f
hg : Arith₁ g
F : Vector ℕ (n + 2) → ℕ :=
  fun v =>
    ((v.head.beta 0).isEqNat (f v.tail.tail)).and
      (v.tail.head.ball fun i => (v.head.beta (i + 1)).isEqNat (g (i ::ᵥ v.head.beta i ::ᵥ v.tail.tail)))
hp :
  Arith₁ fun v => (v.tail.head.beta (v.head + 1)).isEqNat (g (v.head ::ᵥ v.tail.head.beta v.head ::ᵥ v.tail.tail.tail))
⊢ Arith₁ fun v => rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) v.head
Theorem: Nat.Arith₁.prec
Proof state before:
n : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ (n + 2) → ℕ
hf : Arith₁ f
hg : Arith₁ g
F : Vector ℕ (n + 2) → ℕ :=
  fun v =>
    ((v.head.beta 0).isEqNat (f v.tail.tail)).and
      (v.tail.head.ball fun i => (v.head.beta (i + 1)).isEqNat (g (i ::ᵥ v.head.beta i ::ᵥ v.tail.tail)))
hp :
  Arith₁ fun v => (v.tail.head.beta (v.head + 1)).isEqNat (g (v.head ::ᵥ v.tail.head.beta v.head ::ᵥ v.tail.tail.tail))
⊢ Arith₁ fun v => rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) v.head
Tactic:
have hF : Arith₁ F := (and 0 1).comp₂ _
  ((equal 0 1).comp₂ _ ((beta 0 1).comp₂ _ head zero) hf.tail.tail)
  ((@ball (n + 2) (fun v i =>
    isEqNat (Nat.beta v.head (i + 1)) (g (i ::ᵥ Nat.beta v.head i ::ᵥ v.tail.tail))) hp 1).of_eq $ by
      simp[Vector.get_one])
Proof state after:
n : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ (n + 2) → ℕ
hf : Arith₁ f
hg : Arith₁ g
F : Vector ℕ (n + 2) → ℕ :=
  fun v =>
    ((v.head.beta 0).isEqNat (f v.tail.tail)).and
      (v.tail.head.ball fun i => (v.head.beta (i + 1)).isEqNat (g (i ::ᵥ v.head.beta i ::ᵥ v.tail.tail)))
hp :
  Arith₁ fun v => (v.tail.head.beta (v.head + 1)).isEqNat (g (v.head ::ᵥ v.tail.head.beta v.head ::ᵥ v.tail.tail.tail))
hF : Arith₁ F
⊢ Arith₁ fun v => rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) v.head
Theorem: Nat.Arith₁.prec
Proof state before:
n : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ (n + 2) → ℕ
hf : Arith₁ f
hg : Arith₁ g
F : Vector ℕ (n + 2) → ℕ :=
  fun v =>
    ((v.head.beta 0).isEqNat (f v.tail.tail)).and
      (v.tail.head.ball fun i => (v.head.beta (i + 1)).isEqNat (g (i ::ᵥ v.head.beta i ::ᵥ v.tail.tail)))
hp :
  Arith₁ fun v => (v.tail.head.beta (v.head + 1)).isEqNat (g (v.head ::ᵥ v.tail.head.beta v.head ::ᵥ v.tail.tail.tail))
hF : Arith₁ F
⊢ Arith₁ fun v => rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) v.head
Tactic:
have : @Arith₁ (n + 2) (fun v => Nat.beta v.head v.tail.head) :=
  (beta 0 1).of_eq (by simp [Vector.get_one])
Proof state after:
n : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ (n + 2) → ℕ
hf : Arith₁ f
hg : Arith₁ g
F : Vector ℕ (n + 2) → ℕ :=
  fun v =>
    ((v.head.beta 0).isEqNat (f v.tail.tail)).and
      (v.tail.head.ball fun i => (v.head.beta (i + 1)).isEqNat (g (i ::ᵥ v.head.beta i ::ᵥ v.tail.tail)))
hp :
  Arith₁ fun v => (v.tail.head.beta (v.head + 1)).isEqNat (g (v.head ::ᵥ v.tail.head.beta v.head ::ᵥ v.tail.tail.tail))
hF : Arith₁ F
this : Arith₁ fun v => v.head.beta v.tail.head
⊢ Arith₁ fun v => rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) v.head
Theorem: Nat.Arith₁.prec
Proof state before:
n : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ (n + 2) → ℕ
hf : Arith₁ f
hg : Arith₁ g
F : Vector ℕ (n + 2) → ℕ :=
  fun v =>
    ((v.head.beta 0).isEqNat (f v.tail.tail)).and
      (v.tail.head.ball fun i => (v.head.beta (i + 1)).isEqNat (g (i ::ᵥ v.head.beta i ::ᵥ v.tail.tail)))
hp :
  Arith₁ fun v => (v.tail.head.beta (v.head + 1)).isEqNat (g (v.head ::ᵥ v.tail.head.beta v.head ::ᵥ v.tail.tail.tail))
hF : Arith₁ F
this : Arith₁ fun v => v.head.beta v.tail.head
⊢ Arith₁ fun v => rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) v.head
Tactic:
exact (ArithPart₁.map (fun v x => Nat.beta x v.head) this (ArithPart₁.rfindPos hF)).of_eq <| by
  intro v
  simp only [add_succ_sub_one, head_cons, tail_cons, and_pos_iff, isEqNat_pos_iff,
    ball_pos_iff, Bool.decide_and, PFun.coe_val, eq_some_iff, mem_map_iff, mem_rfind,
    mem_some_iff, F]
  suffices ∃ z : ℕ, z.beta 0 = f v.tail ∧ ∀ i < v.head, z.beta (i + 1) = g (i ::ᵥ z.beta i ::ᵥ v.tail) by
    rcases least_number _ this with ⟨z, ⟨hz0, hzs⟩, hzm⟩
    exact ⟨z, ⟨by symm; simp[hz0]; exact hzs,
      by intro m hm; symm; simpa[imp_iff_not_or, not_or] using hzm m hm⟩,
      beta_eq_rec f g hz0 hzs⟩
  let l : List ℕ := recSequence f g v.head v.tail
  exact ⟨unbeta l,
    beta_unbeta_recSequence_zero f g v.head v.tail,
    fun i hi => beta_unbeta_recSequence_succ f g v.head v.tail hi⟩
Proof state after:
no goals
Theorem: Nat.Arith₁.prec
Proof state before:
n : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ (n + 2) → ℕ
hf : Arith₁ f
hg : Arith₁ g
F : Vector ℕ (n + 2) → ℕ :=
  fun v =>
    ((v.head.beta 0).isEqNat (f v.tail.tail)).and
      (v.tail.head.ball fun i => (v.head.beta (i + 1)).isEqNat (g (i ::ᵥ v.head.beta i ::ᵥ v.tail.tail)))
⊢ Vec fun v => v.tail.tail.tail
Tactic:
intro i
Proof state after:
n : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ (n + 2) → ℕ
hf : Arith₁ f
hg : Arith₁ g
F : Vector ℕ (n + 2) → ℕ :=
  fun v =>
    ((v.head.beta 0).isEqNat (f v.tail.tail)).and
      (v.tail.head.ball fun i => (v.head.beta (i + 1)).isEqNat (g (i ::ᵥ v.head.beta i ::ᵥ v.tail.tail)))
i : Fin n
⊢ Arith₁ fun v => ((fun v => v.tail.tail.tail) v).get i
Theorem: Nat.Arith₁.prec
Proof state before:
n : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ (n + 2) → ℕ
hf : Arith₁ f
hg : Arith₁ g
F : Vector ℕ (n + 2) → ℕ :=
  fun v =>
    ((v.head.beta 0).isEqNat (f v.tail.tail)).and
      (v.tail.head.ball fun i => (v.head.beta (i + 1)).isEqNat (g (i ::ᵥ v.head.beta i ::ᵥ v.tail.tail)))
i : Fin n
⊢ Arith₁ fun v => ((fun v => v.tail.tail.tail) v).get i
Tactic:
simp
Proof state after:
n : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ (n + 2) → ℕ
hf : Arith₁ f
hg : Arith₁ g
F : Vector ℕ (n + 2) → ℕ :=
  fun v =>
    ((v.head.beta 0).isEqNat (f v.tail.tail)).and
      (v.tail.head.ball fun i => (v.head.beta (i + 1)).isEqNat (g (i ::ᵥ v.head.beta i ::ᵥ v.tail.tail)))
i : Fin n
⊢ Arith₁ fun v => v.get i.succ.succ.succ
Theorem: Nat.Arith₁.prec
Proof state before:
n : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ (n + 2) → ℕ
hf : Arith₁ f
hg : Arith₁ g
F : Vector ℕ (n + 2) → ℕ :=
  fun v =>
    ((v.head.beta 0).isEqNat (f v.tail.tail)).and
      (v.tail.head.ball fun i => (v.head.beta (i + 1)).isEqNat (g (i ::ᵥ v.head.beta i ::ᵥ v.tail.tail)))
i : Fin n
⊢ Arith₁ fun v => v.get i.succ.succ.succ
Tactic:
exact proj _
Proof state after:
no goals
Theorem: Nat.Arith₁.prec
Proof state before:
n : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ (n + 2) → ℕ
hf : Arith₁ f
hg : Arith₁ g
F : Vector ℕ (n + 2) → ℕ :=
  fun v =>
    ((v.head.beta 0).isEqNat (f v.tail.tail)).and
      (v.tail.head.ball fun i => (v.head.beta (i + 1)).isEqNat (g (i ::ᵥ v.head.beta i ::ᵥ v.tail.tail)))
hp :
  Arith₁ fun v => (v.tail.head.beta (v.head + 1)).isEqNat (g (v.head ::ᵥ v.tail.head.beta v.head ::ᵥ v.tail.tail.tail))
⊢ ∀ (i : Vector ℕ (n + 2)),
    ((i.get 1).ball fun i_1 => (i.head.beta (i_1 + 1)).isEqNat (g (i_1 ::ᵥ i.head.beta i_1 ::ᵥ i.tail.tail))) =
      i.tail.head.ball fun i_1 => (i.head.beta (i_1 + 1)).isEqNat (g (i_1 ::ᵥ i.head.beta i_1 ::ᵥ i.tail.tail))
Tactic:
simp[Vector.get_one]
Proof state after:
no goals
Theorem: Nat.Arith₁.prec
Proof state before:
n : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ (n + 2) → ℕ
hf : Arith₁ f
hg : Arith₁ g
F : Vector ℕ (n + 2) → ℕ :=
  fun v =>
    ((v.head.beta 0).isEqNat (f v.tail.tail)).and
      (v.tail.head.ball fun i => (v.head.beta (i + 1)).isEqNat (g (i ::ᵥ v.head.beta i ::ᵥ v.tail.tail)))
hp :
  Arith₁ fun v => (v.tail.head.beta (v.head + 1)).isEqNat (g (v.head ::ᵥ v.tail.head.beta v.head ::ᵥ v.tail.tail.tail))
hF : Arith₁ F
⊢ ∀ (i : Vector ℕ (n + 2)), (i.get 0).beta (i.get 1) = i.head.beta i.tail.head
Tactic:
simp [Vector.get_one]
Proof state after:
no goals