From 07c096d8960edffeed834be6f4ff74f13a3261c2 Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Mon, 22 Jan 2024 19:21:27 +0900
Subject: [PATCH 1/4] =?UTF-8?q?1.1=20=E3=81=A8=201.2=20=E3=81=AE=E8=A7=A3?=
 =?UTF-8?q?=E7=AD=94=E3=82=92=E8=BF=BD=E5=8A=A0?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .../solutions/getting-to-know/evaluating.lean | 19 +++++++++++++++
 .../functions-and-definitions.lean            | 24 +++++++++++++++++++
 2 files changed, 43 insertions(+)
 create mode 100644 functional-programming-lean/solutions/getting-to-know/evaluating.lean
 create mode 100644 functional-programming-lean/solutions/getting-to-know/functions-and-definitions.lean

diff --git a/functional-programming-lean/solutions/getting-to-know/evaluating.lean b/functional-programming-lean/solutions/getting-to-know/evaluating.lean
new file mode 100644
index 00000000..268c4250
--- /dev/null
+++ b/functional-programming-lean/solutions/getting-to-know/evaluating.lean
@@ -0,0 +1,19 @@
+/- # 1.1 演習問題 -/
+
+/-!
+ * `42 + 19`
+ * `String.append "A" (String.append "B" "C")`
+ * `String.append (String.append "A" "B") "C"`
+ * `if 3 == 3 then 5 else 7`
+ * `if 3 == 4 then "equal" else "not equal"`
+-/
+
+#eval 42 + 19
+
+#eval String.append "A" (String.append "B" "C")
+
+#eval String.append (String.append "A" "B") "C"
+
+#eval if 3 == 3 then 5 else 7
+
+#eval if 3 == 4 then "equal" else "not equal"
diff --git a/functional-programming-lean/solutions/getting-to-know/functions-and-definitions.lean b/functional-programming-lean/solutions/getting-to-know/functions-and-definitions.lean
new file mode 100644
index 00000000..394658ca
--- /dev/null
+++ b/functional-programming-lean/solutions/getting-to-know/functions-and-definitions.lean
@@ -0,0 +1,24 @@
+/- # 1.2 演習問題 -/
+
+/-! ## 1
+関数 `joinStringsWith` を `String -> String -> String -> String` 型の関数であって，その第一引数を第二引数と第三引数の間に配置して新しい文字列を作成するようなものとして定義してください．`joinStringsWith ", " "one" "and another"` は `"one, and another"` に等しくなるはずです.-/
+
+def joinStringsWith (s1 : String) (s2 : String) (s3 : String) : String :=
+  s2 ++ s1 ++ s3
+
+example : joinStringsWith ", " "one" "and another" = "one, and another" := rfl
+
+/-! ## 2
+`joinStringsWith ": "` の型は何でしょうか？ Lean で答えを確認してください．-/
+
+#check (joinStringsWith ": " : String → String → String)
+
+/-! ## 3
+与えられた高さ，幅，奥行きを持つ直方体の体積を計算する関数 `volume` を `Nat → Nat → Nat → Nat` 型の関数として定義してください．
+-/
+
+def volume (h : Nat) (w : Nat) (d : Nat) : Nat := h * w * d
+
+example : volume 3 4 5 = 60 := rfl
+
+#check (volume : Nat → Nat → Nat → Nat)

From 90d13efce3d46d80dfe0f476f64930a3acf646dd Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Mon, 22 Jan 2024 20:11:29 +0900
Subject: [PATCH 2/4] =?UTF-8?q?=E8=A3=9C=E8=B6=B3=E6=83=85=E5=A0=B1?=
 =?UTF-8?q?=E3=82=92=E8=B6=B3=E3=81=99?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .../getting-to-know/functions-and-definitions.lean        | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/functional-programming-lean/solutions/getting-to-know/functions-and-definitions.lean b/functional-programming-lean/solutions/getting-to-know/functions-and-definitions.lean
index 394658ca..f54e1ee7 100644
--- a/functional-programming-lean/solutions/getting-to-know/functions-and-definitions.lean
+++ b/functional-programming-lean/solutions/getting-to-know/functions-and-definitions.lean
@@ -8,6 +8,14 @@ def joinStringsWith (s1 : String) (s2 : String) (s3 : String) : String :=
 
 example : joinStringsWith ", " "one" "and another" = "one, and another" := rfl
 
+/- ### 補足: `String.append` と `++` は同じか？ -/
+
+example (s t : String) : s ++ t = String.append s t := rfl
+
+#synth Append String
+
+#check String.instAppendString
+
 /-! ## 2
 `joinStringsWith ": "` の型は何でしょうか？ Lean で答えを確認してください．-/
 

