 Timestamp:
 Jul 18, 2011, 12:44:31 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/BitVectorTrie.ma
r1070 r1074 352 352 qed. 353 353 354 lemma 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 ] 368 qed. 369 370 371 354 372 lemma lookup_opt_prepare_trie_for_insertion_hit: 355 373 ∀A:Type[0].∀v:A.∀n.∀b:BitVector n.
Note: See TracChangeset
for help on using the changeset viewer.