internlm/Lean-Github huggingface dataset:
Theorem: Array.foldrM_step
Proof state before:
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
⊢ foldrM f b as (start + 1) stop = do
    let b ← f as[start] b
    foldrM f b as start stop
Tactic:
simp only [Array.foldrM]
Proof state after:
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
⊢ (if h : start + 1 ≤ as.size then if stop < start + 1 then foldrM.fold f as stop (start + 1) h b else pure b
    else if stop < as.size then foldrM.fold f as stop as.size ⋯ b else pure b) =
    do
    let b ← f as[start] b
    if h : start ≤ as.size then if stop < start then foldrM.fold f as stop start h b else pure b
      else if stop < as.size then foldrM.fold f as stop as.size ⋯ b else pure b
Theorem: Array.foldrM_step
Proof state before:
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
⊢ (if h : start + 1 ≤ as.size then if stop < start + 1 then foldrM.fold f as stop (start + 1) h b else pure b
    else if stop < as.size then foldrM.fold f as stop as.size ⋯ b else pure b) =
    do
    let b ← f as[start] b
    if h : start ≤ as.size then if stop < start then foldrM.fold f as stop start h b else pure b
      else if stop < as.size then foldrM.fold f as stop as.size ⋯ b else pure b
Tactic:
rw [dif_pos (Nat.succ_le_of_lt hstart)]
Proof state after:
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
⊢ (if stop < start + 1 then foldrM.fold f as stop (start + 1) ⋯ b else pure b) = do
    let b ← f as[start] b
    if h : start ≤ as.size then if stop < start then foldrM.fold f as stop start h b else pure b
      else if stop < as.size then foldrM.fold f as stop as.size ⋯ b else pure b
Theorem: Array.foldrM_step
Proof state before:
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
⊢ (if stop < start + 1 then foldrM.fold f as stop (start + 1) ⋯ b else pure b) = do
    let b ← f as[start] b
    if h : start ≤ as.size then if stop < start then foldrM.fold f as stop start h b else pure b
      else if stop < as.size then foldrM.fold f as stop as.size ⋯ b else pure b
Tactic:
rw [if_pos (Nat.lt_succ_of_le hstop)]
Proof state after:
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
⊢ foldrM.fold f as stop (start + 1) ⋯ b = do
    let b ← f as[start] b
    if h : start ≤ as.size then if stop < start then foldrM.fold f as stop start h b else pure b
      else if stop < as.size then foldrM.fold f as stop as.size ⋯ b else pure b
Theorem: Array.foldrM_step
Proof state before:
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
⊢ foldrM.fold f as stop (start + 1) ⋯ b = do
    let b ← f as[start] b
    if h : start ≤ as.size then if stop < start then foldrM.fold f as stop start h b else pure b
      else if stop < as.size then foldrM.fold f as stop as.size ⋯ b else pure b
Tactic:
simp only [foldrM.fold]
Proof state after:
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
⊢ (if (start + 1 == stop) = true then pure b
    else do
      let __do_lift ← f as[start] b
      foldrM.fold f as stop start ⋯ __do_lift) =
    do
    let b ← f as[start] b
    if h : start ≤ as.size then if stop < start then foldrM.fold f as stop start h b else pure b
      else if stop < as.size then foldrM.fold f as stop as.size ⋯ b else pure b
Theorem: Array.foldrM_step
Proof state before:
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
⊢ (if (start + 1 == stop) = true then pure b
    else do
      let __do_lift ← f as[start] b
      foldrM.fold f as stop start ⋯ __do_lift) =
    do
    let b ← f as[start] b
    if h : start ≤ as.size then if stop < start then foldrM.fold f as stop start h b else pure b
      else if stop < as.size then foldrM.fold f as stop as.size ⋯ b else pure b
Tactic:
split
Proof state after:
case isTrue
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
h✝ : (start + 1 == stop) = true
⊢ pure b = do
    let b ← f as[start] b
    if h : start ≤ as.size then if stop < start then foldrM.fold f as stop start h b else pure b
      else if stop < as.size then foldrM.fold f as stop as.size ⋯ b else pure b

case isFalse
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
h✝ : ¬(start + 1 == stop) = true
⊢ (do
      let __do_lift ← f as[start] b
      foldrM.fold f as stop start ⋯ __do_lift) =
    do
    let b ← f as[start] b
    if h : start ≤ as.size then if stop < start then foldrM.fold f as stop start h b else pure b
      else if stop < as.size then foldrM.fold f as stop as.size ⋯ b else pure b
