Changeset 2305


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.

Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/CostCheck.ma

    r2303 r2305  
    4747] qed.
    4848
    49 axiom check_sound_cost_fn : internal_function → bool.
     49include "basics/lists/listb.ma".
     50include alias "utilities/deqsets.ma".
     51
     52lemma successors_present : ∀g,st.
     53  labels_present g st →
     54  ∀l. l ∈ successors st →
     55  present ?? g l.
     56#g *
     57[ #l1 #PR #l2 #IN >(memb_single … IN) @PR
     58| #cs #l1 #PR #l2 #IN >(memb_single … IN) @PR
     59| #ty #r #c #l1 #PR #l2 #IN >(memb_single … IN) @PR
     60| #ty1 #ty2 #op #r1 #r2  #l1 #PR #l2 #IN >(memb_single … IN) @PR
     61| #ty1 #ty2 #ty3 #op #r1 #r2 #r3 #l1 #PR #l2 #IN >(memb_single … IN) @PR
     62| #ty #r1 #r2 #l1 #PR #l2 #IN >(memb_single … IN) @PR
     63| #ty #r1 #r2 #l1 #PR #l2 #IN >(memb_single … IN) @PR
     64| #id #args #dst #l1 #PR #l2 #IN >(memb_single … IN) @PR
     65| #r #args #dst #l1 #PR #l2 #IN >(memb_single … IN) @PR
     66| #r #l1 #l2 * #PR1 #PR2 #l3 whd in ⊢ (?% → ?); @eqb_elim [ // | #_ #IN >(memb_single … IN) // ]
     67| #_ #l *
     68] qed.
     69
     70include alias "common/Identifiers.ma".
     71
     72(* Check that from [checking] we reach a cost label without going through
     73   [checking_tail], which would form a loop in the CFG.  We also have a set of
     74   labels that we have still [to_check], and return an updated set of labels
     75   to check if the check for the current label is successful. *)
     76let rec check_label_bounded
     77  (g : graph statement)
     78  (CL : graph_closed g)
     79  (checking : label)
     80  (PR : present ?? g checking)
     81  (checking_tail : list label)
     82  (to_check : identifier_set LabelTag)
     83  (term_check : nat)
     84on term_check : gt term_check (id_map_size … to_check) → option (identifier_set LabelTag) ≝
     85let stop_now ≝ Some ? to_check in
     86match term_check return λx. ge x ? → ? with
     87[ O ⇒ λH.⊥
     88| S term_check' ⇒ λH.
     89  let st ≝ lookup_present … g checking PR in
     90  let succs ≝ successors st in
     91  match succs return λsc. (∀l.l∈sc → ?) → ? with
     92  [ nil ⇒ λ_. stop_now
     93  | cons h t ⇒
     94    match t with
     95    [ nil ⇒ λSC. (* single successor *)
     96      match try_remove … to_check h return λx. (∀a,m'. x = ? → ?) → ? with
     97      [ Some to_check' ⇒ λH'.
     98        if h ∈ checking_tail then None ? else
     99        let PR' ≝ ? in
     100        let st' ≝ lookup_present … g h PR' in
     101        if is_cost_label st' then stop_now else
     102          check_label_bounded g CL h PR' (checking::checking_tail) (\snd to_check') term_check' ?
     103      | None ⇒ λ_. stop_now (* already checked successor *)
     104      ] (try_remove_some_card … to_check h)
     105    | cons _ _ ⇒ λ_. stop_now (* all branches are followed by a cost label *)
     106    ]
     107  ] (successors_present g st (CL … checking … (lookup_lookup_present …)))
     108].
     109[ /2 by absurd/
     110| lapply (H' (\fst to_check') (\snd to_check') ?) [ cases to_check' // ]
     111  #E -PR' >E in H; #H' /2/
     112| @SC >memb_hd //
     113] qed.
     114
     115(* An inductive specification of the above function that's easier to work with. *)
     116
     117inductive check_label_bounded_spec (g:graph statement) : label → list label → identifier_set LabelTag → identifier_set LabelTag → Prop ≝
     118| clbs_ret : ∀l,PR,tl,toch.
     119    successors (lookup_present … g l PR) = [ ] →
     120    check_label_bounded_spec g l tl toch toch
     121| clbs_checked : ∀l,PR,l',tl,toch.
     122    successors (lookup_present … g l PR) = [l'] →
     123    ¬ l' ∈ toch →
     124    check_label_bounded_spec g l tl toch toch
     125| clbs_cost : ∀l,PR,l',PR',tl,toch.
     126    successors (lookup_present … g l PR) = [l'] →
     127    l' ∈ toch →
     128    is_cost_label (lookup_present … g l' PR') →
     129    check_label_bounded_spec g l tl toch toch
     130| clbs_step : ∀l,PR,l',PR',tl,toch,toch',toch''.
     131    successors (lookup_present … g l PR) = [l'] →
     132(*    l' ∈ toch → implied *)
     133    ¬ l' ∈ tl →
     134    ¬ is_cost_label (lookup_present … g l' PR') →
     135    try_remove … toch l' = Some ? 〈it,toch'〉 →
     136    check_label_bounded_spec g l' (l::tl) toch' toch'' →
     137    check_label_bounded_spec g l tl toch toch''
     138| clbs_branch : ∀l,PR,x,y,zs,tl,toch.  (* the other check will show that these are cost labels *)
     139    successors (lookup_present … g l PR) = x::y::zs →
     140    check_label_bounded_spec g l tl toch toch.
     141
     142(* TODO: move (or is it somewhere already?) *)
     143lemma if_elim : ∀T:Type[0]. ∀b:bool. ∀e1,e2:T. ∀P:T → Type[0].
     144  (b → P e1) →
     145  (¬b → P e2) →
     146  P (if b then e1 else e2).
     147#T * /2/
     148qed.
     149
     150lemma check_label_bounded_s : ∀term_check,g,CL,checking,PR,checking_tail,to_check,TERM,to_check'.
     151  check_label_bounded g CL checking PR checking_tail to_check term_check TERM = Some ? to_check' →
     152  check_label_bounded_spec g checking checking_tail to_check to_check'.
     153#n elim n
     154[ #a #b #c #d #d #e #g @⊥ /3 by n_plus_1_n_to_False, div_plus_times/ (* ! *)
     155| #term_check #IH #g #CL #checking #PR #checking_tail #to_check #TERM #to_check'
     156  whd in ⊢ (??%? → ?);
     157  generalize in ⊢ (??(?%)? → ?);
     158  lapply (refl ? (successors (lookup_present … PR)))
     159  cases (successors (lookup_present … PR)) in ⊢ (???% → %);
     160  [ #SUCC whd in ⊢ (? → ??%? → ?); #_ #E destruct %1 //
     161  | #h * [ #SUCC whd in ⊢ (? → ??%? → ?); #PR' generalize in ⊢ (??(?%)? → ?);
     162           lapply (refl ? (try_remove … to_check h))
     163           cases (try_remove ????) in ⊢ (???% → %);
     164           [ #RM whd in ⊢ (? → ??%? → ?); #H #E destruct @(clbs_checked … SUCC)
     165             whd in ⊢ (?(?%)); >(proj1 … (try_remove_empty …) RM) //
     166           | * * #to_check'' #RM #H whd in ⊢ (??%? → ?);
     167             @if_elim
     168             [ #IN whd in ⊢ (??%? → ?); #E destruct
     169             | #OUT whd in ⊢ (??%? → ?);
     170               @if_elim
     171               [ #CS #E destruct @(clbs_cost … SUCC … CS)
     172                 cases (try_remove_some ?????? RM) * #L #_ #_ whd in ⊢ (?%); >L //
     173               | #CS #H @(clbs_step … SUCC OUT CS RM) @(IH … H)
     174               ]
     175             ]
     176           ]
     177         | #h2 #t #SUCCS whd in ⊢ (? → ??%? → ?); #PR' #E destruct
     178           @(clbs_branch … SUCCS)
     179         ]
     180  ]
     181] qed.
     182
     183
     184
     185lemma check_label_bounded_subset : ∀g,checking,checking_tail,to_check,to_check'.
     186  check_label_bounded_spec g checking checking_tail to_check to_check' →
     187  set_subset … to_check' to_check.
     188#g #lX #lX' #tX #tX' #S elim S //
     189#l #PR #l' #PR' #tl #toch #toch' #toch'' #SC #NI #CS #RM #H #IH
     190cases (try_remove_some … toch' RM) * #L1 #L2 #L3
     191#id #IN cases (L3 id)
     192[ #E destruct whd in ⊢ (?%); >L1 //
     193| #L4 whd in ⊢ (?%); >L4 @IH @IN
     194] qed.
     195
     196let rec check_graph_bounded
     197  (g : graph statement)
     198  (CL : graph_closed g)
     199  (to_check : identifier_set LabelTag)
     200  (SUB : set_subset … to_check g)
     201  (start : label)
     202  (PR : present ?? g start)
     203  (SMALLER : gt (id_map_size … g) (id_map_size … to_check))
     204  (term_check : nat)
     205on term_check : gt term_check (id_map_size … to_check) → bool ≝
     206match term_check return λx. ge x ? → bool with
     207[ O ⇒ λH.⊥
     208| S term_check' ⇒ λH.
     209  let TERM' ≝ ? in
     210  match check_label_bounded g CL start PR [ ] to_check (id_map_size … g) TERM' return λx. check_label_bounded ???????? = x → ? with
     211  [ None ⇒ λ_. false
     212  | Some to_check' ⇒ λH'.
     213    match choose … to_check' return λx. (∀id,a,m'. x = ? → ?) → (∀id,a,m'. x = ? → ?) → (∀id,a,m'. x = ? → ?) → ? with
     214    [ None ⇒ λ_.λ_.λ_. true
     215    | Some l_to_check'' ⇒ λL,SUB',C.
     216        check_graph_bounded g CL (\snd l_to_check'') ? (\fst (\fst l_to_check'')) ?? term_check' ?
     217    ] (choose_some … to_check') (choose_some_subset … to_check') (choose_some_card … to_check')
     218  ] (refl ??)
     219].
     220[ 2,3,4,5: cases l_to_check'' in C L SUB' ⊢ %; * #l * #to_check'' #C #L #SUB'
     221  lapply (check_label_bounded_subset … (check_label_bounded_s … H')) #SUB''
     222]
     223[ #id #IN @SUB @SUB'' @(SUB' ??? (refl ??)) @IN
     224| @member_present @SUB @SUB'' cases (L ??? (refl ??)) * #L #_ #_ whd in ⊢ (?%); >L //
     225| whd <(C ??? (refl ??)) lapply (subset_card … SUB'') #Z @(transitive_le … Z) /2/
     226| whd <(C ??? (refl ??)) lapply (subset_card … SUB'') #Z @(transitive_le … Z) /2/
     227| /2/
     228| @SMALLER
     229] qed.
     230
     231(* TODO: move *)
     232definition id_set_of_map : ∀tag,A. identifier_map tag A → identifier_set tag ≝
     233λtag,A,m. an_id_map tag unit (map … (λ_. it) (match m with [ an_id_map m' ⇒ m'])).
     234
     235lemma id_set_of_map_subset : ∀tag,A,m.
     236  id_set_of_map tag A m ⊆ m.
     237#tag #A * #m * #id normalize
     238>lookup_opt_map normalize cases (lookup_opt ???) //
     239qed.
     240
     241lemma id_set_of_map_present : ∀tag,A,m,id.
     242  present tag A m id ↔ present tag unit (id_set_of_map … m) id.
     243#tag #A * #m * #id %
     244normalize @not_to_not
     245>lookup_opt_map cases (lookup_opt ???) normalize //
     246#a #E destruct
     247qed.
     248
     249lemma id_set_of_map_card : ∀tag,A,m.
     250  |m| = |id_set_of_map tag A m|.
     251#tag #A * #m whd in ⊢ (??%%); >map_size //
     252qed.
     253
     254definition check_sound_cost_fn : internal_function → bool ≝
     255λfn.
     256  match try_remove … (id_set_of_map … (f_graph fn)) (f_entry fn) return λx. (x = ? → ?) → (∀a,m'. x = ? → ?) → (∀a,m'. x = ? → ?) → ? with
     257  [ None ⇒ λEMP. ⊥
     258  | Some to_check ⇒ λ_.λCARD,L.
     259              check_graph_bounded (f_graph fn) (f_closed fn) (\snd to_check) ? (f_entry fn) ?? (|f_graph fn|) ?
     260  ] (proj1 ?? (try_remove_empty LabelTag unit (id_set_of_map … (f_graph fn)) (f_entry fn)))
     261    (try_remove_some_card ????)
     262    (try_remove_some ????).
     263[ cases (f_entry fn) in EMP; #l #PR cases (proj1 … (id_set_of_map_present …) PR) #PR' #H
     264  @PR' @H %
     265| cases to_check in L ⊢ %; * #m' #L cases (L … (refl ??)) * #L1 #L2 #L3 #id #IN
     266  cases (L3 id)
     267  [ #E destruct whd in ⊢ (?%); cases (f_entry fn) #l * cases (lookup ????) /2/
     268  | #E whd in ⊢ (?%); lapply (id_set_of_map_present … (f_graph fn) id) *
     269    whd in match (present ????); whd in match (present ? unit ??);
     270    lapply (member_present … IN) whd in match (present ? unit ??); <E
     271    cases (lookup … (f_graph fn) id) // #X #_ #Y @⊥ cases (Y X) /2/
     272  ]
     273| cases (f_entry fn) //
     274| 4,5: <id_set_of_map_card in CARD; cases to_check * #m' #CARD >(CARD ?? (refl ??)) //
     275] qed.
     276
    50277axiom check_sound_cost_fn_ok : ∀fn. bool_to_Prop (check_sound_cost_fn fn) ↔ soundly_labelled_fn fn.
    51278
  • src/common/Identifiers.ma

    r2303 r2305  
    891891| #EQ >EQ * #ABS @ABS %
    892892] qed.
     893
     894
     895(* Attempt to choose an entry in the map/set, and if successful return the entry
     896   and the map/set without it. *)
     897
     898definition choose : ∀tag,A. identifier_map tag A → option (identifier tag × A × (identifier_map tag A)) ≝
     899λtag,A,m.
     900  match pm_choose A (match m with [ an_id_map m' ⇒ m' ]) with
     901  [ None ⇒ None ?
     902  | Some x ⇒ Some ? 〈〈an_identifier tag (\fst (\fst x)), \snd (\fst x)〉, an_id_map tag A (\snd x)〉
     903  ].
     904
     905lemma choose_empty : ∀tag,A,m.
     906  choose tag A m = None ? ↔ ∀id. lookup tag A m id = None ?.
     907#tag #A * #m lapply (pm_choose_empty A m) * #H1 #H2 %
     908[ normalize #C * @H1 cases (pm_choose A m) in C ⊢ %; [ // | normalize #x #E destruct ]
     909| normalize #L lapply (pm_choose_empty A m) cases (pm_choose A m)
     910  [ * #H1 #H2 normalize // | #x * #_ #H lapply (H ?) [ #p @(L (an_identifier ? p)) | #E destruct ] ]
     911] qed.
     912
     913lemma choose_some : ∀tag,A,m,id,a,m'.
     914  choose tag A m = Some ? 〈〈id,a〉,m'〉 →
     915  lookup tag A m id = Some A a ∧
     916  lookup tag A m' id = None A ∧
     917  (∀id'. id = id' ∨ lookup tag A m id' = lookup tag A m' id').
     918#tag #A * #m * #id #a * #m' #C
     919lapply (pm_choose_some A m id a m' ?)
     920[ whd in C:(??%?); cases (pm_choose A m) in C ⊢ %; normalize [ #E destruct | * * #x #y #z #E destruct % ] ]
     921* * * #L1 #L2 #L3 #_
     922% [ % [ @L1 | @L2 ] | * #id' cases (L3 id') [ /2/ | #L4 %2 @L4 ] ]
     923qed.
     924
     925lemma choose_some_subset : ∀tag,A,m,id,a,m'.
     926  choose tag A m = Some ? 〈〈id,a〉,m'〉 →
     927  m' ⊆ m.
     928#tag #A #m #id #a #m' #C
     929cases (choose_some … m' C) * #L1 #L2 #L3
     930#id' whd in ⊢ (?% → ?%);
     931cases (L3 id')
     932[ #E destruct >L2 *
     933| #L4 >L4 //
     934] qed.
     935
     936lemma choose_some_card : ∀tag,A,m,id,a,m'.
     937  choose tag A m = Some ? 〈〈id,a〉,m'〉 →
     938  |m| = S (|m'|).
     939#tag #A * #m * #id #a * #m' #C
     940lapply (pm_choose_some A m id a m' ?)
     941[ whd in C:(??%?); cases (pm_choose A m) in C ⊢ %; normalize [ #E destruct | * * #x #y #z #E destruct % ] ]
     942* #_ #H @H
     943qed.
     944
     945(* Remove an element from a map/set, returning the element and a new map/set. *)
     946
     947definition try_remove : ∀tag,A. identifier_map tag A → identifier tag → option (A × (identifier_map tag A)) ≝
     948λtag,A,m,id.
     949  match pm_try_remove A (match id with [ an_identifier id' ⇒ id']) (match m with [ an_id_map m' ⇒ m' ]) with
     950  [ None ⇒ None ?
     951  | Some x ⇒ Some ? 〈\fst x, an_id_map tag A (\snd x)〉
     952  ].
     953
     954lemma try_remove_empty : ∀tag,A,m,id.
     955  try_remove tag A m id = None ? ↔ lookup tag A m id = None ?.
     956#tag #A * #m * #id lapply (pm_try_remove_none A id m) * #H1 #H2 %
     957[ normalize #C @H1 cases (pm_try_remove A id m) in C ⊢ %; [ // | normalize #x #E destruct ]
     958| normalize #L >H2 //
     959] qed.
     960
     961lemma try_remove_some : ∀tag,A,m,id,a,m'.
     962  try_remove tag A m id = Some ? 〈a,m'〉 →
     963  lookup tag A m id = Some A a ∧
     964  lookup tag A m' id = None A ∧
     965  (∀id'. id = id' ∨ lookup tag A m id' = lookup tag A m' id').
     966#tag #A * #m * #id #a * #m' #C
     967lapply (pm_try_remove_some A id m a m' ?)
     968[ whd in C:(??%?); cases (pm_try_remove A id m) in C ⊢ %; normalize [ #E destruct | * #x #y #E destruct % ] ]
     969* * * #L1 #L2 #L3 #_
     970% [ % [ @L1 | @L2 ] | * #id' cases (L3 id') [ /2/ | #L4 %2 @L4 ] ]
     971qed.
     972
     973lemma try_remove_some_card : ∀tag,A,m,id,a,m'.
     974  try_remove tag A m id = Some ? 〈a,m'〉 →
     975  |m| = S (|m'|).
     976#tag #A * #m * #id #a * #m' #C
     977lapply (pm_try_remove_some A id m a m' ?)
     978[ whd in C:(??%?); cases (pm_try_remove A id m) in C ⊢ %; normalize [ #E destruct | * #x #y #E destruct % ] ]
     979* #_ #H @H
     980qed.
     981 
     982
  • 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.