Skip to content

Commit 2ab4883

Browse files
datokratdatokrat
committed
add classes, lemmas, instances
1 parent efe2ab4 commit 2ab4883

File tree

5 files changed

+281
-0
lines changed

5 files changed

+281
-0
lines changed

‎src/Init/Control/Lawful.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,3 +9,4 @@ prelude
99
import Init.Control.Lawful.Basic
1010
import Init.Control.Lawful.Instances
1111
import Init.Control.Lawful.Lemmas
12+
import Init.Control.Lawful.MonadLift

‎src/Init/Control/Lawful/MonadLift.lean‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
/-
2+
Copyright (c) 2021 Microsoft Corporation. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Paul Reichert
5+
-/
6+
module
7+
8+
prelude
9+
import Init.Control.Lawful.MonadLift.Basic
10+
import Init.Control.Lawful.MonadLift.Lemmas
11+
import Init.Control.Lawful.MonadLift.Instances

‎src/Init/Control/Lawful/MonadLift/Basic.lean‎

Lines changed: 52 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,52 @@
1+
/-
2+
Copyright (c) 2021 Microsoft Corporation. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Quang Dao
5+
-/
6+
module
7+
8+
prelude
9+
import Init.Control.Basic
10+
11+
/-!
12+
# LawfulMonadLift and LawfulMonadLiftT
13+
14+
This module provides classes asserting that `MonadLift` and `MonadLiftT` are lawful, which means
15+
that `monadLift` is compatible with `pure` and `bind`.
16+
-/
17+
18+
section MonadLift
19+
20+
/-- The `MonadLift` typeclass only contains the lifting operation. `LawfulMonadLift` further
21+
asserts that lifting commutes with `pure` and `bind`:
22+
```
23+
monadLift (pure a) = pure a
24+
monadLift (ma >>= f) = monadLift ma >>= monadLift ∘ f
25+
```
26+
-/
27+
class LawfulMonadLift (m : semiOutParam (Type u → Type v)) (n : Type u → Type w)
28+
[Monad m] [Monad n] [inst : MonadLift m n] : Prop where
29+
/-- Lifting preserves `pure` -/
30+
monadLift_pure {α : Type u} (a : α) : inst.monadLift (pure a) = pure a
31+
/-- Lifting preserves `bind` -/
32+
monadLift_bind {α β : Type u} (ma : m α) (f : α → m β) :
33+
inst.monadLift (ma >>= f) = inst.monadLift ma >>= (fun x => inst.monadLift (f x))
34+
35+
/-- The `MonadLiftT` typeclass only contains the transitive lifting operation.
36+
`LawfulMonadLiftT` further asserts that lifting commutes with `pure` and `bind`:
37+
```
38+
monadLift (pure a) = pure a
39+
monadLift (ma >>= f) = monadLift ma >>= monadLift ∘ f
40+
```
41+
-/
42+
class LawfulMonadLiftT (m : Type u → Type v) (n : Type u → Type w) [Monad m] [Monad n]
43+
[inst : MonadLiftT m n] : Prop where
44+
/-- Lifting preserves `pure` -/
45+
monadLift_pure {α : Type u} (a : α) : inst.monadLift (pure a) = pure a
46+
/-- Lifting preserves `bind` -/
47+
monadLift_bind {α β : Type u} (ma : m α) (f : α → m β) :
48+
inst.monadLift (ma >>= f) = monadLift ma >>= (fun x => monadLift (f x))
49+
50+
export LawfulMonadLiftT (monadLift_pure monadLift_bind)
51+
52+
end MonadLift

‎src/Init/Control/Lawful/MonadLift/Instances.lean‎

