Changeset 1616 for src/ASM/AssemblyProof.ma

Timestamp:

Dec 14, 2011, 5:57:08 PM (9 years ago)

Author:

sacerdot

Message:

Partially ported to new Matita syntax.
Because of some changes in Fetch.ma, it no longer compiles.

File:

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

src/ASM/AssemblyProof.ma

@@ -2 +2 @@
 include "ASM/Interpret.ma".
 include "ASM/StatusProofs.ma".
+include alias "arithmetics/nat.ma".
 
 definition bit_elim_prop: ∀P: bool → Prop. Prop ≝
@@ -280 +281 @@
       %
     | normalize
-      normalize in IH
+      normalize in IH;
       @ IH
     ]
@@ -344 +345 @@
     (* cases prf in tl H; : ??? WAS WORKING BEFORE *)
     #tl
-    normalize in ⊢ (∀_: %. ?)
+    normalize in ⊢ (∀_: %. ?);
     # H
     whd
-    normalize in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?])
+    normalize in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?]);
     cases (is_a hd (subaddressing_modeel y tl H)) whd // ]
 qed.
@@ -781 +782 @@
     eq_sum A B leq req s s = true.
   #A #B #leq #req #s #leq_refl #req_refl
-  cases s whd in ⊢ (? → ??%?) //
+  cases s whd in ⊢ (? → ??%?); //
 qed.
 
@@ -792 +793 @@
     eq_prod A B leq req s s = true.
   #A #B #leq #req #s #leq_refl #req_refl
-  cases s whd in ⊢ (? → ? → ??%?) #l #r >leq_refl normalize @req_refl
+  cases s whd in ⊢ (? → ? → ??%?); #l #r >leq_refl normalize @req_refl
 qed.
 
@@ -801 +802 @@
   try @eq_addressing_mode_refl
   [1,2,3,4,5,6,7,8,10,16,17,18,19,20:
-    whd in ⊢ (??%?)
+    whd in ⊢ (??%?);
     try %
     >eq_addressing_mode_refl
     >eq_addressing_mode_refl %
   |13,15:
-    whd in ⊢ (??%?)
+    whd in ⊢ (??%?);
     cases arg1
     [*:
@@ -813 +814 @@
     ]
   |11,12:
-    whd in ⊢ (??%?)
+    whd in ⊢ (??%?);
     cases arg1
     [1:
@@ -832 +833 @@
     ]
   |14:
-    whd in ⊢ (??%?)
+    whd in ⊢ (??%?);
     cases arg1
     [ #arg1_left normalize nodelta
@@ -857 +858 @@
     ]
   |*:
-    whd in ⊢ (??%?)
+    whd in ⊢ (??%?);
     cases arg1
     [*: #arg1 >eq_sum_refl
@@ -918 +919 @@
   [1,2,3,4,5,6: #arg1 @eq_addressing_mode_refl
   |7: #arg1 #arg2
-      whd in ⊢ (??%?)
+      whd in ⊢ (??%?);
       >eq_addressing_mode_refl
       >eq_addressing_mode_refl
@@ -1076 +1077 @@
   [ %
   | #n #hd #tl #ih
-    normalize in ⊢ (???%) %
+    normalize in ⊢ (???%); %
   ]
 qed.
 
 lemma Vector_O: ∀A. ∀v: Vector A 0. v ≃ VEmpty A.
- #A #v generalize in match (refl … 0) cases v in ⊢ (??%? → ?%%??) //
+ #A #v generalize in match (refl … 0); cases v in ⊢ (??%? → ?%%??); //
  #n #hd #tl #abs @⊥ destruct (abs)
 qed.
@@ -1087 +1088 @@
 lemma Vector_Sn: ∀A. ∀n.∀v:Vector A (S n).
  ∃hd.∃tl.v ≃ VCons A n hd tl.
- #A #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)))
+ #A #n #v generalize in match (refl … (S n)); cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)));
  [ #abs @⊥ destruct (abs)
  | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]
@@ -1123 +1124 @@
     〈q, r〉 = 〈[[ ]], r〉.
   #A #n #q #r
-  generalize in match (Vector_O A q …)
+  generalize in match (Vector_O A q …);
   #hyp
-  >hyp in ⊢ (??%?)
+  >hyp in ⊢ (??%?);
   %
 qed.
@@ -1244 +1245 @@
     encoding_check code_memory (bitvector_of_nat … intermediate_pc) (bitvector_of_nat … final_pc) l2.
  #code_memory #final_pc #l1 elim l1
-  [ #pc #l2 whd in ⊢ (????% → ?) #H <plus_n_O whd whd in ⊢ (?%?) /2/
+  [ #pc #l2 whd in ⊢ (????% → ?); #H <plus_n_O whd whd in ⊢ (?%?); /2/
   | #hd #tl #IH #pc #l2 * #H1 #H2 >half_add_SO in H2; #H2 cases (IH … H2) <plus_n_Sm
     #K1 #K2 % [2:@K2] whd % // >half_add_SO @K1 ]
@@ -1282 +1283 @@
    68,69,70,71: #ARG2]]
  [1,2,19,20: #arg3 @(list_addressing_mode_tags_elim_prop … arg3) whd try % -arg3 #ARG3]
- normalize in ⊢ (???% → ?)
+ normalize in ⊢ (???% → ?);
  [92,94,42,93,95: @split_elim #vl #vm #E >E -E; [2,4: @(bitvector_3_elim_prop … vl)]
-  normalize in ⊢ (???% → ?)]
- #H >H * #H1 try (whd in ⊢ (% → ?) * #H2)
- try (whd in ⊢ (% → ?) * #H3) whd in ⊢ (% → ?) #H4
- change in ⊢ (let fetched ≝ % in ?) with (fetch0 ??)
+  normalize in ⊢ (???% → ?);]
+ #H >H * #H1 try (whd in ⊢ (% → ?); * #H2)
+ try (whd in ⊢ (% → ?); * #H3) whd in ⊢ (% → ?); #H4
+ [ whd in match fetch; normalize nodelta <H1 (*XXX
+   
  whd in ⊢ (let fetched ≝ ??% in ?) <H1 whd in ⊢ (let fetched ≝ % in ?)
  [17,18,19,20,21,22,23,24,25,26,31,34,35,36,37,38: <H3]
@@ -1293 +1295 @@
   30,31,32,33,34,35,36,37,38,39,40,43,45,48,49,52,53,54,55,56,57,60,61,62,65,66,
   69,70,73,74,78,80,81,84,85,95,98,101,102,103,104,105,106,107,108,109,110: <H2]
- whd >eq_instruction_refl >H4 @eq_bv_refl
+ whd >eq_instruction_refl >H4 @eq_bv_refl*)
 qed.