Changeset 1393 for src/ASM/BitVectorTrie.ma
 Timestamp:
 Oct 17, 2011, 3:50:50 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/BitVectorTrie.ma
r1316 r1393 338 338 qed. 339 339 340 lemma lookup_opt_lookup: 340 lemma lookup_opt_lookup_miss: 341 ∀A:Type[0].∀n:nat.∀b:BitVector n.∀t:BitVectorTrie A n.∀a:A. 342 lookup_opt A n b t = None A → ∀x.lookup A n b t x = x. 343 #A #n #b #t #a generalize in match (refl ? n) elim t in b ⊢ (???% → ??(??%%%)? → ? → ?) 344 [ #a #B #_ #H #x normalize in H; >(BitVector_O B) normalize destruct 345  #h #l #r #Hl #Hr #b #_ #H #x cases (BitVector_Sn h b) #hd #X elim X X; #tl #Hb 346 >Hb >Hb in H; cases hd 347 [ normalize #Hlookup @(Hr ? (refl ? h)) @Hlookup 348  normalize #Hlookup @(Hl ? (refl ? h)) @Hlookup 349 ] 350  #n #B #_ #H #x @lookup_stub 351 ] 352 qed. 353 354 lemma lookup_opt_lookup_hit: 341 355 ∀A:Type[0].∀n:nat.∀b:BitVector n.∀t:BitVectorTrie A n.∀a:A. 342 356 lookup_opt A n b t = Some A a → ∀x.lookup A n b t x = a. 343 357 #A #n #b #t #a generalize in match (refl ? n) elim t in b ⊢ (???% → ??(??%%%)? → ? → ?) 344 358 [ #a #B #_ #H #x normalize in H; >(BitVector_O B) normalize destruct @refl 345  #h #l #r #Hl #Hr #b #_ #H #x cases (BitVector_Sn h b) #hd #X elim X ;X; #tl #Hb359  #h #l #r #Hl #Hr #b #_ #H #x cases (BitVector_Sn h b) #hd #X elim X X; #tl #Hb 346 360 >Hb >Hb in H; cases hd 347 361 [ normalize #Hlookup @(Hr ? (refl ? h)) @Hlookup … … 352 366 qed. 353 367 354 lemma lookup_lookup_opt :368 lemma lookup_lookup_opt_hit: 355 369 ∀A.∀n.∀b.∀t.∀x,a. 356 370 lookup A n b t x = a → x ≠ a → lookup_opt A n b t = Some A a. … … 368 382 qed. 369 383 370 371 372 384 lemma lookup_opt_prepare_trie_for_insertion_hit: 373 385 ∀A:Type[0].∀v:A.∀n.∀b:BitVector n. … … 453 465 ] 454 466  #n #b #_ #P #Hlookup #Hf normalize // ] 455 qed. 467 qed. 456 468 457 469 lemma forall_insert_inv2b: … … 523 535 ] 524 536 ] 525 qed. 537 qed. 526 538 527 539 lemma update_fail : ∀A,n,b,a,t.
Note: See TracChangeset
for help on using the changeset viewer.