From 4ba641ecc5686712cbea69e3751426b918719431 Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Mon, 20 May 2024 02:05:20 +0900
Subject: [PATCH] =?UTF-8?q?the=20option=20monad=20contract=20=E3=81=AE?=
 =?UTF-8?q?=E8=A7=A3=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/Solutions/Monads/Class.lean     | 78 +++++++++++++++++++
 1 file changed, 78 insertions(+)

diff --git a/functional-programming-lean/solutions/Solutions/Monads/Class.lean b/functional-programming-lean/solutions/Solutions/Monads/Class.lean
index 7ddcb8b1..639ea995 100644
--- a/functional-programming-lean/solutions/Solutions/Monads/Class.lean
+++ b/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