chore: upstream Std.Classes.LawfulMonad (except SatisfiesM) (#3340)

src/Init/Control/Lawful.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sebastian Ullrich, Leonardo de Moura
+Authors: Sebastian Ullrich, Leonardo de Moura, Mario Carneiro
 -/
 prelude
 import Init.SimpLemmas
@@ -84,6 +84,36 @@ theorem seqRight_eq_bind [Monad m] [LawfulMonad m] (x : m α) (y : m β) : x *>
 theorem seqLeft_eq_bind [Monad m] [LawfulMonad m] (x : m α) (y : m β) : x <* y = x >>= fun a => y >>= fun _ => pure a := by
   rw [seqLeft_eq]; simp [map_eq_pure_bind, seq_eq_bind_map]
 
+/--
+An alternative constructor for `LawfulMonad` which has more
+defaultable fields in the common case.
+-/
+theorem LawfulMonad.mk' (m : Type u → Type v) [Monad m]
+    (id_map : ∀ {α} (x : m α), id <$> x = x)
+    (pure_bind : ∀ {α β} (x : α) (f : α → m β), pure x >>= f = f x)
+    (bind_assoc : ∀ {α β γ} (x : m α) (f : α → m β) (g : β → m γ),
+      x >>= f >>= g = x >>= fun x => f x >>= g)
+    (map_const : ∀ {α β} (x : α) (y : m β),
+      Functor.mapConst x y = Function.const β x <$> y := by intros; rfl)
+    (seqLeft_eq : ∀ {α β} (x : m α) (y : m β),
+      x <* y = (x >>= fun a => y >>= fun _ => pure a) := by intros; rfl)
+    (seqRight_eq : ∀ {α β} (x : m α) (y : m β), x *> y = (x >>= fun _ => y) := by intros; rfl)
+    (bind_pure_comp : ∀ {α β} (f : α → β) (x : m α),
+      x >>= (fun y => pure (f y)) = f <$> x := by intros; rfl)
+    (bind_map : ∀ {α β} (f : m (α → β)) (x : m α), f >>= (. <$> x) = f <*> x := by intros; rfl)
+    : LawfulMonad m :=
+  have map_pure {α β} (g : α → β) (x : α) : g <$> (pure x : m α) = pure (g x) := by
+    rw [← bind_pure_comp]; simp [pure_bind]
+  { id_map, bind_pure_comp, bind_map, pure_bind, bind_assoc, map_pure,
+    comp_map := by simp [← bind_pure_comp, bind_assoc, pure_bind]
+    pure_seq := by intros; rw [← bind_map]; simp [pure_bind]
+    seq_pure := by intros; rw [← bind_map]; simp [map_pure, bind_pure_comp]
+    seq_assoc := by simp [← bind_pure_comp, ← bind_map, bind_assoc, pure_bind]
+    map_const := funext fun x => funext (map_const x)
+    seqLeft_eq := by simp [seqLeft_eq, ← bind_map, ← bind_pure_comp, pure_bind, bind_assoc]
+    seqRight_eq := fun x y => by
+      rw [seqRight_eq, ← bind_map, ← bind_pure_comp, bind_assoc]; simp [pure_bind, id_map] }
+
 /-! # Id -/
 
 namespace Id
@@ -173,6 +203,16 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (ExceptT ε m) where
 
 end ExceptT
 
+/-! # Except -/
+
+instance : LawfulMonad (Except ε) := LawfulMonad.mk'
+  (id_map := fun x => by cases x <;> rfl)
+  (pure_bind := fun a f => rfl)
+  (bind_assoc := fun a f g => by cases a <;> rfl)
+
+instance : LawfulApplicative (Except ε) := inferInstance
+instance : LawfulFunctor (Except ε) := inferInstance
+
 /-! # ReaderT -/
 
 namespace ReaderT
@@ -307,3 +347,30 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (StateT σ m) where
   bind_assoc     := by intros; apply ext; intros; simp
 
 end StateT
+
+/-! # EStateM -/
+
+instance : LawfulMonad (EStateM ε σ) := .mk'
+  (id_map := fun x => funext <| fun s => by
+    dsimp only [EStateM.instMonadEStateM, EStateM.map]
+    match x s with
+    | .ok _ _ => rfl
+    | .error _ _ => rfl)
+  (pure_bind := fun _ _ => rfl)
+  (bind_assoc := fun x _ _ => funext <| fun s => by
+    dsimp only [EStateM.instMonadEStateM, EStateM.bind]
+    match x s with
+    | .ok _ _ => rfl
+    | .error _ _ => rfl)
+  (map_const := fun _ _ => rfl)
+
+/-! # Option -/
+
+instance : LawfulMonad Option := LawfulMonad.mk'
+  (id_map := fun x => by cases x <;> rfl)
+  (pure_bind := fun x f => rfl)
+  (bind_assoc := fun x f g => by cases x <;> rfl)
+  (bind_pure_comp := fun f x => by cases x <;> rfl)
+
+instance : LawfulApplicative Option := inferInstance
+instance : LawfulFunctor Option := inferInstance