*: fp l0 revised

draft/fp/index.md

@@ -1,7 +1,8 @@
 # Hacking Lean in Lean: A Crash Course
 
 ## [Functional Programming in Lean](./l0)
+### [2023/08/08 revised](./l0/23-08-08)
 
 ## Metaprogramming in Lean, Part I
 
-## Metaprogramming in Lean, Part I
+## Metaprogramming in Lean, Part II

draft/fp/l0/23-08-08.md

@@ -0,0 +1,149 @@
+# 2023/08/08 revised
+
+```Lean4
+import Mathlib.Init.Logic
+
+inductive ℕ where
+  | zero : ℕ
+  | succ : ℕ -> ℕ
+
+def add : ℕ -> ℕ -> ℕ
+  | .zero  , n => n
+  | .succ m, n => .succ $ add m n
+
+variable {A : Type _} {b : Type _}
+
+@[simp] def foldl : (B -> A -> B) -> B -> List A -> B :=
+  fun f acc xs =>
+    match xs with
+    | []      => acc
+    | x :: xs => foldl f (f acc x) xs
+
+-- foldl op acc []        = acc
+-- foldl op acc (x :: xs) = foldl op (op acc x) xs
+
+@[simp] def length : List A -> ℕ :=
+  fun xs =>
+    match xs with
+    | []      => .zero
+    | _ :: xs => .succ $ length xs
+
+@[simp] def length' : List A -> ℕ :=
+  foldl (fun acc _ => .succ acc) .zero
+
+example : let xs := [0, 1, 2, 3, 4]; length' xs = length xs := by
+  rfl
+
+def length'_is_length (xs : List A) : length' xs = length xs := by
+  sorry
+
+@[simp] def append : List A -> List A -> List A :=
+  fun xs ys =>
+    match xs with
+    | []      => ys
+    | x :: xs => x :: append xs ys
+
+-- def append :
+
+example : append [0, 1, 2] [3, 4] = [0, 1, 2, 3, 4] :=
+  rfl
+
+def append_length (xs ys : List A) : add (length xs) (length ys) = length (append xs ys) :=
+  match xs with
+  | []      => by
+      simp
+      rfl
+  | x :: xs => by
+      simp
+      apply congr_arg ℕ.succ
+      apply append_length
+
+def reverse : List A -> List A :=
+  fun xs =>
+    match xs with
+    | []      => []
+    | x :: xs => append (reverse xs) [x]
+
+example : reverse [0, 1, 2, 3, 4, 5] = [5, 4, 3, 2, 1, 0] := by
+  rfl
+
+def reverse' : List A -> List A :=
+  foldl (fun acc x => x :: acc) []
+
+example : let xs := [0, 1, 2, 3, 4, 5]
+  reverse' xs = reverse xs := by
+    rfl
+
+---
+
+def pure' : A -> List A := (· :: [])
+
+def map : (A -> B) -> (List A -> List B) :=
+  fun f xs =>
+    match xs with
+    | [] => []
+    | x :: xs => f x :: map f xs
+
+def join : List (List A) -> List A :=
+  foldl (fun acc xs => append acc xs) []
+
+example : join [[0], [1, 2, 3, 4], [5, 6, 7]] = [0, 1, 2, 3, 4, 5, 6, 7] := by
+  rfl
+
+-- HINT: use `sum` and `map`
+def join_length : sorry := sorry
+
+--- `pure`, `map`, `join` <-> comprehension
+
+-- [42]
+#eval (pure' 42 : List Int)
+
+-- [ x          | x <- [0, 1, 2, 3, 4, 5] ]
+-- [ fun x => x | x <- [0, 1, 2, 3, 4, 5] ]
+#eval map (fun x => x) [0, 1, 2, 3, 4, 5]
+
+-- [ x               | x <- [0, 1, 2, 3, 4, 5] ]
+-- [ fun x => ⟨x, x⟩ | x <- [0, 1, 2, 3, 4, 5] ]
+#eval map (fun x => (⟨x, x⟩ : Int × Int)) [0, 1, 2, 3, 4, 5]
+
+-- [ ⟨x, y⟩            | x <- [0, 1, 2, 3, 4, 5], y <- [0, 1, 2, 3, 4, 5] ]
+-- [ fun x y => ⟨x, y⟩ | x <- [0, 1, 2, 3, 4, 5], y <- [0, 1, 2, 3, 4, 5] ]
+-- [ fun x => fun y => ⟨x, y⟩ | x <- [0, 1, 2, 3, 4, 5], y <- [0, 1, 2, 3, 4, 5] ]
+-- join [ fun x => [ fun y => ⟨x, y⟩ | y <- [0, 1, 2, 3, 4, 5] ] | x <- [0, 1, 2, 3, 4, 5] ]
+#eval join $ map (fun x => (map ((fun y => ⟨x, y⟩) : Int -> Int × Int) [0, 1, 2, 3, 4, 5])) [0, 1, 2, 3, 4, 5]
+
+-- [ x | x <- [0, 1, 2, 3] | x != 2 ]
+-- HINT: [ c | p ] = if p then [c] else []
+
+--- `map`, `join` <-> `bind`
+-- bind xs k = join (map k xs)
+-- join xss  = bind xss id
+
+-- https://leanprover-community.github.io/archive/stream/270676-lean4/topic/Option.20do.20notation.20regression.3F.html
+instance : Monad List where
+  pure := pure'
+  bind := fun xs k => join (map k xs)
+
+-- [ ⟨x, y⟩ | x <- [0, 1, 2, 3, 4, 5], y <- [0, 1, 2, 3, 4, 5] ]
+example : List (Int × Int) := do
+  let x <- [0, 1, 2, 3, 4, 5]
+  let y <- [0, 1, 2, 3, 4, 5]
+  pure ⟨x, y⟩
+
+-- alias `· >>= ·` `bind`
+example : List (Int × Int) :=
+  [0, 1, 2, 3, 4, 5] >>= fun x =>
+    [0, 1, 2, 3, 4, 5] >>= fun y =>
+      pure ⟨x, y⟩
+
+example : List (Int × Int) :=
+  bind [0, 1, 2, 3, 4, 5] (fun x =>
+    bind [0, 1, 2, 3, 4, 5] (fun y =>
+      pure ⟨x, y⟩))
+
+-- we can also use `$`
+example : List (Int × Int) :=
+  bind [0, 1, 2, 3, 4, 5] fun x =>
+    bind [0, 1, 2, 3, 4, 5] fun y =>
+      pure ⟨x, y⟩
+```