Ignore:
Timestamp:
Dec 14, 2011, 5:57:08 PM (8 years ago)
Author:
sacerdot
Message:

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r1607 r1616  
    22include "ASM/Interpret.ma".
    33include "ASM/StatusProofs.ma".
     4include alias "arithmetics/nat.ma".
    45
    56definition bit_elim_prop: ∀P: bool → Prop. Prop ≝
     
    280281      %
    281282    | normalize
    282       normalize in IH
     283      normalize in IH;
    283284      @ IH
    284285    ]
     
    344345    (* cases prf in tl H; : ??? WAS WORKING BEFORE *)
    345346    #tl
    346     normalize in ⊢ (∀_: %. ?)
     347    normalize in ⊢ (∀_: %. ?);
    347348    # H
    348349    whd
    349     normalize in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?])
     350    normalize in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?]);
    350351    cases (is_a hd (subaddressing_modeel y tl H)) whd // ]
    351352qed.
     
    781782    eq_sum A B leq req s s = true.
    782783  #A #B #leq #req #s #leq_refl #req_refl
    783   cases s whd in ⊢ (? → ??%?) //
     784  cases s whd in ⊢ (? → ??%?); //
    784785qed.
    785786
     
    792793    eq_prod A B leq req s s = true.
    793794  #A #B #leq #req #s #leq_refl #req_refl
    794   cases s whd in ⊢ (? → ? → ??%?) #l #r >leq_refl normalize @req_refl
     795  cases s whd in ⊢ (? → ? → ??%?); #l #r >leq_refl normalize @req_refl
    795796qed.
    796797
     
    801802  try @eq_addressing_mode_refl
    802803  [1,2,3,4,5,6,7,8,10,16,17,18,19,20:
    803     whd in ⊢ (??%?)
     804    whd in ⊢ (??%?);
    804805    try %
    805806    >eq_addressing_mode_refl
    806807    >eq_addressing_mode_refl %
    807808  |13,15:
    808     whd in ⊢ (??%?)
     809    whd in ⊢ (??%?);
    809810    cases arg1
    810811    [*:
     
    813814    ]
    814815  |11,12:
    815     whd in ⊢ (??%?)
     816    whd in ⊢ (??%?);
    816817    cases arg1
    817818    [1:
     
    832833    ]
    833834  |14:
    834     whd in ⊢ (??%?)
     835    whd in ⊢ (??%?);
    835836    cases arg1
    836837    [ #arg1_left normalize nodelta
     
    857858    ]
    858859  |*:
    859     whd in ⊢ (??%?)
     860    whd in ⊢ (??%?);
    860861    cases arg1
    861862    [*: #arg1 >eq_sum_refl
     
    918919  [1,2,3,4,5,6: #arg1 @eq_addressing_mode_refl
    919920  |7: #arg1 #arg2
    920       whd in ⊢ (??%?)
     921      whd in ⊢ (??%?);
    921922      >eq_addressing_mode_refl
    922923      >eq_addressing_mode_refl
     
    10761077  [ %
    10771078  | #n #hd #tl #ih
    1078     normalize in ⊢ (???%) %
     1079    normalize in ⊢ (???%); %
    10791080  ]
    10801081qed.
    10811082
    10821083lemma Vector_O: ∀A. ∀v: Vector A 0. v ≃ VEmpty A.
    1083  #A #v generalize in match (refl … 0) cases v in ⊢ (??%? → ?%%??) //
     1084 #A #v generalize in match (refl … 0); cases v in ⊢ (??%? → ?%%??); //
    10841085 #n #hd #tl #abs @⊥ destruct (abs)
    10851086qed.
     
    10871088lemma Vector_Sn: ∀A. ∀n.∀v:Vector A (S n).
    10881089 ∃hd.∃tl.v ≃ VCons A n hd tl.
    1089  #A #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)))
     1090 #A #n #v generalize in match (refl … (S n)); cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)));
    10901091 [ #abs @⊥ destruct (abs)
    10911092 | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]
     
    11231124    〈q, r〉 = 〈[[ ]], r〉.
    11241125  #A #n #q #r
    1125   generalize in match (Vector_O A q …)
     1126  generalize in match (Vector_O A q …);
    11261127  #hyp
    1127   >hyp in ⊢ (??%?)
     1128  >hyp in ⊢ (??%?);
    11281129  %
    11291130qed.
     
    12441245    encoding_check code_memory (bitvector_of_nat … intermediate_pc) (bitvector_of_nat … final_pc) l2.
    12451246 #code_memory #final_pc #l1 elim l1
    1246   [ #pc #l2 whd in ⊢ (????% → ?) #H <plus_n_O whd whd in ⊢ (?%?) /2/
     1247  [ #pc #l2 whd in ⊢ (????% → ?); #H <plus_n_O whd whd in ⊢ (?%?); /2/
    12471248  | #hd #tl #IH #pc #l2 * #H1 #H2 >half_add_SO in H2; #H2 cases (IH … H2) <plus_n_Sm
    12481249    #K1 #K2 % [2:@K2] whd % // >half_add_SO @K1 ]
     
    12821283   68,69,70,71: #ARG2]]
    12831284 [1,2,19,20: #arg3 @(list_addressing_mode_tags_elim_prop … arg3) whd try % -arg3 #ARG3]
    1284  normalize in ⊢ (???% → ?)
     1285 normalize in ⊢ (???% → ?);
    12851286 [92,94,42,93,95: @split_elim #vl #vm #E >E -E; [2,4: @(bitvector_3_elim_prop … vl)]
    1286   normalize in ⊢ (???% → ?)]
    1287  #H >H * #H1 try (whd in ⊢ (% → ?) * #H2)
    1288  try (whd in ⊢ (% → ?) * #H3) whd in ⊢ (% → ?) #H4
    1289  change in ⊢ (let fetched ≝ % in ?) with (fetch0 ??)
     1287  normalize in ⊢ (???% → ?);]
     1288 #H >H * #H1 try (whd in ⊢ (% → ?); * #H2)
     1289 try (whd in ⊢ (% → ?); * #H3) whd in ⊢ (% → ?); #H4
     1290 [ whd in match fetch; normalize nodelta <H1 (*XXX
     1291   
    12901292 whd in ⊢ (let fetched ≝ ??% in ?) <H1 whd in ⊢ (let fetched ≝ % in ?)
    12911293 [17,18,19,20,21,22,23,24,25,26,31,34,35,36,37,38: <H3]
     
    12931295  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,
    12941296  69,70,73,74,78,80,81,84,85,95,98,101,102,103,104,105,106,107,108,109,110: <H2]
    1295  whd >eq_instruction_refl >H4 @eq_bv_refl
     1297 whd >eq_instruction_refl >H4 @eq_bv_refl*)
    12961298qed.
    12971299
Note: See TracChangeset for help on using the changeset viewer.