Theorem: Array.foldl_assoc (GMLInit/Data/Array/Basic.lean)

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]
State after:
no goals

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
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)

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)
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)

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]
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

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
State after:
no goals

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)
State after:
no goals

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
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)

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
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)

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')
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)

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')
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)

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)]
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)

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]
State after:
no goals

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')
State after:
no goals

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'
State after:
no goals

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
State after:
no goals

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'
State after:
no goals