Lines changed: 154 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,154 @@
1+
/-
2+
Copyright (c) 2021 Microsoft Corporation. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Quang Dao, Paul Reichert
5+
-/
6+
module
7+
8+
prelude
9+
import all Init.Control.Option
10+
import all Init.Control.Except
11+
import all Init.Control.ExceptCps
12+
import all Init.Control.StateRef
13+
import all Init.Control.StateCps
14+
import Init.Control.Lawful.MonadLift.Lemmas
15+
import Init.Control.Lawful.Instances
16+
17+
universe u v w x
18+
19+
variable {m : Type u → Type v} {n : Type u → Type w} {o : Type u → Type x}
20+
21+
variable (m n o) in
22+
instance [Monad m] [Monad n] [Monad o] [MonadLift n o] [MonadLiftT m n]
23+
[LawfulMonadLift n o] [LawfulMonadLiftT m n] : LawfulMonadLiftT m o where
24+
monadLift_pure := fun a => by
25+
simp only [monadLift, LawfulMonadLift.monadLift_pure, liftM_pure]
26+
monadLift_bind := fun ma f => by
27+
simp only [monadLift, LawfulMonadLift.monadLift_bind, liftM_bind]
28+
29+
variable (m) in
30+
instance [Monad m] : LawfulMonadLiftT m m where
31+
monadLift_pure _ := rfl
32+
monadLift_bind _ _ := rfl
33+
34+
namespace StateT
35+
36+
variable [Monad m] [LawfulMonad m]
37+
38+
instance {σ : Type u} : LawfulMonadLift m (StateT σ m) where
39+
monadLift_pure _ := by ext; simp [MonadLift.monadLift]
40+
monadLift_bind _ _ := by ext; simp [MonadLift.monadLift]
41+
42+
end StateT
43+
44+
namespace ReaderT
45+
46+
variable [Monad m]
47+
48+
instance {ρ : Type u} : LawfulMonadLift m (ReaderT ρ m) where
49+
monadLift_pure _ := by
50+
funext x
51+
simp only [MonadLift.monadLift, pure, ReaderT.pure]
52+
monadLift_bind _ _ := by
53+
funext x
54+
simp only [bind, ReaderT.bind, MonadLift.monadLift, Function.comp_apply]
55+
56+
end ReaderT
57+
58+
namespace OptionT
59+
60+
variable [Monad m] [LawfulMonad m]
61+
62+
@[simp]
63+
theorem lift_pure {α : Type u} (a : α) : OptionT.lift (pure a : m α) = pure a := by
64+
simp only [OptionT.lift, OptionT.mk, bind_pure_comp, map_pure, pure, OptionT.pure]
65+
66+
@[simp]
67+
theorem lift_bind {α β : Type u} (ma : m α) (f : α → m β) :
68+
OptionT.lift (ma >>= f) = OptionT.lift ma >>= (fun a => OptionT.lift (f a)) := by
69+
simp only [instMonad, OptionT.bind, OptionT.mk, OptionT.lift, bind_pure_comp, bind_map_left,
70+
map_bind]
71+
72+
instance : LawfulMonadLift m (OptionT m) where
73+
monadLift_pure := lift_pure
74+
monadLift_bind := lift_bind
75+
76+
end OptionT
77+
78+
namespace ExceptT
79+
80+
variable [Monad m] [LawfulMonad m]
81+
82+
@[simp]
83+
theorem lift_bind {α β ε : Type u} (ma : m α) (f : α → m β) :
84+
ExceptT.lift (ε := ε) (ma >>= f) = ExceptT.lift ma >>= (fun a => ExceptT.lift (f a)) := by
85+
simp only [instMonad, ExceptT.bind, mk, ExceptT.lift, bind_map_left, ExceptT.bindCont, map_bind]
86+
87+
instance : LawfulMonadLift m (ExceptT ε m) where
88+
monadLift_pure := lift_pure
89+
monadLift_bind := lift_bind
90+
91+
instance : LawfulMonadLift (Except ε) (ExceptT ε m) where
92+
monadLift_pure _ := by
93+
simp only [MonadLift.monadLift, mk, pure, Except.pure, ExceptT.pure]
94+
monadLift_bind ma _ := by
95+
simp only [instMonad, ExceptT.bind, mk, MonadLift.monadLift, pure_bind, ExceptT.bindCont,
96+
Except.instMonad, Except.bind]
97+
rcases ma with _ | _ <;> simp
98+
99+
end ExceptT
100+
101+
namespace StateRefT'
102+
103+
instance {ω σ : Type} {m : Type → Type} [Monad m] : LawfulMonadLift m (StateRefT' ω σ m) where
104+
monadLift_pure _ := by
105+
simp only [MonadLift.monadLift, pure]
106+
unfold StateRefT'.lift ReaderT.pure
107+
simp only
108+
monadLift_bind _ _ := by
109+
simp only [MonadLift.monadLift, bind]
110+
unfold StateRefT'.lift ReaderT.bind
111+
simp only
112+
113+
end StateRefT'
114+
115+
namespace StateCpsT
116+
117+
instance {σ : Type u} [Monad m] [LawfulMonad m] : LawfulMonadLift m (StateCpsT σ m) where
118+
monadLift_pure _ := by
119+
simp only [MonadLift.monadLift, pure]
120+
unfold StateCpsT.lift
121+
simp only [pure_bind]
122+
monadLift_bind _ _ := by
123+
simp only [MonadLift.monadLift, bind]
124+
unfold StateCpsT.lift
125+
simp only [bind_assoc]
126+
127+
end StateCpsT
128+
129+
namespace ExceptCpsT
130+
131+
instance {ε : Type u} [Monad m] [LawfulMonad m] : LawfulMonadLift m (ExceptCpsT ε m) where
132+
monadLift_pure _ := by
133+
simp only [MonadLift.monadLift, pure]
134+
unfold ExceptCpsT.lift
135+
simp only [pure_bind]
136+
monadLift_bind _ _ := by
137+
simp only [MonadLift.monadLift, bind]
138+
unfold ExceptCpsT.lift
139+
simp only [bind_assoc]
140+
141+
end ExceptCpsT
142+
143+
namespace Id
144+
145+
/-- The `pure` operation of a monad `m` can be seen as a lifting operation from `Id` to `m`. -/
146+
instance [Pure m] : MonadLift Id m where
147+
monadLift := pure
148+
149+
/-- The lifting from `Id` to a lawful monad `m` induced by `pure` is lawful. -/
150+
instance [Monad m] [LawfulMonad m] : LawfulMonadLift Id m where
151+
monadLift_pure := fun a => by simp [MonadLift.monadLift, pure]
152+
monadLift_bind := fun x f => by simp [MonadLift.monadLift, bind]
153+
154+
end Id

‎src/Init/Control/Lawful/MonadLift/Lemmas.lean‎

Lines changed: 63 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,63 @@
1+
/-
2+
Copyright (c) 2021 Microsoft Corporation. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Quang Dao
5+
-/
6+
module
7+
8+
prelude
9+
import Init.Control.Lawful.Basic
10+
import Init.Control.Lawful.MonadLift.Basic
11+
12+
universe u v w
13+
14+
variable {m : Type u → Type v} {n : Type u → Type w} [Monad m] [Monad n] [MonadLiftT m n]
15+
[LawfulMonadLiftT m n] {α β : Type u}
16+
17+
theorem monadLift_map [LawfulMonad m] [LawfulMonad n] (f : α → β) (ma : m α) :
18+
monadLift (f <$> ma) = f <$> (monadLift ma : n α) := by
19+
rw [← bind_pure_comp, ← bind_pure_comp, monadLift_bind]
20+
simp only [bind_pure_comp, monadLift_pure]
21+
22+
theorem monadLift_seq [LawfulMonad m] [LawfulMonad n] (mf : m (α → β)) (ma : m α) :
23+
monadLift (mf <*> ma) = monadLift mf <*> (monadLift ma : n α) := by
24+
simp only [seq_eq_bind, monadLift_map, monadLift_bind]
25+
26+
theorem monadLift_seqLeft [LawfulMonad m] [LawfulMonad n] (x : m α) (y : m β) :
27+
monadLift (x <* y) = (monadLift x : n α) <* (monadLift y : n β) := by
28+
simp only [seqLeft_eq, monadLift_map, monadLift_seq]
29+
30+
theorem monadLift_seqRight [LawfulMonad m] [LawfulMonad n] (x : m α) (y : m β) :
31+
monadLift (x *> y) = (monadLift x : n α) *> (monadLift y : n β) := by
32+
simp only [seqRight_eq, monadLift_map, monadLift_seq]
33+
34+
/-! We duplicate the theorems for `monadLift` to `liftM` since `rw` matches on syntax only. -/
35+
36+
@[simp]
37+
theorem liftM_pure (a : α) : liftM (pure a : m α) = pure (f := n) a :=
38+
monadLift_pure _
39+
40+
@[simp]
41+
theorem liftM_bind (ma : m α) (f : α → m β) :
42+
liftM (n := n) (ma >>= f) = liftM ma >>= (fun a => liftM (f a)) :=
43+
monadLift_bind _ _
44+
45+
@[simp]
46+
theorem liftM_map [LawfulMonad m] [LawfulMonad n] (f : α → β) (ma : m α) :
47+
liftM (f <$> ma) = f <$> (liftM ma : n α) :=
48+
monadLift_map _ _
49+
50+
@[simp]
51+
theorem liftM_seq [LawfulMonad m] [LawfulMonad n] (mf : m (α → β)) (ma : m α) :
52+
liftM (mf <*> ma) = liftM mf <*> (liftM ma : n α) :=
53+
monadLift_seq _ _
54+
55+
@[simp]
56+
theorem liftM_seqLeft [LawfulMonad m] [LawfulMonad n] (x : m α) (y : m β) :
57+
liftM (x <* y) = (liftM x : n α) <* (liftM y : n β) :=
58+
monadLift_seqLeft _ _
59+
60+
@[simp]
61+
theorem liftM_seqRight [LawfulMonad m] [LawfulMonad n] (x : m α) (y : m β) :
62+
liftM (x *> y) = (liftM x : n α) *> (liftM y : n β) :=
63+
monadLift_seqRight _ _

0 commit comments

Comments
 (0)