internlm/Lean-Github huggingface dataset:
Theorem: Array.anyM_cons_zero
Proof state before:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
a : α
x : Array α
stop : Nat
h : ¬stop ≤ size x
⊢ (if h : stop + 1 ≤ Nat.succ (size x) then anyM.loop p (cons a x) (stop + 1) h 0
    else anyM.loop p (cons a x) (Nat.succ (size x)) (_ : size (cons a x) ≤ size (cons a x)) 0) =
    do
    let b ← p a
    if b = true then pure true
      else if h : stop ≤ size x then anyM.loop p x stop h 0 else anyM.loop p x (size x) (_ : size x ≤ size x) 0
Tactic:
simp only [dif_neg h, dif_neg (fun h' => h <| Nat.le_of_succ_le_succ h')]
Proof state after:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
a : α
x : Array α
stop : Nat
h : ¬stop ≤ size x
⊢ anyM.loop p (cons a x) (Nat.succ (size x)) (_ : size (cons a x) ≤ size (cons a x)) 0 = do
    let b ← p a
    if b = true then pure true else anyM.loop p x (size x) (_ : size x ≤ size x) 0
Theorem: Array.anyM_cons_zero
Proof state before:
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → m Bool
a : α
x : Array α
stop : Nat
h : ¬stop ≤ size x
⊢ anyM.loop p (cons a x) (Nat.succ (size x)) (_ : size (cons a x) ≤ size (cons a x)) 0 = do
    let b ← p a
    if b = true then pure true else anyM.loop p x (size x) (_ : size x ≤ size x) 0
Tactic:
exact anyM_loop_cons_zero p a x .refl
Proof state after:
no goals
Theorem: Array.any_cons_zero
Proof state before:
α : Type u
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → Bool
stop : Nat
⊢ any (cons a x) p 0 (stop + 1) = (p a || any x p 0 stop)
Tactic:
dsimp [any, Id.run]
Proof state after:
α : Type u
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → Bool
stop : Nat
⊢ anyM p (cons a x) 0 (stop + 1) = (p a || anyM p x 0 stop)
Theorem: Array.any_cons_zero
Proof state before:
α : Type u
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → Bool
stop : Nat
⊢ anyM p (cons a x) 0 (stop + 1) = (p a || anyM p x 0 stop)
Tactic:
rewrite [anyM_cons_zero (m:=Id) p a x]
Proof state after:
α : Type u
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → Bool
stop : Nat
⊢ (do
      let b ← p a
      if b = true then pure true else anyM p x 0 stop) =
    (p a || anyM p x 0 stop)
Theorem: Array.any_cons_zero
Proof state before:
α : Type u
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → Bool
stop : Nat
⊢ (do
      let b ← p a
      if b = true then pure true else anyM p x 0 stop) =
    (p a || anyM p x 0 stop)
Tactic:
dsimp
Proof state after:
α : Type u
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → Bool
stop : Nat
⊢ (if p a = true then true else anyM p x 0 stop) = (p a || anyM p x 0 stop)
Theorem: Array.any_cons_zero
Proof state before:
α : Type u
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → Bool
stop : Nat
⊢ (if p a = true then true else anyM p x 0 stop) = (p a || anyM p x 0 stop)
Tactic:
match p a with
| true => simp only [ite_true, Bool.true_or]
| false => simp only [ite_false, Bool.false_or]
Proof state after:
no goals
Theorem: Array.any_cons_zero
Proof state before:
α : Type u
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → Bool
stop : Nat
⊢ (if true = true then true else anyM p x 0 stop) = (true || anyM p x 0 stop)
Tactic:
simp only [ite_true, Bool.true_or]
Proof state after:
no goals
Theorem: Array.any_cons_zero
Proof state before:
α : Type u
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → Bool
stop : Nat
⊢ (if false = true then true else anyM p x 0 stop) = (false || anyM p x 0 stop)
Tactic:
simp only [ite_false, Bool.false_or]
Proof state after:
no goals
Theorem: Array.any_cons
Proof state before:
α : Type u
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → Bool
⊢ any (cons a x) p 0 (size (cons a x)) = (p a || any x p 0 (size x))
Tactic:
rewrite [size_cons]
Proof state after:
α : Type u
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → Bool
⊢ any (cons a x) p 0 (Nat.succ (size x)) = (p a || any x p 0 (size x))
Theorem: Array.any_cons
Proof state before:
α : Type u
m : Type → Type v
inst✝ : Monad m
a : α
x : Array α
p : α → Bool
⊢ any (cons a x) p 0 (Nat.succ (size x)) = (p a || any x p 0 (size x))
Tactic:
exact any_cons_zero a x p
Proof state after:
no goals
Theorem: Array.any_push
Proof state before:
α : Type u
m : Type → Type v
inst✝ : Monad m
x : Array α
a : α
p : α → Bool
⊢ any (push x a) p 0 (size (push x a)) = (any x p 0 (size x) || p a)
Tactic:
induction x using cons_induction with
| empty =>
  simp only [push_empty_eq_cons, any_cons, any_empty, Bool.or_false, Bool.false_or]
