source: src/common/ExtraMonads.ma @ 3050

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

1) Added general commutation theorem for monads.

2) Added some commutation lemma for push and pop that can be useful
for sigle steps of correctness proof.

3) fixed some bugs.

File size: 16.9 KB
RevLine 
[2570]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  }.
[2590]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)
[2801]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)
[2590]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}.
[2570]75
[3050]76record MonadGenRel (M1 : Monad) (M2 : Monad) : Type[1] ≝
77{ m_gen_rel :5> ∀X,Y.(X → Y → Prop) → (M1 X → M2 Y → Prop)
78; m_gen_return : ∀X,Y,R,x,y.R x y → m_gen_rel X Y R (return x) (return y)
79; m_gen_bind : ∀X,Y,Z,W,R1,R2,m,n.m_gen_rel X Y R1 m n →
80           ∀f,g.(∀x,y.R1 x y → m_gen_rel Z W R2 (f x) (g y)) → m_gen_rel ?? R2 (m_bind … m f) (m_bind … n g)
81; m_gen_bind_inversion  : ∀X,Y,Z,W,R1,R2,m,n.m_gen_rel X Y R1 m n →
82         ∀f,g.(∀x,y.m = return x → n = return y → R1 x y → m_gen_rel Z W R2 (f x) (g y))
83         → m_gen_rel ?? R2 (m_bind … m f) (m_bind … n g)
84; m_gen_rel_ext : ∀X,Y,R1,R2.(∀x,y.R1 x y → R2 x y) → ∀u,v.m_gen_rel X Y R1 u v → m_gen_rel X Y R2 u v
85}.
[2590]86
[2570]87definition res_preserve : MonadFunctRel Res Res ≝
88  mk_MonadFunctRel ??
89  (λX,Y,P,F,m,n.∀x.m = return x → ∃prf.n = return F x prf)
90  ???.
91[ #X #Y #P #F #x #prf #x' whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} %
92| #X #Y #Z #W #P #Q #F #G *
93  [ #u | #e ] #n #H #f #g #K #x
94  whd in ⊢ (??%%→?); #EQ destruct(EQ)
95  cases (H ? (refl …)) #prf #L >L @(K ? prf ? EQ)
96| #X #Y #P #F #G #H #u #v #K #x #EQ
97  cases (K … EQ) #prf #EQ' %{prf} >EQ' >H try %
98]
99qed.
100
[2590]101definition res_preserve1 : MonadFunctRel1 Res Res ≝
102mk_MonadFunctRel1 ??
103(λX,Y,F,m,n.∀y.m = return y → ∃ x. n = return x ∧ y = F x)
[2801]104????.
[2590]105[ #X #Y #F #y #x normalize #EQ destruct(EQ) %{y} % //
106| #X #Y #Z #W #F #G * [#x | #e] #n #H #f #g #H1 #z whd in ⊢ (??%% → ?); #EQ destruct
107  cases(H x (refl …)) #y * #n_spec #x_spec
108  cases(H1 y z ?) [2: <x_spec whd in ⊢ (???%); assumption] #w * #w_spec #z_spec %{w}
109  >n_spec <w_spec % //
[2801]110| #X #Y #Z #W #F #G * [ #x | #e ] #n #H #f #g #H1 #z
111  whd in ⊢ (??%% → ?); [2: #EQ destruct(EQ)] #H2 cases(H x (refl …))
112  #y * #n_spec #x_spec cases(H1 y ? n_spec z ?) [2,3: <x_spec // assumption ] #w
113  * #w_spec #EQz %{w} >n_spec <w_spec % //
[2590]114| #X #Y #F #G #ext #u #v #K #x #u_spec cases(K x u_spec) #y * #v_spec #y_spec %{y}
115  % //
116]
117qed.
118
[3050]119definition gen_res_preserve : MonadGenRel Res Res ≝
120mk_MonadGenRel ??
121(λX,Y,R,m,n.∀x.m = return x → ∃y.n = return y ∧ R x y)
122????.
123[ #X #Y #R #x #y #H #x1 whd in ⊢ (??%% → ?); #EQ destruct(EQ) %{y} %{(refl …)} @H
124| #X #Y #Z #W #R1 #R2 * [#x | #e] #n #H #f #g #H1 #z whd in ⊢ (??%% → ?);
125  #EQ destruct cases(H x (refl …)) #y * whd in ⊢ (???% → ?); #EQ destruct
126  #R1xy cases(H1 x y R1xy z) [2: assumption] #w * #EQw #R2zw %{w} normalize >EQw
127  %{(refl …)} assumption
128| #X #Y #Z #W #R1 #R2 * [#x | #e] #n #H #f #g #H1 #z whd in ⊢ (??%% → ?);
129  #EQ destruct cases(H x (refl …)) #y * whd in ⊢ (???% → ?); #EQ1 destruct
130  #Rxy cases(H1 x y (refl …) (refl …) Rxy z EQ) #w * #EQw #Rzw %{w}
131  normalize %{EQw} assumption
132| #X #Y #R1 #R2 #H #u #v #H1 #x whd in ⊢ (???% → ?); #EQ destruct
133  cases(H1 x (refl …)) #y * whd in ⊢ (???% → ?); #EQ destruct
134  #Rxy %{y} %{(refl …)} @H assumption
135]
136qed.
137
[2570]138definition opt_preserve : MonadFunctRel Option Option ≝
139  mk_MonadFunctRel ??
140  (λX,Y,P,F,m,n.∀x.m = return x → ∃prf.n = return F x prf)
141  ???.
142[ #X #Y #P #F #x #prf #x' whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} %
143| #X #Y #Z #W #P #Q #F #G *
144  [ | #u ] #n #H #f #g #K #x
145  whd in ⊢ (??%%→?); #EQ destruct(EQ)
146  cases (H ? (refl …)) #prf #L >L @(K ? prf ? EQ)
147| #X #Y #P #F #G #H #u #v #K #x #EQ
148  cases (K … EQ) #prf #EQ' %{prf} >EQ' >H try %
149]
150qed.
151
[2590]152definition opt_preserve1 : MonadFunctRel1 Option Option ≝
153  mk_MonadFunctRel1 ??
154  (λX,Y,F,m,n.∀y.m = return y → ∃ x. n = return x ∧ y = F x)
[2801]155????.
[2590]156[ #X #Y #F #y #x normalize #EQ destruct(EQ) %{y} % //
157| #X #Y #Z #W #F #G * [| #x] #n #H #f #g #H1 #z whd in ⊢ (??%% → ?); #EQ destruct
158  cases(H x (refl …)) #y * #n_spec #x_spec
159  cases(H1 y z ?) [2: <x_spec whd in ⊢ (???%); assumption] #w * #w_spec #z_spec %{w}
160  >n_spec <w_spec % //
[2801]161| #X #Y #Z #W #F #G * [ | #x ] #n #H #f #g #H1 #z
162  whd in ⊢ (??%% → ?); [ #EQ destruct(EQ)] #H2 cases(H x (refl …))
163  #y * #n_spec #x_spec cases(H1 y ? n_spec z ?) [2,3: <x_spec // assumption] #w
164  * #w_spec #EQz %{w} >n_spec <w_spec % //
[2590]165| #X #Y #F #G #ext #u #v #K #x #u_spec cases(K x u_spec) #y * #v_spec #y_spec %{y}
166  % //
167]
168qed.
169
[3050]170definition gen_opt_preserve : MonadGenRel Option Option ≝
171mk_MonadGenRel ??
172(λX,Y,R,m,n.∀x.m = return x → ∃y.n = return y ∧ R x y)
173????.
174[ #X #Y #R #x #y #H #x1 whd in ⊢ (??%% → ?); #EQ destruct(EQ) %{y} %{(refl …)} @H
175| #X #Y #Z #W #R1 #R2 * [| #x] #n #H #f #g #H1 #z whd in ⊢ (??%% → ?);
176  #EQ destruct cases(H x (refl …)) #y * whd in ⊢ (???% → ?); #EQ destruct
177  #R1xy cases(H1 x y R1xy z) [2: assumption] #w * #EQw #R2zw %{w} normalize >EQw
178  %{(refl …)} assumption
179| #X #Y #Z #W #R1 #R2 * [| #x] #n #H #f #g #H1 #z whd in ⊢ (??%% → ?);
180  #EQ destruct cases(H x (refl …)) #y * whd in ⊢ (???% → ?); #EQ1 destruct
181  #Rxy cases(H1 x y (refl …) (refl …) Rxy z EQ) #w * #EQw #Rzw %{w}
182  normalize %{EQw} assumption
183| #X #Y #R1 #R2 #H #u #v #H1 #x whd in ⊢ (???% → ?); #EQ destruct
184  cases(H1 x (refl …)) #y * whd in ⊢ (???% → ?); #EQ destruct
185  #Rxy %{y} %{(refl …)} @H assumption
186]
187qed.
188
189
[2570]190definition io_preserve : ∀O,I.MonadFunctRel (IOMonad O I) (IOMonad O I) ≝
191  λO,I.mk_MonadFunctRel ??
192  (λX,Y,P,F,m,n.∀x.m = return x → ∃prf.n = return F x prf)
193  ???.
194[ #X #Y #P #F #x #prf #x' whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} %
195| #X #Y #Z #W #P #Q #F #G *
196  [ #o #f | #u | #e ] #n #H #f #g #K #x
197  whd in ⊢ (??%%→?); #EQ destruct(EQ)
198  cases (H ? (refl …)) #prf #L >L @(K ? prf ? EQ)
199| #X #Y #P #F #G #H #u #v #K #x #EQ
200  cases (K … EQ) #prf #EQ' %{prf} >EQ' >H try %
201]
202qed.
203
[2590]204definition io_preserve1 :  ∀O,I.MonadFunctRel1 (IOMonad O I) (IOMonad O I) ≝
205  λO,I.mk_MonadFunctRel1 ??
206  (λX,Y,F,m,n.∀y.m = return y → ∃ x. n = return x ∧ y = F x)
[2801]207????.
[2590]208[ #X #Y #F #y #x normalize #EQ destruct(EQ) %{y} % //
209| #X #Y #Z #W #F #G * [#o #r | #x | #e] #n #H #f #g #H1 #z whd in ⊢ (??%% → ?); #EQ destruct
210  cases(H x (refl …)) #y * #n_spec #x_spec
211  cases(H1 y z ?) [2: <x_spec whd in ⊢ (???%); assumption] #w * #w_spec #z_spec %{w}
212  >n_spec <w_spec % //
[2801]213| #X #Y #Z #W #F #G * [ #o #r | #x | #e ] #n #H #f #g #H1 #z
214  whd in ⊢ (??%% → ?); #EQ destruct(EQ) cases(H x (refl …))
215  #y * #n_spec #x_spec cases(H1 y ? n_spec z ?) [2,3: <x_spec // assumption] #w
216  * #w_spec #EQz %{w} >n_spec <w_spec % //
[2590]217| #X #Y #F #G #ext #u #v #K #x #u_spec cases(K x u_spec) #y * #v_spec #y_spec %{y}
218  % //
219]
220qed.
221
[3050]222definition gen_io_preserve : ∀O,I.MonadGenRel (IOMonad O I)(IOMonad O I) ≝
223λO,I.mk_MonadGenRel ??
224(λX,Y,R,m,n.∀x.m = return x → ∃y.n = return y ∧ R x y)
225????.
226[ #X #Y #R #x #y #H #x1 whd in ⊢ (??%% → ?); #EQ destruct(EQ) %{y} %{(refl …)} @H
227| #X #Y #Z #W #R1 #R2 * [#o #r | #x | #e ] #n #H #f #g #H1 #z whd in ⊢ (??%% → ?);
228  #EQ destruct cases(H x (refl …)) #y * whd in ⊢ (???% → ?); #EQ destruct
229  #R1xy cases(H1 x y R1xy z) [2: assumption] #w * #EQw #R2zw %{w} normalize >EQw
230  %{(refl …)} assumption
231| #X #Y #Z #W #R1 #R2 * [#o #r | #x | #e ] #n #H #f #g #H1 #z whd in ⊢ (??%% → ?);
232  #EQ destruct cases(H x (refl …)) #y * whd in ⊢ (???% → ?); #EQ1 destruct
233  #Rxy cases(H1 x y (refl …) (refl …) Rxy z EQ) #w * #EQw #Rzw %{w}
234  normalize %{EQw} assumption
235| #X #Y #R1 #R2 #H #u #v #H1 #x whd in ⊢ (???% → ?); #EQ destruct
236  cases(H1 x (refl …)) #y * whd in ⊢ (???% → ?); #EQ destruct
237  #Rxy %{y} %{(refl …)} @H assumption
238]
239qed.
240
[2570]241definition preserving ≝
242  λM1,M2.λFR : MonadFunctRel M1 M2.
243  λX,Y,A,B : Type[0].
244  λP : X → Prop.
245  λQ : A → Prop.
246  λF : ∀x : X.P x → Y.
247  λG : ∀a : A.Q a → B.
248  λf : X → M1 A.
249  λg : Y → M2 B.
250  ∀x,prf.
251  FR … G
252    (f x) (g (F x prf)).
253
[2590]254definition preserving1 ≝   
255  λM1,M2.λFR : MonadFunctRel1 M1 M2.
256  λX,Y,A,B : Type[0].
257  λF : Y → X.
258  λG : B → A.
259  λf : X → M1 A.
260  λg : Y → M2 B.
261  ∀ y.
262  FR ?? G (f (F y)) (g y).
[3050]263 
264definition gen_preserving ≝
265λM1,M2.λFR : MonadGenRel M1 M2.
266 λX,Y,A,B : Type[0].
267 λR1 : X → Y → Prop.
268 λR2 : A → B → Prop.
269 λf : X → M1 A.
270 λg : Y → M2 B.
271 ∀x,y. R1 x y →
272 FR ?? R2 (f x) (g y).
[2590]273
[2570]274definition preserving2 ≝
275  λM1,M2.λFR : MonadFunctRel M1 M2.
276  λX,Y,Z,W,A,B : Type[0].
277  λP : X → Prop.
278  λQ : Y → Prop.
279  λR : A → Prop.
280  λF : ∀x : X.P x → Z.
281  λG : ∀y : Y.Q y → W.
282  λH : ∀a : A.R a → B.
283  λf : X → Y → M1 A.
284  λg : Z → W → M2 B.
285  ∀x,y,prf1,prf2.
286  FR … H
287    (f x y) (g (F x prf1) (G y prf2)).
[2590]288   
289definition preserving21 ≝
290   λM1,M2.λFR : MonadFunctRel1 M1 M2.
291   λX,Y,Z,W,A,B : Type[0].
292   λF : Z → X.
293   λG : W → Y.
294   λH : B → A.
295   λf : X → Y → M1 A.
296   λg : Z → W → M2 B.
297   ∀z,w. FR ?? H (f (F z) (G w)) (g z w).
298   
[3050]299definition gen_preserving2 ≝
300λM1,M2.λFR : MonadGenRel M1 M2.
301  λX,Y,Z,W,A,B : Type[0].
302  λR1 : X → Y → Prop.
303  λR2 : Z → W → Prop.
304  λR3 : A → B → Prop.
305  λf : X → Z → M1 A.
306  λg : Y → W → M2 B.
307  ∀x,y,z,w. R1 x y → R2 z w →
308  FR ?? R3 (f x z) (g y w). 
309
[2570]310lemma res_preserve_error : ∀X,Y,P,F,e,n.res_preserve X Y P F (Error … e) n.
311#X #Y #P #F #e #n #x whd in ⊢ (??%%→?); #EQ destruct(EQ) qed.
312
[2590]313lemma res_preserve_error1 : ∀X,Y,F,e,n.res_preserve1 X Y F (Error … e) n.
[3050]314#X #Y #F #e #n #x whd in ⊢ (??%%→?); #EQ destruct(EQ) qed.
[2590]315
[3050]316lemma res_preserve_error_gen : ∀X,Y,R,e,n.gen_res_preserve X Y R (Error … e) n.
317#X #Y #R #e #n whd #x whd in ⊢ (???% → ?); #EQ destruct qed.
318
[2570]319lemma mfr_return_eq : ∀M1,M2.∀FR : MonadFunctRel M1 M2.
320∀X,Y,P,F,v,n.
321∀prf.n = return F v prf →
322FR X Y P F (return v) n.
323#M1 #M2 #FR #X #Y #P #F #v #n #prf #EQ >EQ @mfr_return qed.
324
[2590]325lemma mfr_return_eq1 :∀M1,M2.∀FR : MonadFunctRel1 M1 M2.
326∀X,Y,F,v,n.
327n = return F v →
328FR X Y F n (return v).
329#M1 #M2 #FR #X #Y #F #v #n #EQ >EQ @mfr_return1
330qed.
331
[3050]332lemma gen_mfr_return_eq : ∀M1,M2.∀FR : MonadGenRel M1 M2.
333∀X,Y,R,x,y,n.R x y →
334n = return x → FR X Y R n (return y).
335#M1 #M2 #FR #X #Y #R #x #y #n #H #EQ destruct @m_gen_return assumption
336qed.
337
[2570]338lemma opt_safe_eq : ∀A,m,x,prf.m = Some A x → opt_safe A m prf = x.
339#A #m #x #prf @opt_safe_elim #x' #EQ >EQ #EQ' destruct % qed.
340
341lemma opt_preserve_none : ∀X,Y,P,F,n.opt_preserve X Y P F (None ?) n.
342#X #Y #P #F #n #x whd in ⊢ (??%%→?); #EQ destruct(EQ) qed.
343
[2590]344lemma opt_preserve_none1 :  ∀X,Y,F,n.opt_preserve1 X Y F (None ?) n.
345#X #Y #F #n #x whd in ⊢ (???% → ?); #EQ destruct qed.
346
[3050]347lemma opt_preserve_none_gen : ∀X,Y,R,n.gen_opt_preserve X Y R (None ?) n.
348#X #Y #R #n whd #x whd in ⊢ (???% → ?); #EQ destruct qed.
349
[2570]350lemma m_list_map_All_ok :
351  ∀M : MonadProps.∀X,Y,f,l.
352  All X (λx.∃y.f x = return y) l → ∃l'.m_list_map M X Y f l = return l'.
353  #M #X #Y #f #l elim l -l
354  [ * %{[ ]} %
355  | #hd #tl #IH * * #y #EQ #H cases (IH H) #ys #EQ'
356    %{(y :: ys)}
357    change with (! y ← ? ;  ? = ?)
358    >EQ >m_return_bind
359    change with (! acc ← m_list_map ????? ; ? = ?) >EQ'
360    @m_return_bind
361qed.
362
363lemma res_eq_from_opt : ∀A,m,a.
364res_to_opt A m = return a → m = return a.
365#A #m #a  cases m #x normalize #EQ destruct(EQ) %
366qed.
367
368lemma res_to_opt_preserve : ∀X,Y,P,F,m,n.
369  res_preserve X Y P F m n → opt_preserve X Y P F (res_to_opt … m) (res_to_opt … n).
370#X #Y #P #F #m #n #H #x #EQ
371cases (H x ?)
372[ #prf #EQ' %{prf} >EQ' %
373| cases m in EQ; normalize #x #EQ destruct %
374]
375qed.
376
[2590]377lemma res_to_opt__preserve : ∀X,Y,F,m,n.
378  res_preserve1 X Y F m n → opt_preserve1 X Y F (res_to_opt … m) (res_to_opt … n).
379#X #Y #F #m #n #H #x #EQ
380whd in H; cases (H x ?)
381[ #y * #y_spec #x_spec %{y} % [ >y_spec %|assumption]
382| cases m in EQ; normalize #x #EQ destruct %
383]
384qed.
385
[3050]386lemma res_to_opt_gen_preserve : ∀X,Y,R,m,n.
387gen_res_preserve X Y R m n → gen_opt_preserve X Y R (res_to_opt … m) (res_to_opt … n).
388#X #Y #R #m #n #H #x #EQ whd in H; cases(H x ?)
389[ #y * #y_spec #Rxy %{y} >y_spec %{(refl …)} assumption
390| cases m in EQ; normalize #x #EQ destruct %
391]
392qed.
393
[2570]394lemma opt_to_res_preserve : ∀X,Y,P,F,m,n,e1,e2.
395       opt_preserve X Y P F m n →
396       res_preserve X Y P F (opt_to_res … e1 m) (opt_to_res … e2 n).
397#X #Y #P #F #m #n #e1 #e2 #H #v #prf
398cases (H … (opt_eq_from_res ???? prf)) #prf' #EQ %{prf'}
399>EQ %
400qed.
401
[2590]402lemma opt_to_res_preserve1 :  ∀X,Y,F,m,n,e1,e2.
403       opt_preserve1 X Y F m n →
404       res_preserve1 X Y F (opt_to_res … e1 m) (opt_to_res … e2 n).
405#X #Y #F #m #n #e1 #e2 #H #x #EQ
406cases(H x ?)
407[ #y * #y_spec #x_spec %{y} % [>y_spec %|assumption]
408| cases m in EQ; normalize [2: #x1] #EQ destruct %
409]
410qed.
411
[3050]412lemma opt_to_res_gen_preserve :  ∀X,Y,R,m,n,e1,e2.
413gen_opt_preserve X Y R m n →
414gen_res_preserve X Y R (opt_to_res … e1 m) (opt_to_res … e2 n).
415#X #Y #R #m #n #e1 #e2 #H #x #EQ whd in H; cases(H x ?)
416[ #y * #y_spec #Rxy %{y} >y_spec %{(refl …)} assumption
417| cases m in EQ; normalize [2: #x] #EQ destruct %
418]
419qed.
420
[2570]421lemma err_eq_from_io : ∀O,I,X,m,v.
422  err_to_io O I X m = return v → m = return v.
423#O #I #X * #x #v normalize #EQ destruct % qed.
424
425lemma res_to_io_preserve : ∀O,I,X,Y,P,F,m,n.
426       res_preserve X Y P F m n →
427       io_preserve O I X Y P F m n.
428#O #I #X #Y #P #F #m #n #H #v #prf
429cases (H … (err_eq_from_io ????? prf)) #prf' #EQ %{prf'}
430>EQ %
431qed.
432
[2590]433lemma res_to_io_preserve1 : ∀O,I,X,Y,F,m,n.
434       res_preserve1 X Y F m n →
435       io_preserve1 O I X Y F m n.
436#O #I #X #Y #F #m #n #H #v #EQ cases(H v (err_eq_from_io ????? EQ))
437#y * #y_spec #v_spec %{y} % // >y_spec %
[2783]438qed.
439
440lemma res_preserve_error11 : ∀X,Y,F,e,n. (∃e'.n = Error … e') →
441res_preserve1 X Y F n (Error … e).
442#X #Y #F #e #n * #e' #n_spec >n_spec @res_preserve_error1
443qed.
Note: See TracBrowser for help on using the repository browser.