Changeset 1882 for src/utilities/bindLists.ma
 Timestamp:
 Apr 6, 2012, 8:02:10 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/bindLists.ma
r1647 r1882 1 include "utilities/monad.ma". 2 include "basics/lists/list.ma". 1 include "utilities/bind_new.ma". 3 2 4 inductive 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 13 interpretation "new blist" 'new t f = (bnew ??? t f). 14 interpretation "cons blist" 'cons hd tl = (bcons ??? hd tl). 15 interpretation "nil blist" 'nil = (bnil ???). 3 definition bind_list ≝ λB,E.bind_new B (list E). 16 4 17 notation > "ν 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 }. 5 coercion blist_from_list : 6 ∀B,E. ∀l:list E. bind_list B E ≝ λB,E,l.bret … l on _l : list ? to bind_list ??. 23 7 24 notation < "hvbox(ν ident i \nbsp 'of' \nbsp t \nbsp 'in' \nbsp break p)" 25 with precedence 48 for 26 @{'new $t (λ${ident i} : $ty. $p) }. 8 unification hint 0 ≔ B,E; 9 Es ≟ list E 10 (**)⊢ 11 bind_list B E ≡ bind_new B Es. 27 12 28 interpretation "unit it" 'it = it. 13 definition bappend : ∀B,E.bind_list B E → bind_list B E → 14 bind_list B E ≝ λB,E. m_bin_op … (append ?). 29 15 30 notation < "hvbox(ν ident i \nbsp 'in' \nbsp break p)" 31 with precedence 48 for 32 @{'new 'it (λ${ident i} : $ty. $p) }. 33 34 let 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 40 let 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 46 let 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 52 let 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 58 interpretation "iterated typed new" 'tnews ts f = (bnews ??? ts f). 59 interpretation "iterated untyped new" 'unews n f = (bnews_n ?? n f). 60 interpretation "iterated typed new strong" 'stnews ts f = (bnews_strong ??? ts f). 61 interpretation "iterated untyped new strong" 'sunews n f = (bnews_n_strong ?? n f). 16 include "ASM/Vector.ma". 17 interpretation "append blist" 'vappend l1 l2 = (bappend ?? l1 l2). 62 18 63 notation > "νν 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 69 notation > "νν ident l : ty 'of' ts opt('with' ident EQ) 'in' f" with precedence 47 for 70 ${default 71 @{ 'stnews $ts (λ${ident l}:$ty.λ${ident EQ}.$f) } 72 @{ 'tnews $ts (λ${ident l}:$ty.$f)} 73 }. 74 75 notation < "hvbox(νν ident l : ty\nbsp 'of' \nbsp ts \nbsp 'with' \nbsp ident EQ : tyeq \nbsp 'in' \nbsp break f)" with precedence 47 for 76 @{ 'stnews $ts (λ${ident l} : $ty.λ${ident EQ} : $tyeq.$f) }. 77 notation < "hvbox(νν ident l : ty\nbsp 'of' \nbsp ts \nbsp 'in' break f)" with precedence 47 for 78 @{ 'tnews $ts (λ${ident l} : $ty.$f) }. 19 definition bcons : ∀B,E.E → bind_list B E → bind_list B E ≝ 20 λB,E,e,l.[e] @@ l. 79 21 80 notation > "νν ident l ^ n opt('with' ident EQ) 'in' f" with precedence 47 for 81 ${default 82 @{ 'sunews $n (λ${ident l}.λ${ident EQ}.$f) } 83 @{ 'unews $n (λ${ident l}.$f)} 84 }. 85 86 notation > "νν ident l : ty ^ n opt('with' ident EQ) 'in' f" with precedence 47 for 87 ${default 88 @{ 'sunews $n (λ${ident l}:$ty.λ${ident EQ}.$f) } 89 @{ 'unews $n (λ${ident l}:$ty.$f)} 90 }. 91 92 notation < "hvbox(νν \nbsp ident l : ty ^ n \nbsp 'with' \nbsp ident EQ : tyeq \nbsp 'in' \nbsp break f)" with precedence 47 for 93 @{ 'sunews $n (λ${ident l} : $ty.λ${ident EQ} : $tyeq.$f) }. 94 notation < "hvbox(νν_ n \nbsp ident l : ty ^ n \nbsp 'in' \nbsp break f)" with precedence 47 for 95 @{ 'unews $n (λ${ident l} : $ty.$f) }. 22 interpretation "cons blist" 'vcons l1 l2 = (bcons ?? l1 l2). 96 23 97 98 axiom bnew_proper : ∀B,T,E. bnew B T E ⊨ eq ? ++> (eq ? ++> eq ?) ++> eq ?. 99 (* the following is equivalent to the above *) 100 theorem bnew_proper' : ∀X,Y,Z.Y (* nonempty *) → 101 ∀f,g : X → bind_list X Y Z. (∀x. f x = g x) → f = g. 102 #X#Y#Z#y#f#g#eqf 103 cut ('new y f = 'new y g) /2 by bnew_proper/ 104 #eq destruct // 105 qed. 106 107 definition blist_of_list : ∀B,T,E. list E → 108 bind_list B T E ≝ 109 λB,T,E,l. 110 let f ≝ λe.λbl. e :: bl in 111 foldr … f [] l. 112 113 114 coercion blist_from_list : 115 ∀B,T,E. ∀l:list E. bind_list B T E ≝ blist_of_list on _l : list ? to bind_list ???. 116 117 let rec bappend A B C (l1 : bind_list A B C) l2 on l1 : bind_list A B C ≝ 118 match l1 with 119 [ bnil ⇒ l2 120  bcons x l1' ⇒ x :: (bappend … l1' l2) 121  bnew t l1' ⇒ νx of t in bappend … (l1' x) l2 122 ]. 123 124 interpretation "append blist" 'append l1 l2 = (bappend ??? l1 l2). 125 126 let rec bbind A B C D (l : bind_list A B C) (f : C → bind_list A B D) on l 127 : bind_list A B D ≝ 128 match l with 129 [ bnil ⇒ bnil … 130  bcons x l1' ⇒ bappend … (f x) (bbind … l1' f) 131  bnew t l1' ⇒ bnew … t (λx. bbind … (l1' x) f) 132 ]. 133 134 interpretation "bind_list bind" 'm_bind m f = (bbind ? ? ? ? m f). 135 136 include "utilities/proper.ma". 137 138 lemma bappend_assoc : ∀A,B,C.∀l1,l2,l3:bind_list A B C. 139 ((l1@l2)@l3) = (l1 @ l2 @ l3). 140 #A#B#C#l1 elim l1 normalize 141 [ 142 (* case bnil *) 143 #l2#l3 // 144  #x#l'#Hi#l2#l3 >Hi // 145  #t#l'#Hi#l2#l3 @bnew_proper // 146 qed. 147 148 lemma bbind_bappend : ∀A,B,C,D.∀l1,l2:bind_list A B C.∀f:C→bind_list A B D. 149 ((l1 @ l2) »= f) = ((l1 »= f) @ (l2 »= f)). 150 #A#B#C#D#l1 elim l1 normalize /2 by bnew_proper/ qed. 151 152 lemma bappend_bnil : ∀A,B,C.∀l : bind_list A B C.( l@[ ]) = l. 153 #A#B#C#l elim l normalize /2 by bnew_proper/ qed. 154 155 definition BindList ≝ 156 λB,T.MakeMonadProps 157 (* the monad *) 158 (λX.bind_list B T X) 159 (* return *) 160 (λE,x.[x]) 161 (* bind *) 162 (bbind B T) 163 ???. 164 [(* ret_bind *) 165 #X#Y#x#f normalize @bappend_bnil 166 (* bind_ret *) 167 #X#m elim m normalize /2 by / 168 #t #l' #Hi @bnew_proper // normalize #s#t#eq destruct @Hi 169 (* bind_bind *) 170 #X#Y#Z#m#f#g elim m normalize 171 [// 172 (* case bcons *) 173 #x #l1' #Hi <Hi @bbind_bappend 174 (* case bnew *) 175 #t #l #Hi @bnew_proper // 176 #x#y #x_eq_y destruct(x_eq_y) @Hi 177 ] 178 ] 179 qed. 180 181 unification hint 0 ≔ B, T, X; 182 N ≟ BindList B T, M ≟ max_def N, O ≟ m_def M 183 (**) ⊢ 184 bind_list B T X ≡ monad O X. 185 186 include "utilities/state.ma". 187 188 let rec bcompile R T E U 189 (fresh : T → state_monad U R) 190 (blist : bind_list R T E) on blist : state_monad U (list E) ≝ 191 match blist with 192 [ bnil ⇒ return [ ] 193  bcons x l ⇒ 194 ! res ← bcompile … fresh l ; 195 return (x :: res) 196  bnew t f ⇒ 197 ! r ← fresh t ; 198 bcompile … fresh (f r) 199 ]. 24 include "utilities/lists.ma". 200 25 201 26 theorem bcompile_append : 202 ∀ E, R, T, U, fresh, bl1, bl2.203 (bcompile E R T U fresh (bl1@ bl2)) ≅27 ∀U, R, E, fresh, bl1, bl2. 28 (bcompile U R (list E) fresh (bl1 @@ bl2)) ≅ 204 29 ( 205 30 ! l1 ← bcompile … fresh bl1 ; … … 207 32 return (l1 @ l2) 208 33 ). 209 #E#R#T#U#fresh#bl1#bl2 210 elim bl1 normalize 211 [ 212 #u @pair_elim // 213  214 #x#bl1' #Hi #u0 >Hi Hi 215 elim (bcompile E R T U fresh bl1' u0) #u1 #l1 216 normalize 217 elim (bcompile E R T U fresh bl2 u1) #u2 #l2 218 normalize // 219  220 #t #blf #Hi #u0 221 @pair_elim normalize #u #r 222 >(Hi r) Hi // 34 #U#R#E#fresh#bl1#bl2 35 #u >bcompile_bbind normalize @pair_elim 36 #u' #l' normalize @pair_elim 37 #u'' #l'' normalize >bcompile_bbind #EQ #EQ' 38 normalize >EQ normalize // 223 39 qed. 40 41 theorem bcompile_cons : 42 ∀U, R, E, fresh, e, bl2. 43 (bcompile U R (list E) fresh (e ::: bl2)) ≅ 44 ! l ← bcompile … fresh bl2 ; return (e :: l). 45 #U#R#E#fresh#e#bl2 #u 46 >bcompile_append normalize // 47 qed.
Note: See TracChangeset
for help on using the changeset viewer.