Changeset 1074 for src/ASM/BitVectorTrie.ma

Timestamp:

Jul 18, 2011, 12:44:31 PM (10 years ago)

Author:

boender

Message:

• added lookup lemma

File:

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

src/ASM/BitVectorTrie.ma

@@ -352 +352 @@
 qed.
 
+lemma lookup_lookup_opt:
+  ∀A.∀n.∀b.∀t.∀x,a.
+  lookup A n b t x = a → x ≠ a → lookup_opt A n b t = Some A a.
+ #A #n #b #t #x #a generalize in match (refl ? n) elim t in b ⊢ (???% → ? → ?)
+ [ #z #B #_ #H #Hx >(BitVector_O B) in H; normalize #H >H @refl
+ | #h #l #r #Hl #Hr #B #_ #H #Hx cases (BitVector_Sn h B) #hd #X elim X; -X #tl #HB
+   >HB >HB in H; cases hd
+   [ normalize #H >(Hr tl (refl ? h) H Hx) @refl
+   | normalize #H >(Hl tl (refl ? h) H Hx) @refl 
+   ]
+ | #n #B #_ #H #Hx cases B in H;
+   [ normalize #Hx' | #n' #b #v normalize #Hx' ]
+   @⊥ @(absurd (eq ? x a)) [1,3: @Hx' |2,4: @Hx ]
+ ]
+qed.
+
+ 
+ 
 lemma lookup_opt_prepare_trie_for_insertion_hit:
  ∀A:Type[0].∀v:A.∀n.∀b:BitVector n.