Changeset 2028 for src/ASM/BitVectorTrie.ma

Timestamp:

Jun 7, 2012, 5:58:26 PM (8 years ago)

Author:

boender

Message:

• bugfix to Assembly (forgotten sigma)
• added add_bitvector_of_nat_plus to Arithmetic
• insert_lookup_opt_miss to BitVectorTrie?

File:

• src/ASM/BitVectorTrie.ma (modified) (2 diffs)

src/ASM/BitVectorTrie.ma

@@ -478 +478 @@
 qed.
 
-lemma insert_lookup_opt:
+lemma insert_lookup_opt_hit:
  ∀A:Type[0].∀v,a:A.∀n.∀c,b:BitVector n.∀t:BitVectorTrie A n.
    lookup_opt … b (insert … c v t) = Some A a → lookup_opt … b t = Some A a ∨ (b = c ∧ a = v).
@@ -503 +503 @@
 qed.
 
+lemma insert_lookup_opt_miss:
+ ∀A:Type[0].∀v:A.∀n.∀c,b:BitVector n.∀t:BitVectorTrie A n.
+   lookup_opt … b (insert … c v t) = None A →
+     (notb (eq_bv n b c)) = true ∧ lookup_opt … b t = None A.
+ #A #v #n #c elim c -c; -n;
+ [ #b #t #Hl normalize in Hl; destruct (Hl)
+ | #n #hd #tl #Hind #b cases (BitVector_Sn … b) #hd' * #tl' #Heq >Heq
+   #t cases (BitVectorTrie_Sn … t)
+   [ * #l * #r #Heq2 >Heq2 cases hd cases hd' #H normalize in H; normalize
+     [1,4: lapply (refl ? (eq_bv ? tl' tl)) cases (eq_bv ? tl' tl) in ⊢ (???% ->%); #Heq3
+       [1,3: >(eq_bv_eq … Heq3) in H; >lookup_opt_insert_hit #H destruct (H)
+       |2,4: >lookup_opt_insert_miss in H;
+         [1,3: #H whd in match eq_bv in Heq3; >Heq3 @conj
+           [1,3: / by refl/
+           |2,4: @H
+           ]
+         |2,4: >Heq3 / by I/
+         ]
+       ]
+     |2,3: @conj
+       [1,3: @refl
+       |2,4: @H
+       ]
+     ]
+   | #Heq2 >Heq2 cases hd cases hd' #H normalize in H; normalize
+     [1,4:  lapply (refl ? (eq_bv ? tl' tl)) cases (eq_bv ? tl' tl) in ⊢ (???% → %); #Heq3
+       [1,3: >(eq_bv_eq … Heq3) in H; >lookup_opt_prepare_trie_for_insertion_hit #X destruct (X)
+       |2,4: >(lookup_opt_prepare_trie_for_insertion_miss) in H; 
+         [1,3: #X @conj
+           [1,3: whd in match (eq_bv ???) in Heq3; >Heq3 / by refl/
+           |2,4: @refl
+           ]
+         |2,4: >Heq3 / by I/
+         ]
+       ] 
+     |2,3: @conj @refl
+     ]
+   ]
+ ]
+qed.
+   
 lemma forall_insert_inv1:
   ∀A.∀n.∀b.∀a.∀t.∀P.