the option monad contract の解答を追加

functional-programming-lean/solutions/Solutions/Monads/Class.lean

@@ -26,3 +26,81 @@ def test (n : Nat) : Option Nat :=
   else some n
 
 example : BinTree.mapM test sample = none := rfl
+
+/-
+### The Option Monad Contract
+
+First, write a convincing argument that the `Monad` instance for `Option` satisfies the monad contract. Then, consider the following instance:
+
+```
+instance : Monad Option where
+  pure x := some x
+  bind opt next := none
+```
+
+Both methods have the correct type. Why does this instance violate the monad contract?
+-/
+
+instance instLawfulMonadOption : LawfulMonad Option where
+  map_const := by
+    intro α β
+    rfl
+  id_map := by
+    intro α x
+    cases x <;> rfl
+  seqLeft_eq := by
+    intro α β x y
+    cases x <;> try rfl
+    cases y <;> rfl
+  seqRight_eq := by
+    intro α β x y
+    cases x <;> try rfl
+    cases y <;> rfl
+  pure_seq := by
+    intro α β g x
+    rfl
+  pure_bind := by
+    intro α β x f
+    dsimp [Bind.bind]
+    rfl
+  bind_pure_comp := by
+    intro α x f y
+    cases y <;> rfl
+  bind_assoc := by
+    intro α β γ x f g
+    cases x <;> rfl
+  bind_map := by
+    intro α β x f
+    cases x <;> rfl
+
+instance (priority := high) : Monad Option where
+  pure x := some x
+  bind opt next := none
+
+instance : LawfulMonad Option where
+  map_const := by
+    intro α β
+    rfl
+  id_map := by
+    intro α x
+    cases x <;> rfl
+  seqLeft_eq := by
+    intro α β x y
+    cases x <;> try rfl
+    cases y <;> rfl
+  seqRight_eq := by
+    intro α β x y
+    cases x <;> try rfl
+    cases y <;> rfl
+  pure_seq := by
+    intro α β g x
+    rfl
+  pure_bind := by
+    intro α β x f
+    dsimp [Bind.bind]
+    sorry
+  bind_pure_comp := by sorry
+  bind_assoc := by
+    intro α β γ x f g
+    cases x <;> rfl
+  bind_map := by sorry