source: C-semantics/IOMonad.ma @ 189

Last change on this file since 189 was 189, checked in by campbell, 10 years ago

Rework monad notation so that it is displayed well in proof mode.

File size: 6.8 KB
Line 
1include "Plogic/russell_support.ma".
2include "extralib.ma".
3include "Errors.ma".
4
5(* IO monad *)
6
7ninductive IO (input,output:Type) (T:Type) : Type ≝
8| Interact : output → (input → IO input output T) → IO input output T
9| Value : T → IO input output T
10| Wrong : IO input output T.
11
12nlet rec bindIO (I,O,T,T':Type) (v:IO I O T) (f:T → IO I O T') on v : IO I O T' ≝
13match v with
14[ Interact out k ⇒ (Interact ??? out (λres. bindIO I O T T' (k res) f))
15| Value v' ⇒ (f v')
16| Wrong ⇒ Wrong I O T'
17].
18
19nlet rec bindIO2 (I,O,T1,T2,T':Type) (v:IO I O (T1×T2)) (f:T1 → T2 → IO I O T') on v : IO I O T' ≝
20match v with
21[ Interact out k ⇒ (Interact ??? out (λres. bindIO2 ?? T1 T2 T' (k res) f))
22| Value v' ⇒ match v' with [ mk_pair v1 v2 ⇒ f v1 v2 ]
23| Wrong ⇒ Wrong ?? T'
24].
25
26ndefinition err_to_io : ∀I,O,T. res T → IO I O T ≝
27λI,O,T,v. match v with [ OK v' ⇒ Value I O T v' | Error ⇒ Wrong I O T ].
28(*ncoercion err_to_io : ∀I,O,A.∀c:res A.IO I O A ≝ err_to_io on _c:res ? to IO ???.*)
29ndefinition err_to_io_sig : ∀I,O,T.∀P:T → Prop. res (sigma T P) → IO I O (sigma T P) ≝
30λI,O,T,P,v. match v with [ OK v' ⇒ Value I O (sigma T P) v' | Error ⇒ Wrong I O (sigma T P) ].
31ncoercion err_to_io_sig : ∀I,O,A.∀P:A → Prop.∀c:res (sigma A P).IO I O (sigma A P) ≝ err_to_io_sig on _c:res (sigma ??) to IO ?? (sigma ??).
32
33
34(* If the original definitions are vague enough, do I need to do this? *)
35notation > "! ident v ← e;: e'" with precedence 40 for @{'bindIO ${e} (λ${ident v}.${e'})}.
36notation > "! ident v : ty ← e;: e'" with precedence 40 for @{'bindIO ${e} (λ${ident v} : ${ty}.${e'})}.
37notation < "vbox(! \nbsp ident v ← e;: e')" with precedence 40 for @{'bindIO ${e} (λ${ident v}.${e'})}.
38notation < "vbox(! \nbsp ident v : ty ← e;: e')" with precedence 40 for @{'bindIO ${e} (λ${ident v} : ${ty}.${e'})}.
39notation > "! 〈ident v1, ident v2〉 ← e;: e'" with precedence 40 for @{'bindIO2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}.
40notation > "! 〈ident v1 : ty1, ident v2 : ty2〉 ← e;: e'" with precedence 40 for @{'bindIO2 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.${e'})}.
41notation < "vbox(! \nbsp 〈ident v1, ident v2〉 ← e;: e')" with precedence 40 for @{'bindIO2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}.
42notation < "vbox(! \nbsp 〈ident v1 : ty1, ident v2 : ty2〉 ← e;: e')" with precedence 40 for @{'bindIO2 ${e} (λ${ident v1} : ${ty2}.λ${ident v2} : ${ty2}.${e'})}.
43interpretation "IO monad bind" 'bindIO e f = (bindIO ???? e f).
44interpretation "IO monad pair bind" 'bindIO2 e f = (bindIO2 ????? e f).
45(**)
46nlet rec P_io (I,O,A:Type) (P:A → Prop) (v:IO I O A) on v : Prop ≝
47match v return λ_.Prop with
48[ Wrong ⇒ True
49| Value z ⇒ P z
50| Interact out k ⇒ ∀v'.P_io I O A P (k v')
51].
52
53nlet rec P_io' (I,O,A:Type) (P:A → Prop) (v:IO I O A) on v : Prop ≝
54match v return λ_.Prop with
55[ Wrong ⇒ False
56| Value z ⇒ P z
57| Interact out k ⇒ ∀v'.P_io' I O A P (k v')
58].
59
60ndefinition P_to_P_option_io : ∀I,O,A.∀P:A → Prop.option (IO I O A) → Prop ≝
61  λI,O,A,P,a.match a with
62   [ None ⇒ False
63   | Some y ⇒ P_io I O A P y
64   ].
65
66nlet rec io_inject_0 (I,O,A:Type) (P:A → Prop) (a:IO I O A) (p:P_io I O A P a) on a : IO I O (sigma A P) ≝
67(match a return λa'.a=a' → ? with
68 [ Wrong ⇒ λ_. Wrong I O ?
69 | Value c ⇒ λe2. Value ??? (sig_intro A P c ?)
70 | Interact out k ⇒ λe2. Interact ??? out (λv. io_inject_0 I O A P (k v) ?)
71 ]) (refl ? a).
72nrewrite > e2 in p; nwhd in ⊢ (% → ?); //;
73nqed.
74
75ndefinition io_inject : ∀I,O,A.∀P:A → Prop.∀a:option (IO I O A).∀p:P_to_P_option_io I O A P a.IO I O (sigma A P) ≝
76  λI,O,A.λP:A → Prop.λa:option (IO I O A).λp:P_to_P_option_io I O A P a.
77  (match a return λa'.a=a' → IO I O (sigma A P) with
78   [ None ⇒ λe1.?
79   | Some b ⇒ λe1. io_inject_0 I O A P b ?
80   ]) (refl ? a).
81##[ nrewrite > e1 in p; nnormalize; *;
82##| nrewrite > e1 in p; nnormalize; //
83##] nqed.
84
85nlet rec io_eject (I,O,A:Type) (P: A → Prop) (a:IO I O (sigma A P)) on a : IO I O A ≝
86match a with
87[ Wrong ⇒ Wrong ???
88| Value b ⇒ match b with [ sig_intro w p ⇒ Value ??? w]
89| Interact out k ⇒ Interact ??? out (λv. io_eject ?? A P (k v))
90].
91
92ncoercion io_inject :
93  ∀I,O,A.∀P:A → Prop.∀a.∀p:P_to_P_option_io I O ? P a.IO I O (sigma A P) ≝ io_inject
94  on a:option (IO ???) to IO ?? (sigma ? ?).
95ncoercion io_eject : ∀I,O,A.∀P:A → Prop.∀c:IO I O (sigma A P).IO I O A ≝ io_eject
96  on _c:IO ?? (sigma ? ?) to IO ???.
97
98ndefinition opt_to_io : ∀I,O,T.option T → IO I O T ≝
99λI,O,T,v. match v with [ None ⇒ Wrong I O T | Some v' ⇒ Value I O T v' ].
100ncoercion opt_to_io : ∀I,O,T.∀v:option T. IO I O T ≝ opt_to_io on _v:option ? to IO ???.
101
102nlemma sig_bindIO_OK: ∀I,O,A,B. ∀P:A → Prop. ∀P':B → Prop. ∀e:IO I O (sigma A P). ∀f:sigma A P → IO I O B.
103  (∀v:A. ∀p:P v. P_io I O ? P' (f (sig_intro A P v p))) →
104  P_io I O ? P' (bindIO I O (sigma A P) B e f).
105#I O A B P P' e f; nelim e;
106##[ #out k IH; #IH'; nwhd; #res; napply IH; //;
107##| #v0; nelim v0; #v Hv IH; nwhd; napply IH;
108##| //;
109##] nqed.
110
111nlemma sig_bindIO2_OK: ∀I,O,A,B,C. ∀P:(A×B) → Prop. ∀P':C → Prop. ∀e:IO I O (sigma (A×B) P). ∀f: A → B → IO I O C.
112  (∀vA:A.∀vB:B. ∀p:P 〈vA,vB〉. P_io I O ? P' (f vA vB)) →
113  P_io I O ? P' (bindIO2 I O A B C e f).
114#I O A B C P P' e f; nelim e;
115##[ #out k IH; #IH'; nwhd; #res; napply IH; napply IH';
116##| #v0; nelim v0; #v; nelim v; #vA vB Hv IH; napply IH; //;
117##| //;
118##] nqed.
119
120nlemma opt_bindIO_OK: ∀I,O,A,B. ∀P:B → Prop. ∀e:option A. ∀f: A → IO I O B.
121  (∀v:A. e = Some A v → P_io I O ? P (f v)) →
122  P_io I O ? P (bindIO I O A B e f).
123#I O A B P e; nelim e; //; #v f H; napply H; //;
124nqed.
125
126nlemma opt_bindIO2_OK: ∀I,O,A,B,C. ∀P:C → Prop. ∀e:option (A×B). ∀f: A → B → IO I O C.
127  (∀vA:A.∀vB:B. e = Some (A×B) 〈vA,vB〉 → P_io I O ? P (f vA vB)) →
128  P_io I O ? P (bindIO2 I O A B C e f).
129#I O A B C P e; nelim e; //; #v; ncases v; #vA vB f H; napply H; //;
130nqed.
131
132nlemma bindIO_OK: ∀I,O,A,B. ∀P:B → Prop. ∀e:IO I O A. ∀f: A → IO I O B.
133  (∀v:A. P_io I O ? P (f v)) →
134  P_io I O ? P (bindIO I O A B e f).
135#I O A B P e; nelim e;
136##[ #out k IH; #f H; nwhd; #res; napply IH; //;
137##| #v f H; napply H;
138##| //;
139##] nqed.
140
141(* TODO: is there a way to prove this without extensionality?
142
143nlemma bind_assoc_r: ∀A,B,C,e,f,g.
144  bindIO B C (bindIO A B e f) g = bindIO A C e (λx.bindIO B C (f x) g).
145#A B C e f g; nelim e;
146##[ #fn args k IH; nwhd in ⊢ (???%);
147nnormalize;
148*)
149
150nlemma extract_subset_pair_io: ∀I,O,A,B,C,P. ∀e:{e:A×B | P e}. ∀Q:A→B→IO I O C. ∀R:C→Prop.
151  (∀a,b. eject ?? e = 〈a,b〉 → P 〈a,b〉 → P_io I O ? R (Q a b)) →
152  P_io I O ? R (match eject ?? e with [ mk_pair a b ⇒ Q a b ]).
153#I O A B C P e Q R; ncases e; #e'; ncases e'; nnormalize;
154##[ *;
155##| #e''; ncases e''; #a b Pab H; nnormalize; /2/;
156##] nqed.
157
Note: See TracBrowser for help on using the repository browser.