Changeset 2161


Ignore:
Timestamp:
Jul 6, 2012, 5:35:01 PM (5 years ago)
Author:
sacerdot
Message:

Most of the old proof restored.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2159 r2161  
    983983          >bitvector_of_nat_inverse_nat_of_bitvector <sigma_pol3 #X >X @bitvector_of_nat_exp_zero
    984984        | >commutative_plus assumption ]]
    985   | cases daemon
    986   ]
    987    
    988 (*   
    989    
    990      % [%
    991     [ >length_append normalize nodelta >IH1 (*CSC: TRUE, LEMMA NEEDED *) cases daemon
    992     |2: (*CSC: NEES JAAP INVARIANT*) cases daemon]]
    993     #ppc' #LTppc' cases hd in prf p2; #label #pi #prf #p2 *
    994     cases daemon (*
    995     ?????????????? PRIMA NON C'ERA L'OR :-(
    996     MANTENERE LO SCHEMA DI PRIMA CON DUE CASI, MA IN UN CASO ppc=0 OVERFLOWED
    997     [2: #eq_S_prefix_bound -IH @(IH2 ? LTppc')
     985  | #ppc' #LTppc' cases hd in prf p2 EQpc_delta2 eq_fetch_pseudo_instruction; #label #pi #prf #p2
     986    #EQpc_delta2 #eq_fetch_pseudo_instruction *
     987    [2: #eq_S_prefix_bound (*@(IH5 ? LTppc')
    998988      @pair_elim #pi' #newppc' #eq_fetch_pseudo_instruction'
    999       @pair_elim 
     989      @pair_elim*) cases daemon
    1000990    | #LTppc_ppc
    1001991      cases (le_to_or_lt_eq … LTppc_ppc)
    1002992      [2: #S_S_eq normalize nodelta in S_S_eq;
    1003993          (*CSC: TRUE, NEEDS SOME WORK *)
    1004           cut (ppc' = ppc) [ cases daemon] -S_S_eq #EQppc' >EQppc' in LTppc'; -ppc'  >prf
    1005           >IH1 (* in ⊢ match % with [_ ⇒ ?];*) #LTppc lapply LTppc
     994          cut (ppc' = ppc) [ cases daemon] -S_S_eq #EQppc' >EQppc' in LTppc'; -ppc' >prf
     995          >IH1 #LTppc lapply LTppc
    1006996          >(add_zero … (bitvector_of_nat 16 (|prefix|))) in ⊢ (% → match % with [_ ⇒ ?]);
    1007997          >fetch_pseudo_instruction_append
     
    1009999          |2: lapply LTppc; >(add_zero … (bitvector_of_nat 16 (|prefix|))) in ⊢ (% → ?); #H @H
    10101000          |4: <prf <p_refl in instr_list_ok; #H @H ]
    1011           #LTppc' @pair_elim #pi' #newppc' #EQpair destruct(EQpair) <IH1 >p2
     1001          #LTppc' @pair_elim #pi' #newppc' #EQpair destruct(EQpair) <IH1 >p2 %
     1002          [ >length_reverse >length_append >length_reverse // ]
    10121003          #j #LTj >nat_of_bitvector_add
    10131004          >nat_of_bitvector_bitvector_of_nat_inverse
    1014           [2,4: (* CSC: TRUE, NEEDS LEMMA, MAYBE ALREADY PROVED *) cases daemon
     1005          [2,4: @(lt_to_le_to_lt … LTj) <EQpc_delta @(transitive_le … pc_delta_ok) %2 %
    10151006          |3: (*CSC: TRUE, NEEDS LEMMA *) cases daemon ]
    10161007          >reverse_append >reverse_reverse >IH3 <(length_reverse … code)
     
    10201011        [ normalize nodelta in LTppc'';
    10211012          @(transitive_le … (nat_of_bitvector … ppc))
    1022           [2: >IH1 >prf >length_append >nat_of_bitvector_bitvector_of_nat_inverse
    1023              [ //
    1024              | <p_refl in instr_list_ok; #instr_list_ok
    1025                @(transitive_le … (S (|instr_list|))) try assumption >prf >length_append // ]
     1013          [2: >IH1 >prf >length_append >nat_of_bitvector_bitvector_of_nat_inverse //
    10261014          | @le_S_S_to_le >nat_of_bitvector_add in LTppc'';
    1027             [ >commutative_plus #H @H 
     1015            [ >commutative_plus #H @H
    10281016            | >nat_of_bitvector_bitvector_of_nat_inverse [2: // ] >commutative_plus
    1029               @(transitive_le … (|instr_list|))
    1030               [2: <p_refl in instr_list_ok;  #instr_list_ok assumption
    1031               | >IH1 >prf >length_append @le_S_S >(commutative_plus (|prefix|))
    1032                 >length_append >nat_of_bitvector_bitvector_of_nat_inverse
    1033                 [2: <p_refl in instr_list_ok; >prf >length_append #H
    1034                     @(transitive_le … H) //
    1035                 | @le_S_S // ]]]]]
    1036       #X lapply (IH2 ppc' X)
     1017              @(transitive_le … instr_list_ok)
     1018              >IH1 >nat_of_bitvector_bitvector_of_nat_inverse [2: assumption ]
     1019              >prf >length_append >length_append <plus_n_Sm @le_S_S normalize
     1020              cases daemon (*CSC: ????
     1021             
     1022               >prf >length_append @le_S_S >(commutative_plus (|prefix|))
     1023              >length_append >nat_of_bitvector_bitvector_of_nat_inverse
     1024              [2: <p_refl in instr_list_ok; >prf >length_append #H
     1025                  @(transitive_le … H) //
     1026              | @le_S_S //*) ]]]]
     1027      #X lapply (IH5 ppc' X)
    10371028      @pair_elim #pi' #newppc' #eq_fetch_pseudoinstruction
    10381029      @pair_elim #len' #assembledi' #eq_assembly_1_pseudoinstruction #IH
    1039       change with (let 〈len,assembledi〉 ≝ assembly_1_pseudoinstruction ????? pi' in ∀j:ℕ. ∀H:j<|assembledi|.?)
    1040       >eq_assembly_1_pseudoinstruction #j #LTj >reverse_append >reverse_reverse #K
    1041       >IH
    1042       [2: >length_reverse <IH3 (*CSC: NEEDS JAAP INVARIANT PLUS SOME WORK *) cases daemon
    1043       | @shift_nth_prefix
    1044       |3: @le_S_S_to_le @(transitive_le … LTppc'') >nat_of_bitvector_add
    1045          [ >commutative_plus %
    1046          | >commutative_plus >IH1 whd in ⊢ (?%?);
    1047            @(transitive_le … (S (|instr_list|)))
    1048            [2:  <p_refl in instr_list_ok;  #instr_list_ok assumption
    1049            | >prf >length_append >length_append <plus_n_Sm >nat_of_bitvector_bitvector_of_nat_inverse
    1050              [ // | <p_refl in instr_list_ok; >prf >length_append #H @(transitive_le … H) // ]]]]
    1051 *)*)qed.
     1030      cases (IH ?)
     1031      [2: cases daemon (*CSC: new proof obligation*) ] #IH6 #IH
     1032      change with (let 〈len,assembledi〉 ≝ assembly_1_pseudoinstruction ????? pi' in ? ∧ ∀j:ℕ. ∀H:j<|assembledi|.?)
     1033      >eq_assembly_1_pseudoinstruction %
     1034      [ cases daemon (*CSC: new proof obligation*)
     1035      | #j #LTj >reverse_append >reverse_reverse #K
     1036        >IH
     1037        [2: >length_reverse <IH3 (*CSC: USE MONOTONICITY *) cases daemon
     1038        | @shift_nth_prefix ]]]]]
     1039(*        |3: @le_S_S_to_le @(transitive_le … LTppc'') >nat_of_bitvector_add
     1040           [ >commutative_plus %
     1041           | >commutative_plus >IH1 whd in ⊢ (?%?);
     1042             @(transitive_le … (S (|instr_list|)))
     1043             [2:  <p_refl in instr_list_ok;  #instr_list_ok assumption
     1044             | >prf >length_append >length_append <plus_n_Sm >nat_of_bitvector_bitvector_of_nat_inverse
     1045               [ // | <p_refl in instr_list_ok; >prf >length_append #H @(transitive_le … H) // ]]]]
     1046*)
     1047qed.
    10521048
    10531049definition assembly_unlabelled_program:
Note: See TracChangeset for help on using the changeset viewer.