Theorem: Array.foldrM_step
Proof state before:
case isTrue
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
h✝ : (start + 1 == stop) = true
⊢ pure b = do
    let b ← f as[start] b
    if h : start ≤ as.size then if stop < start then foldrM.fold f as stop start h b else pure b
      else if stop < as.size then foldrM.fold f as stop as.size ⋯ b else pure b

case isFalse
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
h✝ : ¬(start + 1 == stop) = true
⊢ (do
      let __do_lift ← f as[start] b
      foldrM.fold f as stop start ⋯ __do_lift) =
    do
    let b ← f as[start] b
    if h : start ≤ as.size then if stop < start then foldrM.fold f as stop start h b else pure b
      else if stop < as.size then foldrM.fold f as stop as.size ⋯ b else pure b
Tactic:
next heq =>
  absurd (eq_of_beq heq)
  apply Nat.ne_of_gt
  apply Nat.lt_succ_of_le
  exact hstop
Proof state after:
case isFalse
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
h✝ : ¬(start + 1 == stop) = true
⊢ (do
      let __do_lift ← f as[start] b
      foldrM.fold f as stop start ⋯ __do_lift) =
    do
    let b ← f as[start] b
    if h : start ≤ as.size then if stop < start then foldrM.fold f as stop start h b else pure b
      else if stop < as.size then foldrM.fold f as stop as.size ⋯ b else pure b
Theorem: Array.foldrM_step
Proof state before:
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
heq : (start + 1 == stop) = true
⊢ pure b = do
    let b ← f as[start] b
    if h : start ≤ as.size then if stop < start then foldrM.fold f as stop start h b else pure b
      else if stop < as.size then foldrM.fold f as stop as.size ⋯ b else pure b
Tactic:
absurd (eq_of_beq heq)
Proof state after:
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
heq : (start + 1 == stop) = true
⊢ ¬start + 1 = stop
Theorem: Array.foldrM_step
Proof state before:
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
heq : (start + 1 == stop) = true
⊢ ¬start + 1 = stop
Tactic:
apply Nat.ne_of_gt
Proof state after:
case h
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
heq : (start + 1 == stop) = true
⊢ stop < start + 1
Theorem: Array.foldrM_step
Proof state before:
case h
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
heq : (start + 1 == stop) = true
⊢ stop < start + 1
Tactic:
apply Nat.lt_succ_of_le
Proof state after:
case h.a
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
heq : (start + 1 == stop) = true
⊢ stop ≤ start
Theorem: Array.foldrM_step
Proof state before:
case h.a
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
heq : (start + 1 == stop) = true
⊢ stop ≤ start
Tactic:
exact hstop
Proof state after:
no goals
Theorem: Array.foldrM_step
Proof state before:
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
hne : ¬(start + 1 == stop) = true
⊢ (do
      let __do_lift ← f as[start] b
      foldrM.fold f as stop start ⋯ __do_lift) =
    do
    let b ← f as[start] b
    if h : start ≤ as.size then if stop < start then foldrM.fold f as stop start h b else pure b
      else if stop < as.size then foldrM.fold f as stop as.size ⋯ b else pure b
Tactic:
congr
Proof state after:
case e_a
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
hne : ¬(start + 1 == stop) = true
⊢ (fun __do_lift => foldrM.fold f as stop start ⋯ __do_lift) = fun b =>
    if h : start ≤ as.size then if stop < start then foldrM.fold f as stop start h b else pure b
    else if stop < as.size then foldrM.fold f as stop as.size ⋯ b else pure b
Theorem: Array.foldrM_step
Proof state before:
case e_a
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
hne : ¬(start + 1 == stop) = true
⊢ (fun __do_lift => foldrM.fold f as stop start ⋯ __do_lift) = fun b =>
    if h : start ≤ as.size then if stop < start then foldrM.fold f as stop start h b else pure b
    else if stop < as.size then foldrM.fold f as stop as.size ⋯ b else pure b
Tactic:
funext b
Proof state after:
case e_a.h
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b✝ : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
hne : ¬(start + 1 == stop) = true
b : β
⊢ foldrM.fold f as stop start ⋯ b =
    if h : start ≤ as.size then if stop < start then foldrM.fold f as stop start h b else pure b
    else if stop < as.size then foldrM.fold f as stop as.size ⋯ b else pure b
Theorem: Array.foldrM_step
Proof state before:
case e_a.h
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b✝ : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
hne : ¬(start + 1 == stop) = true
b : β
⊢ foldrM.fold f as stop start ⋯ b =
    if h : start ≤ as.size then if stop < start then foldrM.fold f as stop start h b else pure b
    else if stop < as.size then foldrM.fold f as stop as.size ⋯ b else pure b
