internlm/Lean-Github huggingface dataset:
Theorem: Array.size_append_aux
Proof state before:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
⊢ (as.push bs[start]).size + (stop - (start + 1)) = as.size + (stop - start)
Tactic:
rw [size_push]
Proof state after:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
⊢ as.size + 1 + (stop - (start + 1)) = as.size + (stop - start)
Theorem: Array.size_append_aux
Proof state before:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
⊢ as.size + 1 + (stop - (start + 1)) = as.size + (stop - start)
Tactic:
rw [Nat.sub_succ']
Proof state after:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
⊢ as.size + 1 + (stop - start - 1) = as.size + (stop - start)
Theorem: Array.size_append_aux
Proof state before:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
⊢ as.size + 1 + (stop - start - 1) = as.size + (stop - start)
Tactic:
rw [Nat.add_assoc]
Proof state after:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
⊢ as.size + (1 + (stop - start - 1)) = as.size + (stop - start)
Theorem: Array.size_append_aux
Proof state before:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
⊢ as.size + (1 + (stop - start - 1)) = as.size + (stop - start)
Tactic:
congr
Proof state after:
case e_a
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
⊢ 1 + (stop - start - 1) = stop - start
Theorem: Array.size_append_aux
Proof state before:
case e_a
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
⊢ 1 + (stop - start - 1) = stop - start
Tactic:
rw [Nat.add_comm]
Proof state after:
case e_a
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
⊢ stop - start - 1 + 1 = stop - start
Theorem: Array.size_append_aux
Proof state before:
case e_a
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
⊢ stop - start - 1 + 1 = stop - start
Tactic:
have : 1 ≤ stop - start := by
  rw [Nat.le_sub_iff_add_le hstart]
  rw [Nat.add_comm]
  exact hstart'
Proof state after:
case e_a
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this : 1 ≤ stop - start
⊢ stop - start - 1 + 1 = stop - start
Theorem: Array.size_append_aux
Proof state before:
case e_a
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this : 1 ≤ stop - start
⊢ stop - start - 1 + 1 = stop - start
Tactic:
rw [Nat.sub_add_cancel this]
Proof state after:
no goals
Theorem: Array.size_append_aux
Proof state before:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
⊢ 1 ≤ stop - start
Tactic:
rw [Nat.le_sub_iff_add_le hstart]
Proof state after:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
⊢ 1 + start ≤ stop
Theorem: Array.size_append_aux
Proof state before:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
⊢ 1 + start ≤ stop
Tactic:
rw [Nat.add_comm]
Proof state after:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
⊢ start + 1 ≤ stop
Theorem: Array.size_append_aux
Proof state before:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
⊢ start + 1 ≤ stop
Tactic:
exact hstart'
Proof state after:
no goals
Theorem: Array.get_append_aux_lo
Proof state before:
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : autoParam (i < (foldl push as bs start stop).size) _auto✝
⊢ (foldl push as bs start stop)[i] = as[i]
Tactic:
simp only [autoParam] at h
Proof state after:
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
⊢ (foldl push as bs start stop)[i] = as[i]
Theorem: Array.get_append_aux_lo
Proof state before:
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
heq : start = stop
⊢ (foldl push as bs start stop)[i] = as[i]
Tactic:
congr
Proof state after:
case e_xs
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
heq : start = stop
⊢ foldl push as bs start stop = as
Theorem: Array.get_append_aux_lo
Proof state before:
case e_xs
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
heq : start = stop
⊢ foldl push as bs start stop = as
Tactic:
rw [heq]
Proof state after:
case e_xs
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
heq : start = stop
⊢ foldl push as bs stop stop = as
Theorem: Array.get_append_aux_lo
Proof state before:
case e_xs
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
heq : start = stop
⊢ foldl push as bs stop stop = as
Tactic:
rw [foldl_stop]
Proof state after:
case e_xs.hstop
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
heq : start = stop
⊢ stop ≤ bs.size
Theorem: Array.get_append_aux_lo
Proof state before:
case e_xs.hstop
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
heq : start = stop
⊢ stop ≤ bs.size
Tactic:
exact hstop
Proof state after:
no goals
Theorem: Array.get_append_aux_lo
Proof state before:
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
⊢ (foldl push as bs start stop)[i] = as[i]
Tactic:
have hstart' : start < stop := Nat.lt_of_le_of_ne hstart hne
Proof state after:
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
⊢ (foldl push as bs start stop)[i] = as[i]
Theorem: Array.get_append_aux_lo
Proof state before:
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
⊢ (foldl push as bs start stop)[i] = as[i]
Tactic:
have : start < bs.size := Nat.lt_of_lt_of_le hstart' hstop
Proof state after:
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ (foldl push as bs start stop)[i] = as[i]
Theorem: Array.get_append_aux_lo
Proof state before:
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ (foldl push as bs start stop)[i] = as[i]
Tactic:
have : i < (foldl push (as.push bs[start]) bs (start+1) stop).size := by
  rw [←foldl_step]
  exact h
  exact hstart'
  exact hstop
Proof state after:
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
this : i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ (foldl push as bs start stop)[i] = as[i]
Theorem: Array.get_append_aux_lo
Proof state before:
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
this : i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ (foldl push as bs start stop)[i] = as[i]
Tactic:
transitivity (foldl push (as.push bs[start]) bs (start+1) stop)[i]
Proof state after:
case left
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
this : i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ (foldl push as bs start stop)[i] = (foldl push (as.push bs[start]) bs (start + 1) stop)[i]

case right
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
this : i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ (foldl push (as.push bs[start]) bs (start + 1) stop)[i] = as[i]
Theorem: Array.get_append_aux_lo
Proof state before:
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
Tactic:
rw [←foldl_step]
Proof state after:
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ i < (foldl push as bs start stop).size

case hstart
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ start < stop

case hstop
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ stop ≤ bs.size
Theorem: Array.get_append_aux_lo
Proof state before:
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ i < (foldl push as bs start stop).size

case hstart
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ start < stop

case hstop
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ stop ≤ bs.size
Tactic:
exact h
Proof state after:
case hstart
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ start < stop

case hstop
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ stop ≤ bs.size
Theorem: Array.get_append_aux_lo
Proof state before:
case hstart
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ start < stop

case hstop
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ stop ≤ bs.size
Tactic:
exact hstart'
Proof state after:
case hstop
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ stop ≤ bs.size
Theorem: Array.get_append_aux_lo
Proof state before:
case hstop
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ stop ≤ bs.size
Tactic:
exact hstop
Proof state after:
no goals
Theorem: Array.get_append_aux_lo
Proof state before:
case left
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
this : i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ (foldl push as bs start stop)[i] = (foldl push (as.push bs[start]) bs (start + 1) stop)[i]
Tactic:
congr 1
Proof state after:
case left.e_xs
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
this : i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ foldl push as bs start stop = foldl push (as.push bs[start]) bs (start + 1) stop
Theorem: Array.get_append_aux_lo
Proof state before:
case left.e_xs
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
this : i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ foldl push as bs start stop = foldl push (as.push bs[start]) bs (start + 1) stop
Tactic:
rw [foldl_step]
Proof state after:
case left.e_xs.hstart
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
this : i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ start < stop

case left.e_xs.hstop
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
this : i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ stop ≤ bs.size
Theorem: Array.get_append_aux_lo
Proof state before:
case left.e_xs.hstart
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
this : i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ start < stop

case left.e_xs.hstop
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
this : i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ stop ≤ bs.size
Tactic:
exact hstart'
Proof state after:
case left.e_xs.hstop
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
this : i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ stop ≤ bs.size
Theorem: Array.get_append_aux_lo
Proof state before:
case left.e_xs.hstop
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
this : i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ stop ≤ bs.size
Tactic:
exact hstop
Proof state after:
no goals
Theorem: Array.get_append_aux_lo
Proof state before:
case right
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
this : i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ (foldl push (as.push bs[start]) bs (start + 1) stop)[i] = as[i]
Tactic:
rw [get_append_aux_lo (start+1) stop i hstart' hstop]
Proof state after:
case right
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
this : i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ (as.push bs[start])[i] = as[i]

case right
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
this : i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ i < (as.push bs[start]).size
Theorem: Array.get_append_aux_lo
Proof state before:
case right
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
this : i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ (as.push bs[start])[i] = as[i]

case right
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < as.size
h : i < (foldl push as bs start stop).size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
this : i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ i < (as.push bs[start]).size
Tactic:
rw [get_push_lt]
Proof state after:
no goals
Theorem: Array.get_append_aux_hi
Proof state before:
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < stop - start
ha : autoParam (as.size + i < (foldl push as bs start stop).size) _auto✝
hb : autoParam (start + i < bs.size) _auto✝
⊢ (foldl push as bs start stop)[as.size + i] = bs[start + i]
Tactic:
simp only [autoParam] at ha hb
Proof state after:
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < stop - start
ha : as.size + i < (foldl push as bs start stop).size
hb : start + i < bs.size
⊢ (foldl push as bs start stop)[as.size + i] = bs[start + i]
Theorem: Array.get_append_aux_hi
Proof state before:
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < stop - start
ha : as.size + i < (foldl push as bs start stop).size
hb : start + i < bs.size
heq : start = stop
⊢ (foldl push as bs start stop)[as.size + i] = bs[start + i]
Tactic:
rw [heq, Nat.sub_self] at hi
Proof state after:
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < 0
ha : as.size + i < (foldl push as bs start stop).size
hb : start + i < bs.size
heq : start = stop
⊢ (foldl push as bs start stop)[as.size + i] = bs[start + i]
Theorem: Array.get_append_aux_hi
Proof state before:
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < 0
ha : as.size + i < (foldl push as bs start stop).size
hb : start + i < bs.size
heq : start = stop
⊢ (foldl push as bs start stop)[as.size + i] = bs[start + i]
Tactic:
contradiction
Proof state after:
no goals
Theorem: Array.get_append_aux_hi
Proof state before:
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < stop - start
ha : as.size + i < (foldl push as bs start stop).size
hb : start + i < bs.size
hne : ¬start = stop
⊢ (foldl push as bs start stop)[as.size + i] = bs[start + i]
Tactic:
have hstart' : start < stop := Nat.lt_of_le_of_ne hstart hne
Proof state after:
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < stop - start
ha : as.size + i < (foldl push as bs start stop).size
hb : start + i < bs.size
hne : ¬start = stop
hstart' : start < stop
⊢ (foldl push as bs start stop)[as.size + i] = bs[start + i]
Theorem: Array.get_append_aux_hi
Proof state before:
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < stop - start
ha : as.size + i < (foldl push as bs start stop).size
hb : start + i < bs.size
hne : ¬start = stop
hstart' : start < stop
⊢ (foldl push as bs start stop)[as.size + i] = bs[start + i]
Tactic:
have : start < bs.size := Nat.lt_of_lt_of_le hstart' hstop
Proof state after:
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < stop - start
ha : as.size + i < (foldl push as bs start stop).size
hb : start + i < bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ (foldl push as bs start stop)[as.size + i] = bs[start + i]
Theorem: Array.get_append_aux_hi
Proof state before:
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < stop - start
ha : as.size + i < (foldl push as bs start stop).size
hb : start + i < bs.size
hne : ¬start = stop
hstart' : start < stop
this : start < bs.size
⊢ (foldl push as bs start stop)[as.size + i] = bs[start + i]
Tactic:
have : as.size + i < (foldl push (as.push bs[start]) bs (start+1) stop).size := by
  rw [size_append_aux (start+1) stop (Nat.succ_le_of_lt hstart') hstop]
  rw [size_push]
  rw [Nat.add_assoc]
  apply Nat.add_lt_add_left
  rw [Nat.add_comm]
  rw [Nat.sub_succ']
  rw [Nat.sub_add_cancel]
  exact hi
  rw [Nat.le_sub_iff_add_le hstart]
  rw [Nat.add_comm]
  exact Nat.succ_le_of_lt hstart'
Proof state after:
α : Type u_1
as bs : Array α
start stop i : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hi : i < stop - start
ha : as.size + i < (foldl push as bs start stop).size
hb : start + i < bs.size
hne : ¬start = stop
hstart' : start < stop
this✝ : start < bs.size
this : as.size + i < (foldl push (as.push bs[start]) bs (start + 1) stop).size
⊢ (foldl push as bs start stop)[as.size + i] = bs[start + i]