Changeset 1882 for src/utilities


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

Location:
src/utilities
Files:
7 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.
  • src/utilities/extralib.ma

    r1599 r1882  
    5353
    5454(* should be proved in nat.ma, but it's not! *)
     55(* Paolo: there is eqb_elim which does something very similar *)
    5556lemma eqb_to_Prop : ∀n,m:nat.match eqb n m with [ true ⇒ n = m | false ⇒ n ≠ m ].
    5657#n elim n;
     
    135136 ]
    136137qed.
     138
     139lemma associative_orb : associative ? orb.
     140*** // qed.
     141
     142lemma commutative_orb : commutative ? orb.
     143** // qed.
     144
     145lemma associative_andb : associative ? andb.
     146*** // qed.
     147
     148lemma commutative_andb : commutative ? andb.
     149** // qed.
     150
     151
     152lemma notb_false : ∀b.(¬b) = false → b = true.
     153* [#_ % | normalize #EQ destruct]
     154qed.
     155
     156lemma notb_true : ∀b.(¬b) = true → b = false.
     157* [normalize #EQ destruct | #_ %]
     158qed.
     159
     160
     161
     162notation > "Σ 〈 ident x : tyx, ident y : tyy 〉 . P" with precedence 20 for
     163  @{'sigma (λ${fresh p}.
     164    match ${fresh p} with [mk_Prod (${ident x} : $tyx) (${ident y} : $tyy) ⇒ $P])}.
     165notation > "Σ 〈 ident x, ident y 〉 . P" with precedence 20 for
     166  @{'sigma (λ${fresh p}.
     167    match ${fresh p} with [mk_Prod ${ident x} ${ident y} ⇒ $P])}.
     168notation > "Σ 〈 ident x : tyx, ident y : tyy, ident z : tyz 〉 . P" with precedence 20 for
     169  @{'sigma (λ${fresh p1}.
     170    match ${fresh p1} with [mk_Prod ${fresh p2} (${ident z} : $tyz) ⇒
     171      match ${fresh p2} with [mk_Prod (${ident x} : $tyx) (${ident y} : $tyy) ⇒ $P]])}.
     172notation > "Σ 〈 ident x , ident y , ident z 〉 . P" with precedence 20 for
     173  @{'sigma (λ${fresh p1}.
     174    match ${fresh p1} with [mk_Prod ${fresh p2} ${ident z} ⇒
     175      match ${fresh p2} with [mk_Prod ${ident x} ${ident y} ⇒ $P]])}.
     176
  • src/utilities/lists.ma

    r1647 r1882  
    11include "basics/lists/list.ma".
     2include "ASM/Util.ma". (* coercion from bool to Prop *)
     3
     4lemma All_map : ∀A,B,P,Q,f,l.
     5All A P l →
     6(∀a.P a → Q (f a)) →
     7All B Q (map A B f l).
     8#A #B #P #Q #f #l elim l //
     9#h #t #IH * #Ph #Pt #F % [@(F ? Ph) | @(IH Pt F)] qed.
     10
     11lemma Exists_map : ∀A,B,P,Q,f,l.
     12Exists A P l →
     13(∀a.P a → Q (f a)) →
     14Exists B Q (map A B f l).
     15#A #B #P #Q #f #l elim l //
     16#h #t #IH * #H #F
     17[ %1 @(F ? H) | %2 @(IH H F) ]
     18qed.
    219
    320lemma All_append : ∀A,P,l,r. All A P l → All A P r → All A P (l@r).
     
    3249] qed.
    3350
     51lemma All_split : ∀A,P,l. All A P l → ∀pre,x,post.l = pre @ x :: post → P x.
     52#A #P #l elim l
     53[ * * normalize [2: #y #pre'] #x #post #ABS destruct(ABS)
     54| #hd #tl #IH * #Phd #Ptl * normalize [2: #y #pre'] #x #post #EQ destruct(EQ)
     55  [ @(IH Ptl … (refl …))
     56  | @Phd
     57  ]
     58]
     59qed.
     60
    3461let rec All2 (A,B:Type[0]) (P:A → B → Prop) (la:list A) (lb:list B) on la : Prop ≝
    3562match la with
     
    5784] H.
    5885
     86lemma All_rev : ∀A,P,l.All A P l → All A P (rev ? l).
     87#A#P#l elim l //
     88#h #t #Hi * #Ph #Pt normalize
     89>rev_append_def
     90@All_append
     91[ @(Hi Pt)
     92| %{Ph I}
     93]
     94qed.
     95
     96lemma Exists_rev : ∀A,P,l.Exists A P l → Exists A P (rev ? l).
     97#A#P#l elim l //
     98#h #t #Hi normalize >rev_append_def
     99* [ #Ph @Exists_append_r %{Ph} | #Pt @Exists_append_l @(Hi Pt)]
     100qed.
     101
     102include "utilities/option.ma".
     103
     104lemma find_All : ∀A,B.∀P : A → Prop.∀Q : B → Prop.∀f.(∀x.P x → opt_All ? Q (f x)) →
     105  ∀l. All ? P l → opt_All ? Q (find … f l).
     106#A#B#P#Q#f#H#l elim l [#_%]
     107#x #l' #Hi
     108* #Px #AllPl'
     109whd in ⊢ (???%);
     110lapply (H x Px)
     111lapply (refl ? (f x))
     112generalize in ⊢ (???%→?); #o elim o [2: #b] #fx_eq >fx_eq [//]
     113#_ whd in ⊢ (???%); @(Hi AllPl')
     114qed.
     115
    59116include "utilities/monad.ma".
    60117
     
    65122  list
    66123  (λX,x.[x])
    67   (λX,Y,l,f.\fold [append ?, [ ]]_{x ∈ l} (f x))
    68   ???. normalize
     124  (λX,Y,l,f.foldr … (λx.append ? (f x)) [ ] l)
     125  ????. normalize
    69126[ / by /
    70127| #X#m elim m normalize //
    71128| #X#Y#Z #m #f#g
    72129  elim m normalize [//]
    73   #x#l' #Hi
    74   <(fold_sum ?? (f x) ? [ ] (Append ?))
    75   >Hi //
     130  #x#l' #Hi elim (f x)
     131  [@Hi] normalize #hd #tl #IH >associative_append >IH %
     132|#X#Y#m #f #g #H elim m normalize [//]
     133  #hd #tl #IH >H >IH %
    76134] qed.
    77135
    78136unification hint 0 ≔ X ;
    79 N ≟ max_def List, M ≟ m_def N
     137N ≟ max_def List
    80138(*---------------------------*)⊢
    81 list X ≡ monad M X.
     139list X ≡ monad N X.
     140
     141definition In ≝ λA.λl : list A.λx : A.Exists A (eq ? x) l.
     142
     143lemma All_In : ∀A,P,l,x. All A P l → In A l x → P x.
     144#A#P#l#x #Pl #xl elim (Exists_All … xl Pl)
     145#x' * #EQx' >EQx' //
     146qed.
     147
     148lemma In_All : ∀A,P,l.(∀x.In A l x → P x) → All A P l.
     149#A#P#l elim l
     150[#_ %
     151|#x #l' #IH #H %
     152  [ @H % %
     153  | @IH #y #G @H %2 @G
     154  ]
     155]
     156qed.
     157
     158
     159lemma nth_opt_append_l : ∀A,l1,l2,n.|l1| > n → nth_opt A n (l1 @ l2) = nth_opt A n l1.
     160#A#l1 elim l1 normalize
     161[ #l2 #n #ABS elim (absurd ? ABS ?) //
     162| #x #l' #IH #l2 #n cases n normalize
     163  [//
     164  | #n #H @IH @le_S_S_to_le assumption
     165  ]
     166]
     167qed.
     168
     169lemma nth_opt_append_r : ∀A,l1,l2,n.|l1| ≤ n → nth_opt A n (l1 @ l2) = nth_opt A (n - |l1|) l2.
     170#A#l1 elim l1
     171[#l2 #n #_ <minus_n_O %
     172|#x #l' #IH #l2 #n normalize in match (|?|); whd in match (nth_opt ???);
     173  cases n -n
     174  [  #ABS elim (absurd ? ABS ?) //
     175  | #n #H whd in ⊢ (??%?); >minus_S_S @IH @le_S_S_to_le assumption
     176  ]
     177]
     178qed.
     179
     180lemma nth_opt_append_hit_l : ∀A,l1,l2,n,x. nth_opt A n l1 = Some ? x →
     181  nth_opt A n (l1 @ l2) = Some ? x.
     182#A #l1 elim l1 normalize
     183[ #l2 #n #x #ABS destruct
     184| #hd #tl #IH #l2 * [2: #n] #x normalize /2 by /
     185]
     186qed.
     187
     188lemma nth_opt_append_miss_l : ∀A,l1,l2,n. nth_opt A n l1 = None ? →
     189  nth_opt A n (l1 @ l2) = nth_opt A (n - |l1|) l2.
     190#A #l1 elim l1 normalize
     191[ #l2 #n #_ <minus_n_O %
     192| #hd #tl #IH #l2 * [2: #n] normalize
     193  [ @IH
     194  | #ABS destruct(ABS)
     195  ]
     196]
     197qed.
     198
     199 
     200(* count occurrences satisfying a test *)
     201let rec count A (f : A → bool) (l : list A) on l : ℕ ≝
     202  match l with
     203  [ nil ⇒ 0
     204  | cons x l' ⇒ (if f x then 1 else 0) + count A f l'
     205  ].
     206 
     207theorem count_append : ∀A,f,l1,l2.count A f (l1@l2) = count A f l1 + count A f l2.
     208#A #f #l1 elim l1
     209[ #l2 %
     210| #hd #tl #IH #l2 normalize elim (f hd) normalize >IH %
     211]
     212qed.
     213
     214
     215include "utilities/option.ma".
     216
     217lemma position_of_from_aux : ∀A,test,l,n.
     218  position_of_aux A test l n = !n' ← position_of A test l; return n + n'.
     219#A #test #l elim l
     220[ normalize #_ %
     221| #hd #tl #IH #n
     222  normalize in ⊢ (??%?); >IH
     223  normalize elim (test hd) normalize
     224  [ <plus_n_O %
     225  | >(IH 1) whd in match (position_of ???);
     226    elim (position_of_aux ??? 0) normalize
     227    [ % | #x <plus_n_Sm % ]
     228  ]
     229]
     230qed.
     231
     232definition position_of_safe ≝ λA,test,l.λprf : count A test l ≥ 1.
     233  opt_safe ? (position_of A test l) ?.
     234  lapply prf -prf elim l normalize
     235  [ #ABS elim (absurd ? ABS (not_le_Sn_O 0))
     236  |#hd #tl #IH elim (test hd) normalize
     237    [2: >position_of_from_aux #H
     238      change with (position_of_aux ????) in match (position_of ???);
     239      >(opt_to_opt_safe … (IH H)) @opt_safe_elim normalize #x]
     240    #_ % #ABS destruct(ABS)
     241qed.
     242
     243definition index_of ≝
     244  λA,test,l.λprf : eqb (count A test l) 1.position_of_safe A test l ?.
     245  lapply prf -prf @eqb_elim #EQ * >EQ %
     246qed.
     247
     248lemma position_of_append_hit : ∀A,test,l1,l2,x.
     249  position_of A test (l1@l2) = Some ? x →
     250    position_of A test l1 = Some ? x ∨
     251      (position_of A test l1 = None ? ∧
     252        ! p ← position_of A test l2 ; return (|l1| + p) = Some ? x).
     253#A#test#l1 elim l1
     254[ #l2 #x change with l2 in match (? @ l2); #EQ >EQ %2
     255  % %
     256| #hd #tl #IH #l2 #x
     257  normalize elim (test hd) normalize
     258  [#H %{H}
     259  | >position_of_from_aux
     260    lapply (refl … (position_of A test (tl@l2)))
     261    generalize in ⊢ (???%→?); * [2: #n'] #Heq >Heq
     262    normalize #EQ destruct(EQ)
     263    elim (IH … Heq) -IH
     264    [ #G %
     265    | * #G #H
     266     lapply (refl … (position_of A test l2))
     267     generalize in ⊢ (???%→?); * [2: #x'] #H' >H' in H; normalize
     268     #EQ destruct (EQ) %2 %]
     269    >position_of_from_aux
     270    [1,2: >G % | >H' %]
     271  ]
     272]
     273qed.
     274
     275lemma position_of_hit : ∀A,test,l,x.position_of A test l = Some ? x →
     276  count A test l ≥ 1.
     277#A#test#l elim l normalize
     278[#x #ABS destruct(ABS)
     279|#hd #tl #IH #x elim (test hd) normalize [#EQ destruct(EQ) //]
     280  >position_of_from_aux
     281  lapply (refl … (position_of ? test tl))
     282  generalize in ⊢ (???%→?); * [2: #x'] #Heq >Heq normalize
     283  #EQ destruct(EQ) @(IH … Heq)
     284]
     285qed.
     286
     287lemma position_of_miss : ∀A,test,l.position_of A test l = None ? →
     288  count A test l = 0.
     289#A#test#l elim l normalize
     290[ #_ %
     291|#hd #tl #IH elim (test hd) normalize [#EQ destruct(EQ)]
     292  >position_of_from_aux
     293  lapply (refl … (position_of ? test tl))
     294  generalize in ⊢ (???%→?); * [2: #x'] #Heq >Heq normalize
     295  #EQ destruct(EQ) @(IH … Heq)
     296]
     297qed.
     298
     299
     300lemma position_of_append_miss : ∀A,test,l1,l2.
     301  position_of A test (l1@l2) = None ? →
     302    position_of A test l1 = None ? ∧ position_of A test l2 = None ?.
     303#A#test#l1 elim l1
     304[ #l2 change with l2 in match (? @ l2); #EQ >EQ % %
     305| #hd #tl #IH #l2
     306  normalize elim (test hd) normalize
     307  [#H destruct(H)
     308  | >position_of_from_aux
     309    lapply (refl … (position_of A test (tl@l2)))
     310    generalize in ⊢ (???%→?); * [2: #n'] #Heq >Heq
     311    normalize #EQ destruct(EQ)
     312    elim (IH … Heq) #H1 #H2
     313    >position_of_from_aux
     314    >position_of_from_aux
     315    >H1 >H2 normalize % %
     316  ]
     317]
     318qed.
     319
     320
  • src/utilities/monad.ma

    r1648 r1882  
    22include "basics/relations.ma".
    33include "utilities/setoids.ma".
    4 include "utilities/proper.ma".
     4
     5definition pred_transformer ≝ λA,B : Type[0].(A → Prop) → B → Prop.
     6
     7definition modus_ponens ≝ λA,B.λPT : pred_transformer A B.
     8  ∀P,Q.(∀x.P x → Q x) → ∀y.PT P y → PT Q y.
     9 
     10lemma mp_transitive :
     11  ∀A,B,C,PT1,PT2.modus_ponens A B PT1 → modus_ponens B C PT2 →
     12    modus_ponens A C (PT2 ∘ PT1). /4/ qed.
     13
     14definition rel_transformer ≝ λA,B,C,D : Type[0].
     15  (A → B → Prop) → C → D → Prop.
     16 
     17definition rel_modus_ponens ≝ λA,B,C,D.λRT : rel_transformer A B C D.
     18  ∀P,Q.(∀x,y.P x y → Q x y) → ∀z,w.RT P z w → RT Q z w.
     19 
     20lemma rel_mp_transitive :
     21  ∀A,B,C,D,E,F,RT1,RT2.rel_modus_ponens A B C D RT1 → rel_modus_ponens C D E F RT2 →
     22    rel_modus_ponens … (RT2 ∘ RT1). /4/ qed.
    523 
    6 record MonadDefinition : Type[1] ≝ {
     24record Monad : Type[1] ≝ {
    725  monad : Type[0] → Type[0] ;
    826  m_return : ∀X. X → monad X ;
     
    1129
    1230notation "m »= f" with precedence 49
    13   for @{'m_bind $m $f) }.
     31  for @{'m_bind $m $f }.
    1432
    1533notation > "!_ e; e'"
     
    104122
    105123
    106 include "basics/lists/list.ma".
    107 
    108 
    109 (* add structure and properties as needed *)
    110 record Monad : Type[1] ≝ {
    111   m_def :> MonadDefinition ;
    112   m_map : ∀X, Y. (X → Y) → monad m_def X → monad m_def Y ;
    113   m_map2 : ∀X, Y, Z. (X → Y → Z) →
    114     monad m_def X → monad m_def Y → monad m_def Z;
    115   m_bind2 : ∀X,Y,Z.monad m_def (X×Y) → (X → Y → monad m_def Z) → monad m_def Z;
    116   m_bind3 : ∀X,Y,Z,W.monad m_def (X×Y×Z) → (X → Y → Z → monad m_def W) → monad m_def W;
    117   m_join : ∀X.monad m_def (monad m_def X) → monad m_def X;
    118   m_sigbind2 : ∀A,B,C.∀P:A×B → Prop. monad m_def (Σx:A×B.P x) →
    119       (∀a,b. P 〈a,b〉 → monad m_def C) → monad m_def C;
    120   m_mmap : ∀X,Y.(X → monad m_def Y) → list X → monad m_def (list Y);
    121   m_mmap_sigma : ∀X,Y,P.(X → monad m_def (Σy : Y.P y)) → list X → monad m_def (Σl : list Y.All ? P l)
    122 }.
    123 
    124 interpretation "monad bind2" 'm_bind2 m f = (m_bind2 ? ? ? ? m f).
    125 interpretation "monad bind3" 'm_bind3 m f = (m_bind3 ? ? ? ? ? m f).
    126 interpretation "monad sigbind2" 'm_sigbind2 m f = (m_sigbind2 ????? m f).
    127 
    128 (*
    129 check (λM : Monad.λA,B,C,P.λp.λf : ∀a,b.P 〈a,b〉 → monad M C.! «a,b,H» ← p; f a b H)
    130 *)
    131 
    132124record MonadProps : Type[1] ≝
    133125  { max_def :> Monad
     
    136128  ; m_bind_bind : ∀X,Y,Z. ∀m : monad max_def X.∀f : X → monad max_def Y.
    137129      ∀g : Y → monad max_def Z.! y ← (! x ← m ; f x) ; g y = ! x ← m; ! y ← f x ; g y
     130  ; m_bind_ext_eq : ∀X,Y.∀m : monad max_def X.∀f,g : X → monad max_def Y.
     131      (∀x.f x = g x) → ! x ← m ; f x = ! x ← m ; g x
    138132  }.
    139133
     
    144138  ; sm_eq_trans : ∀X.transitive ? (sm_eq X)
    145139  ; sm_eq_sym : ∀X.symmetric ? (sm_eq X)
    146   ; sm_return_proper : ∀X .m_return smax_def X ⊨ eq ? ++> sm_eq ?
    147   ; sm_bind_proper : ∀X, Y.m_bind smax_def X Y ⊨ sm_eq ? ++> (eq ? ++> sm_eq ?) ++> sm_eq ?
     140  ; sm_return_proper : ∀X,x.sm_eq X (return x) (return x)
     141  ; sm_bind_proper : ∀X,Y,x,y,f,g.sm_eq X x y → (∀x.sm_eq Y (f x) (g x)) → sm_eq Y (x »= f) (y »= g)
    148142  ; sm_return_bind : ∀X,Y.∀x : X.∀f : X → monad smax_def Y.
    149143      sm_eq Y (! y ← return x ; f y) (f x)
     
    153147  }.
    154148
    155 interpretation "monad setoid equality" 'std_eq x y = (sm_eq ?? x y).
    156 
    157 
    158 definition MakeMonad : ?→?→?→Monad ≝ λmonad,m_return,m_bind.
    159   mk_Monad (mk_MonadDefinition monad m_return m_bind)
    160   (* map *)
    161   (λX,Y,f,m.
    162     ! x ← m ;
    163     return f x)
    164   (* map2 *)
    165   (λX,Y,Z,f,m,n.
    166     ! x ← m ;
    167     ! y ← n ;
    168     return (f x y))
    169   (* bind2 *)
    170   (λX,Y,Z,m,f.
    171     ! p ← m ;
    172     let 〈x, y〉 ≝ p in
    173     f x y)
    174   (λX,Y,Z,W,m,f.
    175     ! p ← m ;
    176     let 〈x, y, z〉 ≝ p in
    177     f x y z)
    178   (* join *)
    179   (λX,m.! x ← m ; x)
    180   (* m_sigbind2 *)
    181   (λA,B,C,P,e,f.
     149definition setoid_of_monad : ∀M : SetoidMonadProps.∀X : Type[0].
     150  Setoid ≝
     151  λM,X.mk_Setoid (monad M X) (sm_eq M X) (sm_eq_refl M X) (sm_eq_trans M X) (sm_eq_sym M X).
     152
     153include "hints_declaration.ma".
     154
     155unification hint 0 ≔ M, X;
     156M' ≟ smax_def M, S ≟ setoid_of_monad M X
     157(*-----------------------------*)⊢
     158monad M' X ≡ std_supp S.
     159
     160include "basics/lists/list.ma".
     161
     162definition m_map ≝ λM,X,Y.λf : X → Y.λm : monad M X.
     163  ! x ← m ; return f x.
     164
     165definition m_map2 ≝ λM,X,Y,Z.λf : X → Y → Z.λm : monad M X.λn : monad M Y.
     166  ! x ← m ; ! y ← n ; return f x y.
     167 
     168definition m_bind2 ≝ λM,X,Y,Z.λm : monad M (X × Y).λf : X → Y → monad M Z.
     169  ! p ← m ; f (\fst p) (\snd p).
     170
     171interpretation "monad bind2" 'm_bind2 m f = (m_bind2 ? ? ? ? m f).
     172
     173definition m_bind3 :
     174  ∀M,X,Y,Z,W.monad M (X×Y×Z) → (X → Y → Z → monad M W) → monad M W ≝
     175  λM,X,Y,Z,W,m,f.
     176  ! p ← m ; f (\fst (\fst p)) (\snd (\fst p)) (\snd p).
     177
     178interpretation "monad bind3" 'm_bind3 m f = (m_bind3 ? ? ? ? ? m f).
     179
     180definition m_join : ∀M,X.monad M (monad M X) → monad M X ≝
     181  λM,X,m.! x ← m ; x.
     182
     183definition m_sigbind2 :
     184  ∀M,A,B,C.∀P:A×B → Prop. monad M (Σx:A×B.P x) →
     185      (∀a,b. P 〈a,b〉 → monad M C) → monad M C ≝
     186λM,A,B,C,P,e,f.
    182187    ! e_sig ← e ;
    183188    match e_sig with
     
    187192      λeq_p.  f a b (eq_ind_r ?? (λx.λ_.P x) p_prf ? eq_p)
    188193      ](refl …)
    189     ])
    190   (λX,Y,f,l.foldr … (λel,macc.! r ← f el; !acc ← macc; return (r :: acc)) (return [ ]) l)
    191   (λX,Y,P,f,l.foldr … (λel,macc.
     194    ].
     195
     196interpretation "monad sigbind2" 'm_sigbind2 m f = (m_sigbind2 ????? m f).
     197
     198definition m_list_map :
     199  ∀M,X,Y.(X → monad M Y) → list X → monad M (list Y) ≝
     200  λM,X,Y,f,l.foldr … (λel,macc.! r ← f el; !acc ← macc; return (r :: acc)) (return [ ]) l.
     201
     202definition m_list_map_sigma :
     203  ∀M,X,Y,P.(X → monad M (Σy : Y.P y)) → list X → monad M (Σl : list Y.All ? P l) ≝
     204  λM,X,Y,P,f,l.foldr … (λel,macc.
    192205    ! «r, r_prf» ← f el ;
    193206    ! «acc, acc_prf» ← macc ;
    194207    return (mk_Sig ?? (r :: acc) ?))
    195     (return (mk_Sig … [ ] ?)) l).
    196   % assumption qed.
    197 
    198 definition MakeMonadProps : ?→?→?→?→?→?→MonadProps ≝ λmonad,m_return,m_bind,p1,p2,p3.
    199 mk_MonadProps (MakeMonad monad m_return m_bind) p1 p2 p3.
     208    (return (mk_Sig … [ ] ?)) l. % assumption qed.
     209
     210definition m_bin_op :
     211  ∀M,X,Y,Z.(X → Y → Z) → monad M X → monad M Y → monad M Z ≝
     212  λM,X,Y,Z,op,m,n. ! x ← m ; ! y ← n ; return op x y.
     213
     214unification hint 0 ≔ M, X, Y, Z, m, f ⊢
     215m_bind M (X×Y) Z m (λp.f (\fst p) (\snd p)) ≡ m_bind2 M X Y Z m f.
     216
     217unification hint 0 ≔ M, X, Y, Z, W, m, f ⊢
     218m_bind M (X×Y×Z) W m (λp.f (\fst (\fst p)) (\snd (\fst p)) (\snd p)) ≡
     219m_bind3 M X Y Z W m f.
     220
     221definition MakeMonadProps : ?→?→?→?→?→?→?→MonadProps ≝ λmonad,m_return,m_bind.
     222mk_MonadProps (mk_Monad monad m_return m_bind).
    200223
    201224definition MakeSetoidMonadProps : ?→?→?→?→?→?→?→?→?→?→?→?→SetoidMonadProps ≝
    202   λmonad,m_return,m_bind,sm_eq,p1,p2,p3,p4,p5,p6,p7,p8.
    203   mk_SetoidMonadProps (MakeMonad monad m_return m_bind) sm_eq p1 p2 p3 p4 p5 p6 p7 p8.
     225  λmonad,m_return,m_bind.
     226  mk_SetoidMonadProps (mk_Monad monad m_return m_bind).
     227 
     228record MonadPred (M : Monad) : Type[1] ≝
     229  { m_pred :> ∀X.pred_transformer X (monad M X)
     230  ; mp_return : ∀X,P,x.P x → m_pred X P (return x)
     231  ; mp_bind : ∀X,Y,Pin,Pout,m.m_pred X Pin m →
     232      ∀f.(∀x.Pin x → m_pred Y Pout (f x)) →
     233                  m_pred ? Pout (m_bind … m f)
     234  ; m_pred_mp : ∀X.modus_ponens ?? (m_pred X)
     235  }.
     236
     237record MonadRel (M1 : Monad) (M2 : Monad) : Type[1] ≝
     238  { m_rel :> ∀X,Y.rel_transformer X Y (monad M1 X) (monad M2 Y)
     239  ; mr_return : ∀X,Y,rel,x,y.rel x y → m_rel X Y rel (return x) (return y)
     240  ; mr_bind : ∀X,Y,Z,W,relin,relout,m,n.m_rel X Y relin m n → ∀f,g.(∀x,y.relin x y → m_rel Z W relout (f x) (g y)) →
     241                  m_rel ?? relout (m_bind … m f) (m_bind … n g)
     242  ; m_rel_mp : ∀X,Y.rel_modus_ponens ???? (m_rel X Y)
     243  }.
  • src/utilities/option.ma

    r1647 r1882  
    99  (* bind *)
    1010  (λX,Y,m,f. match m with [ Some x ⇒ f x | None ⇒ None ?])
    11   ???.
    12 // #X[2:#Y#Z]*normalize//qed.
     11  ????.
     12// #X[|*:#Y[#Z]]*normalize//qed.
    1313
    1414include "hints_declaration.ma".
    1515unification hint 0 ≔ X;
    16 N ≟ max_def Option, M ≟ m_def N
     16N ≟ max_def Option
    1717(*---------------*) ⊢
    18 option X ≡ monad M X
     18option X ≡ monad N X
    1919.
    2020
     
    2424  | None ⇒ λeq_m.?
    2525  ] (refl …). elim (absurd … eq_m prf) qed.
     26
     27lemma opt_to_opt_safe : ∀A,m,prf. m = Some ? (opt_safe A m prf).
     28#A *
     29[ #ABS elim (absurd ? (refl ??) ABS)
     30| //
     31] qed.
     32
     33lemma opt_safe_elim : ∀A.∀P : A → Prop.∀m,prf.
     34  (∀x.m = Some ? x → P x) → P (opt_safe ? m prf).
     35#A#P*
     36[#prf elim(absurd … (refl ??) prf)
     37|#x normalize #_ #H @H @refl
     38] qed.
     39
     40definition opt_try_catch : ∀X.option X → (unit → X) → X ≝
     41  λX,m,f.match m with [Some x ⇒ x | None ⇒ f it].
     42
     43notation > "'Try' m 'catch' opt (ident e opt( : ty)) ⇒ f" with precedence 46 for
     44  ${ default
     45    @{ ${ default
     46      @{'trycatch $m (λ${ident e}:$ty.$f)}
     47      @{'trycatch $m (λ${ident e}.$f)}
     48    }}
     49    @{'trycatch $m (λ_.$f)}
     50  }.
     51
     52notation < "hvbox('Try' \nbsp break m \nbsp break 'catch' \nbsp ident e : ty \nbsp ⇒ \nbsp break f)" with precedence 46 for
     53  @{'trycatch $m (λ${ident e}:$ty.$f)}.
     54notation < "hvbox('Try' \nbsp break m \nbsp break 'catch' \nbsp ⇒ \nbsp break f)" with precedence 46 for
     55  @{'trycatch $m (λ_:$ty.$f)}.
     56
     57interpretation "option try and catch" 'trycatch m f = (opt_try_catch ? m f).
     58
     59definition OptPred ≝ λPdef : Prop.mk_MonadPred Option (λX,P,m.Try ! x ← m ; return P x catch ⇒ Pdef) ???.
     60#X[2:#Y]#P1[1,3:#P2[2:#H]*] normalize /2/
     61qed.
     62
     63definition opt_All : ∀X.(X → Prop) → option X → Prop ≝ m_pred … (OptPred True).
     64 
     65lemma opt_All_mp : ∀A,P,Q.(∀x. P x → Q x) → ∀o.opt_All A P o → opt_All ? Q o
     66  ≝ m_pred_mp ….
     67
     68definition opt_Exists : ∀X.(X → Prop) → option X → Prop ≝ m_pred … (OptPred False).
     69 
     70lemma opt_Exists_mp : ∀A,P,Q.(∀x. P x → Q x) → ∀o.opt_Exists A P o → opt_Exists ? Q o
     71  ≝ m_pred_mp ….
     72
  • src/utilities/state.ma

    r1647 r1882  
    1212  (λX,c1,c2.∀s.c1 s = c2 s)
    1313  ????????.
    14 //
     14// normalize
    1515#X
    1616[ (* bind_proper *)
    17   #Y #m#n #m_eq_n
    18   #f #g #f_eq_g
    19   #s
    20   generalize in match (m_eq_n s); -m_eq_n
    21   normalize
    22   #m_eq_n >m_eq_n -m_eq_n
    23   elim (n s) #s' #y
    24   normalize @f_eq_g //
    25 | #m#s normalize
    26   elim (m s) normalize /2 by /
    27 | #Y #Z #m #f #g #s normalize
    28   elim (m s) normalize
    29   #s' #x
    30   elim (f x s') normalize
    31   #s'' #y //
     17  #Y #m #n #f #g #H #G #s >H elim (n s) #s' #x normalize @G
     18| #m#s @pair_elim //
     19| #Y#Z #m #f #g #s elim (m s) //
    3220]
    3321qed.
     
    4129include "hints_declaration.ma".
    4230unification hint 0 ≔ S,X;
    43 N ≟ State S, M ≟ smax_def N, O ≟ m_def M
     31N ≟ State S, M ≟ smax_def N
    4432(*---------------*) ⊢
    45 state_monad S X ≡ monad O X
     33state_monad S X ≡ monad M X
    4634.
    4735
     36definition StatePred ≝ λS.λPs : S → Prop.mk_MonadPred (State S)
     37  (λX,P,m.∀s.Ps s → let m' ≝ m s in Ps (\fst m') ∧ P (\snd m')) ???.
     38[ normalize /2/
     39| normalize #X#Y#P1#P2 #m #H #f #G #s #Ps lapply (H … Ps)
     40  elim (m s) #s' #x normalize * /2/
     41| #X #P #Q #H #m normalize #G #s #Ps elim (G … Ps) /3/
     42]
     43qed.
     44
     45definition StateRel ≝ λS,T.λPs : S → T → Prop.mk_MonadRel (State S) (State T)
     46  (λX,Y,P,m,n.∀s,t.Ps s t → let m' ≝ m s in let n' ≝ n t in
     47    Ps (\fst m') (\fst n') ∧ P (\snd m') (\snd n')) ???.
     48[ normalize /2/
     49| normalize #X#Y#Z#W#P1#P2 #m #n #H #f #g #G #s #t #Ps lapply (H … Ps)
     50  * elim (m s) elim (n t) /2/
     51| #X #Y #P #Q #H #m #n normalize #G #s #t #Ps elim (G … Ps) /3/
     52]
     53qed.
     54
  • src/utilities/trace.ma

    r1635 r1882  
    2626M ≟ Trace T
    2727(*---------------*) ⊢
    28 X × (list T) ≡ monad (m_def M) X
     28X × (list T) ≡ monad M X
    2929.
    3030
Note: See TracChangeset for help on using the changeset viewer.