[1635] | 1 | include "basics/types.ma". |
---|
| 2 | include "basics/relations.ma". |
---|
| 3 | include "utilities/setoids.ma". |
---|
[1882] | 4 | |
---|
| 5 | definition pred_transformer ≝ λA,B : Type[0].(A → Prop) → B → Prop. |
---|
| 6 | |
---|
| 7 | definition 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 | |
---|
| 10 | lemma 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 | |
---|
| 14 | definition rel_transformer ≝ λA,B,C,D : Type[0]. |
---|
| 15 | (A → B → Prop) → C → D → Prop. |
---|
| 16 | |
---|
| 17 | definition 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 | |
---|
| 20 | lemma 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] | 24 | record 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 | |
---|
| 33 | notation > "!_ e; e'" |
---|
| 34 | with precedence 48 for @{'m_bind ${e} (λ_. ${e'})}. |
---|
| 35 | notation > "! ident v ← e; e'" |
---|
[1647] | 36 | with precedence 48 for @{'m_bind ${e} (λ${ident v}. ${e'})}. |
---|
[1635] | 37 | notation > "! ident v : ty ← e; e'" |
---|
| 38 | with precedence 48 for @{'m_bind ${e} (λ${ident v} : ${ty}. ${e'})}. |
---|
[1640] | 39 | notation > "! ident v ← e : ty ; e'" |
---|
| 40 | with precedence 48 for @{'m_bind (${e} : ${ty}) (λ${ident v}.${e'})}. |
---|
[2453] | 41 | notation < "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] | 43 | notation > "! ident v : ty ← e : ty' ; e'" |
---|
| 44 | with precedence 48 for @{'m_bind (${e} : ${ty'}) (λ${ident v} : ${ty}. ${e'})}. |
---|
[1635] | 45 | notation > "! 〈ident v1, ident v2〉 ← e ; e'" |
---|
| 46 | with precedence 48 for @{'m_bind2 ${e} (λ${ident v1}. λ${ident v2}. ${e'})}. |
---|
[1647] | 47 | notation > "! 〈ident v1, ident v2〉 ← e : ty ; e'" |
---|
| 48 | with precedence 48 for @{'m_bind2 (${e} : $ty) (λ${ident v1}. λ${ident v2}. ${e'})}. |
---|
[1635] | 49 | notation > "! 〈ident v1 : ty1, ident v2 : ty2〉 ← e ; e'" |
---|
| 50 | with precedence 48 for @{'m_bind2 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. ${e'})}. |
---|
[2453] | 51 | notation < "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] | 53 | notation > "! 〈ident v1, ident v2, ident v3〉 ← e ; e'" |
---|
| 54 | with precedence 48 for @{'m_bind3 ${e} (λ${ident v1}. λ${ident v2}. λ${ident v3}. ${e'})}. |
---|
[1647] | 55 | notation > "! 〈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] | 57 | notation > "! 〈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] | 59 | notation < "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 *) |
---|
| 63 | notation > "! «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] | 67 | notation < "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 | |
---|
| 72 | notation > "! «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] | 75 | notation < "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 *) |
---|
| 82 | notation > "'do'_ e; e'" |
---|
| 83 | with precedence 48 for @{'m_bind ${e} (λ_. ${e'})}. |
---|
[1640] | 84 | notation > "'do' ident v ← e; e'" |
---|
| 85 | with precedence 48 for @{'m_bind ${e} (λ${ident v}. ${e'})}. |
---|
| 86 | notation > "'do' ident v : ty ← e; e'" |
---|
| 87 | with precedence 48 for @{'m_bind ${e} (λ${ident v} : ${ty}. ${e'})}. |
---|
[1647] | 88 | notation > "'do' ident v ← e : ty ; e'" |
---|
| 89 | with precedence 48 for @{'m_bind (${e} : ${ty}) (λ${ident v}.${e'})}. |
---|
| 90 | notation > "'do' ident v : ty ← e : ty' ; e'" |
---|
| 91 | with precedence 48 for @{'m_bind (${e} : ${ty'}) (λ${ident v} : ${ty}. ${e'})}. |
---|
[1640] | 92 | notation > "'do' 〈ident v1, ident v2〉 ← e ; e'" |
---|
| 93 | with precedence 48 for @{'m_bind2 ${e} (λ${ident v1}. λ${ident v2}. ${e'})}. |
---|
| 94 | notation > "'do' 〈ident v1 : ty1, ident v2 : ty2〉 ← e ; e'" |
---|
| 95 | with precedence 48 for @{'m_bind2 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. ${e'})}. |
---|
| 96 | notation > "'do' 〈ident v1, ident v2, ident v3〉 ← e ; e'" |
---|
| 97 | with precedence 48 for @{'m_bind3 ${e} (λ${ident v1}. λ${ident v2}. λ${ident v3}. ${e'})}. |
---|
| 98 | notation > "'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 *) |
---|
| 102 | notation > "'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] | 107 | notation > "'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] | 111 | notation > "'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] | 116 | notation > "'return' t" with precedence 49 for @{'m_return $t}. |
---|
| 117 | notation < "'return' \nbsp t" with precedence 49 for @{'m_return $t}. |
---|
[1635] | 118 | |
---|
| 119 | interpretation "monad bind" 'm_bind m f = (m_bind ? ? ? m f). |
---|
| 120 | interpretation "monad return" 'm_return x = (m_return ? ? x). |
---|
| 121 | |
---|
[1647] | 122 | |
---|
| 123 | record 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 | |
---|
| 133 | record 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] | 148 | definition 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] | 152 | include "hints_declaration.ma". |
---|
[1949] | 153 | alias symbol "hint_decl" (instance 1) = "hint_decl_Type1". |
---|
[1882] | 154 | unification hint 0 ≔ M, X; |
---|
| 155 | M' ≟ smax_def M, S ≟ setoid_of_monad M X |
---|
| 156 | (*-----------------------------*)⊢ |
---|
| 157 | monad M' X ≡ std_supp S. |
---|
| 158 | |
---|
| 159 | include "basics/lists/list.ma". |
---|
| 160 | |
---|
[1976] | 161 | definition m_map ≝ λM : Monad.λX,Y.λf : X → Y.λm : M X. |
---|
[1882] | 162 | ! x ← m ; return f x. |
---|
| 163 | |
---|
[1976] | 164 | definition 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] | 167 | definition 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 | |
---|
| 170 | interpretation "monad bind2" 'm_bind2 m f = (m_bind2 ? ? ? ? m f). |
---|
| 171 | |
---|
| 172 | definition 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 | |
---|
| 177 | interpretation "monad bind3" 'm_bind3 m f = (m_bind3 ? ? ? ? ? m f). |
---|
| 178 | |
---|
[1976] | 179 | definition m_join : ∀M : Monad.∀X.M (M X) → M X ≝ |
---|
[1882] | 180 | λM,X,m.! x ← m ; x. |
---|
| 181 | |
---|
| 182 | definition 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 | |
---|
| 195 | interpretation "monad sigbind2" 'm_sigbind2 m f = (m_sigbind2 ????? m f). |
---|
| 196 | |
---|
| 197 | definition 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 | |
---|
| 201 | definition 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] | 209 | definition 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] | 213 | unification hint 0 ≔ M, X, Y, Z, m, f ; |
---|
| 214 | P ≟ Prod X Y, F ≟ λp.f (\fst p) (\snd p) ⊢ |
---|
| 215 | m_bind M P Z m F ≡ m_bind2 M X Y Z m f. |
---|
[1882] | 216 | |
---|
[1976] | 217 | unification 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) ⊢ |
---|
| 219 | m_bind M P W m F ≡ m_bind3 M X Y Z W m f. |
---|
[1882] | 220 | |
---|
| 221 | definition MakeMonadProps : ?→?→?→?→?→?→?→MonadProps ≝ λmonad,m_return,m_bind. |
---|
| 222 | mk_MonadProps (mk_Monad monad m_return m_bind). |
---|
| 223 | |
---|
[1647] | 224 | definition MakeSetoidMonadProps : ?→?→?→?→?→?→?→?→?→?→?→?→SetoidMonadProps ≝ |
---|
[1882] | 225 | λmonad,m_return,m_bind. |
---|
| 226 | mk_SetoidMonadProps (mk_Monad monad m_return m_bind). |
---|
| 227 | |
---|
[1949] | 228 | include "basics/russell.ma". |
---|
| 229 | |
---|
[1882] | 230 | record 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 | |
---|
| 239 | record 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] | 245 | coercion 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] | 249 | lemma 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] | 253 | record 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 | }. |
---|