Changeset 2071


Ignore:
Timestamp:
Jun 14, 2012, 3:25:54 AM (5 years ago)
Author:
sacerdot
Message:

More daemons closed, but one is suspect now.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2070 r2071  
    830830    * #IH1 #IH2 whd % [ normalize nodelta >IH1 >length_append cases daemon (*CSC: TRUE, LEMMA NEEDED *)]
    831831    #ppc' #LTppc' cases hd in prf p2; #label #pi #prf #p2 #LTppc_ppc
    832     cases (le_to_or_lt_eq … LTppc')
     832    cases (le_to_or_lt_eq … LTppc_ppc)
    833833    [2: #S_S_eq normalize nodelta in S_S_eq;
    834         (*CSC: FALSE, NEEDS INVARIANT *)
    835         cut (ppc' = ppc) [ normalize nodelta in LTppc_ppc; >IH1 cases daemon] -S_S_eq #EQppc' >EQppc' in LTppc'; -ppc'  >prf
     834        (*CSC: TRUE, NEEDS SOME WORK *)
     835        cut (ppc' = ppc) [ cases daemon] -S_S_eq #EQppc' >EQppc' in LTppc'; -ppc'  >prf
    836836        >IH1 (* in ⊢ match % with [_ ⇒ ?];*) #LTppc lapply LTppc
    837837        >(add_zero … (bitvector_of_nat 16 (|prefix|))) in ⊢ (% → match % with [_ ⇒ ?]);
     
    849849        >(? : nat_of_bitvector … (sigma ppc) = |reverse … code|) [2: cases daemon]
    850850        @nth_safe_prepend
    851     | #LTppc'' lapply (IH2 ppc' ?)
    852       [ @(transitive_le … LTppc'') @le_S_S // ]
     851    | #LTppc''
     852      cut (nat_of_bitvector … ppc' < |instr_list|)
     853      [ normalize nodelta in LTppc'';
     854        @(transitive_le … (nat_of_bitvector … ppc))
     855        [2: >IH1 >prf >length_append >nat_of_bitvector_bitvector_of_nat_inverse
     856           [ //
     857           | <p_refl in instr_list_ok; #instr_list_ok
     858             @(transitive_le … (S (|instr_list|))) try assumption >prf >length_append // ]
     859        | @le_S_S_to_le >nat_of_bitvector_add in LTppc'';
     860          [ >commutative_plus #H @H
     861          | >nat_of_bitvector_bitvector_of_nat_inverse [2: // ] >commutative_plus
     862            @(transitive_le … (S (|instr_list|)))
     863            [2: <p_refl in instr_list_ok;  #instr_list_ok assumption
     864            | >IH1 >prf >length_append @le_S_S >(commutative_plus (|prefix|))
     865              >length_append >nat_of_bitvector_bitvector_of_nat_inverse
     866              [2: <p_refl in instr_list_ok; >prf >length_append #H
     867                  @(transitive_le … H) //
     868              | @le_S_S // ]]]]]
     869      #X lapply (IH2 ppc' X)
    853870      @pair_elim #pi' #newppc' #eq_fetch_pseudoinstruction
    854871      @pair_elim #len' #assembledi' #eq_assembly_1_pseudoinstruction #IH
     
    856873      >eq_assembly_1_pseudoinstruction #j #LTj >reverse_append >reverse_reverse #K
    857874      >IH
    858       [2: (*CSC: FALSE, NEEDS INVARIANT PPC'=PPC TO AVOID @PAIR_ELIM ABOVE? *) cases daemon
     875      [2: (*CSC: FALSE, WE CAN PROVE PPC'<=PPC, SO WHAT? *) cases daemon
    859876      | @shift_nth_prefix
    860       |3: >IH1 >nat_of_bitvector_bitvector_of_nat_inverse try assumption
    861           (*CSC: ALSO FALSE, NEEDS INVARIANT? *) cases daemon
    862       ]
    863     ]
    864   ] 
     877      |3: @le_S_S_to_le @(transitive_le … LTppc'') >nat_of_bitvector_add
     878         [ >commutative_plus %
     879         | >commutative_plus >IH1 whd in ⊢ (?%?);
     880           @(transitive_le … (S (|instr_list|)))
     881           [2:  <p_refl in instr_list_ok;  #instr_list_ok assumption
     882           | >prf >length_append >length_append <plus_n_Sm >nat_of_bitvector_bitvector_of_nat_inverse
     883             [ // | <p_refl in instr_list_ok; >prf >length_append #H @(transitive_le … H) // ]]]]
    865884qed.
    866885
Note: See TracChangeset for help on using the changeset viewer.