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/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
Note: See TracChangeset for help on using the changeset viewer.