internlm/Lean-Github huggingface dataset:
Theorem: SizedArray.foldlMIdx_cons
Proof state before:
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
init : β 0
a : α
x : SizedArray α n
⊢ foldlMIdx.loop f (cons a x) 0 (_ : 0 ≤ n + 1) init = do
    let b ← f 0 init a
    foldlMIdx.loop (fun i b => f (Nat.succ i) b) x 0 (_ : 0 ≤ n) b
Tactic:
conv => lhs; unfold foldlMIdx.loop; simp only [dif_neg n.succ_ne_zero.symm]
Proof state after:
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
init : β 0
a : α
x : SizedArray α n
⊢ (do
      let __do_lift ← f 0 init (cons a x)[0]
      foldlMIdx.loop f (cons a x) (0 + 1) (_ : 0 < n + 1) __do_lift) =
    do
    let b ← f 0 init a
    foldlMIdx.loop (fun i b => f (Nat.succ i) b) x 0 (_ : 0 ≤ n) b
Theorem: SizedArray.foldlMIdx_cons
Proof state before:
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
init : β 0
a : α
x : SizedArray α n
⊢ (do
      let __do_lift ← f 0 init (cons a x)[0]
      foldlMIdx.loop f (cons a x) (0 + 1) (_ : 0 < n + 1) __do_lift) =
    do
    let b ← f 0 init a
    foldlMIdx.loop (fun i b => f (Nat.succ i) b) x 0 (_ : 0 ≤ n) b
Tactic:
apply bind_congr
Proof state after:
case h
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
init : β 0
a : α
x : SizedArray α n
⊢ ∀ (a_1 : β (0 + 1)),
    foldlMIdx.loop f (cons a x) (0 + 1) (_ : 0 < n + 1) a_1 =
      foldlMIdx.loop (fun i b => f (Nat.succ i) b) x 0 (_ : 0 ≤ n) a_1
Theorem: SizedArray.foldlMIdx_cons
Proof state before:
case h
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
init : β 0
a : α
x : SizedArray α n
⊢ ∀ (a_1 : β (0 + 1)),
    foldlMIdx.loop f (cons a x) (0 + 1) (_ : 0 < n + 1) a_1 =
      foldlMIdx.loop (fun i b => f (Nat.succ i) b) x 0 (_ : 0 ≤ n) a_1
