Theorem: SizedArray.foldlMIdx_push (Algdata/Data/Array/Sized.lean)

State before:
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : (i : Nat) → β i → α → m (β (i + 1))
init : β 0
x : SizedArray α n
a : α
⊢ foldlMIdx f init (push x a) = do
    let b ← foldlMIdx f init x
    f n b a
Tactic:
induction x using cons_induction generalizing β f init with
| empty =>
  conv =>
    lhs; unfold foldlMIdx; unfold foldlMIdx.loop
    rw [dif_neg (by decide : 0 ≠ 0+1)]
    change f 0 init a >>= foldlMIdx.loop f (push empty a) 1 (.refl)
    rhs; ext; unfold foldlMIdx.loop; rw [dif_pos rfl]
  conv => rhs; rw [foldlMIdx_empty, pure_bind]
  rw [bind_pure]
| cons a₁ x IH =>
  rw [push_cons_eq_cons_push]
  simp only [foldlMIdx_cons f init a₁]
  rw [bind_assoc]
  apply bind_congr; intro b
  exact IH ..
State after:
no goals

State before:
case empty
α : Type u
β✝ : Type v
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
β : Nat → Type v
f : (i : Nat) → β i → α → m (β (i + 1))
init : β 0
⊢ foldlMIdx f init (push empty a) = do
    let b ← foldlMIdx f init empty
    f 0 b a
Tactic:
conv =>
  lhs; unfold foldlMIdx; unfold foldlMIdx.loop
  rw [dif_neg (by decide : 0 ≠ 0+1)]
  change f 0 init a >>= foldlMIdx.loop f (push empty a) 1 (.refl)
  rhs; ext; unfold foldlMIdx.loop; rw [dif_pos rfl]
State after:
case empty
α : Type u
β✝ : Type v
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
β : Nat → Type v
f : (i : Nat) → β i → α → m (β (i + 1))
init : β 0
⊢ (do
      let x ← f 0 init a
      pure ((_ : 1 = 1) ▸ x)) =
    do
    let b ← foldlMIdx f init empty
    f 0 b a

State before:
case empty
α : Type u
β✝ : Type v
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
β : Nat → Type v
f : (i : Nat) → β i → α → m (β (i + 1))
init : β 0
⊢ (do
      let x ← f 0 init a
      pure ((_ : 1 = 1) ▸ x)) =
    do
    let b ← foldlMIdx f init empty
    f 0 b a
Tactic:
conv => rhs; rw [foldlMIdx_empty, pure_bind]
State after:
case empty
α : Type u
β✝ : Type v
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
β : Nat → Type v
f : (i : Nat) → β i → α → m (β (i + 1))
init : β 0
⊢ (do
      let x ← f 0 init a
      pure ((_ : 1 = 1) ▸ x)) =
    f 0 init a

State before:
case empty
α : Type u
β✝ : Type v
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
β : Nat → Type v
f : (i : Nat) → β i → α → m (β (i + 1))
init : β 0
⊢ (do
      let x ← f 0 init a
      pure ((_ : 1 = 1) ▸ x)) =
    f 0 init a
Tactic:
rw [bind_pure]
State after:
no goals

State before:
α : Type u
β✝ : Type v
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
β : Nat → Type v
f : (i : Nat) → β i → α → m (β (i + 1))
init : β 0
⊢ 0 ≠ 0 + 1
Tactic:
decide
State after:
no goals

State before:
case cons
α : Type u
β✝ : Type v
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
n✝ : Nat
a₁ : α
x : SizedArray α n✝
IH :
  ∀ {β : Nat → Type v} (f : (i : Nat) → β i → α → m (β (i + 1))) (init : β 0),
    foldlMIdx f init (push x a) = do
      let b ← foldlMIdx f init x
      f n✝ b a
β : Nat → Type v
f : (i : Nat) → β i → α → m (β (i + 1))
init : β 0
⊢ foldlMIdx f init (push (cons a₁ x) a) = do
    let b ← foldlMIdx f init (cons a₁ x)
    f (n✝ + 1) b a
