Changeset 1578
 Timestamp:
 Dec 1, 2011, 1:12:49 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r1562 r1578 736 736 λj1.λj2.jmple j1 j2 ∨ j1 = j2. 737 737 738 lemma dec_jmple: ∀x,y:jump_length.jmple x y + ¬(jmple x y). 739 #x #y cases x cases y /3 by inl, inr, nmk, I/ 740 qed. 741 738 742 lemma jmpleq_max_length: ∀ol,nl. 739 743 jmpleq ol (max_length ol nl). … … 799 803 800 804 definition jump_expansion_start: ∀program:list labelled_instruction. 801 Σpolicy:jump_expansion_policy.(∀i.i ≥ program → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧ jump_in_policy program policy ≝ 805 Σpolicy:jump_expansion_policy. 806 (∀i.i ≥ program → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧ 807 jump_in_policy program policy ∧ 808 ∀i.i < program → is_jump (nth i ? program 〈None ?, Comment []〉) → 809 lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈0,short_jump〉 ≝ 802 810 λprogram. 803 811 foldl_strong (option Identifier × pseudo_instruction) 804 (λprefix.Σpolicy:jump_expansion_policy.(∀i.i ≥ prefix → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧ jump_in_policy prefix policy) 812 (λprefix.Σpolicy:jump_expansion_policy. 813 (∀i.i ≥ prefix → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧ 814 jump_in_policy prefix policy ∧ 815 ∀i.i < prefix → is_jump (nth i ? prefix 〈None ?, Comment []〉) → 816 lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈0,short_jump〉) 805 817 program 806 818 (λprefix.λx.λtl.λprf.λpolicy. … … 824 836 ] 825 837 ) (Stub ? ?). 826 @conj 827 (* nonjumps, lookup_opt = None *) 828 [1,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,69,71,73,75,77,79,81,83: 838 [1,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,35,36,37,38,39,40,41,42: 839 @conj 840 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55,57,59,61: 841 @conj 842 #i >append_length <commutative_plus #Hi normalize in Hi; 843 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55,57,59,61: 844 cases (le_to_or_lt_eq … Hi) Hi; #Hi @(proj1 ?? (proj1 ?? (sig2 ?? policy)) i) 845 [2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56,58,60,62: 846 <Hi @le_n_Sn 847 ] 848 @le_S_to_le @le_S_to_le @Hi 849 ] 850 cases (le_to_or_lt_eq … Hi) Hi; #Hi 851 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55,57,59,61: 852 >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) 853 @(proj2 ?? (proj1 ?? (sig2 ?? policy)) i (le_S_S_to_le … Hi)) 854 ] 855 @conj >(injective_S … Hi) 856 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55,57,59,61: 857 >(nth_append_second ? ? prefix ? ? (le_n (prefix))) <minus_n_n #H @⊥ @H 858 ] 859 #H elim H; H; #t1 #H elim H; H #t2 #H 860 lapply (proj1 ?? (proj1 ?? (sig2 ?? policy)) (prefix) (le_n (prefix))) 861 #H2 >H2 in H; #H destruct (H) 862 ] 863 #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) 864 Hi; #Hi 865 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55,57,59,61: 866 #Hj @(proj2 ?? (sig2 ?? policy) i (le_S_S_to_le … Hi)) 867 >(nth_append_first ?? prefix ?? (le_S_S_to_le ?? Hi)) in Hj; // 868 ] 869 >(injective_S … Hi) >(nth_append_second ?? prefix ?? (le_n (prefix))) <minus_n_n 870 #H @⊥ @H 871 2,3,26,27,28,29,30,31,32,33,34: @conj 872 [1,3,5,7,9,11,13,15,17,19,21: @conj 873 [1,3,5,7,9,11,13,15,17,19,21: 874 #i >append_length <commutative_plus #Hi normalize in Hi; >lookup_opt_insert_miss 875 [1,3,5,7,9,11,13,15,17,19,21: 876 @(proj1 ?? (proj1 ?? (sig2 ?? policy)) i (le_S_to_le … Hi)) 877 ] 878 >eq_bv_sym @bitvector_of_nat_abs @lt_to_not_eq @Hi 879 ] 829 880 #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) 830 Hi; #Hi @((proj1 ?? (sig2 ?? policy)) i) 831 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55,57,59,61,63,65: 832 @le_S_to_le @le_S_to_le @Hi 833 2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56,58,60,62,64,66: 834 <Hi @le_n_Sn 881 Hi #Hi 882 [1,3,5,7,9,11,13,15,17,19,21: 883 >(nth_append_first ?? prefix ?? (le_S_S_to_le … Hi)) >lookup_opt_insert_miss 884 [1,3,5,7,9,11,13,15,17,19,21: 885 @(proj2 ?? (proj1 ?? (sig2 ?? policy)) i (le_S_S_to_le … Hi)) 886 ] 887 @bitvector_of_nat_abs @(lt_to_not_eq … (le_S_S_to_le … Hi)) 835 888 ] 836 (* nonjumps, lookup_opt = Some *) 837 2,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,70,72,74,76,78,80,82,84: 838 #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) 839 Hi; #Hi 840 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55,57,59,61,63,65: 841 >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) 842 @((proj2 ?? (sig2 ?? policy)) i (le_S_S_to_le … Hi)) 843 2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56,58,60,62,64,66: 844 @conj >(injective_S … Hi) 845 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55,57,59,61,63,65: 846 >(nth_append_second ? ? prefix ? ? (le_n (prefix))) 847 <minus_n_n #H @⊥ @H 848 2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56,58,60,62,64,66: 849 #H elim H; H; #t1 #H elim H; H #t2 #H 850 lapply (proj1 ?? (sig2 ?? policy) (prefix) (le_n (prefix))) 851 #H2 >H2 in H; #H destruct (H) 852 ] 889 @conj >(injective_S … Hi) #H 890 [2,4,6,8,10,12,14,16,18,20,22: 891 >(nth_append_second ?? prefix ?? (le_n (prefix))) <minus_n_n // 853 892 ] 854 (* jumps, lookup_opt = None *) 855 3,5,51,53,55,57,59,61,63,65,67: #i >append_length <commutative_plus #Hi normalize in Hi; 856 >lookup_opt_insert_miss 857 [1,3,5,7,9,11,13,15,17,19,21,23: @((proj1 ?? (sig2 ?? policy)) i) @(le_S_to_le … Hi) 858 2,4,6,8,10,12,14,16,18,20,22,24: >eq_bv_sym @bitvector_of_nat_abs @lt_to_not_eq @Hi 893 @(ex_intro ?? 0 (ex_intro ?? short_jump (lookup_opt_insert_hit ?? 16 ? policy))) 894 ] 895 #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) 896 Hi #Hi 897 [1,3,5,7,9,11,13,15,17,19,21: 898 >(nth_append_first ?? prefix ?? (le_S_S_to_le … Hi)) #Hj >lookup_opt_insert_miss 899 [1,3,5,7,9,11,13,15,17,19,21: 900 @(proj2 ?? (sig2 ?? policy) i (le_S_S_to_le … Hi) Hj) 859 901 ] 860 (* nonjumps, lookup_opt = Some *) 861 4,6,52,54,56,58,60,62,64,66,68: #i >append_length <commutative_plus #Hi normalize in Hi; 862 cases (le_to_or_lt_eq … Hi) Hi; #Hi 863 [1,3,5,7,9,11,13,15,17,19,21,23: >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) 864 >lookup_opt_insert_miss 865 [1,3,5,7,9,11,13,15,17,19,21,23: @((proj2 ?? (sig2 ?? policy)) i) @(le_S_S_to_le … Hi) 866 2,4,6,8,10,12,14,16,18,20,22,24: @bitvector_of_nat_abs @(lt_to_not_eq … (le_S_S_to_le … Hi)) 867 ] 868 2,4,6,8,10,12,14,16,18,20,22,24: @conj >(injective_S … Hi) #H 869 [2,4,6,8,10,12,14,16,18,20,22,24: >(nth_append_second ? ? prefix ? ? (le_n (prefix))) 870 <minus_n_n // ] 871 @(ex_intro ? ? 0 (ex_intro ? ? short_jump (lookup_opt_insert_hit ? ? 16 ? policy))) 902 @bitvector_of_nat_abs @(lt_to_not_eq … (le_S_S_to_le … Hi)) 903 ] 904 #_ >(injective_S … Hi) @lookup_opt_insert_hit 905 @conj 906 [@conj 907 [ #i #Hi // 908  whd #i #Hi @⊥ @(absurd (i < 0) Hi (not_le_Sn_O ?)) 872 909 ] 873 (* cases for the empty program *) 874 85: #i #Hi // 875 86: whd #i #Hi @⊥ @(absurd (i < 0)) [ @Hi  @not_le_Sn_O ] 910  #i #Hi >nth_nil #Hj @⊥ @Hj 876 911 ] 877 912 qed. … … 1075 1110  S m ⇒ jump_expansion_step program (jump_expansion_internal program m) 1076 1111 ]. 1077 [ @( sig2 … (jump_expansion_start program))1078  @(proj1 … (sig2 …(jump_expansion_step program (jump_expansion_internal program m))))1112 [ @(proj1 ?? (sig2 ?? (jump_expansion_start program))) 1113  @(proj1 ?? (sig2 ?? (jump_expansion_step program (jump_expansion_internal program m)))) 1079 1114 ] 1080 1115 qed. … … 1193 1228 1194 1229 lemma not_exists_forall: 1195 ∀A:Type[0].∀P:A → Prop.¬(∃x.P x) → ∀x.¬P x. 1196 #A #P #Hex #x @nmk #Habs @(absurd ? ? Hex) @(ex_intro … x) @Habs 1197 qed. 1198 1199 lemma de_morgan1: 1230 ∀k:ℕ.∀P:ℕ → Prop.¬(∃x.x < k ∧ P x) → ∀x.x < k → ¬P x. 1231 #k #P #Hex #x #Hx @nmk #Habs @(absurd ? ? Hex) @(ex_intro … x) 1232 @conj [ @Hx  @Habs ] 1233 qed. 1234 1235 lemma not_forall_exists: 1236 ∀k:ℕ.∀P:ℕ → Prop.(∀n.(P n) + (¬P n)) → ¬(∀x.x < k → P x) → ∃x.x < k ∧ ¬P x. 1237 #k #P #Hdec elim k 1238 [ #Hfa @⊥ @(absurd ?? Hfa) #z #Hz @⊥ @(absurd ? Hz) @not_le_Sn_O 1239  k #k #Hind #Hfa cases (Hdec k) 1240 [ #HP elim (Hind ?) 1241 [ Hind; #x #Hx @(ex_intro ?? x) @conj [ @le_S @(proj1 ?? Hx)  @(proj2 ?? Hx) ] 1242  @nmk #H @(absurd ?? Hfa) #x #Hx cases (le_to_or_lt_eq ?? Hx) 1243 [ #H2 @H @(le_S_S_to_le … H2) 1244  #H2 >(injective_S … H2) @HP 1245 ] 1246 ] 1247  #HP @(ex_intro … k) @conj [ @le_n  @HP ] 1248 ] 1249 ] 1250 qed. 1251 1252 (* lemma de_morgan1: 1200 1253 ∀A,B:Prop.¬(A ∧ ¬B) → A → ¬¬B. 1201 1254 #A #B #Hnot #HA @nmk #H @(absurd (A∧¬B)) [ % [ @HA  @H ]  @Hnot ] 1202 qed. 1255 qed. *) 1203 1256 1204 1257 lemma thingie: … … 1215 1268 qed. 1216 1269 1217 lemma incr_or_equal: ∀program:list labelled_instruction.1270 (* lemma incr_or_equal: ∀program:list labelled_instruction. 1218 1271 ∀policy:(Σp:jump_expansion_policy. 1219 1272 (∀i.i ≥ program → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧ 1220 1273 jump_in_policy program p). 1221 1274 policy_equal program policy (jump_expansion_step program policy) ∨ 1222 ∃n:ℕ. jmple1275 ∃n:ℕ.n < (program) ∧ jmple 1223 1276 (\snd (bvt_lookup … (bitvector_of_nat ? n) policy 〈0,short_jump〉)) 1224 1277 (\snd (bvt_lookup … (bitvector_of_nat ? n) (jump_expansion_step program policy) 〈0,short_jump〉)). … … 1230 1283 [ #H %2 elim H H; #i #Hi 1231 1284 cases (proj2 ?? (sig2 ?? (jump_expansion_step program policy)) i (proj1 ?? Hi)) 1232 [ #H @(ex_intro … i H)1285 [ #H @(ex_intro ?? i (conj ?? (proj1 ?? Hi) H)) 1233 1286  #H @⊥ @(absurd ? H (proj2 ?? Hi)) 1234 1287 ] … … 1241 1294 ] 1242 1295 ] 1243 qed. 1296 qed. *) 1297 1298 lemma policy_not_equal_incr: ∀program:list labelled_instruction. 1299 ∀policy:(Σp:jump_expansion_policy. 1300 (∀i.i ≥ program → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧ 1301 jump_in_policy program p). 1302 ¬policy_equal program policy (jump_expansion_step program policy) → 1303 ∃n:ℕ.n < (program) ∧ jmple 1304 (\snd (bvt_lookup … (bitvector_of_nat ? n) policy 〈0,short_jump〉)) 1305 (\snd (bvt_lookup … (bitvector_of_nat ? n) (jump_expansion_step program policy) 〈0,short_jump〉)). 1306 #program #policy #Hp 1307 cases (dec_bounded_exists (λn.jmple 1308 (\snd (bvt_lookup ?? (bitvector_of_nat ? n) policy 〈0,short_jump〉)) 1309 (\snd (bvt_lookup ?? (bitvector_of_nat ? n) (jump_expansion_step program policy) 〈0,short_jump〉))) ? (program)) 1310 [ #H elim H; H #i #Hi @(ex_intro ?? i) @Hi 1311  #abs @⊥ @(absurd ?? Hp) #n #Hn cases (proj2 ?? (sig2 ?? (jump_expansion_step program policy)) n Hn) 1312 [ #Hj @⊥ @(absurd ?? abs) @(ex_intro ?? n) @conj [ @Hn  @Hj ] 1313  #H @H 1314 ] 1315  #n @dec_jmple 1316 ] 1317 qed. 1318 1319 lemma stupid: 1320 ∀program,n. 1321 eject … (jump_expansion_step program (jump_expansion_internal program n)) = 1322 eject … (jump_expansion_internal program (S n)). 1323 // 1324 qed. 1325 1326 let rec measure_int (program: list labelled_instruction) (policy: jump_expansion_policy) (acc: ℕ) 1327 on program: ℕ ≝ 1328 match program with 1329 [ nil ⇒ acc 1330  cons h t ⇒ match (\snd (bvt_lookup ?? (bitvector_of_nat ? (t)) policy 〈0,short_jump〉)) with 1331 [ long_jump ⇒ measure_int t policy (acc + 2) 1332  medium_jump ⇒ measure_int t policy (acc + 1) 1333  _ ⇒ measure_int t policy acc 1334 ] 1335 ]. 1336 1337 definition measure ≝ 1338 λprogram.λpolicy.measure_int program policy 0. 1339 1340 (* lemma measure_le: ∀program.∀policy.∀x,y:ℕ. 1341 x ≤ y → measure_int program policy x ≤ measure_int program policy y. 1342 #program #policy 1343 elim program 1344 [ // 1345  #h #t #Hind #x #y #Hxy whd in match (measure_int ??x); whd in match (measure_int ??y); 1346 cases (\snd (lookup … (bitvector_of_nat ? (t)) policy 〈0,short_jump〉)) 1347 [ @Hind @Hxy 1348 2,3: @Hind @monotonic_le_plus_l @Hxy 1349 ] 1350 ] 1351 qed. *) 1352 1353 lemma measure_plus: ∀program.∀policy.∀x,d:ℕ. 1354 measure_int program policy (x+d) = measure_int program policy x + d. 1355 #program #policy #x #d generalize in match x; x elim d 1356 [ // 1357  d; #d #Hind elim program 1358 [ // 1359  #h #t #Hd #x whd in match (measure_int ???); whd in match (measure_int ?? x); 1360 cases (\snd (lookup … (bitvector_of_nat ? (t)) policy 〈0,short_jump〉)) 1361 [ normalize nodelta @Hd 1362 2,3: normalize nodelta >associative_plus >(commutative_plus (S d) ?) <associative_plus 1363 @Hd 1364 ] 1365 ] 1366 ] 1367 qed. 1368 1369 lemma measure_incr_or_equal: ∀program.∀policy:Σp:jump_expansion_policy. 1370 (∀i.i ≥ program → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧ 1371 jump_in_policy program p.∀l.l ≤ program → ∀acc:ℕ. 1372 measure_int l policy acc ≤ measure_int l (jump_expansion_step program policy) acc. 1373 #program #policy #l (* lapply (le_n (program)) *) elim l l; 1374 [ #Hp #acc normalize @le_n 1375  #h #t #Hind #Hp #acc 1376 cases (proj2 ?? (sig2 ?? (jump_expansion_step program policy)) (t) ?) 1377 [ whd in match (measure_int ???); whd in match (measure_int ?(jump_expansion_step ??)?); 1378 cases (\snd (bvt_lookup ?? (bitvector_of_nat ? (t)) policy 〈0,short_jump〉)) 1379 cases (\snd (bvt_lookup ?? (bitvector_of_nat ? (t)) (jump_expansion_step program policy) 〈0,short_jump〉)) 1380 [1,4,5,7,8,9: #H @⊥ @H 1381 2,3,6: #_ normalize nodelta 1382 [1,2: @(transitive_le ? (measure_int t (jump_expansion_step program policy) acc)) 1383 3: @(transitive_le ? (measure_int t (jump_expansion_step program policy) (acc+1))) 1384 ] 1385 [1,3,5: @Hind @(transitive_le … Hp) @le_n_Sn 1386 2,4,6: >measure_plus [1,2: @le_plus_n_r] >measure_plus @le_plus [ @le_n  //] 1387 ] 1388 ] 1389  #Heq whd in match (measure_int ???); whd in match (measure_int ?(jump_expansion_step ??)?); 1390 >Heq cases (\snd (lookup … (bitvector_of_nat ? (t)) ? 〈0,short_jump〉)) 1391 [ normalize nodelta @Hind @(transitive_le … Hp) @le_n_Sn 1392  normalize nodelta @Hind @(transitive_le … Hp) @le_n_Sn 1393  normalize nodelta @Hind @(transitive_le … Hp) @le_n_Sn 1394 ] 1395  @Hp 1396 ] 1397 ] 1398 qed. 1399 1400 lemma measure_le: ∀program.∀policy. 1401 measure_int program policy 0 ≤ 2*program. 1402 #program #policy elim program 1403 [ normalize @le_n 1404  #h #t #Hind whd in match (measure_int ???); 1405 cases (\snd (lookup ?? (bitvector_of_nat ? (t)) policy 〈0,short_jump〉)) 1406 [ normalize nodelta @(transitive_le ??? Hind) /2 by monotonic_le_times_r/ 1407 2,3: normalize nodelta >measure_plus <times_n_Sm >(commutative_plus 2 ?) 1408 @le_plus [1,3: @Hind 2,4: // ] 1409 ] 1410 ] 1411 qed. 1412 1413 lemma bla: ∀a,b:ℕ.a + a = b + b → a = b. 1414 #a elim a 1415 [ normalize #b // 1416  a #a #Hind #b cases b [ /2 by le_n_O_to_eq/  b #b normalize 1417 <plus_n_Sm <plus_n_Sm #H 1418 >(Hind b (injective_S ?? (injective_S ?? H))) // ] 1419 ] 1420 qed. 1421 1422 lemma sth_not_s: ∀x.x ≠ S x. 1423 #x cases x 1424 [ //  #y // ] 1425 qed. 1426 1427 lemma measure_full: ∀program.∀policy. 1428 measure_int program policy 0 = 2*program → ∀i.i<program → 1429 (\snd (bvt_lookup ?? (bitvector_of_nat ? i) policy 〈0,short_jump〉)) = long_jump. 1430 #program #policy elim program 1431 [ #Hm #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O 1432  #h #t #Hind #Hm #i #Hi cut (measure_int t policy 0 = 2*t) 1433 [ whd in match (measure_int ???) in Hm; 1434 cases (\snd (lookup … (bitvector_of_nat ? (t)) policy 〈0,short_jump〉)) in Hm; 1435 normalize nodelta 1436 [ #H @⊥ @(absurd ? (measure_le t policy)) >H @lt_to_not_le /2 by lt_plus, le_n/ 1437  >measure_plus >commutative_plus #H @⊥ @(absurd ? (measure_le t policy)) 1438 <(plus_to_minus … (sym_eq … H)) @lt_to_not_le normalize 1439 >(commutative_plus (t) 0) <plus_O_n <minus_n_O 1440 >plus_n_Sm @le_n 1441  >measure_plus <times_n_Sm >commutative_plus #H lapply (injective_plus_r … H) // 1442 ] 1443  #Hmt cases (le_to_or_lt_eq … Hi) Hi; 1444 [ #Hi @(Hind Hmt i (le_S_S_to_le … Hi)) 1445  #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm; 1446 cases (\snd (lookup … (bitvector_of_nat ? (t)) policy 〈0,short_jump〉)) in Hm; 1447 normalize nodelta 1448 [ >Hmt normalize <plus_n_O >(commutative_plus (t) (S (t))) 1449 >plus_n_Sm #H @⊥ @(absurd ? (bla ?? H)) @sth_not_s 1450  >measure_plus >Hmt normalize <plus_n_O >commutative_plus normalize 1451 #H @⊥ @(absurd ? (injective_plus_r … (injective_S ?? H))) @sth_not_s 1452  #_ // 1453 ] 1454 ]] 1455 ] 1456 qed. 1457 1458 lemma eq_plus_S_to_lt: 1459 ∀n,m,p:ℕ.n = m + (S p) → m < n. 1460 // 1461 qed. 1462 1463 lemma measure_special: ∀program.∀policy:Σp:jump_expansion_policy. 1464 (∀i.i ≥ program → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧ 1465 jump_in_policy program p. 1466 measure_int program policy 0 = measure_int program (jump_expansion_step program policy) 0 → 1467 policy_equal program policy (jump_expansion_step program policy). 1468 #program lapply (le_n (program)) elim program in ⊢ (?%? → ∀policy.??(?%??)(?%??) → ?%??); 1469 [ #_ #policy #Hm #i #Hi @⊥ @(absurd ? Hi) @not_le_Sn_O 1470  #h #t #Hind #Hp #policy #Hm #i #Hi cases (le_to_or_lt_eq … Hi) Hi; 1471 [ #Hi @Hind 1472 [ @(transitive_le … Hp) // 1473  whd in match (measure_int ???) in Hm; whd in match (measure_int ?(jump_expansion_step ??)?) in Hm; 1474 lapply (proj2 ?? (sig2 ?? (jump_expansion_step program policy)) (t) ?) 1475 [ @(lt_to_le_to_lt … (h::t)) [ //  @Hp ] 1476  cases (\snd (bvt_lookup ?? (bitvector_of_nat ? (t)) policy 〈0,short_jump〉)) in Hm; 1477 cases (\snd (bvt_lookup ?? (bitvector_of_nat ? (t)) (jump_expansion_step program policy) 〈0,short_jump〉)); 1478 normalize nodelta 1479 [1: #H #_ @H 1480 2,3: >measure_plus #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt 1481 @measure_incr_or_equal @(transitive_le … Hp) @le_n_Sn 1482 4,7,8: #_ #H elim H #H2 [1,3,5: @⊥ @H2 2,4,6: destruct (H2) ] 1483 5: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 1) 1484 #H #_ @(injective_plus_r … H) 1485 6: >measure_plus >measure_plus 1486 change with (1+1) in match (2); >assoc_plus1 >(commutative_plus 1 (measure_int ???)) 1487 #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l 1488 @measure_incr_or_equal @(transitive_le … Hp) @le_n_Sn 1489 9: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 2) 1490 #H #_ @(injective_plus_r … H) 1491 ] 1492 ] 1493  @(le_S_S_to_le … Hi) 1494 ] 1495  #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm; 1496 whd in match (measure_int ?(jump_expansion_step ??)?) in Hm; 1497 lapply (proj2 ?? (sig2 ?? (jump_expansion_step program policy)) (t) ?) 1498 [ @(lt_to_le_to_lt … (h::t)) [ //  @Hp ] 1499  cases (\snd (bvt_lookup ?? (bitvector_of_nat ? (t)) policy 〈0,short_jump〉)) in Hm; 1500 cases (\snd (bvt_lookup ?? (bitvector_of_nat ? (t)) (jump_expansion_step program policy) 〈0,short_jump〉)); 1501 normalize nodelta 1502 [1,5,9: #_ #_ // 1503 4,7,8: #_ #H elim H #H2 [1,3,5: @⊥ @H2 2,4,6: destruct (H2) ] 1504 2,3: >measure_plus #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt 1505 @measure_incr_or_equal @(transitive_le … Hp) @le_n_Sn 1506 6: >measure_plus >measure_plus 1507 change with (1+1) in match (2); >assoc_plus1 >(commutative_plus 1 (measure_int ???)) 1508 #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l 1509 @measure_incr_or_equal @(transitive_le … Hp) @le_n_Sn 1510 ] 1511 ] 1512 ] 1513 ] 1514 qed. 1515 1516 lemma dec_is_jump: ∀x.(is_jump x) + (¬is_jump x). 1517 #x cases x #l #i cases i 1518 [#id cases id 1519 [1,2,3,6,7,33,34: 1520 #x #y %2 whd in match (is_jump ?); /2 by nmk/ 1521 4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: 1522 #x %2 whd in match (is_jump ?); /2 by nmk/ 1523 35,36,37: %2 whd in match (is_jump ?); /2 by nmk/ 1524 9,10,14,15: #x %1 // 1525 11,12,13,16,17: #x #y %1 // 1526 ] 1527 2,3: #x %2 /2 by nmk/ 1528 4,5: #x %1 // 1529 6: #x #y %2 /2 by nmk/ 1530 ] 1531 qed. 1532 1533 lemma measure_zero: ∀l.∀program. 1534 l ≤ program → measure_int l (jump_expansion_internal program 0) 0 = 0. 1535 #l #program elim l (* lapply (le_n (program)) elim program in ⊢ (?%? → ?%(?%??)?); *) 1536 [ // 1537  #h #t #Hind #Hp whd in match (measure_int ???); 1538 cases (dec_is_jump (nth (t) ? program 〈None ?, Comment []〉)) #Hj 1539 [ >(lookup_opt_lookup_hit … (proj2 ?? (sig2 ?? (jump_expansion_start program)) (t) ? Hj) 〈0,short_jump〉) 1540 [ normalize nodelta @Hind @le_S_to_le ] 1541 @Hp 1542  >(lookup_opt_lookup_miss … (proj1 ?? (jump_not_in_policy program (jump_expansion_internal program 0) (t) ?) Hj) 〈0,short_jump〉) 1543 [ normalize nodelta @Hind @le_S_to_le ] 1544 @Hp 1545 ] 1546 ] 1547 qed. 1548 1549 definition je_fixpoint: ∀program:list labelled_instruction. 1550 Σp:jump_expansion_policy.∃n.∀k.n < k → policy_equal program (jump_expansion_internal program k) p. 1551 #program @(dp … (jump_expansion_internal program (2*program))) 1552 @(ex_intro … (2*program)) #k #Hk 1553 cases (dec_bounded_exists (λk.policy_equal program (jump_expansion_internal program k) 1554 (jump_expansion_internal program (S k))) ? (2*program)) 1555 [ #H elim H H #x #Hx @pe_trans 1556 [ @(jump_expansion_internal program x) 1557  @pe_sym @equal_remains_equal 1558 [ @(proj2 ?? Hx) 1559  @(transitive_le ? (2*program)) 1560 [ @le_S_S_to_le @le_S @(proj1 ?? Hx) 1561  @le_S_S_to_le @le_S @Hk 1562 ] 1563 ] 1564  @equal_remains_equal 1565 [ @(proj2 ?? Hx) 1566  @le_S_S_to_le @le_S @(proj1 ?? Hx) 1567 ] 1568 ] 1569  #Hnex lapply (not_exists_forall … Hnex) Hnex; #Hfa @pe_sym @equal_remains_equal 1570 [ lapply (measure_full program (jump_expansion_internal program (2*program))) 1571 #Hfull #i #Hi 1572 lapply (proj2 ?? (sig2 ?? (jump_expansion_step program (jump_expansion_internal program (2*program)))) i Hi) 1573 >(Hfull ? i Hi) 1574 [ cases (\snd (bvt_lookup ?? (bitvector_of_nat 16 i) (jump_expansion_step program (jump_expansion_internal program (2*program))) 〈0,short_jump〉)) 1575 [1,2: #H elim H #H2 [1,3: @⊥ @H2 2,4: destruct (H2) ] 1576  #_ // 1577 ] 1578  i @le_to_le_to_eq 1579 [ @measure_le 1580  lapply (le_n (2*program)) elim (2*program) in ⊢ (?%? → %); 1581 [ #_ >measure_zero @le_n 1582  #x #Hind #Hx 1583 cut (measure_int program (jump_expansion_internal program x) 0 < 1584 measure_int program (jump_expansion_internal program (S x)) 0) 1585 [ elim (le_to_or_lt_eq … 1586 (measure_incr_or_equal program (jump_expansion_internal program x) program (le_n (program)) 0)) 1587 [ // 1588  #H @⊥ @(absurd ?? (Hfa x Hx)) @measure_special @H 1589 ] 1590  #H lapply (Hind (le_S_to_le … Hx)) #H2 @(le_to_lt_to_lt … H) @H2 1591 ] 1592 ] 1593 ] 1594 ] 1595  @le_S_to_le @Hk 1596 ] 1597  #n @dec_bounded_forall #m @dec_eq_jump_length 1598 ] 1599 qed. 1244 1600 1245 1601 (**************************************** START OF POLICY ABSTRACTION ********************) 1246 1602 1247 definition policy_type 1603 definition policy_type≝ Word → jump_length. 1248 1604 1249 1605 definition jump_expansion': pseudo_assembly_program → policy_type ≝
Note: See TracChangeset
for help on using the changeset viewer.