Tactic:
intro b
Proof state after:
case h
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
init : β 0
a : α
x : SizedArray α n
b : β (0 + 1)
⊢ foldlMIdx.loop f (cons a x) (0 + 1) (_ : 0 < n + 1) b = foldlMIdx.loop (fun i b => f (Nat.succ i) b) x 0 (_ : 0 ≤ n) b
Theorem: SizedArray.foldlMIdx_cons
Proof state before:
case h
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
init : β 0
a : α
x : SizedArray α n
b : β (0 + 1)
⊢ foldlMIdx.loop f (cons a x) (0 + 1) (_ : 0 < n + 1) b = foldlMIdx.loop (fun i b => f (Nat.succ i) b) x 0 (_ : 0 ≤ n) b
Tactic:
exact foldlMIdx.loop_cons_succ f a x 0 _ _ b
Proof state after:
no goals
Theorem: SizedArray.foldlM_eq_foldlMIdx
Proof state before:
α : Type u
β : Type v
n : Nat
m : Type v → Type w
inst✝ : Monad m
f : β → α → m β
init : β
x : SizedArray α n
⊢ foldlM f init x = foldlMIdx (fun x => f) init x
Tactic:
unfold foldlM
Proof state after:
α : Type u
β : Type v
n : Nat
m : Type v → Type w
inst✝ : Monad m
f : β → α → m β
init : β
x : SizedArray α n
⊢ Array.foldlM f init x.val 0 (Array.size x.val) = foldlMIdx (fun x => f) init x
Theorem: SizedArray.foldlM_eq_foldlMIdx
Proof state before:
α : Type u
β : Type v
n : Nat
m : Type v → Type w
inst✝ : Monad m
f : β → α → m β
init : β
x : SizedArray α n
⊢ Array.foldlM f init x.val 0 (Array.size x.val) = foldlMIdx (fun x => f) init x
Tactic:
rw [Array.foldlM_eq_foldlM_data']
Proof state after:
α : Type u
β : Type v
n : Nat
m : Type v → Type w
inst✝ : Monad m
f : β → α → m β
init : β
x : SizedArray α n
⊢ List.foldlM f init x.val.data = foldlMIdx (fun x => f) init x
Theorem: SizedArray.foldlM_eq_foldlMIdx
Proof state before:
α : Type u
β : Type v
n : Nat
m : Type v → Type w
inst✝ : Monad m
f : β → α → m β
init : β
x : SizedArray α n
⊢ List.foldlM f init x.val.data = foldlMIdx (fun x => f) init x
Tactic:
induction x using cons_induction generalizing init with
| empty => rfl
| cons a x IH =>
  conv => lhs; dsimp [cons]
  rw [foldlMIdx_cons]
  apply bind_congr; intro b
  exact IH b
Proof state after:
no goals
Theorem: SizedArray.foldlM_eq_foldlMIdx
Proof state before:
case empty
α : Type u
β : Type v
n : Nat
m : Type v → Type w
inst✝ : Monad m
f : β → α → m β
init : β
⊢ List.foldlM f init empty.val.data = foldlMIdx (fun x => f) init empty
Tactic:
rfl
Proof state after:
no goals
Theorem: SizedArray.foldlM_eq_foldlMIdx
Proof state before:
case cons
α : Type u
β : Type v
n : Nat
m : Type v → Type w
inst✝ : Monad m
f : β → α → m β
n✝ : Nat
a : α
x : SizedArray α n✝
IH : ∀ (init : β), List.foldlM f init x.val.data = foldlMIdx (fun x => f) init x
init : β
⊢ List.foldlM f init (cons a x).val.data = foldlMIdx (fun x => f) init (cons a x)
Tactic:
conv => lhs; dsimp [cons]
Proof state after:
case cons
α : Type u
β : Type v
n : Nat
m : Type v → Type w
inst✝ : Monad m
f : β → α → m β
n✝ : Nat
a : α
x : SizedArray α n✝
IH : ∀ (init : β), List.foldlM f init x.val.data = foldlMIdx (fun x => f) init x
init : β
⊢ (do
      let s' ← f init a
      List.foldlM f s' x.val.data) =
    foldlMIdx (fun x => f) init (cons a x)
Theorem: SizedArray.foldlM_eq_foldlMIdx
Proof state before:
case cons
α : Type u
β : Type v
n : Nat
m : Type v → Type w
inst✝ : Monad m
f : β → α → m β
n✝ : Nat
a : α
x : SizedArray α n✝
IH : ∀ (init : β), List.foldlM f init x.val.data = foldlMIdx (fun x => f) init x
init : β
⊢ (do
      let s' ← f init a
      List.foldlM f s' x.val.data) =
    foldlMIdx (fun x => f) init (cons a x)
Tactic:
rw [foldlMIdx_cons]
Proof state after:
case cons
α : Type u
β : Type v
n : Nat
m : Type v → Type w
inst✝ : Monad m
f : β → α → m β
n✝ : Nat
a : α
x : SizedArray α n✝
IH : ∀ (init : β), List.foldlM f init x.val.data = foldlMIdx (fun x => f) init x
init : β
⊢ (do
      let s' ← f init a
      List.foldlM f s' x.val.data) =
    do
    let b ← f init a
    foldlMIdx (fun i b => f b) b x
Theorem: SizedArray.foldlM_eq_foldlMIdx
Proof state before:
case cons
α : Type u
β : Type v
n : Nat
m : Type v → Type w
inst✝ : Monad m
f : β → α → m β
n✝ : Nat
a : α
x : SizedArray α n✝
IH : ∀ (init : β), List.foldlM f init x.val.data = foldlMIdx (fun x => f) init x
init : β
⊢ (do
      let s' ← f init a
      List.foldlM f s' x.val.data) =
    do
    let b ← f init a
    foldlMIdx (fun i b => f b) b x
Tactic:
apply bind_congr
Proof state after:
case cons.h
α : Type u
β : Type v
n : Nat
m : Type v → Type w
inst✝ : Monad m
f : β → α → m β
n✝ : Nat
a : α
x : SizedArray α n✝
IH : ∀ (init : β), List.foldlM f init x.val.data = foldlMIdx (fun x => f) init x
init : β
⊢ ∀ (a : β), List.foldlM f a x.val.data = foldlMIdx (fun i b => f b) a x
Theorem: SizedArray.foldlM_eq_foldlMIdx
Proof state before:
case cons.h
α : Type u
β : Type v
n : Nat
m : Type v → Type w
inst✝ : Monad m
f : β → α → m β
n✝ : Nat
a : α
x : SizedArray α n✝
IH : ∀ (init : β), List.foldlM f init x.val.data = foldlMIdx (fun x => f) init x
init : β
⊢ ∀ (a : β), List.foldlM f a x.val.data = foldlMIdx (fun i b => f b) a x
Tactic:
intro b
Proof state after:
case cons.h
α : Type u
β : Type v
n : Nat
m : Type v → Type w
inst✝ : Monad m
f : β → α → m β
n✝ : Nat
a : α
x : SizedArray α n✝
IH : ∀ (init : β), List.foldlM f init x.val.data = foldlMIdx (fun x => f) init x
init b : β
⊢ List.foldlM f b x.val.data = foldlMIdx (fun i b => f b) b x
Theorem: SizedArray.foldlM_eq_foldlMIdx
Proof state before:
case cons.h
α : Type u
β : Type v
n : Nat
m : Type v → Type w
inst✝ : Monad m
f : β → α → m β
n✝ : Nat
a : α
x : SizedArray α n✝
IH : ∀ (init : β), List.foldlM f init x.val.data = foldlMIdx (fun x => f) init x
init b : β
⊢ List.foldlM f b x.val.data = foldlMIdx (fun i b => f b) b x
Tactic:
exact IH b
Proof state after:
no goals
Theorem: SizedArray.foldlMIdx_push
Proof 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 ..
Proof state after:
no goals
Theorem: SizedArray.foldlMIdx_push
Proof 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]
Proof 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
Theorem: SizedArray.foldlMIdx_push
Proof 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]
Proof 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
Theorem: SizedArray.foldlMIdx_push
Proof 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]
Proof state after:
no goals
Theorem: SizedArray.foldlMIdx_push
Proof 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
Proof state after:
no goals
Theorem: SizedArray.foldlMIdx_push
Proof 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]
Proof 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
Theorem: SizedArray.foldlMIdx_push
Proof 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₁]
Proof 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
Theorem: SizedArray.foldlMIdx_push
Proof 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]
Proof 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
Theorem: SizedArray.foldlMIdx_push
Proof 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
Proof 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
Theorem: SizedArray.foldlMIdx_push
Proof 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
Proof 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
Theorem: SizedArray.foldlMIdx_push
Proof 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 ..
Proof state after:
no goals
Theorem: SizedArray.mapM.loop_cons_succ
Proof state before:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
a : α
x : SizedArray α n
i : Nat
hi₁ : i + 1 ≤ n + 1
hi₂ : i ≤ n
b : β
r : SizedArray β i
⊢ loop f (cons a x) (i + 1) hi₁ (cons b r) = do
    let y ← loop f x i hi₂ r
    pure (cons b y)