Tactic:
rw [dif_pos (Nat.le_of_lt hstart)]
Proof state after:
case e_a.h
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b✝ : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
hne : ¬(start + 1 == stop) = true
b : β
⊢ foldrM.fold f as stop start ⋯ b = if stop < start then foldrM.fold f as stop start ⋯ b else pure b
Theorem: Array.foldrM_step
Proof state before:
case e_a.h
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b✝ : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
hne : ¬(start + 1 == stop) = true
b : β
⊢ foldrM.fold f as stop start ⋯ b = if stop < start then foldrM.fold f as stop start ⋯ b else pure b
Tactic:
split
Proof state after:
case e_a.h.isTrue
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b✝ : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
hne : ¬(start + 1 == stop) = true
b : β
h✝ : stop < start
⊢ foldrM.fold f as stop start ⋯ b = foldrM.fold f as stop start ⋯ b

case e_a.h.isFalse
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b✝ : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
hne : ¬(start + 1 == stop) = true
b : β
h✝ : ¬stop < start
⊢ foldrM.fold f as stop start ⋯ b = pure b
Theorem: Array.foldrM_step
Proof state before:
case e_a.h.isTrue
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b✝ : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
hne : ¬(start + 1 == stop) = true
b : β
h✝ : stop < start
⊢ foldrM.fold f as stop start ⋯ b = foldrM.fold f as stop start ⋯ b

case e_a.h.isFalse
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b✝ : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
hne : ¬(start + 1 == stop) = true
b : β
h✝ : ¬stop < start
⊢ foldrM.fold f as stop start ⋯ b = pure b
Tactic:
next => rfl
Proof state after:
case e_a.h.isFalse
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b✝ : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
hne : ¬(start + 1 == stop) = true
b : β
h✝ : ¬stop < start
⊢ foldrM.fold f as stop start ⋯ b = pure b
Theorem: Array.foldrM_step
Proof state before:
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b✝ : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
hne : ¬(start + 1 == stop) = true
b : β
h✝ : stop < start
⊢ foldrM.fold f as stop start ⋯ b = foldrM.fold f as stop start ⋯ b
Tactic:
rfl
Proof state after:
no goals
Theorem: Array.foldrM_step
Proof state before:
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b✝ : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
hne : ¬(start + 1 == stop) = true
b : β
hge : ¬stop < start
this : stop = start
⊢ foldrM.fold f as stop start ⋯ b = pure b
Tactic:
simp [this]
Proof state after:
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b✝ : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
hne : ¬(start + 1 == stop) = true
b : β
hge : ¬stop < start
this : stop = start
⊢ foldrM.fold f as start start ⋯ b = pure b
Theorem: Array.foldrM_step
Proof state before:
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b✝ : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
hne : ¬(start + 1 == stop) = true
b : β
hge : ¬stop < start
this : stop = start
⊢ foldrM.fold f as start start ⋯ b = pure b
Tactic:
unfold foldrM.fold
Proof state after:
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b✝ : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
hne : ¬(start + 1 == stop) = true
b : β
hge : ¬stop < start
this : stop = start
⊢ (if (start == start) = true then pure b
    else
      match start, ⋯ with
      | 0, x => pure b
      | i.succ, h =>
        let_fun this := ⋯;
        do
        let __do_lift ← f as[i] b
        foldrM.fold f as start i ⋯ __do_lift) =
    pure b
Theorem: Array.foldrM_step
Proof state before:
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b✝ : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
hne : ¬(start + 1 == stop) = true
b : β
hge : ¬stop < start
this : stop = start
⊢ (if (start == start) = true then pure b
    else
      match start, ⋯ with
      | 0, x => pure b
      | i.succ, h =>
        let_fun this := ⋯;
        do
        let __do_lift ← f as[i] b
        foldrM.fold f as start i ⋯ __do_lift) =
    pure b
Tactic:
rw [BEq.rfl, if_pos rfl]
Proof state after:
no goals
Theorem: Array.foldrM_step
Proof state before:
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b✝ : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
hne : ¬(start + 1 == stop) = true
b : β
hge : ¬stop < start
⊢ stop = start
Tactic:
antisymmetry using LE.le
Proof state after:
case a
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b✝ : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
hne : ¬(start + 1 == stop) = true
b : β
hge : ¬stop < start
⊢ stop ≤ start

