Ignore:
Timestamp:
Aug 29, 2011, 5:45:03 PM (8 years ago)
Author:
campbell
Message:

Extra results for non-failing map updates.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch/common/Identifiers.ma

    r1105 r1134  
    33include "ASM/Arithmetic.ma".
    44include "common/Errors.ma".
     5include "utilities/option.ma".
    56
    67(* identifiers and their generators are tagged to differentiate them, and to
     
    157158
    158159(* A predicate that an identifier is in a map, and a failure-avoiding lookup
    159    using it. *)
     160   and update using it. *)
    160161
    161162definition present : ∀tag,A. identifier_map tag A → identifier tag → Prop ≝
     
    166167cases H #H'  cases (H' (refl ??)) qed.
    167168
     169definition update_present : ∀tag,A. ∀m:identifier_map tag A. ∀id. present ?? m id → A → identifier_map tag A ≝
     170λtag,A,m,l,p,a.
     171  let l' ≝ match l with [ an_identifier l' ⇒ l' ] in
     172  let m' ≝ match m with [ an_id_map m' ⇒ m' ] in
     173  let u' ≝ update A 16 l' a m' in
     174  match u' return λx. update ????? = x → ? with
     175  [ None ⇒ λE.⊥
     176  | Some m' ⇒ λ_. an_id_map tag A m'
     177  ] (refl ? u').
     178whd in p; whd in p:(?(??%?)) E:(??(???%?%)?);
     179cases l in p E; cases m; -l' -m' #m' #l' whd in ⊢ (?(??(???%%)?) → ??(???%?%)? → ?)
     180#NL #U cases NL #H @H @(update_fail … U)
     181qed.
     182
     183lemma update_still_present : ∀tag,A,m,id,a,id'.
     184  ∀H:present tag A m id.
     185  ∀H':present tag A m id'.
     186  present tag A (update_present tag A m id' H' a) id.
     187#tag #A * #m * #id #a * #id' #H #H'
     188whd whd in ⊢ (?(??(???(%??????)?)?)) normalize nodelta
     189cases (identifier_eq ? (an_identifier tag id) (an_identifier tag id'))
     190[ #E >E @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)) >(update_lookup_opt_same ?????? U)
     191  % #E' destruct
     192| #NE @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)) whd in ⊢ (?(??(???%%)?))
     193  <(update_lookup_opt_other ?????? U id) [ @H | % #E cases NE >E #H @H @refl ]
     194] qed.
    168195
    169196(* Sets *)
Note: See TracChangeset for help on using the changeset viewer.