Ignore:
Timestamp:
Aug 30, 2012, 4:47:54 PM (7 years ago)
Author:
campbell
Message:

RTLabs cost spec checking function implemented (lacks proof, or much
testing due to a bug elsewhere). Includes some new operations on
PostiveMaps? and identifier_maps/sets.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/PositiveMap.ma

    r2303 r2305  
    373373qed.
    374374
     375
     376(* Attempt to choose an entry in the map, and if successful return the entry
     377   and the map without it. *)
     378
     379let rec pm_choose (A:Type[0]) (t:positive_map A) on t : option (Pos × A × (positive_map A)) ≝
     380match t with
     381[ pm_leaf ⇒ None ?
     382| pm_node a l r ⇒
     383  match pm_choose A l with
     384  [ None ⇒
     385    match pm_choose A r with
     386    [ None ⇒
     387      match a with
     388      [ None ⇒ None ?
     389      | Some a ⇒ Some ? 〈〈one, a〉, pm_leaf A〉
     390      ]
     391    | Some x ⇒ Some ? 〈〈p1 (\fst (\fst x)), \snd (\fst x)〉, pm_node A a l (\snd x)〉
     392    ]
     393  | Some x ⇒ Some ? 〈〈p0 (\fst (\fst x)), \snd (\fst x)〉, pm_node A a (\snd x) r〉
     394  ]
     395].
     396
     397lemma pm_choose_empty : ∀A,t.
     398  pm_choose A t = None ? ↔ ∀p. lookup_opt A p t = None A.
     399#A #t elim t
     400[ % //
     401| *
     402  [ #l #r * #IHl #IHl' * #IHr #IHr' %
     403    [ #C *
     404      [ %
     405      | #p whd in C:(??%?) ⊢ (??%?);
     406        @IHr cases (pm_choose A r) in C ⊢ %;
     407        [ //
     408        | #x normalize cases (pm_choose A l) [2: #y] normalize #E destruct
     409        ]
     410      | #p whd in C:(??%?) ⊢ (??%?);
     411        @IHl cases (pm_choose A l) in C ⊢ %;
     412        [ //
     413        | #x normalize #E destruct
     414        ]
     415      ]
     416    | #L whd in ⊢ (??%?); >IHl' [ normalize >IHr' [ % | #p @(L (p1 p)) ] | #p @(L (p0 p)) ]
     417    ]
     418  | #a #l #r #IHl #IHr %
     419    [ normalize cases (pm_choose A l) [2: normalize #x #E destruct ]
     420      normalize cases (pm_choose A r) [2: #x] normalize #E destruct
     421    | #L lapply (L one) normalize #E destruct
     422    ]
     423  ]
     424] qed.
     425
     426lemma pm_choose_empty_card : ∀A,t.
     427  pm_choose A t = None ? ↔ |t| = 0.
     428#A #t elim t
     429[ /2/
     430| * [ #l #r * #IHl #IHl' * #IHr #IHr' %
     431      [ normalize lapply IHl cases (pm_choose A l) [2: #x #_ #E normalize in E; destruct ]
     432        normalize lapply IHr cases (pm_choose A r) [2: #x #_ #_ #E normalize in E; destruct ]
     433        #H1 #H2 #_ >(H1 (refl ??)) >(H2 (refl ??)) %
     434      | normalize #CARD >IHl' [ >IHr' ] /2 by refl, le_n_O_to_eq/
     435      ]
     436    | #a #l #r #_ #_ % normalize
     437      [ cases (pm_choose A l) [ cases (pm_choose A r) [ | #x ] | #x ]
     438        #E normalize in E; destruct
     439      | #E destruct
     440      ]
     441    ]
     442] qed.
     443
     444lemma pm_choose_some : ∀A,t,p,a,t'.
     445  pm_choose A t = Some ? 〈〈p,a〉,t'〉 →
     446  lookup_opt A p t = Some A a ∧
     447  lookup_opt A p t' = None A ∧
     448  (∀q. p = q ∨ lookup_opt A q t = lookup_opt A q t') ∧
     449  |t| = S (|t'|).
     450#A #t elim t
     451[ #p #a #t' normalize #E destruct
     452| #ao #l #r #IHl #IHr *
     453  [ #a #t' normalize
     454    lapply (pm_choose_empty_card A l)
     455    lapply (pm_choose_empty A l)
     456    cases (pm_choose A l) normalize [2: #x #_ #_ #E destruct ] * #EMPl #EMPl' * #CARDl #CARDl'
     457    lapply (pm_choose_empty_card A r)
     458    lapply (pm_choose_empty A r)
     459    cases (pm_choose A r) normalize [2: #x #_ #_ #E destruct ] * #EMPr #EMPr' * #CARDr #CARDr'
     460    cases ao normalize [2:#x] #E destruct
     461    % [ % /2/ * /2/ #q %2 whd in ⊢ (??%%); /2/ | >CARDl >CARDr // ]
     462  | #p #a #t' normalize
     463    lapply (pm_choose_empty_card A l)
     464    lapply (pm_choose_empty A l)
     465    cases (pm_choose A l) normalize [2: #x #_ #_ #E destruct ] * #EMPl #EMPl' * #CARDl #CARDl'
     466    lapply (IHr p)
     467    cases (pm_choose A r) normalize [ #_ cases ao [2:#a'] normalize #E destruct ]
     468    * * #p' #a' #t'' #IH #E destruct
     469    cases (IH ?? (refl ??)) * * #L1 #L2 #L3 #CARD
     470    % [ % [ % [ // | @L2 ]| * /2/ #q cases (L3 q) /2/ #L4 %2 @L4 ] | cases ao normalize >CARD // ]
     471  | #p #a #t' normalize
     472    lapply (IHl p)
     473    cases (pm_choose A l) normalize
     474    [ #_ cases (pm_choose A r) normalize [ cases ao [2:#a'] normalize #E destruct
     475      | #x #E destruct ]
     476    |  * * #p' #a' #t'' #IH #E destruct
     477      cases (IH ?? (refl ??)) * * #L1 #L2 #L3 #CARD
     478      % [ % [ % [ // | @L2 ]| * /2/ #q cases (L3 q) /2/ #L4 %2 @L4 ] | cases ao normalize >CARD // ]
     479    ]
     480  ]
     481] qed.
     482
     483(* Try to remove an element, return updated map if successful *)
     484
     485let rec pm_try_remove (A:Type[0]) (b:Pos) (t:positive_map A) on b : option (A × (positive_map A)) ≝
     486match b with
     487[ one ⇒
     488    match t with
     489    [ pm_leaf ⇒ None ?
     490    | pm_node x l r ⇒ option_map ?? (λx. 〈x, pm_node A (None ?) l r〉) x
     491    ]
     492| p0 tl ⇒
     493    match t with
     494    [ pm_leaf ⇒ None ?
     495    | pm_node x l r ⇒ option_map ?? (λxl. 〈\fst xl, pm_node A x (\snd xl) r〉) (pm_try_remove A tl l)
     496    ]
     497| p1 tl ⇒
     498    match t with
     499    [ pm_leaf ⇒ None ?
     500    | pm_node x l r ⇒ option_map ?? (λxr. 〈\fst xr, pm_node A x l (\snd xr)〉) (pm_try_remove A tl r)
     501    ]
     502].
     503
     504lemma pm_try_remove_none : ∀A,b,t.
     505  pm_try_remove A b t = None ? ↔ lookup_opt A b t = None ?.
     506#A #b elim b
     507[ * [ /2/ | * [ /2/ | #a #l #r % normalize #E destruct ] ]
     508| #p #IH * [ /2/ | #x #l #r % normalize cases (IH r) cases (pm_try_remove A p r)
     509  [ normalize #H #X @H | * #a #t' #_ normalize #_ #X destruct
     510  | normalize // | * #a #t' normalize #A #B #C lapply (B C) #E destruct
     511  ] ]
     512| #p #IH * [ /2/ | #x #l #r % normalize cases (IH l) cases (pm_try_remove A p l)
     513  [ normalize #H #X @H | * #a #t' #_ normalize #_ #X destruct
     514  | normalize // | * #a #t' normalize #A #B #C lapply (B C) #E destruct
     515  ] ]
     516] qed.
     517
     518lemma pm_try_remove_some : ∀A,p,t,a,t'.
     519  pm_try_remove A p t = Some ? 〈a,t'〉 →
     520  lookup_opt A p t = Some A a ∧
     521  lookup_opt A p t' = None A ∧
     522  (∀q. p = q ∨ lookup_opt A q t = lookup_opt A q t') ∧
     523  |t| = S (|t'|).
     524#A #p elim p
     525[ * [ #a #t' #E normalize in E; destruct
     526    | * [ #l #r #a #t' #E normalize in E; destruct
     527        | #a' #l #r #a #t' #E normalize in E; destruct % [ % [ % // | * /2/ ]| // ]
     528        ]
     529    ]
     530| #p' #IH *
     531  [ #a #t' #E normalize in E; destruct
     532  | #x #l #r #a #t' whd in ⊢ (??%? → ?);
     533    lapply (IH r) cases (pm_try_remove A p' r) [ #_ #E normalize in E; destruct ]
     534    * #a' #r' #H #E whd in E:(??%?); destruct
     535    cases (H a r' (refl ??)) * * #L1 #L2 #L3 #CARD
     536    @conj try @conj try @conj
     537    [ @L1 | @L2 | * /2/ #q cases (L3 q) [ /2/ | #E %2 @E ] | cases x normalize >CARD // ]
     538  ]
     539| #p' #IH *
     540  [ #a #t' #E normalize in E; destruct
     541  | #x #l #r #a #t' whd in ⊢ (??%? → ?);
     542    lapply (IH l) cases (pm_try_remove A p' l) [ #_ #E normalize in E; destruct ]
     543    * #a' #l' #H #E whd in E:(??%?); destruct
     544    cases (H a l' (refl ??)) * * #L1 #L2 #L3 #CARD
     545    @conj try @conj try @conj
     546    [ @L1 | @L2 | * /2/ #q cases (L3 q) [ /2/ | #E %2 @E ] | cases x normalize >CARD // ]
     547  ]
     548] qed.
     549
     550
     551
Note: See TracChangeset for help on using the changeset viewer.