Changeset 869 for src

Timestamp:

May 31, 2011, 5:28:21 PM (10 years ago)

Author:

sacerdot

Message:

More progress.

File:

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

src/ASM/AssemblyProof.ma

@@ -544 +544 @@
    construct_costs 〈preamble,instr_list〉 … pc (λx.zero 16) (λx. zero 16) costs i = None …
     → False.
+
+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 BitVector_O: ∀v:BitVector 0. v ≃ VEmpty bool.
+ #v generalize in match (refl … 0) cases v in ⊢ (??%? → ?%%??) //
+ #n #hd #tl #abs @⊥ //
+qed.
+
+lemma BitVector_Sn: ∀n.∀v:BitVector (S n).
+ ∃hd.∃tl.v ≃ VCons bool n hd tl.
+ #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)))
+ [ #abs @⊥ //
+ | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]
+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 #H CSC
+     normalize in H;
+      
+      normalize //
+    | #JMEQ >JMEQ cases hd normalize @lookup_prepare_trie_for_insertion_hit ]
+qed.
 
 definition build_maps' ≝