Theorem: Array.foldlM_eq_foldlM_data'.aux (Algdata/Data/Array/Lemmas.lean)

State before:
α : Type u
m : Type u_1 → Type u_2
β : Type u_1
inst✝ : Monad m
f : β → α → m β
arr : Array α
i j : Nat
H : size arr = i + j
b : β
⊢ foldlM.loop f arr (size arr) (_ : size arr ≤ size arr) i j b = List.foldlM f b (List.drop j arr.data)
Tactic:
induction i generalizing j b with
| zero =>
  simp only [Nat.zero_eq, Nat.zero_add] at H; cases H
  unfold foldlM.loop
  rw [dif_neg (Nat.lt_irrefl _), List.drop_length]
  rfl
| succ i IH =>
  have IH := IH (j+1) $ H.trans $ Nat.succ_add i j
  have : j < arr.size :=
    ((Nat.add_comm ..).trans H.symm) ▸ Nat.lt_add_of_pos_right i.zero_lt_succ
  unfold foldlM.loop
  simp only [dif_pos this, bind_congr IH]
  conv => rhs; rw [← List.get_drop_eq_drop arr.data j this]
State after:
no goals

State before:
case zero
α : Type u
m : Type u_1 → Type u_2
β : Type u_1
inst✝ : Monad m
f : β → α → m β
arr : Array α
j : Nat
H : size arr = Nat.zero + j
b : β
⊢ foldlM.loop f arr (size arr) (_ : size arr ≤ size arr) Nat.zero j b = List.foldlM f b (List.drop j arr.data)
Tactic:
simp only [Nat.zero_eq, Nat.zero_add] at H
State after:
case zero
α : Type u
m : Type u_1 → Type u_2
β : Type u_1
inst✝ : Monad m
f : β → α → m β
arr : Array α
j : Nat
b : β
H : size arr = j
⊢ foldlM.loop f arr (size arr) (_ : size arr ≤ size arr) Nat.zero j b = List.foldlM f b (List.drop j arr.data)

State before:
case zero
α : Type u
m : Type u_1 → Type u_2
β : Type u_1
inst✝ : Monad m
f : β → α → m β
arr : Array α
j : Nat
b : β
H : size arr = j
⊢ foldlM.loop f arr (size arr) (_ : size arr ≤ size arr) Nat.zero j b = List.foldlM f b (List.drop j arr.data)
Tactic:
cases H
State after:
case zero.refl
α : Type u
m : Type u_1 → Type u_2
β : Type u_1
inst✝ : Monad m
f : β → α → m β
arr : Array α
b : β
⊢ foldlM.loop f arr (size arr) (_ : size arr ≤ size arr) Nat.zero (size arr) b =
    List.foldlM f b (List.drop (size arr) arr.data)

State before:
case zero.refl
α : Type u
m : Type u_1 → Type u_2
β : Type u_1
inst✝ : Monad m
f : β → α → m β
arr : Array α
b : β
⊢ foldlM.loop f arr (size arr) (_ : size arr ≤ size arr) Nat.zero (size arr) b =
    List.foldlM f b (List.drop (size arr) arr.data)
Tactic:
unfold foldlM.loop
State after:
case zero.refl
α : Type u
m : Type u_1 → Type u_2
β : Type u_1
inst✝ : Monad m
f : β → α → m β
arr : Array α
b : β
⊢ (if hlt : size arr < size arr then
      match Nat.zero with
      | 0 => pure b
      | Nat.succ i' =>
        let_fun this := (_ : size arr < size arr);
        do
        let __do_lift ← f b arr[size arr]
        foldlM.loop f arr (size arr) (_ : size arr ≤ size arr) i' (size arr + 1) __do_lift
    else pure b) =
    List.foldlM f b (List.drop (size arr) arr.data)

State before:
case zero.refl
α : Type u
m : Type u_1 → Type u_2
β : Type u_1
inst✝ : Monad m
f : β → α → m β
arr : Array α
b : β
⊢ (if hlt : size arr < size arr then
      match Nat.zero with
      | 0 => pure b
      | Nat.succ i' =>
        let_fun this := (_ : size arr < size arr);
        do
        let __do_lift ← f b arr[size arr]
        foldlM.loop f arr (size arr) (_ : size arr ≤ size arr) i' (size arr + 1) __do_lift
    else pure b) =
    List.foldlM f b (List.drop (size arr) arr.data)
