source: src/common/IOMonad.ma @ 1882

Last change on this file since 1882 was 1882, checked in by tranquil, 8 years ago

big update, alas incomplete:
joint changed a bit, and all BE languages need to be updated
started development of blocks to aid preservation results, but still incomplete
if it breaks too many things, feel free to roll back

File size: 7.7 KB
Line 
1include "utilities/extralib.ma".
2include "common/Errors.ma".
3
4(* IO monad *)
5
6inductive IO (output:Type[0]) (input:output → Type[0]) (T:Type[0]) : Type[0] ≝
7| Interact : ∀o:output. (input o → IO output input T) → IO output input T
8| Value : T → IO output input T
9| Wrong : errmsg → IO output input T.
10
11include "utilities/proper.ma".
12(* a weak form of extensionality *)
13axiom interact_proper :
14  ∀O,I,T,o.∀f,g : I o → IO O I T.(∀i. f i = g i) → Interact … o f = Interact … o g.
15
16let rec bindIO (O:Type[0]) (I:O → Type[0]) (T,T':Type[0]) (v:IO O I T) (f:T → IO O I T') on v : IO O I T' ≝
17match v with
18[ Interact out k ⇒ (Interact ??? out (λres. bindIO O I T T' (k res) f))
19| Value v' ⇒ (f v')
20| Wrong m ⇒ Wrong O I T' m
21].
22
23include "utilities/monad.ma".
24
25definition IOMonad ≝ λO,I.
26  MakeMonadProps
27  (* the monad *)
28  (IO O I)
29  (* return *)
30  (λX.Value … X)
31  (* bind *)
32  (bindIO O I)
33  ????. / by /
34[(* bind_ret *)
35 #X#m elim m normalize // #o#f#Hi @interact_proper //
36|(* bind_bind *)
37 #X#Y#Z#m#f#g elim m normalize [2,3://]
38 (* Interact *)
39  #o#f #Hi @interact_proper //
40|#X #Y #m #f #g #H elim m normalize
41  [ #o #x @interact_proper ] //
42]
43qed.
44
45definition bindIO2 ≝ λO,I. m_bind2 (IOMonad O I).
46
47include "hints_declaration.ma".
48
49unification hint 0 ≔ O, I, T;
50  N ≟ IOMonad O I, M ≟ max_def N
51(*******************************************) ⊢
52  IO O I T ≡ monad M T
53.
54
55
56definition err_to_io : ∀O,I,T. res T → IO O I T ≝
57λO,I,T,v. match v with [ OK v' ⇒ Value O I T v' | Error m ⇒ Wrong O I T m ].
58
59coercion err_to_io : ∀O,I,A.∀c:res A.IO O I A ≝ err_to_io on _c:res ? to IO ???.
60
61definition err_to_io_sig : ∀O,I,T.∀P:T → Prop. res (Sig T P) → IO O I (Sig T P) ≝
62λO,I,T,P,v. match v with [ OK v' ⇒ Value O I (Sig T P) v' | Error m ⇒ Wrong O I (Sig T P) m ].
63(*coercion err_to_io_sig : ∀O,I,A.∀P:A → Prop.∀c:res (Sig A P).IO O I (Sig A P) ≝ err_to_io_sig on _c:res (Sig ??) to IO ?? (Sig ??).*)
64
65let rec P_io O I (A:Type[0]) (P:A → Prop) (v:IO O I A) on v : Prop ≝
66match v return λ_.Prop with
67[ Wrong _ ⇒ True
68| Value z ⇒ P z
69| Interact out k ⇒ ∀v'.P_io O I A P (k v')
70].
71
72let rec P_io' O I (A:Type[0]) (P:A → Prop) (v:IO O I A) on v : Prop ≝
73match v return λ_.Prop with
74[ Wrong _ ⇒ False
75| Value z ⇒ P z
76| Interact out k ⇒ ∀v'.P_io' O I A P (k v')
77].
78
79definition P_to_P_option_io : ∀O,I,A.∀P:A → Prop.option (IO O I A) → Prop ≝
80  λO,I,A,P,a.match a with
81   [ None ⇒ False
82   | Some y ⇒ P_io O I A P y
83   ].
84
85let rec io_inject_0 O I (A:Type[0]) (P:A → Prop) (a:IO O I A) (p:P_io O I A P a) on a : IO O I (Sig A P) ≝
86(match a return λa'.P_io O I A P a' → ? with
87 [ Wrong m ⇒ λ_. Wrong O I ? m
88 | Value c ⇒ λp'. Value ??? (mk_Sig A P c p')
89 | Interact out k ⇒ λp'. Interact ??? out (λv. io_inject_0 O I A P (k v) (p' v))
90 ]) p.
91
92definition io_inject : ∀O,I,A.∀P:A → Prop.∀a:option (IO O I A).∀p:P_to_P_option_io O I A P a.IO O I (Sig A P) ≝
93  λO,I,A.λP:A → Prop.λa:option (IO O I A).λp:P_to_P_option_io O I A P a.
94  (match a return λa'.P_to_P_option_io O I A P a' → IO O I (Sig A P) with
95   [ None ⇒ λp'.?
96   | Some b ⇒ λp'. io_inject_0 O I A P b p'
97   ]) p.
98elim p'; qed.
99
100let rec io_eject O I (A:Type[0]) (P: A → Prop) (a:IO O I (Sig A P)) on a : IO O I A ≝
101match a with
102[ Wrong m ⇒ Wrong ??? m
103| Value b ⇒ match b with [ mk_Sig w p ⇒ Value ??? w]
104| Interact out k ⇒ Interact ??? out (λv. io_eject ?? A P (k v))
105].
106
107coercion io_inject :
108  ∀O,I,A.∀P:A → Prop.∀a.∀p:P_to_P_option_io O I ? P a.IO O I (Sig A P) ≝ io_inject
109  on a:option (IO ???) to IO ?? (Sig ? ?).
110coercion io_eject : ∀O,I,A.∀P:A → Prop.∀c:IO O I (Sig A P).IO O I A ≝ io_eject
111  on _c:IO ?? (Sig ? ?) to IO ???.
112
113definition opt_to_io : ∀O,I,T.errmsg → option T → IO O I T ≝
114λO,I,T,m,v. match v with [ None ⇒ Wrong ?? T m | Some v' ⇒ Value ??? v' ].
115
116lemma sig_bindIO_OK: ∀O,I,A,B. ∀P:A → Prop. ∀P':B → Prop. ∀e:IO O I (Sig A P). ∀f:Sig A P → IO O I B.
117  (∀v:A. ∀p:P v. P_io O I ? P' (f (mk_Sig A P v p))) →
118  P_io O I ? P' (bindIO O I (Sig A P) B e f).
119#O #I #A #B #P #P' #e #f elim e;
120[ #out #k #IH #IH' whd; #res @IH //;
121| #v0 elim v0; #v #Hv #IH whd; @IH
122| //;
123] qed.
124
125lemma sig_bindIO2_OK: ∀O,I,A,B,C. ∀P:(A×B) → Prop. ∀P':C → Prop. ∀e:IO O I (Sig (A×B) P). ∀f: A → B → IO O I C.
126  (∀vA:A.∀vB:B. ∀p:P 〈vA,vB〉. P_io O I ? P' (f vA vB)) →
127  P_io O I ? P' (bindIO2 O I A B C e f).
128#I #O #A #B #C #P #P' #e #f elim e;
129[ #out #k #IH #IH' whd; #res @IH @IH'
130| #v0 elim v0; #v elim v; #vA #vB #Hv #IH @IH //;
131| //;
132] qed.
133
134lemma opt_bindIO_OK: ∀O,I,A,B,m. ∀P:B → Prop. ∀e:option A. ∀f: A → IO O I B.
135  (∀v:A. e = Some A v → P_io O I ? P (f v)) →
136  P_io O I ? P (bindIO O I A B (opt_to_io ??? m e) f).
137#I #O #A #B #m #P #e elim e; //; #v #f #H @H //;
138qed.
139
140lemma opt_bindIO2_OK: ∀O,I,A,B,C,m. ∀P:C → Prop. ∀e:option (A×B). ∀f: A → B → IO O I C.
141  (∀vA:A.∀vB:B. e = Some (A×B) 〈vA,vB〉 → P_io O I ? P (f vA vB)) →
142  P_io O I ? P (bindIO2 O I A B C (opt_to_io ??? m e) f).
143#I #O #A #B #C #m #P #e elim e; //; #v cases v; #vA #vB #f #H @H //;
144qed.
145
146lemma res_bindIO_OK: ∀O,I,A,B. ∀P:B → Prop. ∀e:res A. ∀f: A → IO O I B.
147  (∀v:A. e = OK A v → P_io O I ? P (f v)) →
148  P_io O I ? P (bindIO O I A B e f).
149#I #O #A #B #P #e elim e; //; #v #f #H @H //;
150qed.
151
152lemma res_bindIO2_OK: ∀O,I,A,B,C. ∀P:C → Prop. ∀e:res (A×B). ∀f: A → B → IO O I C.
153  (∀vA:A.∀vB:B. e = OK (A×B) 〈vA,vB〉 → P_io O I ? P (f vA vB)) →
154  P_io O I ? P (bindIO2 O I A B C e f).
155#I #O #A #B #C #P #e elim e; //; #v cases v; #vA #vB #f #H @H //;
156qed.
157
158lemma bindIO_OK: ∀O,I,A,B. ∀P:B → Prop. ∀e:IO O I A. ∀f: A → IO O I B.
159  (∀v:A. P_io O I ? P (f v)) →
160  P_io O I ? P (bindIO O I A B e f).
161#I #O #A #B #P #e elim e;
162[ #out #k #IH #f #H whd; #res @IH //;
163| #v #f #H @H
164| //;
165] qed.
166
167lemma bindIO2_OK: ∀O,I,A,B,C. ∀P:C → Prop. ∀e:IO O I (A×B). ∀f: A → B → IO O I C.
168  (∀v1:A.∀v2:B. P_io O I ? P (f v1 v2)) →
169  P_io O I ? P (bindIO2 O I A B C e f).
170#I #O #A #B #C #P #e elim e;
171[ #out #k #IH #f #H whd; #res @IH //;
172| #v cases v; #v1 #v2 #f #H @H
173| //;
174] qed.
175
176lemma P_bindIO_OK: ∀O,I,A,B. ∀P':A → Prop. ∀P:B → Prop. ∀e:IO O I A. ∀f: A → IO O I B.
177  P_io … P' e →
178  (∀v:A. P' v → P_io O I ? P (f v)) →
179  P_io O I ? P (bindIO O I A B e f).
180#I #O #A #B #P' #P #e elim e;
181[ #out #k #IH #f #He #H whd in He ⊢ %; #res @IH /2 by /;
182| #v #f #He #H @H @He
183| //;
184] qed.
185
186lemma P_bindIO2_OK: ∀O,I,A,B,C. ∀P':A×B → Prop. ∀P:C → Prop. ∀e:IO O I (A×B). ∀f: A → B → IO O I C.
187  P_io … P' e →
188  (∀v1:A.∀v2:B. P' 〈v1,v2〉 → P_io O I ? P (f v1 v2)) →
189  P_io O I ? P (bindIO2 O I A B C e f).
190#I #O #A #B #C #P' #P #e elim e;
191[ #out #k #IH #f #He #H whd in He ⊢ %; #res @IH /2 by /;
192| #v cases v; #v1 #v2 #f #He #H @H @He
193| //;
194] qed.
195
196
197(* Is there a way to prove this without extensionality? *)
198(*
199lemma bind_assoc_r: ∀O,I,A,B,C,e,f,g.
200  ∀ext:(∀T1,T2:Type[0].∀f,f':T1 → T2.(∀x.f x = f' x) → f = f').
201  bindIO O I B C (bindIO O I A B e f) g = bindIO O I A C e (λx.bindIO O I B C (f x) g).
202#O #I #A #B #C #e #f #g #ext elim e;
203[ #o #k #IH whd in ⊢ (??%%); @eq_f
204    @ext @IH
205| #v @refl
206| #m @refl
207] qed.
208*)
209definition bind_assoc_r ≝ λO,I.m_bind_bind (IOMonad O I).
210
211(*
212lemma extract_subset_pair_io: ∀O,I,A,B,C,P. ∀e:{e:A×B | P e}. ∀Q:A→B→IO O I C. ∀R:C→Prop.
213  (∀a,b. eject ?? e = 〈a,b〉 → P 〈a,b〉 → P_io O I ? R (Q a b)) →
214  P_io O I ? R (match eject ?? e with [ pair a b ⇒ Q a b ]).
215#I #O #A #B #C #P #e #Q #R cases e; #e' cases e'; normalize;
216[ *;
217| #e'' cases e''; #a #b #Pab #H normalize; /2 by _/;
218] qed.
219*)
Note: See TracBrowser for help on using the repository browser.