source: src/utilities/bindLists.ma @ 1635

Last change on this file since 1635 was 1635, checked in by tranquil, 8 years ago
  • lists with binders and monads
  • Joint.ma and other temprarily forked, awaiting feedback from Claudio
  • translation of RTLabs → RTL refactored with new tools
File size: 6.3 KB
Line 
1include "utilities/monad.ma".
2include "basics/lists/list.ma".
3
4inductive bind_list
5  (B : Type[0])
6  (T : Type[0])
7  (E : Type[0])
8  : Type[0] ≝
9  | bnil : bind_list B T E
10  | bcons : E → bind_list B T E → bind_list B T E
11  | bnew : T → (B → bind_list B T E) → bind_list B T E.
12 
13interpretation "new blist" 'new t f = (bnew ??? t f).
14interpretation "cons blist" 'cons hd tl = (bcons ??? hd tl).
15interpretation "nil blist" 'nil = (bnil ???).
16
17notation > "ν list1 ident x sep , opt('of' t) 'in' f"
18  with precedence 48 for
19  ${ default
20    @{ ${ fold right @{$f} rec acc @{'new $t (λ${ident x}.$acc)} } }
21    @{ ${ fold right @{$f} rec acc @{'new 'it (λ${ident x}.$acc)} } }
22  }.
23
24notation < "hvbox(ν ident i \nbsp 'of' \nbsp t \nbsp 'in' \nbsp break p)"
25 with precedence 48 for
26  @{'new $t (λ${ident i} : $ty. $p) }.
27
28interpretation "unit it" 'it = it.
29
30notation < "hvbox(ν ident i \nbsp 'in' \nbsp break p)"
31 with precedence 48 for
32    @{'new 'it (λ${ident i} : $ty. $p) }.
33   
34let rec bnews B T E (tys : list T) (f : list B → bind_list B T E) on tys : bind_list B T E ≝
35  match tys with
36  [ nil ⇒ f [ ]
37  | cons ty tys ⇒ νx of ty in bnews … tys (λl. f (x :: l))
38  ].
39 
40let rec bnews_strong B T E (tys : list T) (f : ∀l : list B.|l| = |tys| → bind_list B T E) on tys : bind_list B T E ≝
41  match tys return λx.x = tys → bind_list B T E with
42  [ nil ⇒ λprf.f [ ] ?
43  | cons ty tys' ⇒ λprf.νx of ty in bnews_strong … tys' (λl',prf'. f (x :: l') ?)
44  ] (refl …). destruct normalize // qed.
45 
46let rec bnews_n B E n (f : list B → bind_list B unit E) on n : bind_list B unit E ≝
47  match n with
48  [ O ⇒ f [ ]
49  | S n ⇒ νx in bnews_n … n (λl. f (x :: l))
50  ].
51 
52let rec bnews_n_strong B E n (f : ∀l:list B.|l| = n → bind_list B unit E) on n : bind_list B unit E ≝
53  match n return λx.x = n → bind_list B unit E with
54  [ O ⇒ λprf.f [ ] ?
55  | S n' ⇒ λprf.νx in bnews_n_strong … n' (λl',prf'. f (x :: l') ?)
56  ] (refl …). normalize // qed.
57 
58interpretation "iterated typed new" 'tnews ts f = (bnews ??? ts f).
59interpretation "iterated untyped new" 'unews n f = (bnews_n ?? n f).
60interpretation "iterated typed new strong" 'stnews ts f = (bnews_strong ??? ts f).
61interpretation "iterated untyped new strong" 'sunews n f = (bnews_n_strong ?? n f).
62
63notation > "νν ident l 'of' ts opt('with' ident EQ) 'in' f" with precedence 47 for
64 ${default
65   @{ 'stnews $ts (λ${ident l}.λ${ident EQ}.$f) }
66   @{ 'tnews $ts (λ${ident l}.$f)}
67 }.
68 
69notation < "hvbox(νν ident l \nbsp 'of' \nbsp ts \nbsp 'with' \nbsp ident EQ : tyeq \nbsp 'in' \nbsp break f)" with precedence 47 for
70   @{ 'stnews $ts (λ${ident l} : $ty.λ${ident EQ} : $tyeq.$f) }.
71notation < "hvbox(νν ident l \nbsp 'of' \nbsp ts \nbsp 'in'  break f)" with precedence 47 for
72   @{ 'tnews $ts (λ${ident l} : $ty.$f) }.
73
74notation > "νν ident l : n opt('with' ident EQ) 'in' f" with precedence 47 for
75 ${default
76   @{ 'sunews $n (λ${ident l}.λ${ident EQ}.$f) }
77   @{ 'unews $n (λ${ident l}.$f)}
78 }.
79 
80notation < "hvbox(νν ident l : n \nbsp 'with' \nbsp ident EQ : tyeq \nbsp 'in' \nbsp break f)" with precedence 47 for
81   @{ 'sunews $n (λ${ident l} : $ty.λ${ident EQ} : $tyeq.$f) }.
82notation < "hvbox(νν ident l : n \nbsp 'in' \nbsp break f)" with precedence 47 for
83   @{ 'unews $n (λ${ident l} : $ty.$f) }.
84
85
86axiom bnew_proper : ∀B,T,E. bnew B T E ⊨ eq ? ++> (eq ? ++> eq ?) ++> eq ?.
87(* the following is equivalent to the above *)
88theorem bnew_proper' : ∀X,Y,Z.Y (* non-empty *) →
89  ∀f,g : X → bind_list X Y Z.  (∀x. f x = g x) → f = g.
90#X#Y#Z#y#f#g#eqf
91cut ('new y f = 'new y g) /2 by bnew_proper/
92#eq destruct //
93qed.
94
95definition blist_of_list : ∀B,T,E. list E →
96  bind_list B T E ≝
97  λB,T,E,l.
98  let f ≝ λe.λbl. e :: bl in
99  foldr … f [] l.
100 
101 
102coercion blist_from_list nocomposites :
103  ∀B,T,E. ∀l:list E. bind_list B T E ≝ blist_of_list on _l : list ? to bind_list ???.
104
105let rec bappend A B C (l1 : bind_list A B C) l2 on l1 : bind_list A B C ≝
106match l1 with
107[ bnil ⇒ l2
108| bcons x l1' ⇒ x :: (bappend … l1' l2)
109| bnew t l1' ⇒ νx of t in bappend … (l1' x) l2
110].
111
112interpretation "append blist" 'append l1 l2 = (bappend ??? l1 l2).
113
114let rec bbind A B C D (l : bind_list A B C) (f : C → bind_list A B D) on l
115  : bind_list A B D ≝
116  match l with
117  [ bnil ⇒ bnil …
118  | bcons x l1' ⇒ bappend … (f x) (bbind … l1' f)
119  | bnew t l1' ⇒ bnew … t (λx. bbind … (l1' x) f)
120  ].
121 
122interpretation "bind_list bind" 'm_bind m f = (bbind ? ? ? ? m f).
123
124include "utilities/proper.ma".
125
126lemma bappend_assoc : ∀A,B,C.∀l1,l2,l3:bind_list A B C.
127  ((l1@l2)@l3) = (l1 @ l2 @ l3).
128#A#B#C#l1 elim l1 normalize
129[
130(* case bnil *)
131  #l2#l3 //
132| #x#l'#Hi#l2#l3 >Hi //
133| #t#l'#Hi#l2#l3 @bnew_proper //
134qed.
135
136lemma bbind_bappend : ∀A,B,C,D.∀l1,l2:bind_list A B C.∀f:C→bind_list A B D.
137  ((l1 @ l2) »= f) = ((l1 »= f) @ (l2 »= f)).
138#A#B#C#D#l1 elim l1 normalize /2 by bnew_proper/ qed.
139
140lemma bappend_bnil : ∀A,B,C.∀l : bind_list A B C.( l@[ ]) = l.
141#A#B#C#l elim l normalize /2 by bnew_proper/ qed.
142 
143definition BindList ≝
144  λB,T.MakeMonad (mk_MonadDefinition
145  (* the monad *)
146  (λX.bind_list B T X)
147  (* return *)
148  (λE,x.[x])
149  (* bind *)
150  (bbind B T)
151  ???).
152[(* bind_bind *)
153 #X#Y#Z#m#f#g elim m normalize
154 [//
155 |(* case bcons *)
156  #x #l1' #Hi <Hi @bbind_bappend
157 |(* case bnew *)
158  #t #l #Hi @bnew_proper //
159 ]
160|(* bind_ret *)
161 #X#m elim m normalize /2 by /
162 #t #l' #Hi @bnew_proper normalize // #s#t#eq destruct @Hi
163|(* ret_bind *)
164  #X#Y#x#f normalize @bappend_bnil
165]
166qed.
167
168include "utilities/state.ma".
169
170let rec bcompile R T E U
171  (fresh : T → state_monad U R)
172  (blist : bind_list R T E) on blist : state_monad U (list E) ≝
173  match blist with
174  [ bnil ⇒ return [ ]
175  | bcons x l ⇒
176    ! res ← bcompile … fresh l ;
177    return (x :: res)
178  | bnew t f ⇒
179    ! r ← fresh t ;
180    bcompile … fresh (f r)
181  ].
182 
183theorem bcompile_append :
184  ∀E, R, T, U, fresh, bl1, bl2.
185  bcompile E R T U fresh (bl1 @ bl2) ≅
186  (
187  ! l1 ← bcompile … fresh bl1 ;
188  ! l2 ← bcompile … fresh bl2 ;
189  return (l1 @ l2)
190  ).
191  #E#R#T#U#fresh#bl1#bl2
192  elim bl1 normalize
193   [
194     #u @pair_elim //
195   |
196    #x#bl1' #Hi #u0 >Hi -Hi
197    elim (bcompile E R T U fresh bl1' u0) #u1 #l1
198    normalize
199    elim (bcompile E R T U fresh bl2 u1) #u2 #l2
200    normalize //
201   |
202    #t #blf #Hi #u0
203    @pair_elim normalize #u #r
204    >(Hi r) -Hi //
205qed.
Note: See TracBrowser for help on using the repository browser.