Changeset 1070 for src/ASM/BitVectorTrie.ma
 Timestamp:
 Jul 15, 2011, 12:56:48 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/BitVectorTrie.ma
r1052 r1070 358 358 qed. 359 359 360 lemma lookup_opt_prepare_trie_for_insertion_miss: 361 ∀A:Type[0].∀v:A.∀n.∀c,b:BitVector n. 362 (notb (eq_bv ? b c)) → lookup_opt … b (prepare_trie_for_insertion … c v) = None ?. 363 #A #v #n #c elim c 364 [ #b >(BitVector_O … b) normalize #abs @⊥ // 365  #m #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ 366 cases hd cases hd' normalize 367 [2,3: #_ cases tl' // 368 *: change with (bool_to_Prop (notb (eq_bv ???)) → ?) @IH ]] 369 qed. 370 360 371 lemma lookup_opt_insert_hit: 361 372 ∀A:Type[0].∀v:A.∀n.∀b:BitVector n.∀t:BitVectorTrie A n. … … 374 385 ] 375 386 qed. 376 387 388 lemma lookup_opt_insert_miss: 389 ∀A:Type[0].∀v:A.∀n.∀c,b:BitVector n.∀t:BitVectorTrie A n. 390 (notb (eq_bv ? b c)) → lookup_opt … b (insert … c v t) = lookup_opt … b t. 391 #A #v #n #c elim c c n 392 [ #b #t #DIFF @⊥ whd in DIFF; >(BitVector_O … b) in DIFF // 393  #n #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ 394 #t cases(BitVectorTrie_Sn … t) 395 [ * #l * #r #JMEQ >JMEQ cases hd cases hd' #H normalize in H; 396 [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize // @IH // 397  #JMEQ >JMEQ cases hd cases hd' #H normalize in H; 398 [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize 399 [3,4: cases tl' //  *: @lookup_opt_prepare_trie_for_insertion_miss //]]] 400 qed. 401 377 402 lemma forall_insert_inv1: 378 403 ∀A.∀n.∀b.∀a.∀t.∀P.
Note: See TracChangeset
for help on using the changeset viewer.