From e3db6a055ab5ff4aa9848fc7b858f7964dd2ce2b Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Mon, 22 Jan 2024 21:04:13 +0900
Subject: [PATCH 3/4] =?UTF-8?q?1.4=20=E8=A7=A3=E3=81=8F?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .../solutions/getting-to-know/structures.lean | 73 +++++++++++++++++++
 1 file changed, 73 insertions(+)
 create mode 100644 functional-programming-lean/solutions/getting-to-know/structures.lean

diff --git a/functional-programming-lean/solutions/getting-to-know/structures.lean b/functional-programming-lean/solutions/getting-to-know/structures.lean
new file mode 100644
index 00000000..65246917
--- /dev/null
+++ b/functional-programming-lean/solutions/getting-to-know/structures.lean
@@ -0,0 +1,73 @@
+/- # 1.4 Structures 演習問題 -/
+
+/-! ## 1
+Define a structure named `RectangularPrism` that contains the height, width, and depth of a rectangular prism, each as a `Float`.-/
+
+structure RectangularPrism where
+  height : Float
+  width : Float
+  depth : Float
+
+/-! ## 2
+Define a function named `volume : RectangularPrism → Float` that computes the volume of a rectangular prism. -/
+
+def volume (r : RectangularPrism) : Float :=
+  r.height * r.width * r.depth
+
+/-! ## 3
+Define a structure named `Segment` that represents a line segment by its endpoints, and define a function `length : Segment → Float` that computes the length of a line segment. `Segment` should have at most two fields. -/
+
+/-- 本文からコピー -/
+structure Point where
+  x : Float
+  y : Float
+
+/-- 本文からコピー -/
+def distance (p1 : Point) (p2 : Point) : Float :=
+  Float.sqrt (((p2.x - p1.x) ^ 2.0) + ((p2.y - p1.y) ^ 2.0))
+
+structure Segment where
+  s : Point
+  t : Point
+
+def length (seg : Segment) : Float := distance seg.s seg.t
+
+/-! ## 4
+Which names are introduced by the declaration of `RectangularPrism`? -/
+
+#check RectangularPrism.mk
+
+#check RectangularPrism.height
+
+#check RectangularPrism.width
+
+#check RectangularPrism.depth
+
+/-! ## 5
+Which names are introduced by the following declarations of `Hamster` and `Book`? What are their types?-/
+
+/-- 本文からコピー -/
+structure Hamster where
+  name : String
+  fluffy : Bool
+
+/-- 本文からコピー -/
+structure Book where
+  makeBook ::
+  title : String
+  author : String
+  price : Float
+
+#check (Hamster.mk : String → Bool → Hamster)
+
+#check (Hamster.name : Hamster → String)
+
+#check (Hamster.fluffy : Hamster → Bool)
+
+#check (Book.makeBook : String → String → Float → Book)
+
+#check (Book.title : Book → String)
+
+#check (Book.author : Book → String)
+
+#check (Book.price : Book → Float)

From 584e6ddeb077e5b3fc4f641b135776a8e6fc2724 Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Mon, 22 Jan 2024 21:43:53 +0900
Subject: [PATCH 4/4] =?UTF-8?q?1.6=20=E6=BC=94=E7=BF=92=E5=95=8F=E9=A1=8C?=
 =?UTF-8?q?=E3=82=92=E8=A7=A3=E3=81=8F?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .../getting-to-know/polymorphism.lean         | 125 ++++++++++++++++++
 1 file changed, 125 insertions(+)
 create mode 100644 functional-programming-lean/solutions/getting-to-know/polymorphism.lean

