internlm/Lean-Github huggingface dataset:
Theorem: Array.foldlM_step
Proof state before:
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
⊢ foldlM.loop f as stop ⋯ (stop - start) start b = do
    let b ← f b as[start]
    if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
      else foldlM.loop f as as.size ⋯ (as.size - (start + 1)) (start + 1) b
Tactic:
rw [Array.foldlM.loop]
Proof state after:
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
⊢ (if hlt : start < stop then
      match stop - start with
      | 0 => pure b
      | i'.succ =>
        let_fun this := ⋯;
        do
        let __do_lift ← f b as[start]
        foldlM.loop f as stop ⋯ i' (start + 1) __do_lift
    else pure b) =
    do
    let b ← f b as[start]
    if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
      else foldlM.loop f as as.size ⋯ (as.size - (start + 1)) (start + 1) b
Theorem: Array.foldlM_step
Proof state before:
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
⊢ (if hlt : start < stop then
      match stop - start with
      | 0 => pure b
      | i'.succ =>
        let_fun this := ⋯;
        do
        let __do_lift ← f b as[start]
        foldlM.loop f as stop ⋯ i' (start + 1) __do_lift
    else pure b) =
    do
    let b ← f b as[start]
    if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
      else foldlM.loop f as as.size ⋯ (as.size - (start + 1)) (start + 1) b