Tactic:
rw [dif_neg (Nat.lt_irrefl _), List.drop_length]
State after:
case zero.refl
α : Type u
m : Type u_1 → Type u_2
β : Type u_1
inst✝ : Monad m
f : β → α → m β
arr : Array α
b : β
⊢ pure b = List.foldlM f b []

State before:
case zero.refl
α : Type u
m : Type u_1 → Type u_2
β : Type u_1
inst✝ : Monad m
f : β → α → m β
arr : Array α
b : β
⊢ pure b = List.foldlM f b []
Tactic:
rfl
State after:
no goals

State before:
case succ
α : Type u
m : Type u_1 → Type u_2
β : Type u_1
inst✝ : Monad m
f : β → α → m β
arr : Array α
i : Nat
IH :
  ∀ (j : Nat),
    size arr = i + j →
      ∀ (b : β), foldlM.loop f arr (size arr) (_ : size arr ≤ size arr) i j b = List.foldlM f b (List.drop j arr.data)
j : Nat
H : size arr = Nat.succ i + j
b : β
⊢ foldlM.loop f arr (size arr) (_ : size arr ≤ size arr) (Nat.succ i) j b = List.foldlM f b (List.drop j arr.data)
Tactic:
have IH := IH (j+1) $ H.trans $ Nat.succ_add i j
State after:
case succ
α : Type u
m : Type u_1 → Type u_2
β : Type u_1
inst✝ : Monad m
f : β → α → m β
arr : Array α
i : Nat
IH✝ :
  ∀ (j : Nat),
    size arr = i + j →
      ∀ (b : β), foldlM.loop f arr (size arr) (_ : size arr ≤ size arr) i j b = List.foldlM f b (List.drop j arr.data)
j : Nat
H : size arr = Nat.succ i + j
b : β
IH :
  ∀ (b : β),
    foldlM.loop f arr (size arr) (_ : size arr ≤ size arr) i (j + 1) b = List.foldlM f b (List.drop (j + 1) arr.data)
⊢ foldlM.loop f arr (size arr) (_ : size arr ≤ size arr) (Nat.succ i) j b = List.foldlM f b (List.drop j arr.data)

State before:
case succ
α : Type u
m : Type u_1 → Type u_2
β : Type u_1
inst✝ : Monad m
f : β → α → m β
arr : Array α
i : Nat
IH✝ :
  ∀ (j : Nat),
    size arr = i + j →
      ∀ (b : β), foldlM.loop f arr (size arr) (_ : size arr ≤ size arr) i j b = List.foldlM f b (List.drop j arr.data)
j : Nat
H : size arr = Nat.succ i + j
b : β
IH :
  ∀ (b : β),
    foldlM.loop f arr (size arr) (_ : size arr ≤ size arr) i (j + 1) b = List.foldlM f b (List.drop (j + 1) arr.data)
⊢ foldlM.loop f arr (size arr) (_ : size arr ≤ size arr) (Nat.succ i) j b = List.foldlM f b (List.drop j arr.data)
Tactic:
have : j < arr.size :=
  ((Nat.add_comm ..).trans H.symm) ▸ Nat.lt_add_of_pos_right i.zero_lt_succ
State after:
case succ
α : Type u
m : Type u_1 → Type u_2
β : Type u_1
inst✝ : Monad m
f : β → α → m β
arr : Array α
i : Nat
IH✝ :
  ∀ (j : Nat),
    size arr = i + j →
      ∀ (b : β), foldlM.loop f arr (size arr) (_ : size arr ≤ size arr) i j b = List.foldlM f b (List.drop j arr.data)
j : Nat
H : size arr = Nat.succ i + j
b : β
IH :
  ∀ (b : β),
    foldlM.loop f arr (size arr) (_ : size arr ≤ size arr) i (j + 1) b = List.foldlM f b (List.drop (j + 1) arr.data)
this : j < size arr
⊢ foldlM.loop f arr (size arr) (_ : size arr ≤ size arr) (Nat.succ i) j b = List.foldlM f b (List.drop j arr.data)

State before:
case succ
α : Type u
m : Type u_1 → Type u_2
β : Type u_1
inst✝ : Monad m
f : β → α → m β
arr : Array α
i : Nat
IH✝ :
  ∀ (j : Nat),
    size arr = i + j →
      ∀ (b : β), foldlM.loop f arr (size arr) (_ : size arr ≤ size arr) i j b = List.foldlM f b (List.drop j arr.data)
j : Nat
H : size arr = Nat.succ i + j
b : β
IH :
  ∀ (b : β),
    foldlM.loop f arr (size arr) (_ : size arr ≤ size arr) i (j + 1) b = List.foldlM f b (List.drop (j + 1) arr.data)
