feat(data/list/basic): Miscellaneous fold lemmas (#12579)

src/data/list/basic.lean

@@ -2102,6 +2102,17 @@ end
 | b []      l₂ := rfl
 | b (a::l₁) l₂ := by simp only [cons_append, foldr_cons, foldr_append b l₁ l₂]
 
+@[simp] theorem foldl_fixed {a : α} : Π l : list β, foldl (λ a b, a) a l = a
+| []     := rfl
+| (b::l) := by rw [foldl_cons, foldl_fixed l]
+
+@[simp] theorem foldr_fixed {b : β} : Π l : list α, foldr (λ a b, b) b l = b
+| []     := rfl
+| (a::l) := by rw [foldr_cons, foldr_fixed l]
+
+@[simp] theorem foldl_combinator_K {a : α} : Π l : list β, foldl combinator.K a l = a :=
+foldl_fixed
+
 @[simp] theorem foldl_join (f : α → β → α) :
   ∀ (a : α) (L : list (list β)), foldl f a (join L) = foldl (foldl f) a L
 | a []     := rfl

src/logic/function/iterate.lean

@@ -165,3 +165,19 @@ lemma iterate_commute (m n : ℕ) : commute (λ f : α → α, f^[m]) (λ f, f^[
 λ f, iterate_comm f m n
 
 end function
+
+namespace list
+open function
+
+theorem foldl_const (f : α → α) (a : α) (l : list β) : l.foldl (λ b _, f b) a = (f^[l.length]) a :=
+begin
+  induction l with b l H generalizing a,
+  { refl },
+  { rw [length_cons, foldl, iterate_succ_apply, H] }
+end
+
+theorem foldr_const (f : β → β) (b : β) : Π l : list α, l.foldr (λ _, f) b = (f^[l.length]) b
+| []     := rfl
+| (a::l) := by rw [length_cons, foldr, foldr_const l, iterate_succ_apply']
+
+end list