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

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)))
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

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 _)
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

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])
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

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])
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

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⟩
State after:
no goals

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
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

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
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

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 _
State after:
no goals

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]
State after:
no goals

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]
State after:
no goals

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
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

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]
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

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⟩
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)

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
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)

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⟩
State after:
no goals

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⟩
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

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⟩
State after:
no goals

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
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

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]
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)

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
State after:
no goals

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
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)))

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
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

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
State after:
no goals