this : j < size arr
⊢ foldlM.loop f arr (size arr) (_ : size arr ≤ size arr) (Nat.succ i) j b = List.foldlM f b (List.drop j arr.data)
Tactic:
unfold foldlM.loop
State after:
case succ
α : Type u
m : Type u_1 → Type u_2
β : Type u_1
inst✝ : Monad m
f : β → α → m β
arr : Array α
i : Nat
IH✝ :
  ∀ (j : Nat),
    size arr = i + j →
      ∀ (b : β), foldlM.loop f arr (size arr) (_ : size arr ≤ size arr) i j b = List.foldlM f b (List.drop j arr.data)
j : Nat
H : size arr = Nat.succ i + j
b : β
IH :
  ∀ (b : β),
    foldlM.loop f arr (size arr) (_ : size arr ≤ size arr) i (j + 1) b = List.foldlM f b (List.drop (j + 1) arr.data)
this : j < size arr
⊢ (if hlt : j < size arr then
      match Nat.succ i with
      | 0 => pure b
      | Nat.succ i' =>
        let_fun this := (_ : j < size arr);
        do
        let __do_lift ← f b arr[j]
        foldlM.loop f arr (size arr) (_ : size arr ≤ size arr) i' (j + 1) __do_lift
    else pure b) =
    List.foldlM f b (List.drop j arr.data)

State before:
case succ
α : Type u
m : Type u_1 → Type u_2
β : Type u_1
inst✝ : Monad m
f : β → α → m β
arr : Array α
i : Nat
IH✝ :
  ∀ (j : Nat),
    size arr = i + j →
      ∀ (b : β), foldlM.loop f arr (size arr) (_ : size arr ≤ size arr) i j b = List.foldlM f b (List.drop j arr.data)
j : Nat
H : size arr = Nat.succ i + j
b : β
IH :
  ∀ (b : β),
    foldlM.loop f arr (size arr) (_ : size arr ≤ size arr) i (j + 1) b = List.foldlM f b (List.drop (j + 1) arr.data)
this : j < size arr
⊢ (if hlt : j < size arr then
      match Nat.succ i with
      | 0 => pure b
      | Nat.succ i' =>
        let_fun this := (_ : j < size arr);
        do
        let __do_lift ← f b arr[j]
        foldlM.loop f arr (size arr) (_ : size arr ≤ size arr) i' (j + 1) __do_lift
    else pure b) =
    List.foldlM f b (List.drop j arr.data)
Tactic:
simp only [dif_pos this, bind_congr IH]
State after:
case succ
α : Type u
m : Type u_1 → Type u_2
β : Type u_1
inst✝ : Monad m
f : β → α → m β
arr : Array α
i : Nat
IH✝ :
  ∀ (j : Nat),
    size arr = i + j →
      ∀ (b : β), foldlM.loop f arr (size arr) (_ : size arr ≤ size arr) i j b = List.foldlM f b (List.drop j arr.data)
j : Nat
H : size arr = Nat.succ i + j
b : β
IH :
  ∀ (b : β),
    foldlM.loop f arr (size arr) (_ : size arr ≤ size arr) i (j + 1) b = List.foldlM f b (List.drop (j + 1) arr.data)
this : j < size arr
⊢ (do
      let a ← f b arr[j]
      List.foldlM f a (List.drop (j + 1) arr.data)) =
    List.foldlM f b (List.drop j arr.data)

State before:
case succ
α : Type u
m : Type u_1 → Type u_2
β : Type u_1
inst✝ : Monad m
f : β → α → m β
arr : Array α
i : Nat
IH✝ :
  ∀ (j : Nat),
    size arr = i + j →
      ∀ (b : β), foldlM.loop f arr (size arr) (_ : size arr ≤ size arr) i j b = List.foldlM f b (List.drop j arr.data)
j : Nat
H : size arr = Nat.succ i + j
b : β
IH :
  ∀ (b : β),
    foldlM.loop f arr (size arr) (_ : size arr ≤ size arr) i (j + 1) b = List.foldlM f b (List.drop (j + 1) arr.data)
this : j < size arr
⊢ (do
      let a ← f b arr[j]
      List.foldlM f a (List.drop (j + 1) arr.data)) =
    List.foldlM f b (List.drop j arr.data)
Tactic:
conv => rhs; rw [← List.get_drop_eq_drop arr.data j this]
State after:
no goals