Changeset 975 for src/ASM/AssemblyProof.ma

Timestamp:

Jun 16, 2011, 11:34:26 AM (9 years ago)

Author:

sacerdot

Message:

...

File:

• src/ASM/AssemblyProof.ma (modified) (4 diffs)

src/ASM/AssemblyProof.ma

@@ -1032 +1032 @@
 qed.
 
-lemma index_of_internal_None: ∀i,id,instr_list,n.
- occurs_exactly_once id (instr_list@[〈None …,i〉]) →
-  index_of_internal ? (instruction_matches_identifier id) instr_list n =
-   index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈None …,i〉]) n.
- #i #id #instr_list elim instr_list
-  [ #n #abs whd in abs; cases abs
-  | #hd #tl #IH #n whd in ⊢ (% → ??%%); whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ?)
-    cases (instruction_matches_identifier id hd) whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ??%%)
-    [ #H %
-    | #H @IH whd in H; cases (occurs_exactly_once ??) in H ⊢ %
-      [ #_ % | #abs cases abs ]]]
-qed.
-
-lemma address_of_word_labels_code_mem_None: ∀i,id,instr_list.
- occurs_exactly_once id (instr_list@[〈None …,i〉]) →
-  address_of_word_labels_code_mem instr_list id =
-  address_of_word_labels_code_mem (instr_list@[〈None …,i〉]) id.
- #i #id #instr_list #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)(??%?))
- >(index_of_internal_None … H) %
-qed.
-
 lemma occurs_exactly_once_Some:
  ∀id,id',i,prefix.
@@ -1069 +1048 @@
 qed.
 
+lemma index_of_internal_None: ∀i,id,instr_list,n.
+ occurs_exactly_once id (instr_list@[〈None …,i〉]) →
+  index_of_internal ? (instruction_matches_identifier id) instr_list n =
+   index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈None …,i〉]) n.
+ #i #id #instr_list elim instr_list
+  [ #n #abs whd in abs; cases abs
+  | #hd #tl #IH #n whd in ⊢ (% → ??%%); whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ?)
+    cases (instruction_matches_identifier id hd) whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ??%%)
+    [ #H %
+    | #H @IH whd in H; cases (occurs_exactly_once ??) in H ⊢ %
+      [ #_ % | #abs cases abs ]]]
+qed.
+
+lemma index_of_internal_Some_miss: ∀i,id,id'.
+ eq_bv ? id' id = false →
+ ∀instr_list,n.
+ occurs_exactly_once id (instr_list@[〈Some ? id',i〉]) →
+  index_of_internal ? (instruction_matches_identifier id) instr_list n =
+   index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈Some ? id',i〉]) n.
+ #i #id #id' #EQ #instr_list #n #H generalize in match (occurs_exactly_once_Some … H) in ⊢ ?; >EQ
+ change with (occurs_exactly_once ?? → ?) generalize in match n; -n H; elim instr_list
+  [ #n #abs cases abs
+  | #hd #tl #IH #n whd in ⊢ (?% → ??%%) cases (instruction_matches_identifier id hd) normalize nodelta;
+    [ // | #K @IH //]]
+qed.
+
+lemma address_of_word_labels_code_mem_None: ∀i,id,instr_list.
+ occurs_exactly_once id (instr_list@[〈None …,i〉]) →
+  address_of_word_labels_code_mem instr_list id =
+  address_of_word_labels_code_mem (instr_list@[〈None …,i〉]) id.
+ #i #id #instr_list #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)(??%?))
+ >(index_of_internal_None … H) %
+qed.
+
+lemma address_of_word_labels_code_mem_Some_miss: ∀i,id,id',instr_list.
+ eq_bv ? id' id = false →
+  occurs_exactly_once id (instr_list@[〈Some ? id',i〉]) →
+   address_of_word_labels_code_mem instr_list id =
+   address_of_word_labels_code_mem (instr_list@[〈Some … id',i〉]) id.
+ #i #id #id' #instr_list #EQ #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)(??%?))
+ >(index_of_internal_Some_miss … H) //
+qed.
+
 axiom tech_pc_sigma00_append_Some:
  ∀program,prefix,costs,label,i,pc',code,ppc,pc.
@@ -1080 +1102 @@
    construct_costs program … ppc pc (λx.zero 16) (λx. zero 16) costs i = None …
     → False.
+
+lemma eq_false_to_notb: ∀b. b = false → ¬ b.
+ *; //
+qed.
+
+lemma eq_bv_sym: ∀n,v1,v2. eq_bv n v1 v2 = eq_bv n v2 v1.
+ #n #v1 #v2 @(eq_bv_elim … v1 v2) [// | #H >eq_bv_false /2/]
+qed.
 
 definition build_maps' ≝
@@ -1125 +1155 @@
    | #id normalize nodelta; -labels1; cases label; normalize nodelta
      [ #K <address_of_word_labels_code_mem_None [2:@K] @IH2 //
-     | #l
-     ]]
+     | #l #H generalize in match (occurs_exactly_once_Some ???? H) in ⊢ ?;
+       generalize in match (refl … (eq_bv ? l id)); cases (eq_bv … l id) in ⊢ (???% → %)
+        [ #EQ #_ <(eq_bv_to_eq … EQ) >lookup_insert_hit
+          
+        | #EQ change with (occurs_exactly_once ?? → ?) #K >lookup_insert_miss [2: /2/]
+          <(address_of_word_labels_code_mem_Some_miss … EQ … H) @IH2 //]]]
  | (* dummy case *) @⊥ generalize in match (sig2 … t) >p >p1 >p2 >p3 *; #IH1 #IH2 
    @(tech_pc_sigma00_append_None … IH1 (jmeq_to_eq ??? p4)) ]