Ignore:
Timestamp:
Apr 6, 2012, 8:02:10 PM (8 years ago)
Author:
tranquil
Message:

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:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/bindLists.ma

    r1647 r1882  
    1 include "utilities/monad.ma".
    2 include "basics/lists/list.ma".
     1include "utilities/bind_new.ma".
    32
    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 ???).
     3definition bind_list ≝ λB,E.bind_new B (list E).
    164
    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   }.
     5coercion blist_from_list :
     6  ∀B,E. ∀l:list E. bind_list B E ≝ λB,E,l.bret … l on _l : list ? to bind_list ??.
    237
    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) }.
     8unification hint 0 ≔ B,E;
     9Es ≟ list E
     10(*--------------------------*)⊢
     11bind_list B E ≡ bind_new B Es.
    2712
    28 interpretation "unit it" 'it = it.
     13definition bappend : ∀B,E.bind_list B E → bind_list B E →
     14  bind_list B E ≝ λB,E. m_bin_op … (append ?).
    2915
    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).
     16include "ASM/Vector.ma".
     17interpretation "append blist" 'vappend l1 l2 = (bappend ?? l1 l2).
    6218
    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) }.
     19definition bcons : ∀B,E.E → bind_list B E → bind_list B E ≝
     20  λB,E,e,l.[e] @@ l.
    7921
    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) }.
     22interpretation "cons blist" 'vcons l1 l2 = (bcons ?? l1 l2).
    9623
    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 (* non-empty *) →
    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   ].
     24include "utilities/lists.ma".
    20025 
    20126theorem 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)) ≅
    20429  (
    20530  ! l1 ← bcompile … fresh bl1 ;
     
    20732  return (l1 @ l2)
    20833  ).
    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 //
    22339qed.
     40
     41theorem 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 //
     47qed.
Note: See TracChangeset for help on using the changeset viewer.