List.foldl を紹介する

Fixes #917

Examples/Type/List.lean

@@ -73,7 +73,7 @@ end Hidden --#
 
 variable {α β : Type}
 
-/-- #### `List.map` の使用例
+/-- #### List.map の使用例
 
 `xs.map f` は、関数 `f : α → β` をリスト `xs : List α` の各要素に適用して、
 新しく `List β` の項を作る。
@@ -85,3 +85,54 @@ example {a₁ a₂ a₃ : α} (f : α → β)
 -- リストの各要素を 2 倍する
 #guard List.map (fun x => x * 2) [1, 2, 3] = [2, 4, 6]
 
+/- ### foldl
+
+引数に `List α` の項を取る関数は、リストに対する再帰を使って定義されることが多いものです。たとえば、リストの各要素を足し合わせる関数は次のように定義できます。
+-/
+
+/-- 自然数のリストに対して、その総和を計算する -/
+def List.sum : List Nat → Nat
+  | [] => 0
+  | x :: xs => x + xs.sum
+
+#guard [1, 2, 3, 4].sum = 10
+
+/- これが「各要素を足し合わせる」ではなくて「積を計算する」なら次のようになります。-/
+
+/-- 自然数のリストに対して、その積を計算する -/
+def List.prod : List Nat → Nat
+  | [] => 1
+  | x :: xs => x * xs.prod
+
+#guard [1, 2, 3, 4].prod = 24
+
+/- この二つの関数は初期値と、適用する二項演算だけが異なり、後は一致しています。そこでこの共通する部分を抜き出したのが `List.foldl` です。`List.foldl` はリストを消費しながら二項演算を適用していき、最終的な結果を返します。
+-/
+
+/-- `List.foldl` の例示のための型クラス -/
+class FoldInit (α β : Type) where
+  /-- 二項演算 -/
+  op : α → β → α
+
+-- 左結合的な演算子として `⊗` を定義する
+@[inherit_doc] infixl:70 "⊗" => FoldInit.op
+
+/-- #### List.foldl の使用例
+
+初期値が `init : α` で、適用する二項演算が `⊗ : α → β → α` だとする。
+また `⊗` は左結合的、つまり `a ⊗ b ⊗ c = (a ⊗ b) ⊗ c` であるとする。
+このとき `[b₁, b₂, b₃] : List β` に対して、
+`List.foldl` は左に初期値を挿入して順に `⊗` を適用したものに等しい。
+-/
+example [FoldInit α β] {b₁ b₂ b₃ : β} (init : α) :
+    [b₁, b₂, b₃].foldl (· ⊗ ·) init = init ⊗ b₁ ⊗ b₂ ⊗ b₃ := by
+  rfl
+
+-- 総和を foldl で計算した例
+#guard [1, 2, 3, 4].foldl (· + ·) 0 = 10
+
+-- 積を foldl で計算した例
+#guard [1, 2, 3, 4].foldl (· * ·) 1 = 24
+
+-- リストの最大値を foldl で求める例
+#guard [1, 2, 3, 4].foldl (max · ·) 0 = 4