internlm/Lean-Github huggingface dataset:
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
⊢ ∀ (i : Vector ℕ n.succ),
    Part.map (fun x => x.beta i.head) (rfind fun n_1 => Part.some (decide (0 < F (n_1 ::ᵥ i)))) =
      (↑fun v => rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) v.head) i
Tactic:
intro v
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
v : Vector ℕ n.succ
⊢ Part.map (fun x => x.beta v.head) (rfind fun n_1 => Part.some (decide (0 < F (n_1 ::ᵥ v)))) =
    (↑fun v => rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) v.head) v
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
v : Vector ℕ n.succ
⊢ Part.map (fun x => x.beta v.head) (rfind fun n_1 => Part.some (decide (0 < F (n_1 ::ᵥ v)))) =
    (↑fun v => rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) v.head) v
Tactic:
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]
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
v : Vector ℕ n.succ
⊢ ∃ a,
    (true = (decide (a.beta 0 = f v.tail) && decide (∀ m < v.head, a.beta (m + 1) = g (m ::ᵥ a.beta m ::ᵥ v.tail))) ∧
        ∀ {m : ℕ},
          m < a →
            false =
              (decide (m.beta 0 = f v.tail) &&
                decide (∀ m_1 < v.head, m.beta (m_1 + 1) = g (m_1 ::ᵥ m.beta m_1 ::ᵥ v.tail)))) ∧
      a.beta v.head = 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
v : Vector ℕ n.succ
⊢ ∃ a,
    (true = (decide (a.beta 0 = f v.tail) && decide (∀ m < v.head, a.beta (m + 1) = g (m ::ᵥ a.beta m ::ᵥ v.tail))) ∧
        ∀ {m : ℕ},
          m < a →
            false =
              (decide (m.beta 0 = f v.tail) &&
                decide (∀ m_1 < v.head, m.beta (m_1 + 1) = g (m_1 ::ᵥ m.beta m_1 ::ᵥ v.tail)))) ∧
      a.beta v.head = rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) v.head
Tactic:
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⟩
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
v : Vector ℕ n.succ
⊢ ∃ z, z.beta 0 = f v.tail ∧ ∀ i < v.head, z.beta (i + 1) = g (i ::ᵥ z.beta i ::ᵥ v.tail)
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
v : Vector ℕ n.succ
⊢ ∃ z, z.beta 0 = f v.tail ∧ ∀ i < v.head, z.beta (i + 1) = g (i ::ᵥ z.beta i ::ᵥ v.tail)
Tactic:
let l : List ℕ := recSequence f g v.head v.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)))
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
v : Vector ℕ n.succ
l : List ℕ := recSequence f g v.head v.tail
⊢ ∃ z, z.beta 0 = f v.tail ∧ ∀ i < v.head, z.beta (i + 1) = g (i ::ᵥ z.beta i ::ᵥ v.tail)
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
v : Vector ℕ n.succ
l : List ℕ := recSequence f g v.head v.tail
⊢ ∃ z, z.beta 0 = f v.tail ∧ ∀ i < v.head, z.beta (i + 1) = g (i ::ᵥ z.beta i ::ᵥ v.tail)
Tactic:
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)))
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
v : Vector ℕ n.succ
this : ∃ z, z.beta 0 = f v.tail ∧ ∀ i < v.head, z.beta (i + 1) = g (i ::ᵥ z.beta i ::ᵥ v.tail)
⊢ ∃ a,
    (true = (decide (a.beta 0 = f v.tail) && decide (∀ m < v.head, a.beta (m + 1) = g (m ::ᵥ a.beta m ::ᵥ v.tail))) ∧
        ∀ {m : ℕ},
          m < a →
            false =
              (decide (m.beta 0 = f v.tail) &&
                decide (∀ m_1 < v.head, m.beta (m_1 + 1) = g (m_1 ::ᵥ m.beta m_1 ::ᵥ v.tail)))) ∧
      a.beta v.head = rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) v.head
