Changeset 2303 for src/common


Ignore:
Timestamp:
Aug 24, 2012, 5:41:18 PM (7 years ago)
Author:
campbell
Message:

Some preliminary checking of cost labelling properties in RTLabs.

Location:
src/common
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/common/Identifiers.ma

    r2222 r2303  
    286286          (match m with [ an_id_map m' ⇒ m' ]) [ ].
    287287
     288(* Test a predicate on all of the entries in a map.  The predicate is given a
     289   proof that the entry appears in the map. *)
     290
     291definition idmap_all : ∀tag,A. ∀m:identifier_map tag A. (∀id,a. lookup tag A m id = Some A a → bool) → bool ≝
     292λtag,A,m,f. pm_all A (match m with [ an_id_map m' ⇒ m' ])
     293                     (λp,a,H. f (an_identifier tag p) a ?).
     294cases m in H ⊢ %; #m' normalize //
     295qed.
     296
     297inductive idmap_pred_graph : ∀tag,A,m,id,a,L. ∀f:(∀id,a. lookup tag A m id = Some A a → bool). bool → Prop ≝
     298| idmappg : ∀tag,A,m,id,a,L,f. idmap_pred_graph tag A m id a L f (f id a L).
     299
     300lemma idmap_pred_irr : ∀tag,A,m,id,a,L,L'. ∀f:(∀id,a. lookup tag A m id = Some A a → bool).
     301  f id a L = f id a L'.
     302#tag #A #m #id #a #L #L' #f
     303cut (idmap_pred_graph tag A m id a L f (f id a L)) [ % ]
     304cases (f id a L) #H
     305cut (idmap_pred_graph tag A m id a L' f ?) [ 2,5: @H | 1,4: skip ] * //
     306qed.
     307
     308lemma idmap_all_ok : ∀tag,A,m,f.
     309  bool_to_Prop (idmap_all tag A m f) ↔ (∀id,a,H. f id a H).
     310#tag #A * #m #f
     311whd in match (idmap_all ????); @(iff_trans … (pm_all_ok …)) %
     312[ #H * #id #a #PR lapply (H id a PR) #X @eq_true_to_b <X @idmap_pred_irr
     313| #H #p #a #PR @H
     314] qed.
     315
     316
    288317axiom MissingId : String.
    289318
     
    318347] qed.
    319348
    320 include "ASM/Util.ma".
    321 
    322349definition lookup_present : ∀tag,A. ∀m:identifier_map tag A. ∀id. present ?? m id → A ≝
    323350λtag,A,m,id. match lookup ?? m id return λx. x ≠ None ? → ? with [ Some a ⇒ λ_. a | None ⇒ λH.⊥ ].
     
    332359| #a #H @refl
    333360] qed.
     361
     362lemma lookup_is_present : ∀tag,T,m,id,t.
     363  lookup tag T m id = Some T t →
     364  present ?? m id.
     365#tag #T #m #id #t #L normalize >L % #E destruct
     366qed.
     367
     368lemma lookup_present_eq : ∀tag,T,m,id,t.
     369  lookup tag T m id = Some T t →
     370  ∀H. lookup_present tag T m id H = t.
     371#tag #T #m #id #t #L #H
     372lapply (lookup_lookup_present … H) >L #E destruct %
     373qed.
     374
    334375
    335376definition update_present : ∀tag,A. ∀m:identifier_map tag A. ∀id. present ?? m id → A → identifier_map tag A ≝
  • src/common/PositiveMap.ma

    r2104 r2303  
    11include "basics/types.ma".
    22include "utilities/binary/positive.ma".
     3include "ASM/Util.ma". (* bool_to_Prop *)
    34
    45inductive positive_map (A:Type[0]) : Type[0] ≝
     
    292293|*: #p #Hi #a * [2,4: * [2,4: #x] #l #r] normalize >Hi //
    293294] qed.
     295
     296(* Testing all of the entries with a boolean predicate, where the predicate
     297   is given a proof that the entry is in the map. *)
     298
     299let rec pm_all_aux (A:Type[0]) (m,t:positive_map A) (pre:Pos → Pos) on t : (∀p. lookup_opt A (pre p) m = lookup_opt A p t) → (∀p,a.lookup_opt A p m = Some A a → bool) → bool ≝
     300match t return λt. (∀p. lookup_opt A (pre p) m = lookup_opt A p t) → (∀p,a.lookup_opt A p m = Some A a → bool) → bool with
     301[ pm_leaf ⇒ λ_.λ_. true
     302| pm_node a l r ⇒ λH,f.
     303    pm_all_aux A m l (λx. pre (p0 x)) ? f ∧
     304    ((match a return λa. (∀p. ? = lookup_opt A p (pm_node ? a ??)) → ? with [ None ⇒ λ_. true | Some a' ⇒ λH. f (pre one) a' ? ]) H) ∧
     305    pm_all_aux A m r (λx. pre (p1 x)) ? f
     306].
     307[ >H %
     308| #p >H %
     309| #p >H %
     310] qed.
     311
     312definition pm_all : ∀A. ∀m:positive_map A. (∀p,a. lookup_opt A p m = Some A a → bool) → bool ≝
     313λA,m,f. pm_all_aux A m m (λx.x) (λp. refl ??) f.
     314
     315(* Proof irrelevance doesn't seem to apply to arbitrary variables, but we can
     316   use the function graph to show that it's fine. *)
     317   
     318inductive pm_all_pred_graph : ∀A,m,p,a,L. ∀f:∀p:Pos.∀a:A.lookup_opt A p m=Some A a→bool. bool → Prop ≝
     319| pmallpg : ∀A,m,p,a,L. ∀f:∀p:Pos.∀a:A.lookup_opt A p m=Some A a→bool. pm_all_pred_graph A m p a L f (f p a L).
     320
     321lemma pm_all_pred_irr : ∀A,m,p,a,L,L'.
     322 ∀f:∀p:Pos.∀a:A.lookup_opt A p m=Some A a→bool.
     323 f p a L = f p a L'.
     324#A #m #p #a #L #L' #f
     325cut (pm_all_pred_graph A m p a L f (f p a L)) [ % ]
     326cases (f p a L) #H cut (pm_all_pred_graph A m p a L' f ?) [2,5: @H | 1,4: skip]
     327* //
     328qed.
     329
     330lemma pm_all_aux_ok_aux : ∀A,m,t,pre,H,f,a,L.
     331  pm_all_aux A m t pre H f →
     332  lookup_opt A one t = Some A a →
     333  f (pre one) a L.
     334#A #m *
     335[ #pre #H #f #a #L #H #L' normalize in L'; destruct
     336| * [ #l #r #pre #H #f #a #L #H' #L' normalize in L'; destruct
     337    | #a' #l #r #pre #H #f #a #L #AUX #L' normalize in L'; destruct
     338      cases (andb_Prop_true … AUX) #AUX' cases (andb_Prop_true … AUX')
     339      #_ #HERE #_ whd in HERE:(?%); @eq_true_to_b <HERE @pm_all_pred_irr
     340    ]
     341] qed.
     342
     343lemma pm_all_aux_ok : ∀A,m,t,pre,H,f.
     344  bool_to_Prop (pm_all_aux A m t pre H f) ↔ (∀p,a,H. f (pre p) a H).
     345#A #m #t #pre #H #f %
     346[ #H' #p generalize in match pre in H H' ⊢ %; -pre generalize in match t; elim p
     347  [ #t #pre #H #H' #a #L lapply (refl ? (Some A a)) <L in ⊢ (??%? → ?); >H @pm_all_aux_ok_aux //
     348  | #q #IH * [ #pre #H #H' #a #L @⊥ >H in L; normalize #E destruct
     349             | #x #l #r #pre #H #H' #a #L @(IH r)
     350               [ #x >H % | cases (andb_Prop_true … H') #_ // ]
     351             ]
     352  | #q #IH * [ #pre #H #H' #a #L @⊥ >H in L; normalize #E destruct
     353             | #x #l #r #pre #H #H' #a #L @(IH l)
     354               [ #x >H % | cases (andb_Prop_true … H') #H'' cases (andb_Prop_true … H'') // ]
     355             ]
     356  ]
     357| #H' generalize in match pre in H H' ⊢ %; -pre elim t
     358  [ //
     359  | * [2:#x] #l #r #IHl #IHr #pre #H #H' @andb_Prop
     360    [ 1,3: @andb_Prop
     361      [ 1,3: @IHl //
     362      | @(H' one x)
     363      | %
     364      ]
     365    | 2,4: @IHr //
     366    ]
     367  ]
     368] qed.
     369
     370lemma pm_all_ok : ∀A,m,f.
     371  bool_to_Prop (pm_all A m f) ↔ (∀p,a,H. f p a H).
     372#A #m #f @pm_all_aux_ok
     373qed.
     374
Note: See TracChangeset for help on using the changeset viewer.