Changeset 985 for src/ASM/BitVectorTrie.ma
- Timestamp:
- Jun 16, 2011, 4:50:23 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/BitVectorTrie.ma
r782 r985 128 128 ] 129 129 qed. 130 131 lemma BitVectorTrie_O: 132 ∀A:Type[0].∀v:BitVectorTrie A 0.(∃w. v ≃ Leaf A w) ∨ v ≃ Stub A 0. 133 #A #v generalize in match (refl … O) cases v in ⊢ (??%? → (?(??(λ_.?%%??)))(?%%??)) 134 [ #w #_ %1 %[@w] % 135 | #n #l #r #abs @⊥ // 136 | #n #EQ %2 >EQ %] 137 qed. 138 139 lemma BitVectorTrie_Sn: 140 ∀A:Type[0].∀n.∀v:BitVectorTrie A (S n).(∃l,r. v ≃ Node A n l r) ∨ v ≃ Stub A (S n). 141 #A #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → (?(??(λ_.??(λ_.?%%??))))%) 142 [ #m #abs @⊥ // 143 | #m #l #r #EQ %1 <(injective_S … EQ) %[@l] %[@r] // 144 | #m #EQ %2 // ] 145 qed. 146 147 lemma lookup_prepare_trie_for_insertion_hit: 148 ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n. 149 lookup … b (prepare_trie_for_insertion … b v) a = v. 150 #A #a #v #n #b elim b // #m #hd #tl #IH cases hd normalize // 151 qed. 152 153 lemma lookup_insert_hit: 154 ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.∀t:BitVectorTrie A n. 155 lookup … b (insert … b v t) a = v. 156 #A #a #v #n #b elim b -b -n // 157 #n #hd #tl #IH #t cases(BitVectorTrie_Sn … t) 158 [ * #l * #r #JMEQ >JMEQ cases hd normalize // 159 | #JMEQ >JMEQ cases hd normalize @lookup_prepare_trie_for_insertion_hit ] 160 qed. 161 162 lemma lookup_prepare_trie_for_insertion_miss: 163 ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n. 164 (notb (eq_bv ? b c)) → lookup … b (prepare_trie_for_insertion … c v) a = a. 165 #A #a #v #n #c elim c 166 [ #b >(BitVector_O … b) normalize #abs @⊥ // 167 | #m #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ 168 cases hd cases hd' normalize 169 [2,3: #_ cases tl' // 170 |*: change with (bool_to_Prop (notb (eq_bv ???)) → ?) /2/ ]] 171 qed. 172 173 lemma lookup_insert_miss: 174 ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.∀t:BitVectorTrie A n. 175 (notb (eq_bv ? b c)) → lookup … b (insert … c v t) a = lookup … b t a. 176 #A #a #v #n #c elim c -c -n 177 [ #b #t #DIFF @⊥ whd in DIFF; >(BitVector_O … b) in DIFF // 178 | #n #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ 179 #t cases(BitVectorTrie_Sn … t) 180 [ * #l * #r #JMEQ >JMEQ cases hd cases hd' #H normalize in H; 181 [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize // @IH // 182 | #JMEQ >JMEQ cases hd cases hd' #H normalize in H; 183 [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize 184 [3,4: cases tl' // | *: @lookup_prepare_trie_for_insertion_miss //]]] 185 qed.
Note: See TracChangeset
for help on using the changeset viewer.