Changeset 1134


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

Extra results for non-failing map updates.

Location:
Deliverables/D3.3/id-lookup-branch
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch/ASM/BitVectorTrie.ma

    r1074 r1134  
    524524 ]
    525525qed.   
     526
     527lemma update_fail : ∀A,n,b,a,t.
     528  update A n b a t = None ? →
     529  lookup_opt A n b t = None ?.
     530#A #n elim n
     531[ #b @(vector_inv_n … b) #a #t cases (BitVectorTrie_O … t)
     532  [ * #x #E >E normalize #NE destruct
     533  | #E >E normalize //
     534  ]
     535| #m #IH #b @(vector_inv_n … b) #hd #tl #a #t cases (BitVectorTrie_Sn … t)
     536  [ * #t1 * #t2 #E >E cases hd whd in ⊢ (??%? → ??%?)
     537    #X lapply (option_map_none … X) @IH
     538  | #E >E normalize //
     539  ]
     540] qed.
     541
     542lemma update_lookup_opt_same : ∀A,n,b,a,t,t'.
     543  update A n b a t = Some ? t' →
     544  lookup_opt A n b t' = Some ? a.
     545#A #n elim n
     546[ #b #a #t #t' @(vector_inv_n … b)
     547  cases (BitVectorTrie_O … t)
     548  [ * #x #E >E normalize #E' destruct @refl
     549  | #E >E normalize #E' destruct
     550  ]
     551| #m #IH #b #a #t #t'
     552  @(vector_inv_n … b) #bhd #btl
     553  cases (BitVectorTrie_Sn … t)
     554  [ * #t1 * #t2 #E' >E'
     555    whd in ⊢ (??%? → ??%?) cases bhd #U
     556    cases (option_map_some ????? U)
     557    #tn' * #U' #E'' <E''
     558    whd in ⊢ (??%?) whd in ⊢ (??(???%%)?)
     559    @(IH … U')
     560  | #E >E normalize #E' destruct
     561  ]
     562] qed.
     563
     564lemma update_lookup_opt_other : ∀A,n,b,a,t,t'.
     565  update A n b a t = Some ? t' →
     566  ∀b'. b ≠ b' →
     567  lookup_opt A n b' t = lookup_opt A n b' t'.
     568#A #n elim n
     569[ #b #a #t #t' #E #b'
     570  @(vector_inv_n … b) @(vector_inv_n … b')
     571  * #NE cases (NE (refl ??))
     572| #m #IH #b #a #t #t'
     573  @(vector_inv_n … b) #bhd #btl
     574  cases (BitVectorTrie_Sn … t)
     575  [ * #t1 * #t2 #E >E whd in ⊢ (??%? → ?) cases bhd
     576    #U cases (option_map_some ????? U) #tn' * #U' #E' <E'
     577    #b' @(vector_inv_n … b') #bhd' #btl'
     578    cases bhd'
     579    [ 2,3: #_ @refl
     580    | *: #NE whd in ⊢ (??%%) whd in ⊢ (??(???%%)(???%%))
     581         @(IH … U') % #E'' >E'' in NE * #H @H @refl
     582    ]
     583  | #E >E whd in ⊢ (??%? → ?) #NE destruct
     584  ]
     585] qed.
     586
  • 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 *)
  • Deliverables/D3.3/id-lookup-branch/utilities/option.ma

    r761 r1134  
    33definition option_map : ∀A,B:Type[0]. (A → B) → option A → option B ≝
    44λA,B,f,o. match o with [ None ⇒ None B | Some a ⇒ Some B (f a) ].
     5
     6lemma option_map_none : ∀A,B,f,x.
     7  option_map A B f x = None B → x = None A.
     8#A #B #f * [ // | #a #E whd in E:(??%?); destruct ]
     9qed.
     10
     11lemma option_map_some : ∀A,B,f,x,v.
     12  option_map A B f x = Some B v → ∃y. x = Some ? y ∧ f y = v.
     13#A #B #f *
     14[ #v normalize #E destruct
     15| #y #v normalize #E %{y} destruct % //
     16] qed.
     17
     18lemma refute_none_by_refl : ∀A,B:Type[0]. ∀P:A → B. ∀Q:B → Type[0]. ∀x:option A. ∀H:x = None ? → False.
     19  (∀v. x = Some ? v → Q (P v)) →
     20  Q (match x return λy.x = y → ? with [ Some v ⇒ λ_. P v | None ⇒ λE. match H E in False with [ ] ] (refl ? x)).
     21#A #B #P #Q *
     22[ #H cases (H (refl ??))
     23| #a #H #p normalize @p @refl
     24] qed.
     25
Note: See TracChangeset for help on using the changeset viewer.