source: src/common/ExtraMonads.ma @ 3367

Last change on this file since 3367 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
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
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}.
86
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
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)
104????.
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 % //
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 % //
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
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
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
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)
155????.
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 % //
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 % //
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
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
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
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)
207????.
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 % //
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 % //
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
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
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
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).
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).
273
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)).
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   
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
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
313lemma res_preserve_error1 : ∀X,Y,F,e,n.res_preserve1 X Y F (Error … e) n.
314#X #Y #F #e #n #x whd in ⊢ (??%%→?); #EQ destruct(EQ) qed.
315
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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 %
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.