ι : Type ?u.249050
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → α → α
hcomm : Commutative f
hassoc : Associative f
a b c : α
l : List α
⊢ foldl f (f (f a b) c) l = f b (foldl f (f a c) l)
ι : Type ?u.249050
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → α → α
hcomm : Commutative f
hassoc : Associative f
a b c : α
l : List α
⊢ foldl f a (b :: c :: l) = f b (foldl f a (c :: l))
simp only [foldl_cons]
ι : Type ?u.249050
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → α → α
hcomm : Commutative f
hassoc : Associative f
a b c : α
l : List α
⊢ foldl f (f (f a c) b) l = foldl f (f a c) (b :: l)
ι : Type ?u.249050
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → α → α
hcomm : Commutative f
hassoc : Associative f
a b c : α
l : List α
⊢ foldl f (f (f a b) c) l = f b (foldl f (f a c) l)
rw [← foldl_eq_of_comm_of_assoc .., right_comm _ hcomm hassoc]
no goals
ι : Type ?u.249050
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → α → α
hcomm : Commutative f
hassoc : Associative f
a b c : α
l : List α
⊢ foldl f (f (f a c) b) l = foldl f (f a c) (b :: l)
rfl