Merge pull request #12 from lean-ja/add-solution

1 章の演習問題を解き，その解答を solutions ディレクトリに入れる

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"

functional-programming-lean/solutions/getting-to-know/functions-and-definitions.lean

@@ -0,0 +1,32 @@
+/- # 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
+
+/- ### 補足: `String.append` と `++` は同じか？ -/
+
+example (s t : String) : s ++ t = String.append s t := rfl
+
+#synth Append String
+
+#check String.instAppendString
+
+/-! ## 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)

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

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)