Theorem: Array.foldlM_step (GMLInit/Data/Array/Basic.lean)

State before:
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
⊢ let_fun this := ⋯;
  foldlM f b as start stop = do
    let b ← f b as[start]
    foldlM f b as (start + 1) stop
Tactic:
simp only [Array.foldlM]
State after:
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
⊢ (if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - start) start b
    else foldlM.loop f as as.size ⋯ (as.size - start) start b) =
    do
    let b ← f b as[start]
    if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
      else foldlM.loop f as as.size ⋯ (as.size - (start + 1)) (start + 1) b

State before:
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
⊢ (if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - start) start b
    else foldlM.loop f as as.size ⋯ (as.size - start) start b) =
    do
    let b ← f b as[start]
    if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
      else foldlM.loop f as as.size ⋯ (as.size - (start + 1)) (start + 1) b
Tactic:
rw [dif_pos hstop]
State after:
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
⊢ foldlM.loop f as stop ⋯ (stop - start) start b = do
    let b ← f b as[start]
    if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
      else foldlM.loop f as as.size ⋯ (as.size - (start + 1)) (start + 1) b

State before:
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
⊢ foldlM.loop f as stop ⋯ (stop - start) start b = do
    let b ← f b as[start]
    if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
      else foldlM.loop f as as.size ⋯ (as.size - (start + 1)) (start + 1) b
Tactic:
rw [Array.foldlM.loop]
State after:
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
⊢ (if hlt : start < stop then
      match stop - start with
      | 0 => pure b
      | i'.succ =>
        let_fun this := ⋯;
        do
        let __do_lift ← f b as[start]
        foldlM.loop f as stop ⋯ i' (start + 1) __do_lift
    else pure b) =
    do
    let b ← f b as[start]
    if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
      else foldlM.loop f as as.size ⋯ (as.size - (start + 1)) (start + 1) b

State before:
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
⊢ (if hlt : start < stop then
      match stop - start with
      | 0 => pure b
      | i'.succ =>
        let_fun this := ⋯;
        do
        let __do_lift ← f b as[start]
        foldlM.loop f as stop ⋯ i' (start + 1) __do_lift
    else pure b) =
    do
    let b ← f b as[start]
    if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
      else foldlM.loop f as as.size ⋯ (as.size - (start + 1)) (start + 1) b
