Changeset 1616 for src/ASM/AssemblyProof.ma
- Timestamp:
- Dec 14, 2011, 5:57:08 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProof.ma
r1607 r1616 2 2 include "ASM/Interpret.ma". 3 3 include "ASM/StatusProofs.ma". 4 include alias "arithmetics/nat.ma". 4 5 5 6 definition bit_elim_prop: ∀P: bool → Prop. Prop ≝ … … 280 281 % 281 282 | normalize 282 normalize in IH 283 normalize in IH; 283 284 @ IH 284 285 ] … … 344 345 (* cases prf in tl H; : ??? WAS WORKING BEFORE *) 345 346 #tl 346 normalize in ⊢ (∀_: %. ?) 347 normalize in ⊢ (∀_: %. ?); 347 348 # H 348 349 whd 349 normalize in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?]) 350 normalize in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?]); 350 351 cases (is_a hd (subaddressing_modeel y tl H)) whd // ] 351 352 qed. … … 781 782 eq_sum A B leq req s s = true. 782 783 #A #B #leq #req #s #leq_refl #req_refl 783 cases s whd in ⊢ (? → ??%?) //784 cases s whd in ⊢ (? → ??%?); // 784 785 qed. 785 786 … … 792 793 eq_prod A B leq req s s = true. 793 794 #A #B #leq #req #s #leq_refl #req_refl 794 cases s whd in ⊢ (? → ? → ??%?) #l #r >leq_refl normalize @req_refl795 cases s whd in ⊢ (? → ? → ??%?); #l #r >leq_refl normalize @req_refl 795 796 qed. 796 797 … … 801 802 try @eq_addressing_mode_refl 802 803 [1,2,3,4,5,6,7,8,10,16,17,18,19,20: 803 whd in ⊢ (??%?) 804 whd in ⊢ (??%?); 804 805 try % 805 806 >eq_addressing_mode_refl 806 807 >eq_addressing_mode_refl % 807 808 |13,15: 808 whd in ⊢ (??%?) 809 whd in ⊢ (??%?); 809 810 cases arg1 810 811 [*: … … 813 814 ] 814 815 |11,12: 815 whd in ⊢ (??%?) 816 whd in ⊢ (??%?); 816 817 cases arg1 817 818 [1: … … 832 833 ] 833 834 |14: 834 whd in ⊢ (??%?) 835 whd in ⊢ (??%?); 835 836 cases arg1 836 837 [ #arg1_left normalize nodelta … … 857 858 ] 858 859 |*: 859 whd in ⊢ (??%?) 860 whd in ⊢ (??%?); 860 861 cases arg1 861 862 [*: #arg1 >eq_sum_refl … … 918 919 [1,2,3,4,5,6: #arg1 @eq_addressing_mode_refl 919 920 |7: #arg1 #arg2 920 whd in ⊢ (??%?) 921 whd in ⊢ (??%?); 921 922 >eq_addressing_mode_refl 922 923 >eq_addressing_mode_refl … … 1076 1077 [ % 1077 1078 | #n #hd #tl #ih 1078 normalize in ⊢ (???%) %1079 normalize in ⊢ (???%); % 1079 1080 ] 1080 1081 qed. 1081 1082 1082 1083 lemma 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 ⊢ (??%? → ?%%??); // 1084 1085 #n #hd #tl #abs @⊥ destruct (abs) 1085 1086 qed. … … 1087 1088 lemma Vector_Sn: ∀A. ∀n.∀v:Vector A (S n). 1088 1089 ∃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 ⊢ (??%? → ??(λ_.??(λ_.?%%??))); 1090 1091 [ #abs @⊥ destruct (abs) 1091 1092 | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ] … … 1123 1124 〈q, r〉 = 〈[[ ]], r〉. 1124 1125 #A #n #q #r 1125 generalize in match (Vector_O A q …) 1126 generalize in match (Vector_O A q …); 1126 1127 #hyp 1127 >hyp in ⊢ (??%?) 1128 >hyp in ⊢ (??%?); 1128 1129 % 1129 1130 qed. … … 1244 1245 encoding_check code_memory (bitvector_of_nat … intermediate_pc) (bitvector_of_nat … final_pc) l2. 1245 1246 #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/ 1247 1248 | #hd #tl #IH #pc #l2 * #H1 #H2 >half_add_SO in H2; #H2 cases (IH … H2) <plus_n_Sm 1248 1249 #K1 #K2 % [2:@K2] whd % // >half_add_SO @K1 ] … … 1282 1283 68,69,70,71: #ARG2]] 1283 1284 [1,2,19,20: #arg3 @(list_addressing_mode_tags_elim_prop … arg3) whd try % -arg3 #ARG3] 1284 normalize in ⊢ (???% → ?) 1285 normalize in ⊢ (???% → ?); 1285 1286 [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 1290 1292 whd in ⊢ (let fetched ≝ ??% in ?) <H1 whd in ⊢ (let fetched ≝ % in ?) 1291 1293 [17,18,19,20,21,22,23,24,25,26,31,34,35,36,37,38: <H3] … … 1293 1295 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, 1294 1296 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*) 1296 1298 qed. 1297 1299
Note: See TracChangeset
for help on using the changeset viewer.