Changeset 2420 for src/RTLabs/CostInj.ma


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.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/CostInj.ma

    r2418 r2420  
    4848].
    4949
    50 definition domain_of_pm : ∀A. positive_map A → positive_map unit ≝
    51 λA,t. fold A (positive_map unit) (λp,a,b. insert unit p it b) t (pm_leaf unit).
    52 
    53 lemma pm_fold_ignore_adding_junk : ∀A. ∀m. ∀f,g:Pos → Pos. ∀s.
    54   (∀p,q. f p ≠ g q) →
    55   ∀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.
    56 #A #m elim m
    57 [ normalize //
    58 | #oa #l #r #IHl #IHr
    59   #f #g #s #not_g #p
    60   normalize
    61   >IHr
    62   [ >IHl
    63     [ cases oa
    64       [ normalize %
    65       | #a normalize >(lookup_opt_insert_miss ?? (f p)) [ % | @not_g ]
    66       ]
    67     | #x #y % #E cases (not_g x (p0 y)) #H @H @E
    68     ]
    69   | #x #y % #E cases (not_g x (p1 y)) #H @H @E
    70   ]
    71 ] qed.
    72 
    73 lemma pm_fold_ind_gen : ∀A,B,m,f,b.
    74   ∀pre:Pos→Pos. (∀x,y.pre x = pre y → x = y) → ∀ps. (∀p. lookup_opt ? (pre p) ps = None ?) →
    75   ∀P:B → positive_map unit → Prop.
    76   P b ps →
    77   (∀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)) →
    78   P (fold A B (λx. f (pre x)) m b) (fold ?? (λp,a,b. insert unit (pre p) it b) m ps).
    79 #A #B #m elim m
    80 [ //
    81 | #oa #l #r #IHl #IHr
    82   #f #b #pre #PRE #ps #PS #P #emp #step whd in ⊢ (?%%);
    83   @IHr
    84   [ #x #y #E lapply (PRE … E) #E' destruct //
    85   | #p change with ((λx. pre (p1 x)) p) in match (pre (p1 p)); >pm_fold_ignore_adding_junk
    86     [ cases oa [ @PS | #a >(lookup_opt_insert_miss ?? (pre (p1 p))) [ @PS | % #E lapply (PRE … E) #E' destruct ] ]
    87     | #p #q % #E lapply (PRE … E) #E' destruct
    88     ]
    89   | @IHl
    90     [ #x #y #E lapply (PRE … E) #E' destruct //
    91     | #p cases oa [ @PS | #a >(lookup_opt_insert_miss ?? (pre (p0 p))) [ @PS | % #E lapply (PRE … E) #E' destruct ] ]
    92     | cases oa in step ⊢ %; [ #_ @emp | #a #step normalize @step [ @PS | % | @emp ] ]
    93     | #p #ps' #a #b' @step
    94     ]
    95   | #p #ps' #a #b' @step
    96   ]
    97 ] qed.
    98 
    99 lemma pm_fold_ext : ∀A,B,m,f,b.
    100   fold A B f m b = fold A B (λx:Pos. f x) m b.
    101 #A #B #m elim m /4/
    102 qed.
    103 
    104 lemma pm_fold_ind : ∀A,B,f,m,b. ∀P:B → positive_map unit → Prop.
    105   P b (pm_leaf unit) →
    106   (∀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)) →
    107   P (fold A B f m b) (domain_of_pm A m).
    108 #A #B #f #m #b #P #emp #step
    109 >pm_fold_ext
    110 whd in ⊢ (??%);
    111 @(pm_fold_ind_gen A B m f b (λx.x) ? (pm_leaf unit) ???)
    112 [ //
    113 | //
    114 | @emp
    115 | @step
    116 ] qed.
    117 
    118 lemma pm_fold_eq : ∀A,B,b,f.
    119   (∀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)) →
    120   ∀p,s1,s2.
    121   lookup_opt B p s1 = lookup_opt B p s2 →
    122   lookup_opt B p (fold A (positive_map B) f b s1) = lookup_opt B p (fold A (positive_map B) f b s2).
    123 #A #B #b elim b
    124 [ #f #H #p #s1 #s2 #H @H
    125 | #oa #l #r #IHl #IHr #f #H #p #s1 #s2 #H'
    126   whd in match (fold ???? s1);
    127   whd in match (fold ???? s2);
    128   @IHr [ #q #k #a #s1' #s2' #H'' @H @H'' ]
    129   @IHl [ #q #k #a #s1' #s2' #H'' @H @H'' ]
    130   cases oa [ @H' | #a @H @H' ]
    131 ] qed.
    132 
    133 
    134 
    135 lemma pm_fold_ignore_prefix : ∀A. ∀m. ∀pre:Pos → Pos. (∀x,y. pre x = pre y → x = y) →
    136   ∀p. ∀pre'.
    137       lookup_opt unit (pre p) (fold A ? (λx,a,b. insert unit (pre (pre' x)) it b) m (pm_leaf ?)) =
    138       lookup_opt unit p (fold A ? (λx,a,b. insert unit (pre' x) it b) m (pm_leaf ?)).
    139 #A #m #pre #PRE
    140 cut (∀p. lookup_opt unit (pre p) (pm_leaf unit) = lookup_opt unit p (pm_leaf unit)) [ // ]
    141 generalize in match (pm_leaf unit) in ⊢ ((? → ??%?) → ? → ? → ??%?);
    142 generalize in match (pm_leaf unit);
    143 elim m
    144 [ #s1 #s2 #S #p #pre' @S
    145 | #oa #l #r #IHl #IHr
    146   #s1 #s2 #S #p #pre'
    147   whd in ⊢ (??(???%)(???%));
    148   @(IHr ???? (λx. pre' (p1 x)))
    149   #p' @IHl
    150   #p'' cases oa
    151   [ @S
    152   | #a cases (decidable_eq_pos p'' (pre' one))
    153     [ #E destruct
    154       >(lookup_opt_insert_hit ?? (pre (pre' one)))
    155       >(lookup_opt_insert_hit ?? (pre' one))
    156       %
    157     | #NE >(lookup_opt_insert_miss ??? (pre (pre' one)))
    158       [ >(lookup_opt_insert_miss ??? (pre' one)) //
    159       | % #E @(absurd … (PRE … E) NE)
    160       ]
    161     ]
    162   ]
    163 ] qed.
    164 
    165 lemma domain_of_pm_present : ∀A,m,p.
    166   lookup_opt A p m ≠ None ? ↔ lookup_opt unit p (domain_of_pm A m) ≠ None ?.
    167 
    168 #A #m whd in match (domain_of_pm ??);
    169 elim m
    170 [ #p normalize /3/
    171 | #oa #l #r #IHl #IHr
    172   whd in match (fold ???? (pm_leaf unit));
    173   *
    174   [ change with ((λx:Pos. one) one) in ⊢ (??(?(??(??%?)?)));
    175     >pm_fold_ignore_adding_junk [2: #p #q % #E destruct ]
    176     change with ((λx:Pos. one) one) in ⊢ (??(?(??(??%?)?)));
    177     >pm_fold_ignore_adding_junk [2: #p #q % #E destruct ]
    178     cases oa
    179     [ normalize /3/
    180     | #a change with (insert unit one ??) in ⊢ (??(?(??(???%)?)));
    181       >(lookup_opt_insert_hit ?? one) normalize
    182       % #_ % #E destruct
    183     ]
    184   | #p >(pm_fold_eq ??????? (pm_leaf unit))
    185     [ >pm_fold_ignore_prefix [2: #x #y #E destruct % ]
    186       @IHr
    187     | >pm_fold_ignore_adding_junk [2: #x #y % #E destruct ]
    188       cases oa
    189       [ %
    190       | #a >(lookup_opt_insert_miss ?? (p1 p)) [2: % #E destruct ]
    191         %
    192       ]
    193     | #x #y #a #s1 #s2 #S cases (decidable_eq_pos x (p1 y))
    194       [ #E destruct
    195         >(lookup_opt_insert_hit ?? (p1 y))
    196         >(lookup_opt_insert_hit ?? (p1 y))
    197         %
    198       | #NE >(lookup_opt_insert_miss ?? x … NE)
    199         >(lookup_opt_insert_miss ?? x … NE)
    200         @S
    201       ]
    202     ] 
    203   | #p
    204     >pm_fold_ignore_adding_junk [2: #x #y % #E destruct ]
    205     >(pm_fold_eq ??????? (pm_leaf unit))
    206     [ >pm_fold_ignore_prefix [2: #x #y #E destruct % ]
    207       @IHl
    208     | cases oa
    209       [ %
    210       | #a >(lookup_opt_insert_miss ?? (p0 p)) [2: % #E destruct ]
    211         %
    212       ]
    213     | #x #y #a #s1 #s2 #S cases (decidable_eq_pos x (p0 y))
    214       [ #E destruct
    215         >(lookup_opt_insert_hit ?? (p0 y))
    216         >(lookup_opt_insert_hit ?? (p0 y))
    217         %
    218       | #NE >(lookup_opt_insert_miss ?? x … NE)
    219         >(lookup_opt_insert_miss ?? x … NE)
    220         @S
    221       ]
    222     ]
    223   ]
    224 ] qed.
    225 
    226 
    227 (* Returns the domain of a map as the canonical set (one made only from the
    228    empty set and addition. *)
    229 definition domain_of_map : ∀tag,A. identifier_map tag A → identifier_set tag ≝
    230 λtag,A,m. an_id_map tag unit (domain_of_pm A (match m with [ an_id_map m ⇒ m ])).
    231 lemma domain_of_map_present : ∀tag,A,m,id.
    232   present tag A m id ↔ present tag unit (domain_of_map … m) id.
    233 #tag #A * #m * #p @domain_of_pm_present
    234 qed.
    235 
    236 lemma foldi_ind : ∀A,B,tag,f,m,b. ∀P:B → identifier_set tag → Prop.
    237   P b (empty_set …) →
    238   (∀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)) →
    239   P (foldi A B tag f m b) (domain_of_map … m).
    240 #A #B #tag #f * #m #b #P #P0 #STEP
    241 whd in match (foldi ??????); change with (an_id_map ?? (domain_of_pm A m)) in match (domain_of_map ???);
    242 @pm_fold_ind
    243 [ @P0
    244 | #p #ps #a #b0 #FR #L #pre @(STEP (an_identifier tag p) (an_id_map tag unit ps))
    245   [ normalize >FR /3/
    246   | @L
    247   | @pre
    248   ]
    249 ] qed.
    250 
    251 lemma foldi_ind' : ∀A,B,tag,f,m,b,b'. ∀P:B → identifier_set tag → Prop.
    252   P b (empty_set …) →
    253   (∀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)) →
    254   foldi A B tag f m b = b' →
    255   P b' (domain_of_map … m).
    256 #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11  destruct @foldi_ind /2/
    257 qed.
    25850
    25951lemma reverse_label_map_ok : ∀g,r.
Note: See TracChangeset for help on using the changeset viewer.