| cons b x IH =>
  simp only [push_cons_eq_cons_push, any_cons, IH]
  exact Eq.symm <| Bool.or_assoc (p b) (x.any p) (p a)
Proof state after:
no goals
Theorem: Array.any_push
Proof state before:
case empty
α : Type u
m : Type → Type v
inst✝ : Monad m
a : α
p : α → Bool
⊢ any (push #[] a) p 0 (size (push #[] a)) = (any #[] p 0 (size #[]) || p a)
Tactic:
simp only [push_empty_eq_cons, any_cons, any_empty, Bool.or_false, Bool.false_or]
Proof state after:
no goals
Theorem: Array.any_push
Proof state before:
case cons
α : Type u
m : Type → Type v
inst✝ : Monad m
a : α
p : α → Bool
b : α
x : Array α
IH : any (push x a) p 0 (size (push x a)) = (any x p 0 (size x) || p a)
⊢ any (push (cons b x) a) p 0 (size (push (cons b x) a)) = (any (cons b x) p 0 (size (cons b x)) || p a)
Tactic:
simp only [push_cons_eq_cons_push, any_cons, IH]
Proof state after:
case cons
α : Type u
m : Type → Type v
inst✝ : Monad m
a : α
p : α → Bool
b : α
x : Array α
IH : any (push x a) p 0 (size (push x a)) = (any x p 0 (size x) || p a)
⊢ (p b || (any x p 0 (size x) || p a)) = (p b || any x p 0 (size x) || p a)
Theorem: Array.any_push
Proof state before:
case cons
α : Type u
m : Type → Type v
inst✝ : Monad m
a : α
p : α → Bool
b : α
x : Array α
IH : any (push x a) p 0 (size (push x a)) = (any x p 0 (size x) || p a)
⊢ (p b || (any x p 0 (size x) || p a)) = (p b || any x p 0 (size x) || p a)
Tactic:
exact Eq.symm <| Bool.or_assoc (p b) (x.any p) (p a)
Proof state after:
no goals
Theorem: Array.any_eq_any_data
Proof state before:
α : Type u
m : Type → Type v
inst✝ : Monad m
x : Array α
p : α → Bool
⊢ any x p 0 (size x) = List.any x.data p
Tactic:
induction x using cons_induction with
| empty => rfl
| cons a x IH =>
  conv => lhs; simp only [any_cons]
  conv => rhs; simp only [data_cons, List.any_cons]
  rw [IH]
Proof state after:
no goals
Theorem: Array.any_eq_any_data
Proof state before:
case empty
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → Bool
⊢ any #[] p 0 (size #[]) = List.any #[].data p
Tactic:
rfl
Proof state after:
no goals
Theorem: Array.any_eq_any_data
Proof state before:
case cons
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → Bool
a : α
x : Array α
IH : any x p 0 (size x) = List.any x.data p
⊢ any (cons a x) p 0 (size (cons a x)) = List.any (cons a x).data p
Tactic:
conv => lhs; simp only [any_cons]
Proof state after:
case cons
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → Bool
a : α
x : Array α
IH : any x p 0 (size x) = List.any x.data p
⊢ (p a || any x p 0 (size x)) = List.any (cons a x).data p
Theorem: Array.any_eq_any_data
Proof state before:
case cons
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → Bool
a : α
x : Array α
IH : any x p 0 (size x) = List.any x.data p
⊢ (p a || any x p 0 (size x)) = List.any (cons a x).data p
Tactic:
conv => rhs; simp only [data_cons, List.any_cons]
Proof state after:
case cons
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → Bool
a : α
x : Array α
IH : any x p 0 (size x) = List.any x.data p
⊢ (p a || any x p 0 (size x)) = (p a || List.any x.data p)
Theorem: Array.any_eq_any_data
Proof state before:
case cons
α : Type u
m : Type → Type v
inst✝ : Monad m
p : α → Bool
a : α
x : Array α
IH : any x p 0 (size x) = List.any x.data p
⊢ (p a || any x p 0 (size x)) = (p a || List.any x.data p)
Tactic:
rw [IH]
Proof state after:
no goals
Theorem: Array.mem_cons
Proof state before:
α : Type u
inst✝ : DecidableEq α
a b : α
x : Array α
⊢ any (cons b x) (fun x => a == x) 0 (size (cons b x)) = true ↔ a = b ∨ a ∈ x
Tactic:
rewrite [any_cons]
Proof state after:
α : Type u
inst✝ : DecidableEq α
a b : α
x : Array α
⊢ (a == b || any x (fun x => a == x) 0 (size x)) = true ↔ a = b ∨ a ∈ x
Theorem: Array.mem_cons
Proof state before:
α : Type u
inst✝ : DecidableEq α
a b : α
x : Array α
⊢ (a == b || any x (fun x => a == x) 0 (size x)) = true ↔ a = b ∨ a ∈ x
Tactic:
simp only [Bool.or_eq_true, beq_iff_eq]
Proof state after:
α : Type u
inst✝ : DecidableEq α
a b : α
x : Array α
⊢ a = b ∨ any x (fun x => a == x) 0 (size x) = true ↔ a = b ∨ a ∈ x
Theorem: Array.mem_cons
Proof state before:
α : Type u
inst✝ : DecidableEq α
a b : α
x : Array α
⊢ a = b ∨ any x (fun x => a == x) 0 (size x) = true ↔ a = b ∨ a ∈ x
Tactic:
exact Iff.rfl
Proof state after:
no goals
Theorem: Array.mem_push
Proof state before:
α : Type u
inst✝ : DecidableEq α
a b : α
x : Array α
⊢ any (push x b) (fun x => a == x) 0 (size (push x b)) = true ↔ a ∈ x ∨ a = b
Tactic:
rewrite [any_push]
Proof state after:
α : Type u
inst✝ : DecidableEq α
a b : α
x : Array α
⊢ (any x (fun x => a == x) 0 (size x) || a == b) = true ↔ a ∈ x ∨ a = b
Theorem: Array.mem_push
Proof state before:
α : Type u
inst✝ : DecidableEq α
a b : α
x : Array α
⊢ (any x (fun x => a == x) 0 (size x) || a == b) = true ↔ a ∈ x ∨ a = b
Tactic:
simp only [Bool.or_eq_true, beq_iff_eq]
Proof state after:
α : Type u
inst✝ : DecidableEq α
a b : α
x : Array α
⊢ any x (fun x => a == x) 0 (size x) = true ∨ a = b ↔ a ∈ x ∨ a = b
Theorem: Array.mem_push
Proof state before:
α : Type u
inst✝ : DecidableEq α
a b : α
x : Array α
⊢ any x (fun x => a == x) 0 (size x) = true ∨ a = b ↔ a ∈ x ∨ a = b
Tactic:
exact Iff.rfl
Proof state after:
no goals
Theorem: Array.mem_iff_mem_data
Proof state before:
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ a ∈ x ↔ a ∈ x.data
Tactic:
induction x using cons_induction with
| empty =>
  simp only [not_mem_empty, data_toArray, List.not_mem_nil]
| cons v x IH =>
  rw [mem_cons, data_cons, List.mem_cons, IH]
Proof state after:
no goals
Theorem: Array.mem_iff_mem_data
Proof state before:
case empty
α : Type u
inst✝ : DecidableEq α
a : α
⊢ a ∈ #[] ↔ a ∈ #[].data
Tactic:
simp only [not_mem_empty, data_toArray, List.not_mem_nil]
Proof state after:
no goals
Theorem: Array.mem_iff_mem_data
Proof state before:
case cons
α : Type u
inst✝ : DecidableEq α
a v : α
x : Array α
IH : a ∈ x ↔ a ∈ x.data
⊢ a ∈ cons v x ↔ a ∈ (cons v x).data
Tactic:
rw [mem_cons, data_cons, List.mem_cons, IH]
Proof state after:
no goals
Theorem: Array.mem_iff_get
Proof state before:
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ a ∈ x ↔ ∃ i hi, x[i] = a
Tactic:
rewrite [mem_iff_mem_data, List.mem_iff_get]
Proof state after:
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (∃ n, List.get x.data n = a) ↔ ∃ i hi, x[i] = a
Theorem: Array.mem_iff_get
Proof state before:
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (∃ n, List.get x.data n = a) ↔ ∃ i hi, x[i] = a
Tactic:
simp only [getElem_eq_data_get]
Proof state after:
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (∃ n, List.get x.data n = a) ↔ ∃ i hi, List.get x.data { val := i, isLt := hi } = a
Theorem: Array.mem_iff_get
Proof state before:
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (∃ n, List.get x.data n = a) ↔ ∃ i hi, List.get x.data { val := i, isLt := hi } = a
Tactic:
constructor
Proof state after:
case mp
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (∃ n, List.get x.data n = a) → ∃ i hi, List.get x.data { val := i, isLt := hi } = a

case mpr
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (∃ i hi, List.get x.data { val := i, isLt := hi } = a) → ∃ n, List.get x.data n = a
Theorem: Array.mem_iff_get
Proof state before:
case mp
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (∃ n, List.get x.data n = a) → ∃ i hi, List.get x.data { val := i, isLt := hi } = a

case mpr
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (∃ i hi, List.get x.data { val := i, isLt := hi } = a) → ∃ n, List.get x.data n = a
Tactic:
. exact fun ⟨i,hxi⟩ => ⟨i.1,i.2,hxi⟩
Proof state after:
case mpr
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (∃ i hi, List.get x.data { val := i, isLt := hi } = a) → ∃ n, List.get x.data n = a
Theorem: Array.mem_iff_get
Proof state before:
case mpr
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (∃ i hi, List.get x.data { val := i, isLt := hi } = a) → ∃ n, List.get x.data n = a
Tactic:
. exact fun ⟨i,hi,hxi⟩ => ⟨⟨i,hi⟩,hxi⟩
Proof state after:
no goals
Theorem: Array.mem_iff_get
Proof state before:
case mp
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (∃ n, List.get x.data n = a) → ∃ i hi, List.get x.data { val := i, isLt := hi } = a
Tactic:
exact fun ⟨i,hxi⟩ => ⟨i.1,i.2,hxi⟩
Proof state after:
no goals
Theorem: Array.mem_iff_get
Proof state before:
case mpr
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (∃ i hi, List.get x.data { val := i, isLt := hi } = a) → ∃ n, List.get x.data n = a
Tactic:
exact fun ⟨i,hi,hxi⟩ => ⟨⟨i,hi⟩,hxi⟩
Proof state after:
no goals
Theorem: Array.foldlM_eq_foldlM_data'.aux
Proof 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]
Proof state after:
no goals
Theorem: Array.foldlM_eq_foldlM_data'.aux
Proof 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
Proof 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)
Theorem: Array.foldlM_eq_foldlM_data'.aux
Proof 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
Proof 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)
Theorem: Array.foldlM_eq_foldlM_data'.aux
Proof 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
Proof 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)
Theorem: Array.foldlM_eq_foldlM_data'.aux
Proof 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]
Proof 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 []
Theorem: Array.foldlM_eq_foldlM_data'.aux
Proof 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
Proof state after:
no goals
Theorem: Array.foldlM_eq_foldlM_data'.aux
Proof 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
Proof 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)
Theorem: Array.foldlM_eq_foldlM_data'.aux
Proof 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
Proof 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)
Theorem: Array.foldlM_eq_foldlM_data'.aux
Proof 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
Proof 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)
Theorem: Array.foldlM_eq_foldlM_data'.aux
Proof 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]
Proof 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)
Theorem: Array.foldlM_eq_foldlM_data'.aux
Proof 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]
Proof state after:
no goals
Theorem: Array.foldlM_eq_foldlM_data'
Proof state before:
α : Type u
m : Type u_1 → Type u_2
β : Type u_1
inst✝ : Monad m
f : β → α → m β
init : β
arr : Array α
⊢ foldlM f init arr 0 (size arr) = List.foldlM f init arr.data
Tactic:
simp only [foldlM, Nat.le_refl, dif_pos, Nat.sub_zero]
Proof state after:
α : Type u
m : Type u_1 → Type u_2
β : Type u_1
inst✝ : Monad m
f : β → α → m β
init : β
arr : Array α
⊢ foldlM.loop f arr (size arr) (_ : size arr ≤ size arr) (size arr) 0 init = List.foldlM f init arr.data
Theorem: Array.foldlM_eq_foldlM_data'
Proof state before:
α : Type u
m : Type u_1 → Type u_2
β : Type u_1
inst✝ : Monad m
f : β → α → m β
init : β
arr : Array α
⊢ foldlM.loop f arr (size arr) (_ : size arr ≤ size arr) (size arr) 0 init = List.foldlM f init arr.data
Tactic:
exact foldlM_eq_foldlM_data'.aux f arr arr.size 0 rfl init
Proof state after:
no goals