Changeset 2189 for src

Timestamp:

Jul 17, 2012, 1:03:37 AM (9 years ago)

Author:

sacerdot

Message:

Proof very close to completion.

File:

• src/ASM/Assembly.ma (modified) (3 diffs)

src/ASM/Assembly.ma

@@ -977 +977 @@
       | * * #IH3a #IH3b #IH3c >IH3b <EQpc_delta >EQpc_delta2 >eq_fetch_pseudo_instruction
         >IH3c try % assumption ]
-(*        cut (ppc ≠ zero …)
-        [% #EQppc_zero @(absurd … IH3b) >IH2' [ @not_eq_O_S ] assumption ] #Not_eq_ppc_zero
-        cut (bitvector_of_nat ? (S (pred (nat_of_bitvector … ppc))) = ppc)
-        [ inversion (nat_of_bitvector … ppc)
-          [2: #p #_ #H normalize in match (pred ?);
-              lapply(eq_f … (bitvector_of_nat 16) … H) >bitvector_of_nat_inverse_nat_of_bitvector
-              #H' <H' %
-          | #H @⊥
-            lapply(eq_f … (bitvector_of_nat 16) … H) >bitvector_of_nat_inverse_nat_of_bitvector
-            #H' @(absurd ?? Not_eq_ppc_zero) >H' % ]] #EQppc lapply ppc_ok; <EQppc #S_pred_ppc_ok
-        cases (sigma_pol_ok2 (bitvector_of_nat 16 (pred (nat_of_bitvector 16 ppc))) ?)
-        [2: @(transitive_lt … ppc_ok) >nat_of_bitvector_bitvector_of_nat_inverse
-            [2: cases daemon (*CSC: True *) | cases daemon (*CSC: True*) ]
-        | #Sigma_pol1 *
-          [ cases daemon (*??????????*)
-          | * #Sigma_pol2 #Sigma_pol3 lapply (Sigma_pol2 … S_pred_ppc_ok ?)
-            [ cases daemon (*CSC: True *) ]
-            whd in ⊢ (% → ?); <eq_create_label_cost_map #H >H % ]]]*)
-    | %(* >length_append >commutative_plus >length_reverse <IH3 <EQpc_delta
-       #abs >abs in sigma_pol4; *
-       [ #abs' cases (absurd ? abs' (not_le_Sn_n …))
-       | * #abs' #_ <abs' >length_append <plus_n_Sm <plus_n_O @eq_f >IH1
-         >nat_of_bitvector_bitvector_of_nat_inverse // ]*)
+    | % (*CSC: Stupid proof of True, drop fake invariant *)
     | >length_append >length_reverse
       cases IH3 -IH3
@@ -1032 +1010 @@
           >nat_of_bitvector_add >nat_of_bitvector_bitvector_of_nat_inverse // ]]
   | #ppc' #LTppc' cases hd in prf p2 EQpc_delta2 eq_fetch_pseudo_instruction; #label #pi #prf #p2
-    #EQpc_delta2 #eq_fetch_pseudo_instruction *
-    [2: #eq_S_prefix_bound
-      cut (instr_list = prefix @ [〈label,pi〉 ]) [ cases daemon (*CSC: easy *) ] #EQinstr_list
-      @pair_elim #pi' #newppc' #eq_fetch_pseudo_instruction'
-      @pair_elim #len #assembledi #eq_assembly_1_pseudoinstruction %
-      [
-      |
-      ]
-    | #LTppc_ppc
-      cases (le_to_or_lt_eq … LTppc_ppc)
-      [2: #S_S_eq normalize nodelta in S_S_eq;
-          (*CSC: TRUE, NEEDS SOME WORK *)
-          cut (ppc' = ppc) [ cases daemon] -S_S_eq #EQppc' >EQppc' in LTppc'; -ppc' >prf
-          >IH1 #LTppc lapply LTppc
-          >(add_zero … (bitvector_of_nat 16 (|prefix|))) in ⊢ (% → match % with [_ ⇒ ?]);
-          >fetch_pseudo_instruction_append
-          [3: @le_S_S @le_O_n
-          |2: lapply LTppc; >(add_zero … (bitvector_of_nat 16 (|prefix|))) in ⊢ (% → ?); #H @H
-          |4: <prf <p_refl in instr_list_ok; #H @H ]
-          #LTppc' @pair_elim #pi' #newppc' #EQpair destruct(EQpair) <IH1 >p2 %
-          [ >length_reverse >length_append >length_reverse // ]
-          #j #LTj >nat_of_bitvector_add
-          >nat_of_bitvector_bitvector_of_nat_inverse
-          [2,4: @(lt_to_le_to_lt … LTj) <EQpc_delta @(transitive_le … pc_delta_ok) %2 %
-          |3: (*CSC: TRUE, NEEDS LEMMA *) cases daemon ]
-          >reverse_append >reverse_reverse
-          cases IH3 -IH3
-          [ #IH3 >IH3 <(length_reverse … code) @nth_safe_prepend
-          | cases daemon (*CSC: ?????????? *) ]
-      | #LTppc''
-        cut (nat_of_bitvector … ppc' < |instr_list|)
-        [ normalize nodelta in LTppc'';
-          @(transitive_le … (nat_of_bitvector … ppc))
-          [2: >IH1 >prf >length_append >nat_of_bitvector_bitvector_of_nat_inverse //
-          | @le_S_S_to_le >nat_of_bitvector_add in LTppc'';
-            [ >commutative_plus #H @H
-            | >nat_of_bitvector_bitvector_of_nat_inverse [2: // ] >commutative_plus
-              @(transitive_le … instr_list_ok)
-              >IH1 >nat_of_bitvector_bitvector_of_nat_inverse [2: assumption ]
-              >prf >length_append >length_append <plus_n_Sm @le_S_S normalize
-              cases daemon (*CSC: ????
-              
-               >prf >length_append @le_S_S >(commutative_plus (|prefix|))
-              >length_append >nat_of_bitvector_bitvector_of_nat_inverse
-              [2: <p_refl in instr_list_ok; >prf >length_append #H
-                  @(transitive_le … H) //
-              | @le_S_S //*) ]]]]
-      #X lapply (IH4 ppc' X)
+    #EQpc_delta2 #eq_fetch_pseudo_instruction #OR_lt_eq
+    cut (ppc' = ppc ∨ ppc' ≠ ppc) [cases daemon (*CSC: True*)] *
+    [ #EQppc' >EQppc' in LTppc'; -ppc' >prf
+      >IH1 #LTppc lapply LTppc
+      >(add_zero … (bitvector_of_nat 16 (|prefix|))) in ⊢ (% → match % with [_ ⇒ ?]);
+      >fetch_pseudo_instruction_append
+      [3: @le_S_S @le_O_n
+      |2: lapply LTppc; >(add_zero … (bitvector_of_nat 16 (|prefix|))) in ⊢ (% → ?); #H @H
+      |4: <prf <p_refl in instr_list_ok; #H @H ]
+      #LTppc' @pair_elim #pi' #newppc' #EQpair destruct(EQpair) <IH1 >p2 %
+      [ >length_reverse >length_append >length_reverse // ]
+      #j #LTj >nat_of_bitvector_add
+      >nat_of_bitvector_bitvector_of_nat_inverse
+      [2,4: @(lt_to_le_to_lt … LTj) <EQpc_delta @(transitive_le … pc_delta_ok) %2 %
+      |3: @(lt_to_le_to_lt … (nat_of_bitvector … (sigma ppc) + pc_delta))
+          [ >EQpc_delta @monotonic_lt_plus_r assumption
+          | cases sigma_pol4
+            [ #H @(transitive_le … H) %2 %
+            | * #_ #EQ >EQ % ]]]
+      >reverse_append >reverse_reverse
+      cases IH3 -IH3
+      [ #IH3 >IH3 <(length_reverse … code) @nth_safe_prepend
+      | * * #IH3a #IH3b #IH3c >IH3a @⊥
+        cut (|program| = 0)
+        [ <EQpc_delta >EQpc_delta2 >eq_fetch_pseudo_instruction @IH3c // ] #EQprogram
+        @(absurd ?? (not_le_Sn_O j)) <EQprogram assumption ]
+    | #NEQppc'
+      lapply (IH4 … LTppc')
       @pair_elim #pi' #newppc' #eq_fetch_pseudoinstruction
       @pair_elim #len' #assembledi' #eq_assembly_1_pseudoinstruction #IH
@@ -1091 +1049 @@
         [2: >length_reverse (*CSC: ?????????? <IH3 (*CSC: USE MONOTONICITY *)*) cases daemon
         | @shift_nth_prefix ]]]]]
-(*        |3: @le_S_S_to_le @(transitive_le … LTppc'') >nat_of_bitvector_add
-           [ >commutative_plus %
-           | >commutative_plus >IH1 whd in ⊢ (?%?);
-             @(transitive_le … (S (|instr_list|)))
-             [2:  <p_refl in instr_list_ok;  #instr_list_ok assumption
-             | >prf >length_append >length_append <plus_n_Sm >nat_of_bitvector_bitvector_of_nat_inverse
-               [ // | <p_refl in instr_list_ok; >prf >length_append #H @(transitive_le … H) // ]]]]
-*)
-cases daemon
 qed.