Changeset 1928 for src/common


Ignore:
Timestamp:
May 9, 2012, 1:36:35 PM (8 years ago)
Author:
mulligan
Message:

Moved code from in ASM/ASMCosts*.ma and ASM/CostsProof.ma that should rightfully be in another file. Added a new file, ASM/UtilBranch.ma for code that should rightfully be in ASM/Util.ma but is incomplete (i.e. daemons).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Identifiers.ma

    r1908 r1928  
    308308  <(update_lookup_opt_other ????? U id) [ @H | % #E cases NE >E #H @H @refl ]
    309309] qed.
     310
     311lemma lookup_present_add_hit:
     312  ∀tag, A, map, k, v, k_pres.
     313    lookup_present tag A (add … map k v) k k_pres = v.
     314  #tag #a #map #k #v #k_pres
     315  lapply (lookup_lookup_present … (add … map k v) … k_pres)
     316  >lookup_add_hit #Some_assm destruct(Some_assm)
     317  <e0 %
     318qed.
     319
     320lemma lookup_present_add_miss:
     321  ∀tag, A, map, k, k', v, k_pres', k_pres''.
     322    k' ≠ k →
     323      lookup_present tag A (add … map k v) k' k_pres' = lookup_present tag A map k' k_pres''.
     324  #tag #A #map #k #k' #v #k_pres' #k_pres'' #neq_assm
     325  lapply (lookup_lookup_present … (add … map k v) ? k_pres')
     326  >lookup_add_miss try assumption
     327  #Some_assm
     328  lapply (lookup_lookup_present … map k') >Some_assm #Some_assm'
     329  lapply (Some_assm' k_pres'') #Some_assm'' destruct assumption
     330qed.
     331
     332lemma present_add_present:
     333  ∀tag, a, map, k, k', v.
     334    k' ≠ k →
     335      present tag a (add tag a map k v) k' →
     336        present tag a map k'.
     337  #tag #a #map #k #k' #v #neq_hyp #present_hyp
     338  whd in match present; normalize nodelta
     339  whd in match present in present_hyp; normalize nodelta in present_hyp;
     340  cases (not_None_to_Some a … present_hyp) #v' #Some_eq_hyp
     341  lapply (lookup_add_cases tag ?????? Some_eq_hyp) *
     342  [1:
     343    * #k_eq_hyp @⊥ /2/
     344  |2:
     345    #Some_eq_hyp' /2/
     346  ]
     347qed.
     348
     349lemma present_add_hit:
     350  ∀tag, a, map, k, v.
     351    present tag a (add tag a map k v) k.
     352  #tag #a #map #k #v
     353  whd >lookup_add_hit
     354  % #absurd destruct
     355qed.
     356
     357lemma present_add_miss:
     358  ∀tag, a, map, k, k', v.
     359    k' ≠ k → present tag a map k' → present tag a (add tag a map k v) k'.
     360  #tag #a #map #k #k' #v #neq_assm #present_assm
     361  whd >lookup_add_miss assumption
     362qed.
    310363
    311364
Note: See TracChangeset for help on using the changeset viewer.