Changeset 2161 for src

Timestamp:

Jul 6, 2012, 5:35:01 PM (9 years ago)

Author:

sacerdot

Message:

Most of the old proof restored.

File:

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

src/ASM/Assembly.ma

@@ -983 +983 @@
           >bitvector_of_nat_inverse_nat_of_bitvector <sigma_pol3 #X >X @bitvector_of_nat_exp_zero
         | >commutative_plus assumption ]]
-  | cases daemon
-  ]
-    
-(*    
-    
-     % [%
-    [ >length_append normalize nodelta >IH1 (*CSC: TRUE, LEMMA NEEDED *) cases daemon
-    |2: (*CSC: NEES JAAP INVARIANT*) cases daemon]]
-    #ppc' #LTppc' cases hd in prf p2; #label #pi #prf #p2 *
-    cases daemon (*
-    ?????????????? PRIMA NON C'ERA L'OR :-(
-    MANTENERE LO SCHEMA DI PRIMA CON DUE CASI, MA IN UN CASO ppc=0 OVERFLOWED
-    [2: #eq_S_prefix_bound -IH @(IH2 ? LTppc')
+  | #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 (*@(IH5 ? LTppc')
       @pair_elim #pi' #newppc' #eq_fetch_pseudo_instruction'
-      @pair_elim 
+      @pair_elim*) cases daemon
     | #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 (* in ⊢ match % with [_ ⇒ ?];*) #LTppc lapply LTppc
+          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
@@ -1009 +999 @@
           |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
+          #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: (* CSC: TRUE, NEEDS LEMMA, MAYBE ALREADY PROVED *) cases daemon
+          [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 >IH3 <(length_reverse … code)
@@ -1020 +1011 @@
         [ normalize nodelta in LTppc'';
           @(transitive_le … (nat_of_bitvector … ppc))
-          [2: >IH1 >prf >length_append >nat_of_bitvector_bitvector_of_nat_inverse
-             [ //
-             | <p_refl in instr_list_ok; #instr_list_ok
-               @(transitive_le … (S (|instr_list|))) try assumption >prf >length_append // ]
+          [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 
+            [ >commutative_plus #H @H
             | >nat_of_bitvector_bitvector_of_nat_inverse [2: // ] >commutative_plus
-              @(transitive_le … (|instr_list|))
-              [2: <p_refl in instr_list_ok;  #instr_list_ok assumption
-              | >IH1 >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 (IH2 ppc' X)
+              @(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 (IH5 ppc' X)
       @pair_elim #pi' #newppc' #eq_fetch_pseudoinstruction
       @pair_elim #len' #assembledi' #eq_assembly_1_pseudoinstruction #IH
-      change with (let 〈len,assembledi〉 ≝ assembly_1_pseudoinstruction ????? pi' in ∀j:ℕ. ∀H:j<|assembledi|.?)
-      >eq_assembly_1_pseudoinstruction #j #LTj >reverse_append >reverse_reverse #K
-      >IH
-      [2: >length_reverse <IH3 (*CSC: NEEDS JAAP INVARIANT PLUS SOME WORK *) 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) // ]]]]
-*)*)qed.
+      cases (IH ?)
+      [2: cases daemon (*CSC: new proof obligation*) ] #IH6 #IH
+      change with (let 〈len,assembledi〉 ≝ assembly_1_pseudoinstruction ????? pi' in ? ∧ ∀j:ℕ. ∀H:j<|assembledi|.?)
+      >eq_assembly_1_pseudoinstruction %
+      [ cases daemon (*CSC: new proof obligation*)
+      | #j #LTj >reverse_append >reverse_reverse #K
+        >IH
+        [2: >length_reverse <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) // ]]]]
+*)
+qed.
 
 definition assembly_unlabelled_program: