Changeset 985 for src/ASM/BitVectorTrie.ma

Timestamp:

Jun 16, 2011, 4:50:23 PM (9 years ago)

Author:

sacerdot

Message:

1) Major refactoring: proofs moved where they should be.
2) New build_map that never fails.

File:

• src/ASM/BitVectorTrie.ma (modified) (1 diff)

src/ASM/BitVectorTrie.ma

@@ -128 +128 @@
   ]
 qed.
+
+lemma BitVectorTrie_O:
+ ∀A:Type[0].∀v:BitVectorTrie A 0.(∃w. v ≃ Leaf A w) ∨ v ≃ Stub A 0.
+ #A #v generalize in match (refl … O) cases v in ⊢ (??%? → (?(??(λ_.?%%??)))(?%%??))
+  [ #w #_ %1 %[@w] %
+  | #n #l #r #abs @⊥ //
+  | #n #EQ %2 >EQ %]
+qed.
+
+lemma BitVectorTrie_Sn:
+ ∀A:Type[0].∀n.∀v:BitVectorTrie A (S n).(∃l,r. v ≃ Node A n l r) ∨ v ≃ Stub A (S n).
+ #A #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → (?(??(λ_.??(λ_.?%%??))))%)
+  [ #m #abs @⊥ //
+  | #m #l #r #EQ %1 <(injective_S … EQ) %[@l] %[@r] //
+  | #m #EQ %2 // ]
+qed.
+
+lemma lookup_prepare_trie_for_insertion_hit:
+ ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.
+  lookup … b (prepare_trie_for_insertion … b v) a = v. 
+ #A #a #v #n #b elim b // #m #hd #tl #IH cases hd normalize //
+qed.
+ 
+lemma lookup_insert_hit:
+ ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.∀t:BitVectorTrie A n.
+  lookup … b (insert … b v t) a = v.
+ #A #a #v #n #b elim b -b -n //
+ #n #hd #tl #IH #t cases(BitVectorTrie_Sn … t)
+  [ * #l * #r #JMEQ >JMEQ cases hd normalize //
+  | #JMEQ >JMEQ cases hd normalize @lookup_prepare_trie_for_insertion_hit ]
+qed.
+
+lemma lookup_prepare_trie_for_insertion_miss:
+ ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.
+  (notb (eq_bv ? b c)) → lookup … b (prepare_trie_for_insertion … c v) a = a.
+ #A #a #v #n #c elim c
+  [ #b >(BitVector_O … b) normalize #abs @⊥ //
+  | #m #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ
+    cases hd cases hd' normalize
+    [2,3: #_ cases tl' //
+    |*: change with (bool_to_Prop (notb (eq_bv ???)) → ?) /2/ ]]
+qed.
+  
+lemma lookup_insert_miss:
+ ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.∀t:BitVectorTrie A n.
+  (notb (eq_bv ? b c)) → lookup … b (insert … c v t) a = lookup … b t a.
+ #A #a #v #n #c elim c -c -n
+  [ #b #t #DIFF @⊥ whd in DIFF; >(BitVector_O … b) in DIFF //
+  | #n #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ
+    #t cases(BitVectorTrie_Sn … t)
+    [ * #l * #r #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
+     [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize // @IH //
+    | #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
+     [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize
+     [3,4: cases tl' // | *: @lookup_prepare_trie_for_insertion_miss //]]]
+qed.