Tactic:
rw [push_cons_eq_cons_push]
State after:
case cons
α : Type u
β✝ : Type v
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
n✝ : Nat
a₁ : α
x : SizedArray α n✝
IH :
  ∀ {β : Nat → Type v} (f : (i : Nat) → β i → α → m (β (i + 1))) (init : β 0),
    foldlMIdx f init (push x a) = do
      let b ← foldlMIdx f init x
      f n✝ b a
β : Nat → Type v
f : (i : Nat) → β i → α → m (β (i + 1))
init : β 0
⊢ foldlMIdx f init (cons a₁ (push x a)) = do
    let b ← foldlMIdx f init (cons a₁ x)
    f (n✝ + 1) b a

State before:
case cons
α : Type u
β✝ : Type v
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
n✝ : Nat
a₁ : α
x : SizedArray α n✝
IH :
  ∀ {β : Nat → Type v} (f : (i : Nat) → β i → α → m (β (i + 1))) (init : β 0),
    foldlMIdx f init (push x a) = do
      let b ← foldlMIdx f init x
      f n✝ b a
β : Nat → Type v
f : (i : Nat) → β i → α → m (β (i + 1))
init : β 0
⊢ foldlMIdx f init (cons a₁ (push x a)) = do
    let b ← foldlMIdx f init (cons a₁ x)
    f (n✝ + 1) b a
Tactic:
simp only [foldlMIdx_cons f init a₁]
State after:
case cons
α : Type u
β✝ : Type v
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
n✝ : Nat
a₁ : α
x : SizedArray α n✝
IH :
  ∀ {β : Nat → Type v} (f : (i : Nat) → β i → α → m (β (i + 1))) (init : β 0),
    foldlMIdx f init (push x a) = do
      let b ← foldlMIdx f init x
      f n✝ b a
β : Nat → Type v
f : (i : Nat) → β i → α → m (β (i + 1))
init : β 0
⊢ (do
      let b ← f 0 init a₁
      foldlMIdx (fun i b => f (Nat.succ i) b) b (push x a)) =
    do
    let b ←
      do
        let b ← f 0 init a₁
        foldlMIdx (fun i b => f (Nat.succ i) b) b x
    f (n✝ + 1) b a

State before:
case cons
α : Type u
β✝ : Type v
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
n✝ : Nat
a₁ : α
x : SizedArray α n✝
IH :
  ∀ {β : Nat → Type v} (f : (i : Nat) → β i → α → m (β (i + 1))) (init : β 0),
    foldlMIdx f init (push x a) = do
      let b ← foldlMIdx f init x
      f n✝ b a
β : Nat → Type v
f : (i : Nat) → β i → α → m (β (i + 1))
init : β 0
⊢ (do
      let b ← f 0 init a₁
      foldlMIdx (fun i b => f (Nat.succ i) b) b (push x a)) =
    do
    let b ←
      do
        let b ← f 0 init a₁
        foldlMIdx (fun i b => f (Nat.succ i) b) b x
    f (n✝ + 1) b a
Tactic:
rw [bind_assoc]
State after:
case cons
α : Type u
β✝ : Type v
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
n✝ : Nat
a₁ : α
x : SizedArray α n✝
IH :
  ∀ {β : Nat → Type v} (f : (i : Nat) → β i → α → m (β (i + 1))) (init : β 0),
    foldlMIdx f init (push x a) = do
      let b ← foldlMIdx f init x
      f n✝ b a
β : Nat → Type v
f : (i : Nat) → β i → α → m (β (i + 1))
init : β 0
⊢ (do
      let b ← f 0 init a₁
      foldlMIdx (fun i b => f (Nat.succ i) b) b (push x a)) =
    do
    let x_1 ← f 0 init a₁
    let b ← foldlMIdx (fun i b => f (Nat.succ i) b) x_1 x
    f (n✝ + 1) b a