Tactic:
rcases least_number _ this with ⟨z, ⟨hz0, hzs⟩, hzm⟩
Proof state after:
case intro.intro.intro
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
v : Vector ℕ n.succ
this : ∃ z, z.beta 0 = f v.tail ∧ ∀ i < v.head, z.beta (i + 1) = g (i ::ᵥ z.beta i ::ᵥ v.tail)
z : ℕ
hzm : ∀ z_1 < z, ¬(z_1.beta 0 = f v.tail ∧ ∀ i < v.head, z_1.beta (i + 1) = g (i ::ᵥ z_1.beta i ::ᵥ v.tail))
hz0 : z.beta 0 = f v.tail
hzs : ∀ i < v.head, z.beta (i + 1) = g (i ::ᵥ z.beta i ::ᵥ v.tail)
⊢ ∃ a,
    (true = (decide (a.beta 0 = f v.tail) && decide (∀ m < v.head, a.beta (m + 1) = g (m ::ᵥ a.beta m ::ᵥ v.tail))) ∧
        ∀ {m : ℕ},
          m < a →
            false =
              (decide (m.beta 0 = f v.tail) &&
                decide (∀ m_1 < v.head, m.beta (m_1 + 1) = g (m_1 ::ᵥ m.beta m_1 ::ᵥ v.tail)))) ∧
      a.beta v.head = rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) v.head
Theorem: Nat.Arith₁.prec
Proof state before:
case intro.intro.intro
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
v : Vector ℕ n.succ
this : ∃ z, z.beta 0 = f v.tail ∧ ∀ i < v.head, z.beta (i + 1) = g (i ::ᵥ z.beta i ::ᵥ v.tail)
z : ℕ
hzm : ∀ z_1 < z, ¬(z_1.beta 0 = f v.tail ∧ ∀ i < v.head, z_1.beta (i + 1) = g (i ::ᵥ z_1.beta i ::ᵥ v.tail))
hz0 : z.beta 0 = f v.tail
hzs : ∀ i < v.head, z.beta (i + 1) = g (i ::ᵥ z.beta i ::ᵥ v.tail)
⊢ ∃ a,
    (true = (decide (a.beta 0 = f v.tail) && decide (∀ m < v.head, a.beta (m + 1) = g (m ::ᵥ a.beta m ::ᵥ v.tail))) ∧
        ∀ {m : ℕ},
          m < a →
            false =
              (decide (m.beta 0 = f v.tail) &&
                decide (∀ m_1 < v.head, m.beta (m_1 + 1) = g (m_1 ::ᵥ m.beta m_1 ::ᵥ v.tail)))) ∧
      a.beta v.head = rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) v.head
