source: src/utilities/monad.ma @ 1882

Last change on this file since 1882 was 1882, checked in by tranquil, 8 years ago

big update, alas incomplete:
joint changed a bit, and all BE languages need to be updated
started development of blocks to aid preservation results, but still incomplete
if it breaks too many things, feel free to roll back

File size: 11.0 KB
Line 
1include "basics/types.ma".
2include "basics/relations.ma".
3include "utilities/setoids.ma".
4
5definition pred_transformer ≝ λA,B : Type[0].(A → Prop) → B → Prop.
6
7definition modus_ponens ≝ λA,B.λPT : pred_transformer A B.
8  ∀P,Q.(∀x.P x → Q x) → ∀y.PT P y → PT Q y.
9 
10lemma mp_transitive :
11  ∀A,B,C,PT1,PT2.modus_ponens A B PT1 → modus_ponens B C PT2 →
12    modus_ponens A C (PT2 ∘ PT1). /4/ qed.
13
14definition rel_transformer ≝ λA,B,C,D : Type[0].
15  (A → B → Prop) → C → D → Prop.
16 
17definition rel_modus_ponens ≝ λA,B,C,D.λRT : rel_transformer A B C D.
18  ∀P,Q.(∀x,y.P x y → Q x y) → ∀z,w.RT P z w → RT Q z w.
19 
20lemma rel_mp_transitive :
21  ∀A,B,C,D,E,F,RT1,RT2.rel_modus_ponens A B C D RT1 → rel_modus_ponens C D E F RT2 →
22    rel_modus_ponens … (RT2 ∘ RT1). /4/ qed.
23 
24record Monad : Type[1] ≝ {
25  monad : Type[0] → Type[0] ;
26  m_return : ∀X. X → monad X ;
27  m_bind : ∀X,Y. monad X → (X → monad Y) → monad Y
28}.
29
30notation "m »= f" with precedence 49
31  for @{'m_bind $m $f }.
32
33notation > "!_ e; e'"
34  with precedence 48 for @{'m_bind ${e} (λ_. ${e'})}.
35notation > "! ident v ← e; e'"
36  with precedence 48 for @{'m_bind ${e} (λ${ident v}. ${e'})}.
37notation > "! ident v : ty ← e; e'"
38  with precedence 48 for @{'m_bind ${e} (λ${ident v} : ${ty}. ${e'})}.
39notation < "vbox(! \nbsp ident v ← e ; break e')"
40  with precedence 48 for @{'m_bind ${e} (λ${ident v}.${e'})}.
41notation > "! ident v ← e : ty ; e'"
42  with precedence 48 for @{'m_bind (${e} : ${ty}) (λ${ident v}.${e'})}.
43notation < "vbox(! \nbsp ident v : ty \nbsp ←  \nbsp e ; break e')"
44  with precedence 48 for @{'m_bind ${e} (λ${ident v} : ${ty}. ${e'})}.
45notation > "! ident v : ty ← e : ty' ; e'"
46  with precedence 48 for @{'m_bind (${e} : ${ty'}) (λ${ident v} : ${ty}. ${e'})}.
47notation > "! 〈ident v1, ident v2〉 ← e ; e'"
48  with precedence 48 for @{'m_bind2 ${e} (λ${ident v1}. λ${ident v2}. ${e'})}.
49notation > "! 〈ident v1, ident v2〉 ← e : ty ; e'"
50  with precedence 48 for @{'m_bind2 (${e} : $ty) (λ${ident v1}. λ${ident v2}. ${e'})}.
51notation > "! 〈ident v1 : ty1, ident v2 : ty2〉 ← e ; e'"
52  with precedence 48 for @{'m_bind2 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. ${e'})}.
53notation < "vbox(! \nbsp 〈ident v1, ident v2〉 ← e ; break e')"
54  with precedence 48 for @{'m_bind2 ${e} (λ${ident v1}. λ${ident v2}. ${e'})}.
55notation < "vbox(! \nbsp 〈ident v1 : ty1, ident v2 : ty2〉  \nbsp ←  \nbsp e ; break e')"
56  with precedence 48 for @{'m_bind2 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. ${e'})}.
57notation > "! 〈ident v1, ident v2, ident v3〉 ← e ; e'"
58  with precedence 48 for @{'m_bind3 ${e} (λ${ident v1}. λ${ident v2}. λ${ident v3}. ${e'})}.
59notation > "! 〈ident v1, ident v2, ident v3〉 ← e : ty ; e'"
60  with precedence 48 for @{'m_bind3 (${e} : ${ty}) (λ${ident v1}. λ${ident v2}. λ${ident v3}. ${e'})}.
61notation > "! 〈ident v1 : ty1, ident v2 : ty2, ident v3 : ty3〉 ← e ; e'"
62  with precedence 48 for @{'m_bind3 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. λ${ident v3} : ${ty3}. ${e'})}.
63notation < "vbox(! \nbsp 〈ident v1, ident v2, ident v3〉 \nbsp ← \nbsp e ; break e')"
64  with precedence 48 for @{'m_bind3 ${e} (λ${ident v1}. λ${ident v2}. λ${ident v3}. ${e'})}.
65notation < "vbox(! \nbsp 〈ident v1 : ty1, ident v2 : ty2, ident v3 : ty3〉 \nbsp ← e \nbsp ; break e')"
66  with precedence 48 for @{'m_bind3 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. λ${ident v3} : ${ty3}. ${e'})}.
67
68(* dependent pair versions *)
69notation > "! «ident v1, ident v2» ← e ; e'"
70  with precedence 48 for
71  @{'m_bind ${e} (λ${fresh p_sig}.
72    match ${fresh p_sig} with [mk_Sig ${ident v1} ${ident v2} ⇒ ${e'}])}.
73notation < "vbox(! \nbsp «ident v1, ident v2» \nbsp ← \nbsp e ; break e')"
74  with precedence 48 for
75  @{'m_bind ${e} (λ${fresh p_sig}.
76    match ${fresh p_sig} with [mk_Sig ${ident v1} ${ident v2} ⇒ ${e'}])}.
77   
78notation > "! «ident v1, ident v2, ident H» ← e ; e'"
79  with precedence 48 for
80  @{'m_sigbind2 ${e} (λ${ident v1},${ident v2},${ident H}. ${e'})}.
81notation < "vbox(! \nbsp «ident v1, ident v2, ident H» \nbsp ← \nbsp e ; e')"
82  with precedence 48 for
83  @{'m_sigbind2 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.
84    λ${ident H} : ${ty3}. ${e'})}.
85   
86 
87(*alternative do notation for backward compatibility *)
88notation > "'do'_ e; e'"
89  with precedence 48 for @{'m_bind ${e} (λ_. ${e'})}.
90notation > "'do' ident v ← e; e'"
91  with precedence 48 for @{'m_bind ${e} (λ${ident v}. ${e'})}.
92notation > "'do' ident v : ty ← e; e'"
93  with precedence 48 for @{'m_bind ${e} (λ${ident v} : ${ty}. ${e'})}.
94notation > "'do' ident v ← e : ty ; e'"
95  with precedence 48 for @{'m_bind (${e} : ${ty}) (λ${ident v}.${e'})}.
96notation > "'do' ident v : ty ← e : ty' ; e'"
97  with precedence 48 for @{'m_bind (${e} : ${ty'}) (λ${ident v} : ${ty}. ${e'})}.
98notation > "'do' 〈ident v1, ident v2〉 ← e ; e'"
99  with precedence 48 for @{'m_bind2 ${e} (λ${ident v1}. λ${ident v2}. ${e'})}.
100notation > "'do' 〈ident v1 : ty1, ident v2 : ty2〉 ← e ; e'"
101  with precedence 48 for @{'m_bind2 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. ${e'})}.
102notation > "'do' 〈ident v1, ident v2, ident v3〉 ← e ; e'"
103  with precedence 48 for @{'m_bind3 ${e} (λ${ident v1}. λ${ident v2}. λ${ident v3}. ${e'})}.
104notation > "'do' 〈ident v1 : ty1, ident v2 : ty2, ident v3 : ty3〉 ← e ; e'"
105  with precedence 48 for @{'m_bind3 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. λ${ident v3} : ${ty3}. ${e'})}.
106
107(* dependent pair versions *)
108notation > "'do' «ident v1, ident v2» ← e ; e'"
109  with precedence 48 for
110  @{'m_bind ${e} (λ${fresh p_sig}.
111    match ${fresh p_sig} with [mk_Sig ${ident v1} ${ident v2} ⇒ ${e'}])}.
112
113notation > "'do' «ident v1, ident v2, ident H» ← e ; e'"
114  with precedence 48 for
115  @{'m_sigbind2 ${e} (λ${ident v1},${ident v2},${ident H}. ${e'})}.
116
117notation > "'return' t" with precedence 49 for @{'m_return $t}.
118notation < "'return' \nbsp t" with precedence 49 for @{'m_return $t}.
119
120interpretation "monad bind" 'm_bind m f = (m_bind ? ? ? m f).
121interpretation "monad return" 'm_return x = (m_return ? ? x).
122
123
124record MonadProps : Type[1] ≝
125  { max_def :> Monad
126  ; m_return_bind : ∀X,Y.∀x : X.∀f : X → monad max_def Y. ! y ← return x ; f y = f x
127  ; m_bind_return : ∀X.∀m : monad max_def X.! x ← m ; return x = m
128  ; m_bind_bind : ∀X,Y,Z. ∀m : monad max_def X.∀f : X → monad max_def Y.
129      ∀g : Y → monad max_def Z.! y ← (! x ← m ; f x) ; g y = ! x ← m; ! y ← f x ; g y
130  ; m_bind_ext_eq : ∀X,Y.∀m : monad max_def X.∀f,g : X → monad max_def Y.
131      (∀x.f x = g x) → ! x ← m ; f x = ! x ← m ; g x
132  }.
133
134record SetoidMonadProps : Type[1] ≝
135  { smax_def :> Monad
136  ; sm_eq : ∀X.relation (monad smax_def X)
137  ; sm_eq_refl : ∀X.reflexive ? (sm_eq X)
138  ; sm_eq_trans : ∀X.transitive ? (sm_eq X)
139  ; sm_eq_sym : ∀X.symmetric ? (sm_eq X)
140  ; sm_return_proper : ∀X,x.sm_eq X (return x) (return x)
141  ; sm_bind_proper : ∀X,Y,x,y,f,g.sm_eq X x y → (∀x.sm_eq Y (f x) (g x)) → sm_eq Y (x »= f) (y »= g)
142  ; sm_return_bind : ∀X,Y.∀x : X.∀f : X → monad smax_def Y.
143      sm_eq Y (! y ← return x ; f y) (f x)
144  ; sm_bind_return : ∀X.∀m : monad smax_def X.sm_eq X (! x ← m ; return x) m
145  ; sm_bind_bind : ∀X,Y,Z. ∀m : monad smax_def X.∀f : X → monad smax_def Y.
146      ∀g : Y → monad smax_def Z.sm_eq Z (! y ← (! x ← m ; f x) ; g y) (! x ← m; ! y ← f x ; g y)
147  }.
148
149definition setoid_of_monad : ∀M : SetoidMonadProps.∀X : Type[0].
150  Setoid ≝
151  λM,X.mk_Setoid (monad M X) (sm_eq M X) (sm_eq_refl M X) (sm_eq_trans M X) (sm_eq_sym M X).
152
153include "hints_declaration.ma".
154
155unification hint 0 ≔ M, X;
156M' ≟ smax_def M, S ≟ setoid_of_monad M X
157(*-----------------------------*)⊢
158monad M' X ≡ std_supp S.
159
160include "basics/lists/list.ma".
161
162definition m_map ≝ λM,X,Y.λf : X → Y.λm : monad M X.
163  ! x ← m ; return f x.
164
165definition m_map2 ≝ λM,X,Y,Z.λf : X → Y → Z.λm : monad M X.λn : monad M Y.
166  ! x ← m ; ! y ← n ; return f x y.
167 
168definition m_bind2 ≝ λM,X,Y,Z.λm : monad M (X × Y).λf : X → Y → monad M Z.
169  ! p ← m ; f (\fst p) (\snd p).
170
171interpretation "monad bind2" 'm_bind2 m f = (m_bind2 ? ? ? ? m f).
172
173definition m_bind3 :
174  ∀M,X,Y,Z,W.monad M (X×Y×Z) → (X → Y → Z → monad M W) → monad M W ≝
175  λM,X,Y,Z,W,m,f.
176  ! p ← m ; f (\fst (\fst p)) (\snd (\fst p)) (\snd p).
177
178interpretation "monad bind3" 'm_bind3 m f = (m_bind3 ? ? ? ? ? m f).
179
180definition m_join : ∀M,X.monad M (monad M X) → monad M X ≝
181  λM,X,m.! x ← m ; x.
182
183definition m_sigbind2 :
184  ∀M,A,B,C.∀P:A×B → Prop. monad M (Σx:A×B.P x) →
185      (∀a,b. P 〈a,b〉 → monad M C) → monad M C ≝
186λM,A,B,C,P,e,f.
187    ! e_sig ← e ;
188    match e_sig with
189    [ mk_Sig p p_prf ⇒
190      match p return λx.x = p → ? with
191      [ mk_Prod a b ⇒
192      λeq_p.  f a b (eq_ind_r ?? (λx.λ_.P x) p_prf ? eq_p)
193      ](refl …)
194    ].
195
196interpretation "monad sigbind2" 'm_sigbind2 m f = (m_sigbind2 ????? m f).
197
198definition m_list_map :
199  ∀M,X,Y.(X → monad M Y) → list X → monad M (list Y) ≝
200  λM,X,Y,f,l.foldr … (λel,macc.! r ← f el; !acc ← macc; return (r :: acc)) (return [ ]) l.
201
202definition m_list_map_sigma :
203  ∀M,X,Y,P.(X → monad M (Σy : Y.P y)) → list X → monad M (Σl : list Y.All ? P l) ≝
204  λM,X,Y,P,f,l.foldr … (λel,macc.
205    ! «r, r_prf» ← f el ;
206    ! «acc, acc_prf» ← macc ;
207    return (mk_Sig ?? (r :: acc) ?))
208    (return (mk_Sig … [ ] ?)) l. % assumption qed.
209
210definition m_bin_op :
211  ∀M,X,Y,Z.(X → Y → Z) → monad M X → monad M Y → monad M Z ≝
212  λM,X,Y,Z,op,m,n. ! x ← m ; ! y ← n ; return op x y.
213
214unification hint 0 ≔ M, X, Y, Z, m, f ⊢
215m_bind M (X×Y) Z m (λp.f (\fst p) (\snd p)) ≡ m_bind2 M X Y Z m f.
216
217unification hint 0 ≔ M, X, Y, Z, W, m, f ⊢
218m_bind M (X×Y×Z) W m (λp.f (\fst (\fst p)) (\snd (\fst p)) (\snd p)) ≡
219m_bind3 M X Y Z W m f.
220
221definition MakeMonadProps : ?→?→?→?→?→?→?→MonadProps ≝ λmonad,m_return,m_bind.
222mk_MonadProps (mk_Monad monad m_return m_bind).
223
224definition MakeSetoidMonadProps : ?→?→?→?→?→?→?→?→?→?→?→?→SetoidMonadProps ≝
225  λmonad,m_return,m_bind.
226  mk_SetoidMonadProps (mk_Monad monad m_return m_bind).
227 
228record MonadPred (M : Monad) : Type[1] ≝
229  { m_pred :> ∀X.pred_transformer X (monad M X)
230  ; mp_return : ∀X,P,x.P x → m_pred X P (return x)
231  ; mp_bind : ∀X,Y,Pin,Pout,m.m_pred X Pin m →
232      ∀f.(∀x.Pin x → m_pred Y Pout (f x)) →
233                  m_pred ? Pout (m_bind … m f)
234  ; m_pred_mp : ∀X.modus_ponens ?? (m_pred X)
235  }.
236
237record MonadRel (M1 : Monad) (M2 : Monad) : Type[1] ≝
238  { m_rel :> ∀X,Y.rel_transformer X Y (monad M1 X) (monad M2 Y)
239  ; mr_return : ∀X,Y,rel,x,y.rel x y → m_rel X Y rel (return x) (return y)
240  ; mr_bind : ∀X,Y,Z,W,relin,relout,m,n.m_rel X Y relin m n → ∀f,g.(∀x,y.relin x y → m_rel Z W relout (f x) (g y)) →
241                  m_rel ?? relout (m_bind … m f) (m_bind … n g)
242  ; m_rel_mp : ∀X,Y.rel_modus_ponens ???? (m_rel X Y)
243  }.
Note: See TracBrowser for help on using the repository browser.