Changeset 862 for src

Timestamp:

May 31, 2011, 2:33:18 AM (10 years ago)

Author:

sacerdot

Message:

...

File:

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

src/ASM/AssemblyProof.ma

@@ -389 +389 @@
 qed.
 
-axiom occurs_exactly_once: Identifier → list labelled_instruction → Prop.
+let rec does_not_occur (id:Identifier) (l:list labelled_instruction) on l: bool ≝
+ match l with
+  [ nil ⇒ true
+  | cons hd tl ⇒ notb (address_of_word_labels_internal id hd) ∧ does_not_occur id tl].
+
+lemma does_not_occur_None:
+ ∀id,i,list_instr.
+  does_not_occur id (list_instr@[〈None …,i〉]) =
+  does_not_occur id list_instr.
+ #id #i #list_instr elim list_instr
+  [ % | #hd #tl #IH whd in ⊢ (??%%) >IH %]
+qed.
+
+let rec occurs_exactly_once (id:Identifier) (l:list labelled_instruction) on l : bool ≝
+ match l with
+  [ nil ⇒ false
+  | cons hd tl ⇒
+     if address_of_word_labels_internal id hd then
+      does_not_occur id tl
+     else
+      occurs_exactly_once id tl ].
+
+lemma occurs_exactly_once_None:
+ ∀id,i,list_instr.
+  occurs_exactly_once id (list_instr@[〈None …,i〉]) =
+  occurs_exactly_once id list_instr.
+ #id #i #list_instr elim list_instr
+  [ % | #hd #tl #IH whd in ⊢ (??%%) >IH >does_not_occur_None %]
+qed.
+
+coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0]. 
 
 lemma index_of_internal_None: ∀i,id,instr_list,n.
@@ -396 +426 @@
    index_of_internal ? (address_of_word_labels_internal id) (instr_list@[〈None …,i〉]) n.
  #i #id #instr_list elim instr_list
-  [ #n #abs (* ASSURDO *)
-  | #hd #tl #IH #n #H whd in ⊢ (??%%) cases (address_of_word_labels_internal id hd)
-    whd in ⊢ (??%%)
-    [ %
-    | @IH 
-    ]]
+  [ #n #abs whd in abs; cases abs
+  | #hd #tl #IH #n whd in ⊢ (% → ??%%); whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ?)
+    cases (address_of_word_labels_internal id hd) whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ??%%)
+    [ #H %
+    | #H @IH whd in H; cases (occurs_exactly_once ??) in H ⊢ %
+      [ #_ % | #abs cases abs ]]]
 qed.
 
@@ -409 +439 @@
   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.
 
 definition build_maps' ≝
@@ -451 +483 @@
    whd in ⊢ (??(????%?)?) -labels1;
    cases label in Hid
-    [ #Hid whd in ⊢ (??(????%?)?)
-      (* COMPLETARE *)
-      >IH1 -IH1
-       [       
-       |
-       ]
-    | -label #label whd in ⊢ (??(????%?)?)
+    [ #Hid whd in ⊢ (??(????%?)?) >IH1 -IH1
+       [ >(address_of_word_labels_code_mem_None … Hid)
+         (* MANCA LEMMA: INDIRIZZO TROVATO NEL PROGRAMMA! *)
+       | whd in Hid >occurs_exactly_once_None in Hid // ]
+    | -label #label #Hid whd in ⊢ (??(????%?)?)
       
     ]