Tactic:
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⟩
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
this✝ : Arith₁ fun v => v.head.beta v.tail.head
v : Vector ℕ n.succ
this : ∃ z, z.beta 0 = f v.tail ∧ ∀ i < v.head, z.beta (i + 1) = g (i ::ᵥ z.beta i ::ᵥ v.tail)
z : ℕ
hzm : ∀ z_1 < z, ¬(z_1.beta 0 = f v.tail ∧ ∀ i < v.head, z_1.beta (i + 1) = g (i ::ᵥ z_1.beta i ::ᵥ v.tail))
hz0 : z.beta 0 = f v.tail
hzs : ∀ i < v.head, z.beta (i + 1) = g (i ::ᵥ z.beta i ::ᵥ v.tail)
⊢ true = (decide (z.beta 0 = f v.tail) && decide (∀ m < v.head, z.beta (m + 1) = g (m ::ᵥ z.beta m ::ᵥ v.tail)))
Tactic:
symm
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
v : Vector ℕ n.succ
this : ∃ z, z.beta 0 = f v.tail ∧ ∀ i < v.head, z.beta (i + 1) = g (i ::ᵥ z.beta i ::ᵥ v.tail)
z : ℕ
hzm : ∀ z_1 < z, ¬(z_1.beta 0 = f v.tail ∧ ∀ i < v.head, z_1.beta (i + 1) = g (i ::ᵥ z_1.beta i ::ᵥ v.tail))
hz0 : z.beta 0 = f v.tail
hzs : ∀ i < v.head, z.beta (i + 1) = g (i ::ᵥ z.beta i ::ᵥ v.tail)
⊢ (decide (z.beta 0 = f v.tail) && decide (∀ m < v.head, z.beta (m + 1) = g (m ::ᵥ z.beta m ::ᵥ v.tail))) = true
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
v : Vector ℕ n.succ
this : ∃ z, z.beta 0 = f v.tail ∧ ∀ i < v.head, z.beta (i + 1) = g (i ::ᵥ z.beta i ::ᵥ v.tail)
z : ℕ
hzm : ∀ z_1 < z, ¬(z_1.beta 0 = f v.tail ∧ ∀ i < v.head, z_1.beta (i + 1) = g (i ::ᵥ z_1.beta i ::ᵥ v.tail))
hz0 : z.beta 0 = f v.tail
hzs : ∀ i < v.head, z.beta (i + 1) = g (i ::ᵥ z.beta i ::ᵥ v.tail)
⊢ (decide (z.beta 0 = f v.tail) && decide (∀ m < v.head, z.beta (m + 1) = g (m ::ᵥ z.beta m ::ᵥ v.tail))) = true
Tactic:
simp[hz0]
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
v : Vector ℕ n.succ
this : ∃ z, z.beta 0 = f v.tail ∧ ∀ i < v.head, z.beta (i + 1) = g (i ::ᵥ z.beta i ::ᵥ v.tail)
z : ℕ
hzm : ∀ z_1 < z, ¬(z_1.beta 0 = f v.tail ∧ ∀ i < v.head, z_1.beta (i + 1) = g (i ::ᵥ z_1.beta i ::ᵥ v.tail))
hz0 : z.beta 0 = f v.tail
hzs : ∀ i < v.head, z.beta (i + 1) = g (i ::ᵥ z.beta i ::ᵥ v.tail)
⊢ ∀ m < v.head, z.beta (m + 1) = g (m ::ᵥ z.beta m ::ᵥ v.tail)
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
v : Vector ℕ n.succ
this : ∃ z, z.beta 0 = f v.tail ∧ ∀ i < v.head, z.beta (i + 1) = g (i ::ᵥ z.beta i ::ᵥ v.tail)
z : ℕ
hzm : ∀ z_1 < z, ¬(z_1.beta 0 = f v.tail ∧ ∀ i < v.head, z_1.beta (i + 1) = g (i ::ᵥ z_1.beta i ::ᵥ v.tail))
hz0 : z.beta 0 = f v.tail
hzs : ∀ i < v.head, z.beta (i + 1) = g (i ::ᵥ z.beta i ::ᵥ v.tail)
⊢ ∀ m < v.head, z.beta (m + 1) = g (m ::ᵥ z.beta m ::ᵥ v.tail)
Tactic:
exact hzs
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
this✝ : Arith₁ fun v => v.head.beta v.tail.head
v : Vector ℕ n.succ
this : ∃ z, z.beta 0 = f v.tail ∧ ∀ i < v.head, z.beta (i + 1) = g (i ::ᵥ z.beta i ::ᵥ v.tail)
z : ℕ
hzm : ∀ z_1 < z, ¬(z_1.beta 0 = f v.tail ∧ ∀ i < v.head, z_1.beta (i + 1) = g (i ::ᵥ z_1.beta i ::ᵥ v.tail))
hz0 : z.beta 0 = f v.tail
hzs : ∀ i < v.head, z.beta (i + 1) = g (i ::ᵥ z.beta i ::ᵥ v.tail)
⊢ ∀ {m : ℕ},
    m < z →
      false =
        (decide (m.beta 0 = f v.tail) && decide (∀ m_1 < v.head, m.beta (m_1 + 1) = g (m_1 ::ᵥ m.beta m_1 ::ᵥ v.tail)))
Tactic:
intro m hm
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
v : Vector ℕ n.succ
this : ∃ z, z.beta 0 = f v.tail ∧ ∀ i < v.head, z.beta (i + 1) = g (i ::ᵥ z.beta i ::ᵥ v.tail)
z : ℕ
hzm : ∀ z_1 < z, ¬(z_1.beta 0 = f v.tail ∧ ∀ i < v.head, z_1.beta (i + 1) = g (i ::ᵥ z_1.beta i ::ᵥ v.tail))
hz0 : z.beta 0 = f v.tail
hzs : ∀ i < v.head, z.beta (i + 1) = g (i ::ᵥ z.beta i ::ᵥ v.tail)
m : ℕ
hm : m < z
⊢ false =
    (decide (m.beta 0 = f v.tail) && decide (∀ m_1 < v.head, m.beta (m_1 + 1) = g (m_1 ::ᵥ m.beta m_1 ::ᵥ v.tail)))
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
v : Vector ℕ n.succ
this : ∃ z, z.beta 0 = f v.tail ∧ ∀ i < v.head, z.beta (i + 1) = g (i ::ᵥ z.beta i ::ᵥ v.tail)
z : ℕ
hzm : ∀ z_1 < z, ¬(z_1.beta 0 = f v.tail ∧ ∀ i < v.head, z_1.beta (i + 1) = g (i ::ᵥ z_1.beta i ::ᵥ v.tail))
hz0 : z.beta 0 = f v.tail
hzs : ∀ i < v.head, z.beta (i + 1) = g (i ::ᵥ z.beta i ::ᵥ v.tail)
m : ℕ
hm : m < z
⊢ false =
    (decide (m.beta 0 = f v.tail) && decide (∀ m_1 < v.head, m.beta (m_1 + 1) = g (m_1 ::ᵥ m.beta m_1 ::ᵥ v.tail)))
