Changeset 1074


Ignore:
Timestamp:
Jul 18, 2011, 12:44:31 PM (8 years ago)
Author:
boender
Message:
  • added lookup lemma
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/BitVectorTrie.ma

    r1070 r1074  
    352352qed.
    353353
     354lemma lookup_lookup_opt:
     355  ∀A.∀n.∀b.∀t.∀x,a.
     356  lookup A n b t x = a → x ≠ a → lookup_opt A n b t = Some A a.
     357 #A #n #b #t #x #a generalize in match (refl ? n) elim t in b ⊢ (???% → ? → ?)
     358 [ #z #B #_ #H #Hx >(BitVector_O B) in H; normalize #H >H @refl
     359 | #h #l #r #Hl #Hr #B #_ #H #Hx cases (BitVector_Sn h B) #hd #X elim X; -X #tl #HB
     360   >HB >HB in H; cases hd
     361   [ normalize #H >(Hr tl (refl ? h) H Hx) @refl
     362   | normalize #H >(Hl tl (refl ? h) H Hx) @refl
     363   ]
     364 | #n #B #_ #H #Hx cases B in H;
     365   [ normalize #Hx' | #n' #b #v normalize #Hx' ]
     366   @⊥ @(absurd (eq ? x a)) [1,3: @Hx' |2,4: @Hx ]
     367 ]
     368qed.
     369
     370 
     371 
    354372lemma lookup_opt_prepare_trie_for_insertion_hit:
    355373 ∀A:Type[0].∀v:A.∀n.∀b:BitVector n.
Note: See TracChangeset for help on using the changeset viewer.