Ignore:
Timestamp:
Dec 20, 2011, 2:38:50 PM (8 years ago)
Author:
boender
Message:
  • strengthened insert_lookup_opt
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/BitVectorTrie.ma

    r1609 r1632  
    478478lemma insert_lookup_opt:
    479479 ∀A:Type[0].∀v,a:A.∀n.∀c,b:BitVector n.∀t:BitVectorTrie A n.
    480    lookup_opt … b (insert … c v t) = Some A a → lookup_opt … b t = Some A a ∨ a = v.
     480   lookup_opt … b (insert … c v t) = Some A a → lookup_opt … b t = Some A a ∨ (b = c ∧ a = v).
    481481 #A #v #a #n #c elim c -c; -n;
    482  [ #b #t #Hl normalize in Hl; %2 destruct (Hl) @refl
     482 [ #b #t #Hl normalize in Hl; %2 destruct (Hl) @conj [ @BitVector_O | @refl ]
    483483 | #n #hd #tl #Hind #b cases (BitVector_Sn … b) #hd' * #tl' #Heq >Heq
    484484   #t cases (BitVectorTrie_Sn … t)
    485485   [ * #l * #r #Heq2 >Heq2 cases hd cases hd' #H normalize in H; normalize
    486      [1,4: @(Hind tl' ? H)
     486     [1,4: cases (Hind tl' ? H) #Hi2 [1,3: %1 @Hi2 |2,4: %2 @conj
     487       [1,3: >(proj1 ?? Hi2) @refl
     488       |2,4: @(proj2 ?? Hi2) ] ]
    487489     |2,3: %1 @H
    488490     ]
    489491   | #Heq2 >Heq2 cases hd cases hd' #H normalize in H; normalize
    490492     [1,4: lapply (refl ? (eq_bv ? tl' tl)) cases (eq_bv ? tl' tl) in ⊢ (???% → %); #Heq3
    491        [1,3: >(eq_bv_eq … Heq3) in H; >lookup_opt_prepare_trie_for_insertion_hit #X destruct (X) %2 //
     493       [1,3: >(eq_bv_eq … Heq3) in H; >lookup_opt_prepare_trie_for_insertion_hit #X destruct (X) %2 /2 by pair_destruct/
    492494       |2,4: >(lookup_opt_prepare_trie_for_insertion_miss) in H;
    493495         [1,3: #X %1 //
Note: See TracChangeset for help on using the changeset viewer.