Changeset 2420 for src/common


Ignore:
Timestamp:
Oct 30, 2012, 12:32:31 PM (7 years ago)
Author:
campbell
Message:

Tidy away generic results about folds on positive/identifier maps.

Location:
src/common
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/common/Identifiers.ma

    r2418 r2420  
    326326  ].
    327327
     328(* Fold over the entries in a map.  There are some lemmas to help reason about
     329   this near the bottom of the file (they require sets). *)
     330
    328331definition foldi:
    329332  ∀A, B: Type[0].
     
    11201123
    11211124
    1122 
     1125(* Returns the domain of a map as the canonical set (one made only from the
     1126   empty set and addition. *)
     1127definition domain_of_map : ∀tag,A. identifier_map tag A → identifier_set tag ≝
     1128λtag,A,m. an_id_map tag unit (domain_of_pm A (match m with [ an_id_map m ⇒ m ])).
     1129lemma domain_of_map_present : ∀tag,A,m,id.
     1130  present tag A m id ↔ present tag unit (domain_of_map … m) id.
     1131#tag #A * #m * #p @domain_of_pm_present
     1132qed.
     1133
     1134(* Some lemmas for reasoning about folds. *)
     1135
     1136lemma foldi_ind : ∀A,B,tag,f,m,b. ∀P:B → identifier_set tag → Prop.
     1137  P b (empty_set …) →
     1138  (∀k,ks,a,b. ¬present ?? ks k → lookup ?? m k = Some ? a → P b ks → P (f k a b) (add_set tag ks k)) →
     1139  P (foldi A B tag f m b) (domain_of_map … m).
     1140#A #B #tag #f * #m #b #P #P0 #STEP
     1141whd in match (foldi ??????); change with (an_id_map ?? (domain_of_pm A m)) in match (domain_of_map ???);
     1142@pm_fold_ind
     1143[ @P0
     1144| #p #ps #a #b0 #FR #L #pre @(STEP (an_identifier tag p) (an_id_map tag unit ps))
     1145  [ normalize >FR /3/
     1146  | @L
     1147  | @pre
     1148  ]
     1149] qed.
     1150
     1151lemma foldi_ind' : ∀A,B,tag,f,m,b,b'. ∀P:B → identifier_set tag → Prop.
     1152  P b (empty_set …) →
     1153  (∀k,ks,a,b. ¬present ?? ks k → lookup ?? m k = Some ? a → P b ks → P (f k a b) (add_set tag ks k)) →
     1154  foldi A B tag f m b = b' →
     1155  P b' (domain_of_map … m).
     1156#H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11  destruct @foldi_ind /2/
     1157qed.
     1158
  • src/common/PositiveMap.ma

    r2415 r2420  
    120120            fold A B (λx.f (p1 x)) r b
    121121].   
     122
     123definition domain_of_pm : ∀A. positive_map A → positive_map unit ≝
     124λA,t. fold A (positive_map unit) (λp,a,b. insert unit p it b) t (pm_leaf unit).
     125
     126(* Build some results about fold using domain_of_pm. *)
     127
     128lemma pm_fold_ignore_adding_junk : ∀A. ∀m. ∀f,g:Pos → Pos. ∀s.
     129  (∀p,q. f p ≠ g q) →
     130  ∀p. lookup_opt unit (f p) (fold A ? (λx,a,b. insert unit (g x) it b) m s) = lookup_opt unit (f p) s.
     131#A #m elim m
     132[ normalize //
     133| #oa #l #r #IHl #IHr
     134  #f #g #s #not_g #p
     135  normalize
     136  >IHr
     137  [ >IHl
     138    [ cases oa
     139      [ normalize %
     140      | #a normalize >(lookup_opt_insert_miss ?? (f p)) [ % | @not_g ]
     141      ]
     142    | #x #y % #E cases (not_g x (p0 y)) #H @H @E
     143    ]
     144  | #x #y % #E cases (not_g x (p1 y)) #H @H @E
     145  ]
     146] qed.
     147
     148lemma pm_fold_ind_gen : ∀A,B,m,f,b.
     149  ∀pre:Pos→Pos. (∀x,y.pre x = pre y → x = y) → ∀ps. (∀p. lookup_opt ? (pre p) ps = None ?) →
     150  ∀P:B → positive_map unit → Prop.
     151  P b ps →
     152  (∀p,ps,a,b. lookup_opt unit (pre p) ps = None unit → lookup_opt A p m = Some A a → P b ps → P (f (pre p) a b) (insert unit (pre p) it ps)) →
     153  P (fold A B (λx. f (pre x)) m b) (fold ?? (λp,a,b. insert unit (pre p) it b) m ps).
     154#A #B #m elim m
     155[ //
     156| #oa #l #r #IHl #IHr
     157  #f #b #pre #PRE #ps #PS #P #emp #step whd in ⊢ (?%%);
     158  @IHr
     159  [ #x #y #E lapply (PRE … E) #E' destruct //
     160  | #p change with ((λx. pre (p1 x)) p) in match (pre (p1 p)); >pm_fold_ignore_adding_junk
     161    [ cases oa [ @PS | #a >(lookup_opt_insert_miss ?? (pre (p1 p))) [ @PS | % #E lapply (PRE … E) #E' destruct ] ]
     162    | #p #q % #E lapply (PRE … E) #E' destruct
     163    ]
     164  | @IHl
     165    [ #x #y #E lapply (PRE … E) #E' destruct //
     166    | #p cases oa [ @PS | #a >(lookup_opt_insert_miss ?? (pre (p0 p))) [ @PS | % #E lapply (PRE … E) #E' destruct ] ]
     167    | cases oa in step ⊢ %; [ #_ @emp | #a #step normalize @step [ @PS | % | @emp ] ]
     168    | #p #ps' #a #b' @step
     169    ]
     170  | #p #ps' #a #b' @step
     171  ]
     172] qed.
     173
     174lemma pm_fold_ext : ∀A,B,m,f,b.
     175  fold A B f m b = fold A B (λx:Pos. f x) m b.
     176#A #B #m elim m /4/
     177qed.
     178
     179(* Main result about folds.  (Rather than producing a result about just the
     180   domain of m we could use the whole mapping, but we'd need a function to
     181   canonicalise maps because their representation can contain some junk.) *)
     182
     183lemma pm_fold_ind : ∀A,B,f,m,b. ∀P:B → positive_map unit → Prop.
     184  P b (pm_leaf unit) →
     185  (∀p,ps,a,b. lookup_opt unit p ps = None unit → lookup_opt A p m = Some A a → P b ps → P (f p a b) (insert unit p it ps)) →
     186  P (fold A B f m b) (domain_of_pm A m).
     187#A #B #f #m #b #P #emp #step
     188>pm_fold_ext
     189whd in ⊢ (??%);
     190@(pm_fold_ind_gen A B m f b (λx.x) ? (pm_leaf unit) ???)
     191[ //
     192| //
     193| @emp
     194| @step
     195] qed.
     196
     197lemma pm_fold_eq : ∀A,B,b,f.
     198  (∀p,k:Pos. ∀a,s1,s2. lookup_opt B p s1 = lookup_opt B p s2 → lookup_opt B p (f k a s1) = lookup_opt B p (f k a s2)) →
     199  ∀p,s1,s2.
     200  lookup_opt B p s1 = lookup_opt B p s2 →
     201  lookup_opt B p (fold A (positive_map B) f b s1) = lookup_opt B p (fold A (positive_map B) f b s2).
     202#A #B #b elim b
     203[ #f #H #p #s1 #s2 #H @H
     204| #oa #l #r #IHl #IHr #f #H #p #s1 #s2 #H'
     205  whd in match (fold ???? s1);
     206  whd in match (fold ???? s2);
     207  @IHr [ #q #k #a #s1' #s2' #H'' @H @H'' ]
     208  @IHl [ #q #k #a #s1' #s2' #H'' @H @H'' ]
     209  cases oa [ @H' | #a @H @H' ]
     210] qed.
     211
     212
     213lemma pm_fold_ignore_prefix : ∀A. ∀m. ∀pre:Pos → Pos. (∀x,y. pre x = pre y → x = y) →
     214  ∀p. ∀pre'.
     215      lookup_opt unit (pre p) (fold A ? (λx,a,b. insert unit (pre (pre' x)) it b) m (pm_leaf ?)) =
     216      lookup_opt unit p (fold A ? (λx,a,b. insert unit (pre' x) it b) m (pm_leaf ?)).
     217#A #m #pre #PRE
     218cut (∀p. lookup_opt unit (pre p) (pm_leaf unit) = lookup_opt unit p (pm_leaf unit)) [ // ]
     219generalize in match (pm_leaf unit) in ⊢ ((? → ??%?) → ? → ? → ??%?);
     220generalize in match (pm_leaf unit);
     221elim m
     222[ #s1 #s2 #S #p #pre' @S
     223| #oa #l #r #IHl #IHr
     224  #s1 #s2 #S #p #pre'
     225  whd in ⊢ (??(???%)(???%));
     226  @(IHr ???? (λx. pre' (p1 x)))
     227  #p' @IHl
     228  #p'' cases oa
     229  [ @S
     230  | #a cases (decidable_eq_pos p'' (pre' one))
     231    [ #E destruct
     232      >(lookup_opt_insert_hit ?? (pre (pre' one)))
     233      >(lookup_opt_insert_hit ?? (pre' one))
     234      %
     235    | #NE >(lookup_opt_insert_miss ??? (pre (pre' one)))
     236      [ >(lookup_opt_insert_miss ??? (pre' one)) //
     237      | % #E @(absurd … (PRE … E) NE)
     238      ]
     239    ]
     240  ]
     241] qed.
     242
     243(* Link the domain of a map (used in the result about fold) to the original
     244   map. *)
     245
     246lemma domain_of_pm_present : ∀A,m,p.
     247  lookup_opt A p m ≠ None ? ↔ lookup_opt unit p (domain_of_pm A m) ≠ None ?.
     248
     249#A #m whd in match (domain_of_pm ??);
     250elim m
     251[ #p normalize /3/
     252| #oa #l #r #IHl #IHr
     253  whd in match (fold ???? (pm_leaf unit));
     254  *
     255  [ change with ((λx:Pos. one) one) in ⊢ (??(?(??(??%?)?)));
     256    >pm_fold_ignore_adding_junk [2: #p #q % #E destruct ]
     257    change with ((λx:Pos. one) one) in ⊢ (??(?(??(??%?)?)));
     258    >pm_fold_ignore_adding_junk [2: #p #q % #E destruct ]
     259    cases oa
     260    [ normalize /3/
     261    | #a change with (insert unit one ??) in ⊢ (??(?(??(???%)?)));
     262      >(lookup_opt_insert_hit ?? one) normalize
     263      % #_ % #E destruct
     264    ]
     265  | #p >(pm_fold_eq ??????? (pm_leaf unit))
     266    [ >pm_fold_ignore_prefix [2: #x #y #E destruct % ]
     267      @IHr
     268    | >pm_fold_ignore_adding_junk [2: #x #y % #E destruct ]
     269      cases oa
     270      [ %
     271      | #a >(lookup_opt_insert_miss ?? (p1 p)) [2: % #E destruct ]
     272        %
     273      ]
     274    | #x #y #a #s1 #s2 #S cases (decidable_eq_pos x (p1 y))
     275      [ #E destruct
     276        >(lookup_opt_insert_hit ?? (p1 y))
     277        >(lookup_opt_insert_hit ?? (p1 y))
     278        %
     279      | #NE >(lookup_opt_insert_miss ?? x … NE)
     280        >(lookup_opt_insert_miss ?? x … NE)
     281        @S
     282      ]
     283    ] 
     284  | #p
     285    >pm_fold_ignore_adding_junk [2: #x #y % #E destruct ]
     286    >(pm_fold_eq ??????? (pm_leaf unit))
     287    [ >pm_fold_ignore_prefix [2: #x #y #E destruct % ]
     288      @IHl
     289    | cases oa
     290      [ %
     291      | #a >(lookup_opt_insert_miss ?? (p0 p)) [2: % #E destruct ]
     292        %
     293      ]
     294    | #x #y #a #s1 #s2 #S cases (decidable_eq_pos x (p0 y))
     295      [ #E destruct
     296        >(lookup_opt_insert_hit ?? (p0 y))
     297        >(lookup_opt_insert_hit ?? (p0 y))
     298        %
     299      | #NE >(lookup_opt_insert_miss ?? x … NE)
     300        >(lookup_opt_insert_miss ?? x … NE)
     301        @S
     302      ]
     303    ]
     304  ]
     305] qed.
     306
    122307
    123308lemma update_fail : ∀A,b,a,t.
Note: See TracChangeset for help on using the changeset viewer.