State before:
case cons
α : Type u
β✝ : Type v
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
n✝ : Nat
a₁ : α
x : SizedArray α n✝
IH :
  ∀ {β : Nat → Type v} (f : (i : Nat) → β i → α → m (β (i + 1))) (init : β 0),
    foldlMIdx f init (push x a) = do
      let b ← foldlMIdx f init x
      f n✝ b a
β : Nat → Type v
f : (i : Nat) → β i → α → m (β (i + 1))
init : β 0
⊢ (do
      let b ← f 0 init a₁
      foldlMIdx (fun i b => f (Nat.succ i) b) b (push x a)) =
    do
    let x_1 ← f 0 init a₁
    let b ← foldlMIdx (fun i b => f (Nat.succ i) b) x_1 x
    f (n✝ + 1) b a
Tactic:
apply bind_congr
State after:
case cons.h
α : Type u
β✝ : Type v
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
n✝ : Nat
a₁ : α
x : SizedArray α n✝
IH :
  ∀ {β : Nat → Type v} (f : (i : Nat) → β i → α → m (β (i + 1))) (init : β 0),
    foldlMIdx f init (push x a) = do
      let b ← foldlMIdx f init x
      f n✝ b a
β : Nat → Type v
f : (i : Nat) → β i → α → m (β (i + 1))
init : β 0
⊢ ∀ (a_1 : β (0 + 1)),
    foldlMIdx (fun i b => f (Nat.succ i) b) a_1 (push x a) = do
      let b ← foldlMIdx (fun i b => f (Nat.succ i) b) a_1 x
      f (n✝ + 1) b a

State before:
case cons.h
α : Type u
β✝ : Type v
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
n✝ : Nat
a₁ : α
x : SizedArray α n✝
IH :
  ∀ {β : Nat → Type v} (f : (i : Nat) → β i → α → m (β (i + 1))) (init : β 0),
    foldlMIdx f init (push x a) = do
      let b ← foldlMIdx f init x
      f n✝ b a
β : Nat → Type v
f : (i : Nat) → β i → α → m (β (i + 1))
init : β 0
⊢ ∀ (a_1 : β (0 + 1)),
    foldlMIdx (fun i b => f (Nat.succ i) b) a_1 (push x a) = do
      let b ← foldlMIdx (fun i b => f (Nat.succ i) b) a_1 x
      f (n✝ + 1) b a
Tactic:
intro b
State after:
case cons.h
α : Type u
β✝ : Type v
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
n✝ : Nat
a₁ : α
x : SizedArray α n✝
IH :
  ∀ {β : Nat → Type v} (f : (i : Nat) → β i → α → m (β (i + 1))) (init : β 0),
    foldlMIdx f init (push x a) = do
      let b ← foldlMIdx f init x
      f n✝ b a
β : Nat → Type v
f : (i : Nat) → β i → α → m (β (i + 1))
init : β 0
b : β (0 + 1)
⊢ foldlMIdx (fun i b => f (Nat.succ i) b) b (push x a) = do
    let b ← foldlMIdx (fun i b => f (Nat.succ i) b) b x
    f (n✝ + 1) b a

State before:
case cons.h
α : Type u
β✝ : Type v
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
n✝ : Nat
a₁ : α
x : SizedArray α n✝
IH :
  ∀ {β : Nat → Type v} (f : (i : Nat) → β i → α → m (β (i + 1))) (init : β 0),
    foldlMIdx f init (push x a) = do
      let b ← foldlMIdx f init x
      f n✝ b a
β : Nat → Type v
f : (i : Nat) → β i → α → m (β (i + 1))
init : β 0
b : β (0 + 1)
⊢ foldlMIdx (fun i b => f (Nat.succ i) b) b (push x a) = do
    let b ← foldlMIdx (fun i b => f (Nat.succ i) b) b x
    f (n✝ + 1) b a
Tactic:
exact IH ..
State after:
no goals