source: src/common/ExtraMonads.ma @ 2801

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

Partial commit not yet finished

File size: 11.8 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; mfr_bind_inversion1 :  ∀X,Y,Z,W,F,G,m,n. m_frel1 X Y F m n →
72       ∀f,g.(∀x.m = return F x → n = return x → m_frel1 Z W G (f (F x)) (g x)) → m_frel1 ?? G (m_bind … m f) (m_bind … n g)
73; 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
74}.
75
76
77definition res_preserve : MonadFunctRel Res Res ≝
78  mk_MonadFunctRel ??
79  (λX,Y,P,F,m,n.∀x.m = return x → ∃prf.n = return F x prf)
80  ???.
81[ #X #Y #P #F #x #prf #x' whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} %
82| #X #Y #Z #W #P #Q #F #G *
83  [ #u | #e ] #n #H #f #g #K #x
84  whd in ⊢ (??%%→?); #EQ destruct(EQ)
85  cases (H ? (refl …)) #prf #L >L @(K ? prf ? EQ)
86| #X #Y #P #F #G #H #u #v #K #x #EQ
87  cases (K … EQ) #prf #EQ' %{prf} >EQ' >H try %
88]
89qed.
90
91definition res_preserve1 : MonadFunctRel1 Res Res ≝
92mk_MonadFunctRel1 ??
93(λX,Y,F,m,n.∀y.m = return y → ∃ x. n = return x ∧ y = F x)
94????.
95[ #X #Y #F #y #x normalize #EQ destruct(EQ) %{y} % //
96| #X #Y #Z #W #F #G * [#x | #e] #n #H #f #g #H1 #z whd in ⊢ (??%% → ?); #EQ destruct
97  cases(H x (refl …)) #y * #n_spec #x_spec
98  cases(H1 y z ?) [2: <x_spec whd in ⊢ (???%); assumption] #w * #w_spec #z_spec %{w}
99  >n_spec <w_spec % //
100| #X #Y #Z #W #F #G * [ #x | #e ] #n #H #f #g #H1 #z
101  whd in ⊢ (??%% → ?); [2: #EQ destruct(EQ)] #H2 cases(H x (refl …))
102  #y * #n_spec #x_spec cases(H1 y ? n_spec z ?) [2,3: <x_spec // assumption ] #w
103  * #w_spec #EQz %{w} >n_spec <w_spec % //
104| #X #Y #F #G #ext #u #v #K #x #u_spec cases(K x u_spec) #y * #v_spec #y_spec %{y}
105  % //
106]
107qed.
108
109definition opt_preserve : MonadFunctRel Option Option ≝
110  mk_MonadFunctRel ??
111  (λX,Y,P,F,m,n.∀x.m = return x → ∃prf.n = return F x prf)
112  ???.
113[ #X #Y #P #F #x #prf #x' whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} %
114| #X #Y #Z #W #P #Q #F #G *
115  [ | #u ] #n #H #f #g #K #x
116  whd in ⊢ (??%%→?); #EQ destruct(EQ)
117  cases (H ? (refl …)) #prf #L >L @(K ? prf ? EQ)
118| #X #Y #P #F #G #H #u #v #K #x #EQ
119  cases (K … EQ) #prf #EQ' %{prf} >EQ' >H try %
120]
121qed.
122
123definition opt_preserve1 : MonadFunctRel1 Option Option ≝
124  mk_MonadFunctRel1 ??
125  (λX,Y,F,m,n.∀y.m = return y → ∃ x. n = return x ∧ y = F x)
126????.
127[ #X #Y #F #y #x normalize #EQ destruct(EQ) %{y} % //
128| #X #Y #Z #W #F #G * [| #x] #n #H #f #g #H1 #z whd in ⊢ (??%% → ?); #EQ destruct
129  cases(H x (refl …)) #y * #n_spec #x_spec
130  cases(H1 y z ?) [2: <x_spec whd in ⊢ (???%); assumption] #w * #w_spec #z_spec %{w}
131  >n_spec <w_spec % //
132| #X #Y #Z #W #F #G * [ | #x ] #n #H #f #g #H1 #z
133  whd in ⊢ (??%% → ?); [ #EQ destruct(EQ)] #H2 cases(H x (refl …))
134  #y * #n_spec #x_spec cases(H1 y ? n_spec z ?) [2,3: <x_spec // assumption] #w
135  * #w_spec #EQz %{w} >n_spec <w_spec % //
136| #X #Y #F #G #ext #u #v #K #x #u_spec cases(K x u_spec) #y * #v_spec #y_spec %{y}
137  % //
138]
139qed.
140
141definition io_preserve : ∀O,I.MonadFunctRel (IOMonad O I) (IOMonad O I) ≝
142  λO,I.mk_MonadFunctRel ??
143  (λX,Y,P,F,m,n.∀x.m = return x → ∃prf.n = return F x prf)
144  ???.
145[ #X #Y #P #F #x #prf #x' whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} %
146| #X #Y #Z #W #P #Q #F #G *
147  [ #o #f | #u | #e ] #n #H #f #g #K #x
148  whd in ⊢ (??%%→?); #EQ destruct(EQ)
149  cases (H ? (refl …)) #prf #L >L @(K ? prf ? EQ)
150| #X #Y #P #F #G #H #u #v #K #x #EQ
151  cases (K … EQ) #prf #EQ' %{prf} >EQ' >H try %
152]
153qed.
154
155definition io_preserve1 :  ∀O,I.MonadFunctRel1 (IOMonad O I) (IOMonad O I) ≝
156  λO,I.mk_MonadFunctRel1 ??
157  (λX,Y,F,m,n.∀y.m = return y → ∃ x. n = return x ∧ y = F x)
158????.
159[ #X #Y #F #y #x normalize #EQ destruct(EQ) %{y} % //
160| #X #Y #Z #W #F #G * [#o #r | #x | #e] #n #H #f #g #H1 #z whd in ⊢ (??%% → ?); #EQ destruct
161  cases(H x (refl …)) #y * #n_spec #x_spec
162  cases(H1 y z ?) [2: <x_spec whd in ⊢ (???%); assumption] #w * #w_spec #z_spec %{w}
163  >n_spec <w_spec % //
164| #X #Y #Z #W #F #G * [ #o #r | #x | #e ] #n #H #f #g #H1 #z
165  whd in ⊢ (??%% → ?); #EQ destruct(EQ) cases(H x (refl …))
166  #y * #n_spec #x_spec cases(H1 y ? n_spec z ?) [2,3: <x_spec // assumption] #w
167  * #w_spec #EQz %{w} >n_spec <w_spec % //
168| #X #Y #F #G #ext #u #v #K #x #u_spec cases(K x u_spec) #y * #v_spec #y_spec %{y}
169  % //
170]
171qed.
172
173definition preserving ≝
174  λM1,M2.λFR : MonadFunctRel M1 M2.
175  λX,Y,A,B : Type[0].
176  λP : X → Prop.
177  λQ : A → Prop.
178  λF : ∀x : X.P x → Y.
179  λG : ∀a : A.Q a → B.
180  λf : X → M1 A.
181  λg : Y → M2 B.
182  ∀x,prf.
183  FR … G
184    (f x) (g (F x prf)).
185
186definition preserving1 ≝   
187  λM1,M2.λFR : MonadFunctRel1 M1 M2.
188  λX,Y,A,B : Type[0].
189  λF : Y → X.
190  λG : B → A.
191  λf : X → M1 A.
192  λg : Y → M2 B.
193  ∀ y.
194  FR ?? G (f (F y)) (g y).
195
196definition preserving2 ≝
197  λM1,M2.λFR : MonadFunctRel M1 M2.
198  λX,Y,Z,W,A,B : Type[0].
199  λP : X → Prop.
200  λQ : Y → Prop.
201  λR : A → Prop.
202  λF : ∀x : X.P x → Z.
203  λG : ∀y : Y.Q y → W.
204  λH : ∀a : A.R a → B.
205  λf : X → Y → M1 A.
206  λg : Z → W → M2 B.
207  ∀x,y,prf1,prf2.
208  FR … H
209    (f x y) (g (F x prf1) (G y prf2)).
210   
211definition preserving21 ≝
212   λM1,M2.λFR : MonadFunctRel1 M1 M2.
213   λX,Y,Z,W,A,B : Type[0].
214   λF : Z → X.
215   λG : W → Y.
216   λH : B → A.
217   λf : X → Y → M1 A.
218   λg : Z → W → M2 B.
219   ∀z,w. FR ?? H (f (F z) (G w)) (g z w).
220   
221lemma res_preserve_error : ∀X,Y,P,F,e,n.res_preserve X Y P F (Error … e) n.
222#X #Y #P #F #e #n #x whd in ⊢ (??%%→?); #EQ destruct(EQ) qed.
223
224lemma res_preserve_error1 : ∀X,Y,F,e,n.res_preserve1 X Y F (Error … e) n.
225#X #Y #F #e #n #x whd in ⊢ (??%%→?); #EQ destruct(EQ) qed.
226
227lemma mfr_return_eq : ∀M1,M2.∀FR : MonadFunctRel M1 M2.
228∀X,Y,P,F,v,n.
229∀prf.n = return F v prf →
230FR X Y P F (return v) n.
231#M1 #M2 #FR #X #Y #P #F #v #n #prf #EQ >EQ @mfr_return qed.
232
233lemma mfr_return_eq1 :∀M1,M2.∀FR : MonadFunctRel1 M1 M2.
234∀X,Y,F,v,n.
235n = return F v →
236FR X Y F n (return v).
237#M1 #M2 #FR #X #Y #F #v #n #EQ >EQ @mfr_return1
238qed.
239
240lemma opt_safe_eq : ∀A,m,x,prf.m = Some A x → opt_safe A m prf = x.
241#A #m #x #prf @opt_safe_elim #x' #EQ >EQ #EQ' destruct % qed.
242
243lemma opt_preserve_none : ∀X,Y,P,F,n.opt_preserve X Y P F (None ?) n.
244#X #Y #P #F #n #x whd in ⊢ (??%%→?); #EQ destruct(EQ) qed.
245
246lemma opt_preserve_none1 :  ∀X,Y,F,n.opt_preserve1 X Y F (None ?) n.
247#X #Y #F #n #x whd in ⊢ (???% → ?); #EQ destruct qed.
248
249lemma m_list_map_All_ok :
250  ∀M : MonadProps.∀X,Y,f,l.
251  All X (λx.∃y.f x = return y) l → ∃l'.m_list_map M X Y f l = return l'.
252  #M #X #Y #f #l elim l -l
253  [ * %{[ ]} %
254  | #hd #tl #IH * * #y #EQ #H cases (IH H) #ys #EQ'
255    %{(y :: ys)}
256    change with (! y ← ? ;  ? = ?)
257    >EQ >m_return_bind
258    change with (! acc ← m_list_map ????? ; ? = ?) >EQ'
259    @m_return_bind
260qed.
261
262lemma res_eq_from_opt : ∀A,m,a.
263res_to_opt A m = return a → m = return a.
264#A #m #a  cases m #x normalize #EQ destruct(EQ) %
265qed.
266
267lemma res_to_opt_preserve : ∀X,Y,P,F,m,n.
268  res_preserve X Y P F m n → opt_preserve X Y P F (res_to_opt … m) (res_to_opt … n).
269#X #Y #P #F #m #n #H #x #EQ
270cases (H x ?)
271[ #prf #EQ' %{prf} >EQ' %
272| cases m in EQ; normalize #x #EQ destruct %
273]
274qed.
275
276lemma res_to_opt__preserve : ∀X,Y,F,m,n.
277  res_preserve1 X Y F m n → opt_preserve1 X Y F (res_to_opt … m) (res_to_opt … n).
278#X #Y #F #m #n #H #x #EQ
279whd in H; cases (H x ?)
280[ #y * #y_spec #x_spec %{y} % [ >y_spec %|assumption]
281| cases m in EQ; normalize #x #EQ destruct %
282]
283qed.
284
285lemma opt_to_res_preserve : ∀X,Y,P,F,m,n,e1,e2.
286       opt_preserve X Y P F m n →
287       res_preserve X Y P F (opt_to_res … e1 m) (opt_to_res … e2 n).
288#X #Y #P #F #m #n #e1 #e2 #H #v #prf
289cases (H … (opt_eq_from_res ???? prf)) #prf' #EQ %{prf'}
290>EQ %
291qed.
292
293lemma opt_to_res_preserve1 :  ∀X,Y,F,m,n,e1,e2.
294       opt_preserve1 X Y F m n →
295       res_preserve1 X Y F (opt_to_res … e1 m) (opt_to_res … e2 n).
296#X #Y #F #m #n #e1 #e2 #H #x #EQ
297cases(H x ?)
298[ #y * #y_spec #x_spec %{y} % [>y_spec %|assumption]
299| cases m in EQ; normalize [2: #x1] #EQ destruct %
300]
301qed.
302
303lemma err_eq_from_io : ∀O,I,X,m,v.
304  err_to_io O I X m = return v → m = return v.
305#O #I #X * #x #v normalize #EQ destruct % qed.
306
307lemma res_to_io_preserve : ∀O,I,X,Y,P,F,m,n.
308       res_preserve X Y P F m n →
309       io_preserve O I X Y P F m n.
310#O #I #X #Y #P #F #m #n #H #v #prf
311cases (H … (err_eq_from_io ????? prf)) #prf' #EQ %{prf'}
312>EQ %
313qed.
314
315lemma res_to_io_preserve1 : ∀O,I,X,Y,F,m,n.
316       res_preserve1 X Y F m n →
317       io_preserve1 O I X Y F m n.
318#O #I #X #Y #F #m #n #H #v #EQ cases(H v (err_eq_from_io ????? EQ))
319#y * #y_spec #v_spec %{y} % // >y_spec %
320qed.
321
322lemma res_preserve_error11 : ∀X,Y,F,e,n. (∃e'.n = Error … e') →
323res_preserve1 X Y F n (Error … e).
324#X #Y #F #e #n * #e' #n_spec >n_spec @res_preserve_error1
325qed.
Note: See TracBrowser for help on using the repository browser.