case a
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b✝ : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
hne : ¬(start + 1 == stop) = true
b : β
hge : ¬stop < start
⊢ start ≤ stop
Theorem: Array.foldrM_step
Proof state before:
case a
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b✝ : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
hne : ¬(start + 1 == stop) = true
b : β
hge : ¬stop < start
⊢ stop ≤ start
Tactic:
exact hstop
Proof state after:
no goals
Theorem: Array.foldrM_step
Proof state before:
case a
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b✝ : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
hne : ¬(start + 1 == stop) = true
b : β
hge : ¬stop < start
⊢ start ≤ stop
Tactic:
exact Nat.le_of_not_gt hge
Proof state after:
no goals
Theorem: Array.foldr_stop
Proof state before:
α : Type u_1
β : Type u_2
f : α → β → β
b : β
as : Array α
stop : Nat
hstop : stop ≤ as.size
⊢ foldr f b as stop stop = b
Tactic:
apply foldrM_stop
Proof state after:
case hstop
α : Type u_1
β : Type u_2
f : α → β → β
b : β
as : Array α
stop : Nat
hstop : stop ≤ as.size
⊢ stop ≤ as.size
Theorem: Array.foldr_stop
Proof state before:
case hstop
α : Type u_1
β : Type u_2
f : α → β → β
b : β
as : Array α
stop : Nat
hstop : stop ≤ as.size
⊢ stop ≤ as.size
Tactic:
assumption
Proof state after:
no goals
Theorem: Array.foldr_step
Proof state before:
α : Type u_1
β : Type u_2
f : α → β → β
b : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
⊢ foldr f b as (start + 1) stop = foldr f (f as[start] b) as start stop
Tactic:
apply foldrM_step
Proof state after:
case hstop
α : Type u_1
β : Type u_2
f : α → β → β
b : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
⊢ stop ≤ start
Theorem: Array.foldr_step
Proof state before:
case hstop
α : Type u_1
β : Type u_2
f : α → β → β
b : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
⊢ stop ≤ start
Tactic:
assumption
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
⊢ (foldl push as bs start stop).size = as.size + (stop - start)
Tactic:
by_cases start = stop with
| isTrue heq =>
  rw [heq]
  rw [foldl_stop]
  rw [Nat.sub_self]
  rw [Nat.add_zero]
  exact hstop
| isFalse hne =>
  have hstart' : start < stop := Nat.lt_of_le_of_ne hstart hne
  rw [foldl_step push as bs start stop hstart' hstop]
  rw [size_append_aux (start+1) stop hstart' hstop]
  rw [size_push]
  rw [Nat.sub_succ']
  rw [Nat.add_assoc]
  congr
  rw [Nat.add_comm]
  have : 1 ≤ stop - start := by
    rw [Nat.le_sub_iff_add_le hstart]
    rw [Nat.add_comm]
    exact hstart'
  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
heq : start = stop
⊢ (foldl push as bs start stop).size = as.size + (stop - start)
Tactic:
rw [heq]
Proof state after:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
heq : start = stop
⊢ (foldl push as bs stop stop).size = as.size + (stop - 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
heq : start = stop
⊢ (foldl push as bs stop stop).size = as.size + (stop - stop)
Tactic:
rw [foldl_stop]
Proof state after:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
heq : start = stop
⊢ as.size = as.size + (stop - stop)

case hstop
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
heq : start = stop
⊢ stop ≤ bs.size
Theorem: Array.size_append_aux
Proof state before:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
heq : start = stop
⊢ as.size = as.size + (stop - stop)

case hstop
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
heq : start = stop
⊢ stop ≤ bs.size
Tactic:
rw [Nat.sub_self]
Proof state after:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
heq : start = stop
⊢ as.size = as.size + 0

case hstop
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
heq : start = stop
⊢ stop ≤ bs.size
Theorem: Array.size_append_aux
Proof state before:
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
heq : start = stop
⊢ as.size = as.size + 0

case hstop
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
heq : start = stop
⊢ stop ≤ bs.size
Tactic:
rw [Nat.add_zero]
Proof state after:
case hstop
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
heq : start = stop
⊢ stop ≤ bs.size
Theorem: Array.size_append_aux
Proof state before:
case hstop
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
heq : start = stop
⊢ stop ≤ bs.size
Tactic:
exact hstop
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
⊢ (foldl push as bs start stop).size = as.size + (stop - start)
Tactic:
have hstart' : start < stop := Nat.lt_of_le_of_ne hstart hne
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
⊢ (foldl push as bs start stop).size = 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
⊢ (foldl push as bs start stop).size = as.size + (stop - start)
Tactic:
rw [foldl_step push as bs start stop hstart' hstop]
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
⊢ (foldl push (as.push bs[start]) bs (start + 1) stop).size = 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
⊢ (foldl push (as.push bs[start]) bs (start + 1) stop).size = as.size + (stop - start)
Tactic:
rw [size_append_aux (start+1) stop hstart' hstop]
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.push bs[start]).size + (stop - (start + 1)) = as.size + (stop - start)