Tactic:
rw [dif_pos hstart]
Proof state after:
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
⊢ (match stop - start with
    | 0 => pure b
    | i'.succ =>
      let_fun this := ⋯;
      do
      let __do_lift ← f b as[start]
      foldlM.loop f as stop ⋯ i' (start + 1) __do_lift) =
    do
    let b ← f b as[start]
    if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
      else foldlM.loop f as as.size ⋯ (as.size - (start + 1)) (start + 1) b
Theorem: Array.foldlM_step
Proof state before:
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
⊢ (match stop - start with
    | 0 => pure b
    | i'.succ =>
      let_fun this := ⋯;
      do
      let __do_lift ← f b as[start]
      foldlM.loop f as stop ⋯ i' (start + 1) __do_lift) =
    do
    let b ← f b as[start]
    if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
      else foldlM.loop f as as.size ⋯ (as.size - (start + 1)) (start + 1) b
Tactic:
split
Proof state after:
case h_1
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
i✝ : Nat
heq✝ : stop - start = 0
⊢ pure b = do
    let b ← f b as[start]
    if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
      else foldlM.loop f as as.size ⋯ (as.size - (start + 1)) (start + 1) b

case h_2
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
i✝ i'✝ : Nat
heq✝ : stop - start = i'✝.succ
⊢ (let_fun this := ⋯;
    do
    let __do_lift ← f b as[start]
    foldlM.loop f as stop ⋯ i'✝ (start + 1) __do_lift) =
    do
    let b ← f b as[start]
    if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
      else foldlM.loop f as as.size ⋯ (as.size - (start + 1)) (start + 1) b
Theorem: Array.foldlM_step
Proof state before:
case h_1
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
i✝ : Nat
heq✝ : stop - start = 0
⊢ pure b = do
    let b ← f b as[start]
    if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
      else foldlM.loop f as as.size ⋯ (as.size - (start + 1)) (start + 1) b

case h_2
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
i✝ i'✝ : Nat
heq✝ : stop - start = i'✝.succ
⊢ (let_fun this := ⋯;
    do
    let __do_lift ← f b as[start]
    foldlM.loop f as stop ⋯ i'✝ (start + 1) __do_lift) =
    do
    let b ← f b as[start]
    if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
      else foldlM.loop f as as.size ⋯ (as.size - (start + 1)) (start + 1) b
Tactic:
next heq =>
  absurd heq
  apply Nat.sub_ne_zero_of_lt hstart
Proof state after:
case h_2
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
i✝ i'✝ : Nat
heq✝ : stop - start = i'✝.succ
⊢ (let_fun this := ⋯;
    do
    let __do_lift ← f b as[start]
    foldlM.loop f as stop ⋯ i'✝ (start + 1) __do_lift) =
    do
    let b ← f b as[start]
    if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
      else foldlM.loop f as as.size ⋯ (as.size - (start + 1)) (start + 1) b
Theorem: Array.foldlM_step
Proof state before:
case h_2
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
i✝ i'✝ : Nat
heq✝ : stop - start = i'✝.succ
⊢ (let_fun this := ⋯;
    do
    let __do_lift ← f b as[start]
    foldlM.loop f as stop ⋯ i'✝ (start + 1) __do_lift) =
    do
    let b ← f b as[start]
    if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
      else foldlM.loop f as as.size ⋯ (as.size - (start + 1)) (start + 1) b
Tactic:
next heq =>
  simp
  congr
  funext b
  rw [dif_pos hstop]
  rw [Nat.sub_succ, heq, Nat.pred_succ]
Proof state after:
no goals
Theorem: Array.foldlM_step
Proof state before:
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
i✝ : Nat
heq : stop - start = 0
⊢ pure b = do
    let b ← f b as[start]
    if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
      else foldlM.loop f as as.size ⋯ (as.size - (start + 1)) (start + 1) b
Tactic:
absurd heq
Proof state after:
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
i✝ : Nat
heq : stop - start = 0
⊢ ¬stop - start = 0
Theorem: Array.foldlM_step
Proof state before:
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
i✝ : Nat
heq : stop - start = 0
⊢ ¬stop - start = 0
Tactic:
apply Nat.sub_ne_zero_of_lt hstart
Proof state after:
no goals
Theorem: Array.foldlM_step
Proof state before:
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
i✝ i'✝ : Nat
heq : stop - start = i'✝.succ
⊢ (let_fun this := ⋯;
    do
    let __do_lift ← f b as[start]
    foldlM.loop f as stop ⋯ i'✝ (start + 1) __do_lift) =
    do
    let b ← f b as[start]
    if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
      else foldlM.loop f as as.size ⋯ (as.size - (start + 1)) (start + 1) b
Tactic:
simp
Proof state after:
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
i✝ i'✝ : Nat
heq : stop - start = i'✝.succ
⊢ (do
      let __do_lift ← f b as[start]
      foldlM.loop f as stop ⋯ i'✝ (start + 1) __do_lift) =
    do
    let b ← f b as[start]
    if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
      else foldlM.loop f as as.size ⋯ (as.size - (start + 1)) (start + 1) b
Theorem: Array.foldlM_step
Proof state before:
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
i✝ i'✝ : Nat
heq : stop - start = i'✝.succ
⊢ (do
      let __do_lift ← f b as[start]
      foldlM.loop f as stop ⋯ i'✝ (start + 1) __do_lift) =
    do
    let b ← f b as[start]
    if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
      else foldlM.loop f as as.size ⋯ (as.size - (start + 1)) (start + 1) b
Tactic:
congr
Proof state after:
case e_a
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
i✝ i'✝ : Nat
heq : stop - start = i'✝.succ
⊢ (fun __do_lift => foldlM.loop f as stop ⋯ i'✝ (start + 1) __do_lift) = fun b =>
    if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
    else foldlM.loop f as as.size ⋯ (as.size - (start + 1)) (start + 1) b
Theorem: Array.foldlM_step
Proof state before:
case e_a
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
i✝ i'✝ : Nat
heq : stop - start = i'✝.succ
⊢ (fun __do_lift => foldlM.loop f as stop ⋯ i'✝ (start + 1) __do_lift) = fun b =>
    if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
    else foldlM.loop f as as.size ⋯ (as.size - (start + 1)) (start + 1) b
Tactic:
funext b
Proof state after:
case e_a.h
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b✝ : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
i✝ i'✝ : Nat
heq : stop - start = i'✝.succ
b : β
⊢ foldlM.loop f as stop ⋯ i'✝ (start + 1) b =
    if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
    else foldlM.loop f as as.size ⋯ (as.size - (start + 1)) (start + 1) b
Theorem: Array.foldlM_step
Proof state before:
case e_a.h
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b✝ : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
i✝ i'✝ : Nat
heq : stop - start = i'✝.succ
b : β
⊢ foldlM.loop f as stop ⋯ i'✝ (start + 1) b =
    if h : stop ≤ as.size then foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
    else foldlM.loop f as as.size ⋯ (as.size - (start + 1)) (start + 1) b
Tactic:
rw [dif_pos hstop]
Proof state after:
case e_a.h
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b✝ : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
i✝ i'✝ : Nat
heq : stop - start = i'✝.succ
b : β
⊢ foldlM.loop f as stop ⋯ i'✝ (start + 1) b = foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
Theorem: Array.foldlM_step
Proof state before:
case e_a.h
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b✝ : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
i✝ i'✝ : Nat
heq : stop - start = i'✝.succ
b : β
⊢ foldlM.loop f as stop ⋯ i'✝ (start + 1) b = foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
Tactic:
rw [Nat.sub_succ, heq, Nat.pred_succ]
Proof state after:
no goals
Theorem: Array.foldl_stop
Proof state before:
β : Type u_2
α : Type u_1
f : β → α → β
b : β
as : Array α
stop : Nat
hstop : stop ≤ as.size
⊢ foldl f b as stop stop = b
Tactic:
apply foldlM_stop
Proof state after:
case hstop
β : Type u_2
α : Type u_1
f : β → α → β
b : β
as : Array α
stop : Nat
hstop : stop ≤ as.size
⊢ stop ≤ as.size
Theorem: Array.foldl_stop
Proof state before:
case hstop
β : Type u_2
α : Type u_1
f : β → α → β
b : β
as : Array α
stop : Nat
hstop : stop ≤ as.size
⊢ stop ≤ as.size
Tactic:
assumption
Proof state after:
no goals
Theorem: Array.foldl_step
Proof state before:
β : Type u_2
α : Type u_1
f : β → α → β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
⊢ let_fun this := ⋯;
  foldl f b as start stop = foldl f (f b as[start]) as (start + 1) stop
Tactic:
apply foldlM_step
Proof state after:
case hstart
β : Type u_2
α : Type u_1
f : β → α → β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
⊢ start < stop

case hstop
β : Type u_2
α : Type u_1
f : β → α → β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
⊢ stop ≤ as.size
Theorem: Array.foldl_step
Proof state before:
case hstart
β : Type u_2
α : Type u_1
f : β → α → β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
⊢ start < stop

case hstop
β : Type u_2
α : Type u_1
f : β → α → β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
⊢ stop ≤ as.size
Tactic:
assumption
Proof state after:
case hstop
β : Type u_2
α : Type u_1
f : β → α → β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
⊢ stop ≤ as.size
Theorem: Array.foldl_step
Proof state before:
case hstop
β : Type u_2
α : Type u_1
f : β → α → β
b : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
⊢ stop ≤ as.size
Tactic:
assumption
Proof state after:
no goals
Theorem: Array.foldl_assoc
Proof state before:
β : Sort ?u.17044
α : Type u_1
f : β → α → β
b✝ : β
h : α → α → α
inst✝ : Std.Associative h
as : Array α
b c : α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ as.size
⊢ foldl h (h b c) as start stop = h b (foldl h c as start stop)
Tactic:
by_cases start = stop with
| isTrue heq =>
  cases heq
  rw [foldl_stop] <;> try (exact hstop)
  rw [foldl_stop]; exact hstop
| isFalse hne =>
  have hstart' : start < stop := Nat.lt_of_le_of_ne hstart hne
  have : start < as.size := Nat.lt_of_lt_of_le hstart' hstop
  rw [foldl_step h (h b c)] <;> try (first | exact hstop | exact hstart')
  rw [foldl_step h c] <;> try (first | exact hstop | exact hstart')
  rw [Std.Associative.assoc (op:=h)]
  rw [foldl_assoc as b (h c as[start]) (start+1) stop hstart' hstop]
Proof state after:
no goals
Theorem: Array.foldl_assoc
Proof state before:
β : Sort ?u.17044
α : Type u_1
f : β → α → β
b✝ : β
h : α → α → α
inst✝ : Std.Associative h
as : Array α
b c : α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ as.size
heq : start = stop
⊢ foldl h (h b c) as start stop = h b (foldl h c as start stop)
Tactic:
cases heq
Proof state after:
case refl
β : Sort ?u.17044
α : Type u_1
f : β → α → β
b✝ : β
h : α → α → α
inst✝ : Std.Associative h
as : Array α
b c : α
start : Nat
hstart : start ≤ start
hstop : start ≤ as.size
⊢ foldl h (h b c) as start start = h b (foldl h c as start start)
Theorem: Array.foldl_assoc
Proof state before:
case refl
β : Sort ?u.17044
α : Type u_1
f : β → α → β
b✝ : β
h : α → α → α
inst✝ : Std.Associative h
as : Array α
b c : α
start : Nat
hstart : start ≤ start
hstop : start ≤ as.size
⊢ foldl h (h b c) as start start = h b (foldl h c as start start)
Tactic:
rw [foldl_stop] <;> try (exact hstop)
Proof state after:
case refl
β : Sort ?u.17044
α : Type u_1
f : β → α → β
b✝ : β
h : α → α → α
inst✝ : Std.Associative h
as : Array α
b c : α
start : Nat
hstart : start ≤ start
hstop : start ≤ as.size
⊢ h b c = h b (foldl h c as start start)
Theorem: Array.foldl_assoc
Proof state before:
case refl
β : Sort ?u.17044
α : Type u_1
f : β → α → β
b✝ : β
h : α → α → α
inst✝ : Std.Associative h
as : Array α
b c : α
start : Nat
hstart : start ≤ start
hstop : start ≤ as.size
⊢ h b c = h b (foldl h c as start start)
Tactic:
rw [foldl_stop]
Proof state after:
case refl.hstop
β : Sort ?u.17044
α : Type u_1
f : β → α → β
b✝ : β
h : α → α → α
inst✝ : Std.Associative h
as : Array α
b c : α
start : Nat
hstart : start ≤ start
hstop : start ≤ as.size
⊢ start ≤ as.size
Theorem: Array.foldl_assoc
Proof state before:
case refl.hstop
β : Sort ?u.17044
α : Type u_1
f : β → α → β
b✝ : β
h : α → α → α
inst✝ : Std.Associative h
as : Array α
b c : α
start : Nat
hstart : start ≤ start
hstop : start ≤ as.size
⊢ start ≤ as.size
Tactic:
exact hstop
Proof state after:
no goals
Theorem: Array.foldl_assoc
Proof state before:
case refl.hstop
β : Sort ?u.17044
α : Type u_1
f : β → α → β
b✝ : β
h : α → α → α
inst✝ : Std.Associative h
as : Array α
b c : α
start : Nat
hstart : start ≤ start
hstop : start ≤ as.size
⊢ start ≤ as.size
Tactic:
(exact hstop)
Proof state after:
no goals
Theorem: Array.foldl_assoc
Proof state before:
β : Sort ?u.17044
α : Type u_1
f : β → α → β
b✝ : β
h : α → α → α
inst✝ : Std.Associative h
as : Array α
b c : α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ as.size
hne : ¬start = stop
⊢ foldl h (h b c) as start stop = h b (foldl h c as start stop)
Tactic:
have hstart' : start < stop := Nat.lt_of_le_of_ne hstart hne
Proof state after:
β : Sort ?u.17044
α : Type u_1
f : β → α → β
b✝ : β
h : α → α → α
inst✝ : Std.Associative h
as : Array α
b c : α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ as.size
hne : ¬start = stop
hstart' : start < stop
⊢ foldl h (h b c) as start stop = h b (foldl h c as start stop)
Theorem: Array.foldl_assoc
Proof state before:
β : Sort ?u.17044
α : Type u_1
f : β → α → β
b✝ : β
h : α → α → α
inst✝ : Std.Associative h
as : Array α
b c : α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ as.size
hne : ¬start = stop
hstart' : start < stop
⊢ foldl h (h b c) as start stop = h b (foldl h c as start stop)
Tactic:
have : start < as.size := Nat.lt_of_lt_of_le hstart' hstop
Proof state after:
β : Sort ?u.17044
α : Type u_1
f : β → α → β
b✝ : β
h : α → α → α
inst✝ : Std.Associative h
as : Array α
b c : α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ as.size
hne : ¬start = stop
hstart' : start < stop
this : start < as.size
⊢ foldl h (h b c) as start stop = h b (foldl h c as start stop)
Theorem: Array.foldl_assoc
Proof state before:
β : Sort ?u.17044
α : Type u_1
f : β → α → β
b✝ : β
h : α → α → α
inst✝ : Std.Associative h
as : Array α
b c : α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ as.size
hne : ¬start = stop
hstart' : start < stop
this : start < as.size
⊢ foldl h (h b c) as start stop = h b (foldl h c as start stop)
Tactic:
rw [foldl_step h (h b c)] <;> try (first | exact hstop | exact hstart')
Proof state after:
β : Sort ?u.17044
α : Type u_1
f : β → α → β
b✝ : β
h : α → α → α
inst✝ : Std.Associative h
as : Array α
b c : α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ as.size
hne : ¬start = stop
hstart' : start < stop
this : start < as.size
⊢ foldl h (h (h b c) as[start]) as (start + 1) stop = h b (foldl h c as start stop)
Theorem: Array.foldl_assoc
Proof state before:
β : Sort ?u.17044
α : Type u_1
f : β → α → β
b✝ : β
h : α → α → α
inst✝ : Std.Associative h
as : Array α
b c : α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ as.size
hne : ¬start = stop
hstart' : start < stop
this : start < as.size
⊢ foldl h (h (h b c) as[start]) as (start + 1) stop = h b (foldl h c as start stop)
Tactic:
rw [foldl_step h c] <;> try (first | exact hstop | exact hstart')
Proof state after:
β : Sort ?u.17044
α : Type u_1
f : β → α → β
b✝ : β
h : α → α → α
inst✝ : Std.Associative h
as : Array α
b c : α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ as.size
hne : ¬start = stop
hstart' : start < stop
this : start < as.size
⊢ foldl h (h (h b c) as[start]) as (start + 1) stop = h b (foldl h (h c as[start]) as (start + 1) stop)
Theorem: Array.foldl_assoc
Proof state before:
β : Sort ?u.17044
α : Type u_1
f : β → α → β
b✝ : β
h : α → α → α
inst✝ : Std.Associative h
as : Array α
b c : α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ as.size
hne : ¬start = stop
hstart' : start < stop
this : start < as.size
⊢ foldl h (h (h b c) as[start]) as (start + 1) stop = h b (foldl h (h c as[start]) as (start + 1) stop)
Tactic:
rw [Std.Associative.assoc (op:=h)]
Proof state after:
β : Sort ?u.17044
α : Type u_1
f : β → α → β
b✝ : β
h : α → α → α
inst✝ : Std.Associative h
as : Array α
b c : α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ as.size
hne : ¬start = stop
hstart' : start < stop
this : start < as.size
⊢ foldl h (h b (h c as[start])) as (start + 1) stop = h b (foldl h (h c as[start]) as (start + 1) stop)
Theorem: Array.foldl_assoc
Proof state before:
β : Sort ?u.17044
α : Type u_1
f : β → α → β
b✝ : β
h : α → α → α
inst✝ : Std.Associative h
as : Array α
b c : α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ as.size
hne : ¬start = stop
hstart' : start < stop
this : start < as.size
⊢ foldl h (h b (h c as[start])) as (start + 1) stop = h b (foldl h (h c as[start]) as (start + 1) stop)
Tactic:
rw [foldl_assoc as b (h c as[start]) (start+1) stop hstart' hstop]
Proof state after:
no goals
Theorem: Array.foldl_assoc
Proof state before:
case hstop
β : Sort ?u.17044
α : Type u_1
f : β → α → β
b✝ : β
h : α → α → α
inst✝ : Std.Associative h
as : Array α
b c : α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ as.size
hne : ¬start = stop
hstart' : start < stop
this : start < as.size
⊢ stop ≤ as.size
Tactic:
(first | exact hstop | exact hstart')
Proof state after:
no goals
Theorem: Array.foldl_assoc
Proof state before:
case hstop
β : Sort ?u.17044
α : Type u_1
f : β → α → β
b✝ : β
h : α → α → α
inst✝ : Std.Associative h
as : Array α
b c : α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ as.size
hne : ¬start = stop
hstart' : start < stop
this : start < as.size
⊢ stop ≤ as.size
Tactic:
first | exact hstop | exact hstart'
Proof state after:
no goals
Theorem: Array.foldl_assoc
Proof state before:
case hstop
β : Sort ?u.17044
α : Type u_1
f : β → α → β
b✝ : β
h : α → α → α
inst✝ : Std.Associative h
as : Array α
b c : α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ as.size
hne : ¬start = stop
hstart' : start < stop
this : start < as.size
⊢ stop ≤ as.size
Tactic:
exact hstop
Proof state after:
no goals
Theorem: Array.foldl_assoc
Proof state before:
case hstart
β : Sort ?u.17044
α : Type u_1
f : β → α → β
b✝ : β
h : α → α → α
inst✝ : Std.Associative h
as : Array α
b c : α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ as.size
hne : ¬start = stop
hstart' : start < stop
this : start < as.size
⊢ start < stop
Tactic:
exact hstart'
Proof state after:
no goals
Theorem: Array.foldrM_stop
Proof state before:
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b : β
as : Array α
stop : Nat
hstop : stop ≤ as.size
⊢ foldrM f b as stop stop = pure b
Tactic:
simp only [Array.foldrM]
Proof state after:
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b : β
as : Array α
stop : Nat
hstop : stop ≤ as.size
⊢ (if h : stop ≤ as.size then if stop < stop then foldrM.fold f as stop stop h b else pure b
    else if stop < as.size then foldrM.fold f as stop as.size ⋯ b else pure b) =
    pure b
Theorem: Array.foldrM_stop
Proof state before:
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b : β
as : Array α
stop : Nat
hstop : stop ≤ as.size
⊢ (if h : stop ≤ as.size then if stop < stop then foldrM.fold f as stop stop h b else pure b
    else if stop < as.size then foldrM.fold f as stop as.size ⋯ b else pure b) =
    pure b
Tactic:
rw [dif_pos hstop]
Proof state after:
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b : β
as : Array α
stop : Nat
hstop : stop ≤ as.size
⊢ (if stop < stop then foldrM.fold f as stop stop hstop b else pure b) = pure b
Theorem: Array.foldrM_stop
Proof state before:
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b : β
as : Array α
stop : Nat
hstop : stop ≤ as.size
⊢ (if stop < stop then foldrM.fold f as stop stop hstop b else pure b) = pure b
Tactic:
rw [if_neg (by irreflexivity)]
Proof state after:
no goals
Theorem: Array.foldrM_stop
Proof state before:
α : Type u_1
β : Type u_3
m : Type u_3 → Type u_2
inst✝ : Monad m
f : α → β → m β
b : β
as : Array α
stop : Nat
hstop : stop ≤ as.size
⊢ ¬stop < stop
Tactic:
irreflexivity
Proof state after:
no goals