source: src/common/ExtraMonads.ma @ 2755

Last change on this file since 2755 was 2590, checked in by piccolo, 7 years ago

added monad machineary for ERTL to ERTLptr translation
eval_seq_no_pc case in place in ERTLptr translation

File size: 10.6 KB
Line 
1(**************************************************************************)
2(*       ___                                                              *)
3(*      ||M||                                                             *)
4(*      ||A||       A project by Andrea Asperti                           *)
5(*      ||T||                                                             *)
6(*      ||I||       Developers:                                           *)
7(*      ||T||         The HELM team.                                      *)
8(*      ||A||         http://helm.cs.unibo.it                             *)
9(*      \   /                                                             *)
10(*       \ /        This file is distributed under the terms of the       *)
11(*        v         GNU General Public License Version 2                  *)
12(*                                                                        *)
13(**************************************************************************)
14
15include "common/Errors.ma".
16include "common/IOMonad.ma".
17
18lemma option_bind_inverse : ∀A,B.∀m : option A.∀f : A → option B.∀r.
19  ! x ← m ; f x = return r →
20  ∃x.m = return x ∧ f x = return r.
21#A #B * normalize [2:#x] #f #r #EQ destruct
22%{x} %{EQ} %
23qed.
24
25lemma bind_option_inversion_star:
26  ∀A,B: Type[0].∀P : Prop.∀f: option A. ∀g: A → option B. ∀y: B.
27  (∀x.f = Some … x → g x = Some … y → P) →
28  (! x ← f ; g x = Some … y) → P.
29#A #B #P #f #g #y #H #G elim (option_bind_inverse ????? G) #x * @H qed.
30
31interpretation "option bind inversion" 'bind_inversion =
32  (bind_option_inversion_star ???????).
33
34lemma bind_inversion_star : ∀X,Y.∀P : Prop.
35∀m : res X.∀f : X → res Y.∀v : Y.
36(∀x. m = return x → f x = return v → P) →
37! x ← m ; f x = return v → P.
38#X #Y #P #m #f #v #H #G
39elim (bind_inversion ????? G) #x * @H qed.
40
41interpretation "res bind inversion" 'bind_inversion =
42  (bind_inversion_star ???????).
43
44lemma IO_bind_inversion:
45  ∀O,I,A,B.∀P : Prop.∀f: IO O I A. ∀g: A → IO O I B. ∀y: B.
46  (∀x.f = return x → g x = return y → P) →
47  (! x ← f ; g x = return y) → P.
48#O #I #A #B #P #f #g #y cases f normalize
49[ #o #f #_ #H destruct
50| #a #G #H @(G ? (refl …) H)
51| #e #_ #H destruct
52] qed.
53
54interpretation "IO bind inversion" 'bind_inversion =
55  (IO_bind_inversion ?????????).
56 
57record MonadFunctRel (M1 : Monad) (M2 : Monad) : Type[1] ≝
58  { m_frel :6> ∀X,Y.∀P : X → Prop.(∀x.P x → Y) → (M1 X → M2 Y → Prop)
59  ; mfr_return : ∀X,Y,P,F,x,prf.m_frel X Y P F (return x) (return (F x prf))
60  ; mfr_bind : ∀X,Y,Z,W,P,Q,F,G,m,n.
61      m_frel X Y P F m n → ∀f,g.(∀x,prf.m_frel Z W Q G (f x) (g (F x prf))) →
62                  m_frel ?? Q G (m_bind … m f) (m_bind … n g)
63  ; m_frel_ext : ∀X,Y,P,F,G.(∀x,prf1,prf2.F x prf1 = G x prf2) → ∀u,v.m_frel X Y P F u v → m_frel X Y P G u v
64  }.
65 
66record MonadFunctRel1 (M1 : Monad) (M2 : Monad) : Type[1] ≝
67{ m_frel1  :5> ∀X,Y.(Y → X) → (M1 X → M2 Y → Prop)
68; mfr_return1 : ∀X,Y,F,y.m_frel1 X Y F (return (F y)) (return y)
69; mfr_bind1 : ∀X,Y,Z,W,F,G,m,n. m_frel1 X Y F m n →
70       ∀f,g.(∀x.m_frel1 Z W G (f (F x)) (g x)) → m_frel1 ?? G (m_bind … m f) (m_bind … n g)
71; m_frel_ext1 : ∀X,Y,F,G.(∀x.F  x = G x) → ∀ u,v.m_frel1 X Y F u v → m_frel1 X Y G u v
72}.
73
74
75definition res_preserve : MonadFunctRel Res Res ≝
76  mk_MonadFunctRel ??
77  (λX,Y,P,F,m,n.∀x.m = return x → ∃prf.n = return F x prf)
78  ???.
79[ #X #Y #P #F #x #prf #x' whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} %
80| #X #Y #Z #W #P #Q #F #G *
81  [ #u | #e ] #n #H #f #g #K #x
82  whd in ⊢ (??%%→?); #EQ destruct(EQ)
83  cases (H ? (refl …)) #prf #L >L @(K ? prf ? EQ)
84| #X #Y #P #F #G #H #u #v #K #x #EQ
85  cases (K … EQ) #prf #EQ' %{prf} >EQ' >H try %
86]
87qed.
88
89definition res_preserve1 : MonadFunctRel1 Res Res ≝
90mk_MonadFunctRel1 ??
91(λX,Y,F,m,n.∀y.m = return y → ∃ x. n = return x ∧ y = F x)
92???.
93[ #X #Y #F #y #x normalize #EQ destruct(EQ) %{y} % //
94| #X #Y #Z #W #F #G * [#x | #e] #n #H #f #g #H1 #z whd in ⊢ (??%% → ?); #EQ destruct
95  cases(H x (refl …)) #y * #n_spec #x_spec
96  cases(H1 y z ?) [2: <x_spec whd in ⊢ (???%); assumption] #w * #w_spec #z_spec %{w}
97  >n_spec <w_spec % //
98| #X #Y #F #G #ext #u #v #K #x #u_spec cases(K x u_spec) #y * #v_spec #y_spec %{y}
99  % //
100]
101qed.
102
103definition opt_preserve : MonadFunctRel Option Option ≝
104  mk_MonadFunctRel ??
105  (λX,Y,P,F,m,n.∀x.m = return x → ∃prf.n = return F x prf)
106  ???.
107[ #X #Y #P #F #x #prf #x' whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} %
108| #X #Y #Z #W #P #Q #F #G *
109  [ | #u ] #n #H #f #g #K #x
110  whd in ⊢ (??%%→?); #EQ destruct(EQ)
111  cases (H ? (refl …)) #prf #L >L @(K ? prf ? EQ)
112| #X #Y #P #F #G #H #u #v #K #x #EQ
113  cases (K … EQ) #prf #EQ' %{prf} >EQ' >H try %
114]
115qed.
116
117definition opt_preserve1 : MonadFunctRel1 Option Option ≝
118  mk_MonadFunctRel1 ??
119  (λX,Y,F,m,n.∀y.m = return y → ∃ x. n = return x ∧ y = F x)
120???.
121[ #X #Y #F #y #x normalize #EQ destruct(EQ) %{y} % //
122| #X #Y #Z #W #F #G * [| #x] #n #H #f #g #H1 #z whd in ⊢ (??%% → ?); #EQ destruct
123  cases(H x (refl …)) #y * #n_spec #x_spec
124  cases(H1 y z ?) [2: <x_spec whd in ⊢ (???%); assumption] #w * #w_spec #z_spec %{w}
125  >n_spec <w_spec % //
126| #X #Y #F #G #ext #u #v #K #x #u_spec cases(K x u_spec) #y * #v_spec #y_spec %{y}
127  % //
128]
129qed.
130
131definition io_preserve : ∀O,I.MonadFunctRel (IOMonad O I) (IOMonad O I) ≝
132  λO,I.mk_MonadFunctRel ??
133  (λX,Y,P,F,m,n.∀x.m = return x → ∃prf.n = return F x prf)
134  ???.
135[ #X #Y #P #F #x #prf #x' whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} %
136| #X #Y #Z #W #P #Q #F #G *
137  [ #o #f | #u | #e ] #n #H #f #g #K #x
138  whd in ⊢ (??%%→?); #EQ destruct(EQ)
139  cases (H ? (refl …)) #prf #L >L @(K ? prf ? EQ)
140| #X #Y #P #F #G #H #u #v #K #x #EQ
141  cases (K … EQ) #prf #EQ' %{prf} >EQ' >H try %
142]
143qed.
144
145definition io_preserve1 :  ∀O,I.MonadFunctRel1 (IOMonad O I) (IOMonad O I) ≝
146  λO,I.mk_MonadFunctRel1 ??
147  (λX,Y,F,m,n.∀y.m = return y → ∃ x. n = return x ∧ y = F x)
148???.
149[ #X #Y #F #y #x normalize #EQ destruct(EQ) %{y} % //
150| #X #Y #Z #W #F #G * [#o #r | #x | #e] #n #H #f #g #H1 #z whd in ⊢ (??%% → ?); #EQ destruct
151  cases(H x (refl …)) #y * #n_spec #x_spec
152  cases(H1 y z ?) [2: <x_spec whd in ⊢ (???%); assumption] #w * #w_spec #z_spec %{w}
153  >n_spec <w_spec % //
154| #X #Y #F #G #ext #u #v #K #x #u_spec cases(K x u_spec) #y * #v_spec #y_spec %{y}
155  % //
156]
157qed.
158
159definition preserving ≝
160  λM1,M2.λFR : MonadFunctRel M1 M2.
161  λX,Y,A,B : Type[0].
162  λP : X → Prop.
163  λQ : A → Prop.
164  λF : ∀x : X.P x → Y.
165  λG : ∀a : A.Q a → B.
166  λf : X → M1 A.
167  λg : Y → M2 B.
168  ∀x,prf.
169  FR … G
170    (f x) (g (F x prf)).
171
172definition preserving1 ≝   
173  λM1,M2.λFR : MonadFunctRel1 M1 M2.
174  λX,Y,A,B : Type[0].
175  λF : Y → X.
176  λG : B → A.
177  λf : X → M1 A.
178  λg : Y → M2 B.
179  ∀ y.
180  FR ?? G (f (F y)) (g y).
181
182definition preserving2 ≝
183  λM1,M2.λFR : MonadFunctRel M1 M2.
184  λX,Y,Z,W,A,B : Type[0].
185  λP : X → Prop.
186  λQ : Y → Prop.
187  λR : A → Prop.
188  λF : ∀x : X.P x → Z.
189  λG : ∀y : Y.Q y → W.
190  λH : ∀a : A.R a → B.
191  λf : X → Y → M1 A.
192  λg : Z → W → M2 B.
193  ∀x,y,prf1,prf2.
194  FR … H
195    (f x y) (g (F x prf1) (G y prf2)).
196   
197definition preserving21 ≝
198   λM1,M2.λFR : MonadFunctRel1 M1 M2.
199   λX,Y,Z,W,A,B : Type[0].
200   λF : Z → X.
201   λG : W → Y.
202   λH : B → A.
203   λf : X → Y → M1 A.
204   λg : Z → W → M2 B.
205   ∀z,w. FR ?? H (f (F z) (G w)) (g z w).
206   
207lemma res_preserve_error : ∀X,Y,P,F,e,n.res_preserve X Y P F (Error … e) n.
208#X #Y #P #F #e #n #x whd in ⊢ (??%%→?); #EQ destruct(EQ) qed.
209
210lemma res_preserve_error1 : ∀X,Y,F,e,n.res_preserve1 X Y F (Error … e) n.
211#X #Y #F #e #n #x whd in ⊢ (??%%→?); #EQ destruct(EQ) qed.
212
213lemma mfr_return_eq : ∀M1,M2.∀FR : MonadFunctRel M1 M2.
214∀X,Y,P,F,v,n.
215∀prf.n = return F v prf →
216FR X Y P F (return v) n.
217#M1 #M2 #FR #X #Y #P #F #v #n #prf #EQ >EQ @mfr_return qed.
218
219lemma mfr_return_eq1 :∀M1,M2.∀FR : MonadFunctRel1 M1 M2.
220∀X,Y,F,v,n.
221n = return F v →
222FR X Y F n (return v).
223#M1 #M2 #FR #X #Y #F #v #n #EQ >EQ @mfr_return1
224qed.
225
226lemma opt_safe_eq : ∀A,m,x,prf.m = Some A x → opt_safe A m prf = x.
227#A #m #x #prf @opt_safe_elim #x' #EQ >EQ #EQ' destruct % qed.
228
229lemma opt_preserve_none : ∀X,Y,P,F,n.opt_preserve X Y P F (None ?) n.
230#X #Y #P #F #n #x whd in ⊢ (??%%→?); #EQ destruct(EQ) qed.
231
232lemma opt_preserve_none1 :  ∀X,Y,F,n.opt_preserve1 X Y F (None ?) n.
233#X #Y #F #n #x whd in ⊢ (???% → ?); #EQ destruct qed.
234
235lemma m_list_map_All_ok :
236  ∀M : MonadProps.∀X,Y,f,l.
237  All X (λx.∃y.f x = return y) l → ∃l'.m_list_map M X Y f l = return l'.
238  #M #X #Y #f #l elim l -l
239  [ * %{[ ]} %
240  | #hd #tl #IH * * #y #EQ #H cases (IH H) #ys #EQ'
241    %{(y :: ys)}
242    change with (! y ← ? ;  ? = ?)
243    >EQ >m_return_bind
244    change with (! acc ← m_list_map ????? ; ? = ?) >EQ'
245    @m_return_bind
246qed.
247
248lemma res_eq_from_opt : ∀A,m,a.
249res_to_opt A m = return a → m = return a.
250#A #m #a  cases m #x normalize #EQ destruct(EQ) %
251qed.
252
253lemma res_to_opt_preserve : ∀X,Y,P,F,m,n.
254  res_preserve X Y P F m n → opt_preserve X Y P F (res_to_opt … m) (res_to_opt … n).
255#X #Y #P #F #m #n #H #x #EQ
256cases (H x ?)
257[ #prf #EQ' %{prf} >EQ' %
258| cases m in EQ; normalize #x #EQ destruct %
259]
260qed.
261
262lemma res_to_opt__preserve : ∀X,Y,F,m,n.
263  res_preserve1 X Y F m n → opt_preserve1 X Y F (res_to_opt … m) (res_to_opt … n).
264#X #Y #F #m #n #H #x #EQ
265whd in H; cases (H x ?)
266[ #y * #y_spec #x_spec %{y} % [ >y_spec %|assumption]
267| cases m in EQ; normalize #x #EQ destruct %
268]
269qed.
270
271lemma opt_to_res_preserve : ∀X,Y,P,F,m,n,e1,e2.
272       opt_preserve X Y P F m n →
273       res_preserve X Y P F (opt_to_res … e1 m) (opt_to_res … e2 n).
274#X #Y #P #F #m #n #e1 #e2 #H #v #prf
275cases (H … (opt_eq_from_res ???? prf)) #prf' #EQ %{prf'}
276>EQ %
277qed.
278
279lemma opt_to_res_preserve1 :  ∀X,Y,F,m,n,e1,e2.
280       opt_preserve1 X Y F m n →
281       res_preserve1 X Y F (opt_to_res … e1 m) (opt_to_res … e2 n).
282#X #Y #F #m #n #e1 #e2 #H #x #EQ
283cases(H x ?)
284[ #y * #y_spec #x_spec %{y} % [>y_spec %|assumption]
285| cases m in EQ; normalize [2: #x1] #EQ destruct %
286]
287qed.
288
289lemma err_eq_from_io : ∀O,I,X,m,v.
290  err_to_io O I X m = return v → m = return v.
291#O #I #X * #x #v normalize #EQ destruct % qed.
292
293lemma res_to_io_preserve : ∀O,I,X,Y,P,F,m,n.
294       res_preserve X Y P F m n →
295       io_preserve O I X Y P F m n.
296#O #I #X #Y #P #F #m #n #H #v #prf
297cases (H … (err_eq_from_io ????? prf)) #prf' #EQ %{prf'}
298>EQ %
299qed.
300
301lemma res_to_io_preserve1 : ∀O,I,X,Y,F,m,n.
302       res_preserve1 X Y F m n →
303       io_preserve1 O I X Y F m n.
304#O #I #X #Y #F #m #n #H #v #EQ cases(H v (err_eq_from_io ????? EQ))
305#y * #y_spec #v_spec %{y} % // >y_spec %
306qed.
Note: See TracBrowser for help on using the repository browser.