diff --git a/functional-programming-lean/solutions/getting-to-know/polymorphism.lean b/functional-programming-lean/solutions/getting-to-know/polymorphism.lean
new file mode 100644
index 00000000..103ad287
--- /dev/null
+++ b/functional-programming-lean/solutions/getting-to-know/polymorphism.lean
@@ -0,0 +1,125 @@
+/- # 1.6 演習問題 -/
+
+/-! ## 1
+Write a function to find the last entry in a list. It should return an `Option`.
+-/
+
+variable {α : Type}
+
+def tail (l : List α) : Option α :=
+  match l with
+  | [] => none
+  | x :: xs =>
+    match xs with
+    | [] => some x
+    | _ => tail xs
+
+example : tail [1, 1, 2, 3, 5] = some 5 := rfl
+
+example : tail ([] : List Nat) = none := rfl
+
+/-! ## 2
+Write a function that finds the first entry in a list that satisfies a given predicate. Start the definition with `def List.findFirst? {α : Type} (xs : List α) (predicate : α → Bool) : Option α :=`
+-/
+
+def List.findFirst? {α : Type} (xs : List α) (predicate : α → Bool) : Option α :=
+  match xs with
+  | [] => none
+  | x :: xs =>
+    if predicate x then
+      some x
+    else
+      List.findFirst? xs predicate
+
+example : List.findFirst? [1, 1, 2, 3, 4] (fun x => x % 2 == 0) = some 2 := rfl
+
+/-! ## 3
+Write a function Prod.swap that swaps the two fields in a pair. Start the definition with `def Prod.swap {α β : Type} (pair : α × β) : β × α :=`
+-/
+
+def Prod.swap {α β : Type} (pair : α × β) : β × α := (pair.snd, pair.fst)
+
+example : Prod.swap (1, 2) = (2, 1) := rfl
+
+/-! ## 4
+Rewrite the `PetName` example to use a custom datatype and compare it to the version that uses `Sum`.
+-/
+
+namespace Example
+
+def PetName : Type := String ⊕ String
+
+def animals : List PetName :=
+  [Sum.inl "Spot", Sum.inr "Tiger", Sum.inl "Fifi", Sum.inl "Rex", Sum.inr "Floof"]
+
+def howManyDogs (pets : List PetName) : Nat :=
+  match pets with
+  | [] => 0
+  | Sum.inl _ :: morePets => howManyDogs morePets + 1
+  | Sum.inr _ :: morePets => howManyDogs morePets
+
+end Example
+
+section
+
+inductive PetName where
+| dog : String → PetName
+| cat : String → PetName
+
+open PetName
+
+def animals : List PetName :=
+  [dog "Spot", cat "Tiger", dog "Fifi", dog "Rex", cat "Floof"]
+
+def howManyDogs (pets : List PetName) : Nat :=
+  match pets with
+  | [] => 0
+  | dog _ :: morePets => howManyDogs morePets + 1
+  | cat _ :: morePets => howManyDogs morePets
+
+example : howManyDogs animals = 3 := rfl
+
+end
+
+/-! ## 5
+Write a function `zip` that combines two lists into a list of pairs. The resulting list should be as long as the shortest input list. Start the definition with `def zip {α β : Type} (xs : List α) (ys : List β) : List (α × β) :=.` -/
+
+def zip {α β : Type} (xs : List α) (ys : List β) : List (α × β) :=
+  match xs, ys with
+  | [], _ => []
+  | _, [] => []
+  | x :: xs, y :: ys => (x, y) :: zip xs ys
+
+example : zip [1, 2, 3] ["a", "b", "c"] = [(1, "a"), (2, "b"), (3, "c")] := rfl
+
+example : zip [1, 2, 3] ["a", "b"] = [(1, "a"), (2, "b")] := rfl
+
+/-! ## 6
+Write a polymorphic function `take` that returns the first n entries in a list, where n is a `Nat`. If the list contains fewer than n entries, then the resulting list should be the input list. `#eval take 3 ["bolete", "oyster"]` should yield `["bolete", "oyster"]`, and `#eval take 1 ["bolete", "oyster"]` should yield `["bolete"]`.-/
+
+def take {α : Type} (n : Nat) (xs : List α) : List α :=
+  match n, xs with
+  -- どんなリストでも最初のゼロ個を取ったら空リスト
+  | 0, _ => []
+  -- リストから何も取れなくなったら空リストを返す
+  | _, [] => []
+  -- リストから最初の要素を取り出して残りのリストを再帰的に処理する
+  | n + 1, x :: xs => x :: take n xs
+
+example : take 3 ["bolete", "oyster"] = ["bolete", "oyster"] := rfl
+
+example : take 1 ["bolete", "oyster"] = ["bolete"] := rfl
+
+/-! ## 7
+Using the analogy between types and arithmetic, write a function that distributes products over sums. In other words, it should have type `α × (β ⊕ γ) → (α × β) ⊕ (α × γ)`. -/
+
+def distribute {α β γ : Type} : α × (β ⊕ γ) → (α × β) ⊕ (α × γ)
+  | (a, Sum.inl b) => Sum.inl (a, b)
+  | (a, Sum.inr c) => Sum.inr (a, c)
+
+/-! ## 8
+Using the analogy between types and arithmetic, write a function that turns multiplication by two into a sum. In other words, it should have type `Bool × α → α ⊕ α`. -/
+
+def mulByTwo {α : Type} : Bool × α → α ⊕ α
+  | (true, a) => Sum.inl a
+  | (false, a) => Sum.inr a