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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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