source: src/utilities/monad.ma @ 2453

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

come changes in monad notation to

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