Tactic:
symm
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
v : Vector ℕ n.succ
this : ∃ z, z.beta 0 = f v.tail ∧ ∀ i < v.head, z.beta (i + 1) = g (i ::ᵥ z.beta i ::ᵥ v.tail)
z : ℕ
hzm : ∀ z_1 < z, ¬(z_1.beta 0 = f v.tail ∧ ∀ i < v.head, z_1.beta (i + 1) = g (i ::ᵥ z_1.beta i ::ᵥ v.tail))
hz0 : z.beta 0 = f v.tail
hzs : ∀ i < v.head, z.beta (i + 1) = g (i ::ᵥ z.beta i ::ᵥ v.tail)
m : ℕ
hm : m < z
⊢ (decide (m.beta 0 = f v.tail) && decide (∀ m_1 < v.head, m.beta (m_1 + 1) = g (m_1 ::ᵥ m.beta m_1 ::ᵥ v.tail))) =
    false
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
v : Vector ℕ n.succ
this : ∃ z, z.beta 0 = f v.tail ∧ ∀ i < v.head, z.beta (i + 1) = g (i ::ᵥ z.beta i ::ᵥ v.tail)
z : ℕ
hzm : ∀ z_1 < z, ¬(z_1.beta 0 = f v.tail ∧ ∀ i < v.head, z_1.beta (i + 1) = g (i ::ᵥ z_1.beta i ::ᵥ v.tail))
hz0 : z.beta 0 = f v.tail
hzs : ∀ i < v.head, z.beta (i + 1) = g (i ::ᵥ z.beta i ::ᵥ v.tail)
m : ℕ
hm : m < z
⊢ (decide (m.beta 0 = f v.tail) && decide (∀ m_1 < v.head, m.beta (m_1 + 1) = g (m_1 ::ᵥ m.beta m_1 ::ᵥ v.tail))) =
    false
Tactic:
simpa[imp_iff_not_or, not_or] using hzm m hm
Proof state after:
no goals
Theorem: Nat.Arith₁.of_primrec
Proof state before:
n : ℕ
f : Vector ℕ n → ℕ
hf : Primrec' f
⊢ Arith₁ f
Tactic:
induction hf
Proof 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
Theorem: Nat.Arith₁.of_primrec
Proof state before:
n : ℕ
f : Vector ℕ n → ℕ
⊢ Arith₁ fun x => 0
Tactic:
case zero               => exact zero
Proof state after:
no goals
Theorem: Nat.Arith₁.of_primrec
Proof state before:
n : ℕ
f : Vector ℕ n → ℕ
⊢ Arith₁ fun v => v.head.succ
Tactic:
case succ               => exact (@succ 1 0).of_eq (by simp)
Proof state after:
no goals
Theorem: Nat.Arith₁.of_primrec
Proof state before:
n : ℕ
f : Vector ℕ n → ℕ
n✝ : ℕ
i : Fin n✝
⊢ Arith₁ fun v => v.get i
Tactic:
case get i              => exact proj i
Proof state after:
no goals
Theorem: Nat.Arith₁.of_primrec
Proof 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
Proof state after:
no goals
Theorem: Nat.Arith₁.of_primrec
Proof 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
Proof state after:
no goals
Theorem: Nat.Arith₁.of_primrec
Proof state before:
n : ℕ
f : Vector ℕ n → ℕ
⊢ Arith₁ fun x => 0
Tactic:
exact zero
Proof state after:
no goals
Theorem: Nat.Arith₁.of_primrec
Proof state before:
n : ℕ
f : Vector ℕ n → ℕ
⊢ Arith₁ fun v => v.head.succ
Tactic:
exact (@succ 1 0).of_eq (by simp)
Proof state after:
no goals
Theorem: Nat.Arith₁.of_primrec
Proof state before:
n : ℕ
f : Vector ℕ n → ℕ
⊢ ∀ (i : Vector ℕ 1), i.get 0 + 1 = i.head.succ
Tactic:
simp
Proof state after:
no goals
Theorem: Nat.Arith₁.of_primrec
Proof state before:
n : ℕ
f : Vector ℕ n → ℕ
n✝ : ℕ
i : Fin n✝
⊢ Arith₁ fun v => v.get i
Tactic:
exact proj i
Proof state after:
no goals
Theorem: Nat.Arith₁.of_primrec
Proof 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
Proof state after:
no goals
Theorem: Nat.Arith₁.of_primrec
Proof 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
Proof state after:
no goals