Ignore:
Timestamp:
Aug 30, 2012, 4:47:54 PM (8 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/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
Note: See TracChangeset for help on using the changeset viewer.