Changeset 1578


Ignore:
Timestamp:
Dec 1, 2011, 1:12:49 PM (8 years ago)
Author:
boender
Message:
  • proof of termination of policy completed (needs some clean-up work though)
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r1562 r1578  
    736736  λj1.λj2.jmple j1 j2 ∨ j1 = j2.
    737737 
     738lemma 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/
     740qed.
     741 
    738742lemma jmpleq_max_length: ∀ol,nl.
    739743  jmpleq ol (max_length ol nl).
     
    799803 
    800804definition 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〉 ≝
    802810  λprogram.
    803811  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〉)
    805817  program
    806818  (λprefix.λx.λtl.λprf.λpolicy.
     
    824836   ]
    825837  ) (Stub ? ?).
    826 @conj
    827 (* non-jumps, 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  ]
    829880  #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))
    835888  ]
    836 (* non-jumps, 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 //
    853892  ]
    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)
    859901  ]
    860 (* non-jumps, 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 ?))
    872909  ]
    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
    876911]
    877912qed.
     
    10751110  | S m ⇒ jump_expansion_step program (jump_expansion_internal program m)
    10761111  ].
    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))))
    10791114]
    10801115qed.
     
    11931228
    11941229lemma 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 ]
     1233qed.
     1234
     1235lemma 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 ]
     1250qed.
     1251
     1252(* lemma de_morgan1:
    12001253 ∀A,B:Prop.¬(A ∧ ¬B) → A → ¬¬B.
    12011254 #A #B #Hnot #HA @nmk #H @(absurd (A∧¬B)) [ % [ @HA | @H ] | @Hnot ]
    1202 qed.
     1255qed. *)
    12031256
    12041257lemma thingie:
     
    12151268qed.
    12161269
    1217 lemma incr_or_equal: ∀program:list labelled_instruction.
     1270(* lemma incr_or_equal: ∀program:list labelled_instruction.
    12181271  ∀policy:(Σp:jump_expansion_policy.
    12191272    (∀i.i ≥ |program| → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧
    12201273    jump_in_policy program p).
    12211274  policy_equal program policy (jump_expansion_step program policy) ∨
    1222   ∃n:ℕ.jmple
     1275  ∃n:ℕ.n < (|program|) ∧ jmple
    12231276    (\snd (bvt_lookup … (bitvector_of_nat ? n) policy 〈0,short_jump〉))
    12241277    (\snd (bvt_lookup … (bitvector_of_nat ? n) (jump_expansion_step program policy) 〈0,short_jump〉)).
     
    12301283   [ #H %2 elim H -H; #i #Hi
    12311284     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))
    12331286     | #H @⊥ @(absurd ? H (proj2 ?? Hi))
    12341287     ]
     
    12411294     ]
    12421295   ]
    1243 qed. 
     1296qed. *)
     1297
     1298lemma 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 ]
     1317qed.
     1318
     1319lemma stupid:
     1320  ∀program,n.
     1321  eject … (jump_expansion_step program (jump_expansion_internal program n)) =
     1322  eject … (jump_expansion_internal program (S n)).
     1323 //
     1324qed.
     1325
     1326let 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
     1337definition 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 ]
     1351qed. *)
     1352
     1353lemma 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 ]
     1367qed.
     1368   
     1369lemma 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  ]
     1398qed.
     1399
     1400lemma 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 ]
     1411qed.
     1412
     1413lemma 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 ]
     1420qed.
     1421
     1422lemma sth_not_s: ∀x.x ≠ S x.
     1423 #x cases x
     1424 [ // | #y // ]
     1425qed.
     1426
     1427lemma 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 ]
     1456qed.
     1457
     1458lemma eq_plus_S_to_lt:
     1459  ∀n,m,p:ℕ.n = m + (S p) → m < n.
     1460 //
     1461qed.
     1462
     1463lemma 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 ] 
     1514qed.
     1515
     1516lemma 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]
     1531qed.
     1532 
     1533lemma 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 ]
     1547qed.
     1548 
     1549definition 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 ]
     1599qed.
    12441600
    12451601(**************************************** START OF POLICY ABSTRACTION ********************)
    12461602
    1247 definition policy_type ≝ Word → jump_length.
     1603definition policy_type≝ Word → jump_length.
    12481604
    12491605definition jump_expansion': pseudo_assembly_program → policy_type ≝
Note: See TracChangeset for help on using the changeset viewer.