Tactic:
cases Nat.eq_or_lt_of_le hi₂ with
| inl heq =>
  cases heq; unfold loop; simp only [Nat.lt_irrefl, dif_neg, pure_bind]
| inr hlt =>
  conv =>
    lhs; unfold loop
    rw [dif_pos (Nat.succ_lt_succ hlt)]
    rw [get_cons_succ a x (hi₁:=Nat.succ_lt_succ hlt) (hi₂:=hlt)]
    rhs; ext b'; rw [push_cons_eq_cons_push]
    rw [mapM.loop_cons_succ f a x (hi₁:=Nat.succ_lt_succ hlt) (hi₂:=hlt) b (r.push b')]
  conv =>
    rhs; unfold loop; rw [dif_pos hlt, bind_assoc]
Proof state after:
no goals
Theorem: SizedArray.mapM.loop_cons_succ
Proof state before:
case inl
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
a : α
x : SizedArray α n
i : Nat
hi₁ : i + 1 ≤ n + 1
hi₂ : i ≤ n
b : β
r : SizedArray β i
heq : i = n
⊢ loop f (cons a x) (i + 1) hi₁ (cons b r) = do
    let y ← loop f x i hi₂ r
    pure (cons b y)
Tactic:
cases heq
Proof state after:
case inl.refl
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
a : α
x : SizedArray α n
b : β
hi₁ : n + 1 ≤ n + 1
hi₂ : n ≤ n
r : SizedArray β n
⊢ loop f (cons a x) (n + 1) hi₁ (cons b r) = do
    let y ← loop f x n hi₂ r
    pure (cons b y)
Theorem: SizedArray.mapM.loop_cons_succ
Proof state before:
case inl.refl
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
a : α
x : SizedArray α n
b : β
hi₁ : n + 1 ≤ n + 1
hi₂ : n ≤ n
r : SizedArray β n
⊢ loop f (cons a x) (n + 1) hi₁ (cons b r) = do
    let y ← loop f x n hi₂ r
    pure (cons b y)
Tactic:
unfold loop
Proof state after:
case inl.refl
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
a : α
x : SizedArray α n
b : β
hi₁ : n + 1 ≤ n + 1
hi₂ : n ≤ n
r : SizedArray β n
⊢ (if hlt : n + 1 < n + 1 then do
      let __do_lift ← f (cons a x)[n + 1]
      loop f (cons a x) (n + 1 + 1) hlt (push (cons b r) __do_lift)
    else
      let_fun this := (_ : n + 1 = n + 1);
      pure (this ▸ cons b r)) =
    do
    let y ←
      if hlt : n < n then do
          let __do_lift ← f x[n]
          loop f x (n + 1) hlt (push r __do_lift)
        else
          let_fun this := (_ : n = n);
          pure (this ▸ r)
    pure (cons b y)
Theorem: SizedArray.mapM.loop_cons_succ
Proof state before:
case inl.refl
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
a : α
x : SizedArray α n
b : β
hi₁ : n + 1 ≤ n + 1
hi₂ : n ≤ n
r : SizedArray β n
⊢ (if hlt : n + 1 < n + 1 then do
      let __do_lift ← f (cons a x)[n + 1]
      loop f (cons a x) (n + 1 + 1) hlt (push (cons b r) __do_lift)
    else
      let_fun this := (_ : n + 1 = n + 1);
      pure (this ▸ cons b r)) =
    do
    let y ←
      if hlt : n < n then do
          let __do_lift ← f x[n]
          loop f x (n + 1) hlt (push r __do_lift)
        else
          let_fun this := (_ : n = n);
          pure (this ▸ r)
    pure (cons b y)
Tactic:
simp only [Nat.lt_irrefl, dif_neg, pure_bind]
Proof state after:
no goals
Theorem: SizedArray.mapM.loop_cons_succ
Proof state before:
case inr
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
a : α
x : SizedArray α n
i : Nat
hi₁ : i + 1 ≤ n + 1
hi₂ : i ≤ n
b : β
r : SizedArray β i
hlt : i < n
⊢ loop f (cons a x) (i + 1) hi₁ (cons b r) = do
    let y ← loop f x i hi₂ r
    pure (cons b y)
Tactic:
conv =>
  lhs; unfold loop
  rw [dif_pos (Nat.succ_lt_succ hlt)]
  rw [get_cons_succ a x (hi₁:=Nat.succ_lt_succ hlt) (hi₂:=hlt)]
  rhs; ext b'; rw [push_cons_eq_cons_push]
  rw [mapM.loop_cons_succ f a x (hi₁:=Nat.succ_lt_succ hlt) (hi₂:=hlt) b (r.push b')]
Proof state after:
case inr
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
a : α
x : SizedArray α n
i : Nat
hi₁ : i + 1 ≤ n + 1
hi₂ : i ≤ n
b : β
r : SizedArray β i
hlt : i < n
⊢ (do
      let b' ← f x[i]
      let y ← loop f x (i + 1) hlt (push r b')
      pure (cons b y)) =
    do
    let y ← loop f x i hi₂ r
    pure (cons b y)
Theorem: SizedArray.mapM.loop_cons_succ
Proof state before:
case inr
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
a : α
x : SizedArray α n
i : Nat
hi₁ : i + 1 ≤ n + 1
hi₂ : i ≤ n
b : β
r : SizedArray β i
hlt : i < n
⊢ (do
      let b' ← f x[i]
      let y ← loop f x (i + 1) hlt (push r b')
      pure (cons b y)) =
    do
    let y ← loop f x i hi₂ r
    pure (cons b y)
Tactic:
conv =>
  rhs; unfold loop; rw [dif_pos hlt, bind_assoc]
Proof state after:
no goals
Theorem: SizedArray.mapM_cons
Proof state before:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
a : α
x : SizedArray α n
⊢ mapM f (cons a x) = do
    let b ← f a
    let y ← mapM f x
    pure (cons b y)
Tactic:
conv =>
  lhs; unfold mapM; unfold mapM.loop
  rw [dif_pos n.zero_lt_succ, get_cons_zero a x]
  rhs; ext b; change mapM.loop f (cons a x) (0+1) (n.zero_lt_succ) (cons b empty)
Proof state after:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
a : α
x : SizedArray α n
⊢ (do
      let b ← f a
      mapM.loop f (cons a x) (0 + 1) (_ : 0 < Nat.succ n) (cons b empty)) =
    do
    let b ← f a
    let y ← mapM f x
    pure (cons b y)
Theorem: SizedArray.mapM_cons
Proof state before:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
a : α
x : SizedArray α n
⊢ (do
      let b ← f a
      mapM.loop f (cons a x) (0 + 1) (_ : 0 < Nat.succ n) (cons b empty)) =
    do
    let b ← f a
    let y ← mapM f x
    pure (cons b y)
Tactic:
apply bind_congr
Proof state after:
case h
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
a : α
x : SizedArray α n
⊢ ∀ (a_1 : β),
    mapM.loop f (cons a x) (0 + 1) (_ : 0 < Nat.succ n) (cons a_1 empty) = do
      let y ← mapM f x
      pure (cons a_1 y)