Tactic:
rw [dif_pos hstart]
State after:
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
⊢ (match stop - start with
    | 0 => pure b
    | i'.succ =>
      let_fun this := ⋯;
      do
      let __do_lift ← f b as[start]
      foldlM.loop f as stop ⋯ i' (start + 1) __do_lift) =
    do
    let b ← f b as[start]
    if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
      else foldlM.loop f as as.size ⋯ (as.size - (start + 1)) (start + 1) b

State before:
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
⊢ (match stop - start with
    | 0 => pure b
    | i'.succ =>
      let_fun this := ⋯;
      do
      let __do_lift ← f b as[start]
      foldlM.loop f as stop ⋯ i' (start + 1) __do_lift) =
    do
    let b ← f b as[start]
    if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
      else foldlM.loop f as as.size ⋯ (as.size - (start + 1)) (start + 1) b
Tactic:
split
State after:
case h_1
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
i✝ : Nat
heq✝ : stop - start = 0
⊢ pure b = do
    let b ← f b as[start]
    if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
      else foldlM.loop f as as.size ⋯ (as.size - (start + 1)) (start + 1) b

case h_2
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
i✝ i'✝ : Nat
heq✝ : stop - start = i'✝.succ
⊢ (let_fun this := ⋯;
    do
    let __do_lift ← f b as[start]
    foldlM.loop f as stop ⋯ i'✝ (start + 1) __do_lift) =
    do
    let b ← f b as[start]
    if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
      else foldlM.loop f as as.size ⋯ (as.size - (start + 1)) (start + 1) b

State before:
case h_1
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
i✝ : Nat
heq✝ : stop - start = 0
⊢ pure b = do
    let b ← f b as[start]
    if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
      else foldlM.loop f as as.size ⋯ (as.size - (start + 1)) (start + 1) b

case h_2
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
i✝ i'✝ : Nat
heq✝ : stop - start = i'✝.succ
⊢ (let_fun this := ⋯;
    do
    let __do_lift ← f b as[start]
    foldlM.loop f as stop ⋯ i'✝ (start + 1) __do_lift) =
    do
    let b ← f b as[start]
    if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
      else foldlM.loop f as as.size ⋯ (as.size - (start + 1)) (start + 1) b
Tactic:
next heq =>
  absurd heq
  apply Nat.sub_ne_zero_of_lt hstart
State after:
case h_2
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
i✝ i'✝ : Nat
heq✝ : stop - start = i'✝.succ
⊢ (let_fun this := ⋯;
    do
    let __do_lift ← f b as[start]
    foldlM.loop f as stop ⋯ i'✝ (start + 1) __do_lift) =
    do
    let b ← f b as[start]
    if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
      else foldlM.loop f as as.size ⋯ (as.size - (start + 1)) (start + 1) b

State before:
case h_2
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
i✝ i'✝ : Nat
heq✝ : stop - start = i'✝.succ
⊢ (let_fun this := ⋯;
    do
    let __do_lift ← f b as[start]
    foldlM.loop f as stop ⋯ i'✝ (start + 1) __do_lift) =
    do
    let b ← f b as[start]
    if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
      else foldlM.loop f as as.size ⋯ (as.size - (start + 1)) (start + 1) b
Tactic:
next heq =>
  simp
  congr
  funext b
  rw [dif_pos hstop]
  rw [Nat.sub_succ, heq, Nat.pred_succ]
State after:
no goals

State before:
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
i✝ : Nat
heq : stop - start = 0
⊢ pure b = do
    let b ← f b as[start]
    if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
      else foldlM.loop f as as.size ⋯ (as.size - (start + 1)) (start + 1) b
Tactic:
absurd heq
State after:
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
i✝ : Nat
heq : stop - start = 0
⊢ ¬stop - start = 0

State before:
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
i✝ : Nat
heq : stop - start = 0
⊢ ¬stop - start = 0
Tactic:
apply Nat.sub_ne_zero_of_lt hstart
State after:
no goals

State before:
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
i✝ i'✝ : Nat
heq : stop - start = i'✝.succ
⊢ (let_fun this := ⋯;
    do
    let __do_lift ← f b as[start]
    foldlM.loop f as stop ⋯ i'✝ (start + 1) __do_lift) =
    do
    let b ← f b as[start]
    if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
      else foldlM.loop f as as.size ⋯ (as.size - (start + 1)) (start + 1) b
Tactic:
simp
State after:
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
i✝ i'✝ : Nat
heq : stop - start = i'✝.succ
⊢ (do
      let __do_lift ← f b as[start]
      foldlM.loop f as stop ⋯ i'✝ (start + 1) __do_lift) =
    do
    let b ← f b as[start]
    if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
      else foldlM.loop f as as.size ⋯ (as.size - (start + 1)) (start + 1) b

State before:
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
i✝ i'✝ : Nat
heq : stop - start = i'✝.succ
⊢ (do
      let __do_lift ← f b as[start]
      foldlM.loop f as stop ⋯ i'✝ (start + 1) __do_lift) =
    do
    let b ← f b as[start]
    if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
      else foldlM.loop f as as.size ⋯ (as.size - (start + 1)) (start + 1) b
Tactic:
congr
State after:
case e_a
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
i✝ i'✝ : Nat
heq : stop - start = i'✝.succ
⊢ (fun __do_lift => foldlM.loop f as stop ⋯ i'✝ (start + 1) __do_lift) = fun b =>
    if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
    else foldlM.loop f as as.size ⋯ (as.size - (start + 1)) (start + 1) b

State before:
case e_a
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
i✝ i'✝ : Nat
heq : stop - start = i'✝.succ
⊢ (fun __do_lift => foldlM.loop f as stop ⋯ i'✝ (start + 1) __do_lift) = fun b =>
    if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
    else foldlM.loop f as as.size ⋯ (as.size - (start + 1)) (start + 1) b
Tactic:
funext b
State after:
case e_a.h
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b✝ : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
i✝ i'✝ : Nat
heq : stop - start = i'✝.succ
b : β
⊢ foldlM.loop f as stop ⋯ i'✝ (start + 1) b =
    if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
    else foldlM.loop f as as.size ⋯ (as.size - (start + 1)) (start + 1) b

State before:
case e_a.h
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b✝ : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
i✝ i'✝ : Nat
heq : stop - start = i'✝.succ
b : β
⊢ foldlM.loop f as stop ⋯ i'✝ (start + 1) b =
    if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
    else foldlM.loop f as as.size ⋯ (as.size - (start + 1)) (start + 1) b
Tactic:
rw [dif_pos hstop]
State after:
case e_a.h
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b✝ : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
i✝ i'✝ : Nat
heq : stop - start = i'✝.succ
b : β
⊢ foldlM.loop f as stop ⋯ i'✝ (start + 1) b = foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b

State before:
case e_a.h
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b✝ : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
i✝ i'✝ : Nat
heq : stop - start = i'✝.succ
b : β
⊢ foldlM.loop f as stop ⋯ i'✝ (start + 1) b = foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
Tactic:
rw [Nat.sub_succ, heq, Nat.pred_succ]
State after:
no goals