source: src/common/ExtraMonads.ma @ 2570

Last change on this file since 2570 was 2570, checked in by piccolo, 8 years ago

ERTLtoERTLptr in place

File size: 6.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
66definition res_preserve : MonadFunctRel Res Res ≝
67  mk_MonadFunctRel ??
68  (λX,Y,P,F,m,n.∀x.m = return x → ∃prf.n = return F x prf)
69  ???.
70[ #X #Y #P #F #x #prf #x' whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} %
71| #X #Y #Z #W #P #Q #F #G *
72  [ #u | #e ] #n #H #f #g #K #x
73  whd in ⊢ (??%%→?); #EQ destruct(EQ)
74  cases (H ? (refl …)) #prf #L >L @(K ? prf ? EQ)
75| #X #Y #P #F #G #H #u #v #K #x #EQ
76  cases (K … EQ) #prf #EQ' %{prf} >EQ' >H try %
77]
78qed.
79
80definition opt_preserve : MonadFunctRel Option Option ≝
81  mk_MonadFunctRel ??
82  (λX,Y,P,F,m,n.∀x.m = return x → ∃prf.n = return F x prf)
83  ???.
84[ #X #Y #P #F #x #prf #x' whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} %
85| #X #Y #Z #W #P #Q #F #G *
86  [ | #u ] #n #H #f #g #K #x
87  whd in ⊢ (??%%→?); #EQ destruct(EQ)
88  cases (H ? (refl …)) #prf #L >L @(K ? prf ? EQ)
89| #X #Y #P #F #G #H #u #v #K #x #EQ
90  cases (K … EQ) #prf #EQ' %{prf} >EQ' >H try %
91]
92qed.
93
94definition io_preserve : ∀O,I.MonadFunctRel (IOMonad O I) (IOMonad O I) ≝
95  λO,I.mk_MonadFunctRel ??
96  (λX,Y,P,F,m,n.∀x.m = return x → ∃prf.n = return F x prf)
97  ???.
98[ #X #Y #P #F #x #prf #x' whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} %
99| #X #Y #Z #W #P #Q #F #G *
100  [ #o #f | #u | #e ] #n #H #f #g #K #x
101  whd in ⊢ (??%%→?); #EQ destruct(EQ)
102  cases (H ? (refl …)) #prf #L >L @(K ? prf ? EQ)
103| #X #Y #P #F #G #H #u #v #K #x #EQ
104  cases (K … EQ) #prf #EQ' %{prf} >EQ' >H try %
105]
106qed.
107
108definition preserving ≝
109  λM1,M2.λFR : MonadFunctRel M1 M2.
110  λX,Y,A,B : Type[0].
111  λP : X → Prop.
112  λQ : A → Prop.
113  λF : ∀x : X.P x → Y.
114  λG : ∀a : A.Q a → B.
115  λf : X → M1 A.
116  λg : Y → M2 B.
117  ∀x,prf.
118  FR … G
119    (f x) (g (F x prf)).
120
121definition preserving2 ≝
122  λM1,M2.λFR : MonadFunctRel M1 M2.
123  λX,Y,Z,W,A,B : Type[0].
124  λP : X → Prop.
125  λQ : Y → Prop.
126  λR : A → Prop.
127  λF : ∀x : X.P x → Z.
128  λG : ∀y : Y.Q y → W.
129  λH : ∀a : A.R a → B.
130  λf : X → Y → M1 A.
131  λg : Z → W → M2 B.
132  ∀x,y,prf1,prf2.
133  FR … H
134    (f x y) (g (F x prf1) (G y prf2)).
135
136lemma res_preserve_error : ∀X,Y,P,F,e,n.res_preserve X Y P F (Error … e) n.
137#X #Y #P #F #e #n #x whd in ⊢ (??%%→?); #EQ destruct(EQ) qed.
138
139lemma mfr_return_eq : ∀M1,M2.∀FR : MonadFunctRel M1 M2.
140∀X,Y,P,F,v,n.
141∀prf.n = return F v prf →
142FR X Y P F (return v) n.
143#M1 #M2 #FR #X #Y #P #F #v #n #prf #EQ >EQ @mfr_return qed.
144
145lemma opt_safe_eq : ∀A,m,x,prf.m = Some A x → opt_safe A m prf = x.
146#A #m #x #prf @opt_safe_elim #x' #EQ >EQ #EQ' destruct % qed.
147
148lemma opt_preserve_none : ∀X,Y,P,F,n.opt_preserve X Y P F (None ?) n.
149#X #Y #P #F #n #x whd in ⊢ (??%%→?); #EQ destruct(EQ) qed.
150
151lemma m_list_map_All_ok :
152  ∀M : MonadProps.∀X,Y,f,l.
153  All X (λx.∃y.f x = return y) l → ∃l'.m_list_map M X Y f l = return l'.
154  #M #X #Y #f #l elim l -l
155  [ * %{[ ]} %
156  | #hd #tl #IH * * #y #EQ #H cases (IH H) #ys #EQ'
157    %{(y :: ys)}
158    change with (! y ← ? ;  ? = ?)
159    >EQ >m_return_bind
160    change with (! acc ← m_list_map ????? ; ? = ?) >EQ'
161    @m_return_bind
162qed.
163
164lemma res_eq_from_opt : ∀A,m,a.
165res_to_opt A m = return a → m = return a.
166#A #m #a  cases m #x normalize #EQ destruct(EQ) %
167qed.
168
169lemma res_to_opt_preserve : ∀X,Y,P,F,m,n.
170  res_preserve X Y P F m n → opt_preserve X Y P F (res_to_opt … m) (res_to_opt … n).
171#X #Y #P #F #m #n #H #x #EQ
172cases (H x ?)
173[ #prf #EQ' %{prf} >EQ' %
174| cases m in EQ; normalize #x #EQ destruct %
175]
176qed.
177
178lemma opt_to_res_preserve : ∀X,Y,P,F,m,n,e1,e2.
179       opt_preserve X Y P F m n →
180       res_preserve X Y P F (opt_to_res … e1 m) (opt_to_res … e2 n).
181#X #Y #P #F #m #n #e1 #e2 #H #v #prf
182cases (H … (opt_eq_from_res ???? prf)) #prf' #EQ %{prf'}
183>EQ %
184qed.
185
186lemma err_eq_from_io : ∀O,I,X,m,v.
187  err_to_io O I X m = return v → m = return v.
188#O #I #X * #x #v normalize #EQ destruct % qed.
189
190lemma res_to_io_preserve : ∀O,I,X,Y,P,F,m,n.
191       res_preserve X Y P F m n →
192       io_preserve O I X Y P F m n.
193#O #I #X #Y #P #F #m #n #H #v #prf
194cases (H … (err_eq_from_io ????? prf)) #prf' #EQ %{prf'}
195>EQ %
196qed.
197
Note: See TracBrowser for help on using the repository browser.