Changeset 1593


Ignore:
Timestamp:
Dec 7, 2011, 3:48:32 PM (8 years ago)
Author:
boender
Message:
  • cleaned up Assembly, moved some definitions elsewhere
Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r1592 r1593  
    409409qed.
    410410
     411(* definition of & operations on jump length *)
    411412inductive jump_length: Type[0] ≝
    412413  | short_jump: jump_length
     
    414415  | long_jump: jump_length.
    415416
     417definition max_length: jump_length → jump_length → jump_length ≝
     418  λj1.λj2.
     419  match j1 with
     420  [ long_jump   ⇒ long_jump
     421  | medium_jump ⇒
     422    match j2 with
     423    [ long_jump ⇒ long_jump
     424    | _         ⇒ medium_jump
     425    ]
     426  | short_jump  ⇒ j2
     427  ].
     428
     429definition jmple: jump_length → jump_length → Prop ≝
     430  λj1.λj2.
     431  match j1 with
     432  [ short_jump  ⇒
     433    match j2 with
     434    [ short_jump ⇒ False
     435    | _          ⇒ True
     436    ]
     437  | medium_jump ⇒
     438    match j2 with
     439    [ long_jump ⇒ True
     440    | _         ⇒ False
     441    ]
     442  | long_jump   ⇒ False
     443  ].
     444
     445definition jmpleq: jump_length → jump_length → Prop ≝
     446  λj1.λj2.jmple j1 j2 ∨ j1 = j2.
     447 
     448lemma dec_jmple: ∀x,y:jump_length.jmple x y + ¬(jmple x y).
     449 #x #y cases x cases y /3 by inl, inr, nmk, I/
     450qed.
     451 
     452lemma jmpleq_max_length: ∀ol,nl.
     453  jmpleq ol (max_length ol nl).
     454 #ol #nl cases ol cases nl
     455 /2 by or_introl, or_intror, I/
     456qed.
     457
     458lemma dec_eq_jump_length: ∀a,b:jump_length.(a = b) + (a ≠ b).
     459  #a #b cases a cases b /2/
     460  %2 @nmk #H destruct (H)
     461qed.
     462
     463 
    416464(* jump_expansion_policy: instruction number ↦ 〈pc, jump_length〉 *)
    417465definition jump_expansion_policy ≝ BitVectorTrie (ℕ × jump_length) 16.
     
    548596definition label_map ≝ identifier_map ASMTag (nat × nat).
    549597
     598definition is_label ≝
     599  λx:labelled_instruction.λl:Identifier.
     600  let 〈lbl,instr〉 ≝ x in
     601  match lbl with
     602  [ Some l' ⇒ l' = l
     603  | _       ⇒ False
     604  ].
     605
    550606definition add_instruction_size: ℕ → jump_length → pseudo_instruction → ℕ ≝
    551607  λpc.λjmp_len.λinstr.
     
    557613    ] in
    558614  pc + (|bv|).
    559  
    560 definition is_label ≝
    561   λx:labelled_instruction.λl:Identifier.
    562   let 〈lbl,instr〉 ≝ x in
    563   match lbl with
    564   [ Some l' ⇒ l' = l
    565   | _       ⇒ False
    566   ].
    567  
     615
    568616lemma label_does_not_occur:
    569617  ∀i,p,l.
     
    705753  ].
    706754
    707 definition max_length: jump_length → jump_length → jump_length ≝
    708   λj1.λj2.
    709   match j1 with
    710   [ long_jump   ⇒ long_jump
    711   | medium_jump ⇒
    712     match j2 with
    713     [ long_jump ⇒ long_jump
    714     | _         ⇒ medium_jump
    715     ]
    716   | short_jump  ⇒ j2
    717   ].
    718 
    719 definition jmple: jump_length → jump_length → Prop ≝
    720   λj1.λj2.
    721   match j1 with
    722   [ short_jump  ⇒
    723     match j2 with
    724     [ short_jump ⇒ False
    725     | _          ⇒ True
    726     ]
    727   | medium_jump ⇒
    728     match j2 with
    729     [ long_jump ⇒ True
    730     | _         ⇒ False
    731     ]
    732   | long_jump   ⇒ False
    733   ].
    734 
    735 definition jmpleq: jump_length → jump_length → Prop ≝
    736   λj1.λj2.jmple j1 j2 ∨ j1 = j2.
    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  
    742 lemma jmpleq_max_length: ∀ol,nl.
    743   jmpleq ol (max_length ol nl).
    744  #ol #nl cases ol cases nl
    745  /2 by or_introl, or_intror, I/
    746 qed.
    747  
    748755definition is_jump' ≝
    749756  λx:preinstruction Identifier.
     
    771778  ].
    772779
     780lemma dec_is_jump: ∀x.(is_jump x) + (¬is_jump x).
     781#x cases x #l #i cases i
     782[#id cases id
     783 [1,2,3,6,7,33,34:
     784  #x #y %2 whd in match (is_jump ?); /2 by nmk/
     785 |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32:
     786  #x %2 whd in match (is_jump ?); /2 by nmk/
     787 |35,36,37: %2 whd in match (is_jump ?); /2 by nmk/
     788 |9,10,14,15: #x %1 //
     789 |11,12,13,16,17: #x #y %1 //
     790 ]
     791|2,3: #x %2 /2 by nmk/
     792|4,5: #x %1 //
     793|6: #x #y %2 /2 by nmk/
     794]
     795qed.
     796 
     797
    773798definition jump_in_policy ≝
    774799  λprefix:list labelled_instruction.λpolicy:jump_expansion_policy.
     
    776801  (is_jump (nth i ? prefix 〈None ?, Comment []〉) ↔
    777802   ∃p,j.lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈p,j〉).
    778  
    779 lemma le_S_to_le: ∀n,m:ℕ.S n ≤ m → n ≤ m.
    780  /2/ qed.
    781  
     803
     804(* these should be moved to BitVector at some point *) 
    782805lemma bitvector_of_nat_ok:
    783806  ∀n,x,y:ℕ.x < 2^n → y < 2^n → eq_bv n (bitvector_of_nat n x) (bitvector_of_nat n y) → x = y.
     
    789812
    790813lemma bitvector_of_nat_abs:
    791   ∀n,x,y:ℕ.x < 2^n → y < 2^n → x ≠y → ¬eq_bv n (bitvector_of_nat n x) (bitvector_of_nat n y).
     814  ∀n,x,y:ℕ.x < 2^n → y < 2^n → x ≠ y → ¬eq_bv n (bitvector_of_nat n x) (bitvector_of_nat n y).
    792815 #n #x #y #Hx #Hy #Heq @notb_elim
    793816 lapply (refl ? (eq_bv ? (bitvector_of_nat n x) (bitvector_of_nat n y)))
     
    797820 ]
    798821qed.
    799 
    800822
    801823lemma jump_not_in_policy: ∀prefix:list labelled_instruction.
     
    12131235qed.
    12141236
    1215 lemma le_plus:
    1216   ∀n,m:ℕ.n ≤ m → ∃k:ℕ.m = n + k.
    1217  #n #m elim m -m;
    1218  [ #Hn % [ @O | <(le_n_O_to_eq n Hn) // ]
    1219  | #m #Hind #Hn cases (le_to_or_lt_eq … Hn) -Hn; #Hn
    1220    [ elim (Hind (le_S_S_to_le … Hn)) #k #Hk % [ @(S k) | >Hk // ]
    1221    | % [ @O | <Hn // ]
    1222    ]
    1223  ]
    1224 qed.
    1225 
    1226 theorem plus_Sn_m1: ∀n,m:nat. S m + n = m + S n.
    1227 #n (elim n) normalize /2 by S_pred/ qed.
    1228 
    12291237lemma pe_step: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
    12301238 ∀p1,p2:Σpolicy.
     
    12531261 ]
    12541262qed.
    1255    
     1263
     1264(* this is in the stdlib, but commented out, why? *)
     1265theorem plus_Sn_m1: ∀n,m:nat. S m + n = m + S n.
     1266  #n (elim n) normalize /2 by S_pred/ qed.
     1267
    12561268lemma equal_remains_equal: ∀program:(Σl:list labelled_instruction.|l| < 2^16).∀n:ℕ.
    12571269  policy_equal program (jump_expansion_internal program n) (jump_expansion_internal program (S n)) →
    12581270  ∀k.k ≥ n → policy_equal program (jump_expansion_internal program n) (jump_expansion_internal program k).
    1259  #program #n #Heq #k #Hk elim (le_plus … Hk); #z #H >H -H -Hk -k;
     1271 #program #n #Heq #k #Hk elim (le_plus_k … Hk); #z #H >H -H -Hk -k;
    12601272 lapply Heq -Heq; lapply n -n; elim z -z;
    12611273 [ #n #Heq <plus_n_O @pe_refl 
     
    12671279qed.
    12681280
    1269 lemma dec_bounded_forall:
    1270   ∀P:ℕ → Prop.(∀n.(P n) + (¬P n)) → ∀k.(∀n.n < k → P n) + ¬(∀n.n < k → P n).
    1271  #P #HP_dec #k elim k -k
    1272  [ %1 #n #Hn @⊥ @(absurd (n < 0) Hn) @not_le_Sn_O
    1273  | #k #Hind cases Hind
    1274    [ #Hk cases (HP_dec k)
    1275      [ #HPk %1 #n #Hn cases (le_to_or_lt_eq … Hn)
    1276        [ #H @(Hk … (le_S_S_to_le … H))
    1277        | #H >(injective_S … H) @HPk
    1278        ]
    1279      | #HPk %2 @nmk #Habs @(absurd (P k)) [ @(Habs … (le_n (S k))) | @HPk ]
    1280      ]
    1281    | #Hk %2 @nmk #Habs @(absurd (∀n.n<k→P n)) [ #n' #Hn' @(Habs … (le_S … Hn')) | @Hk ]
    1282    ]
    1283  ]
    1284 qed.
    1285 
    1286 lemma dec_bounded_exists:
    1287   ∀P:ℕ→Prop.(∀n.(P n) + (¬P n)) → ∀k.(∃n.n < k ∧ P n) + ¬(∃n.n < k ∧ P n).
    1288  #P #HP_dec #k elim k -k
    1289  [ %2 @nmk #Habs elim Habs #n #Hn @(absurd (n < 0) (proj1 … Hn)) @not_le_Sn_O
    1290  | #k #Hind cases Hind
    1291    [ #Hk %1 elim Hk #n #Hn @(ex_intro … n) @conj [ @le_S @(proj1 … Hn) | @(proj2 … Hn) ]
    1292    | #Hk cases (HP_dec k)
    1293      [ #HPk %1 @(ex_intro … k) @conj [ @le_n | @HPk ]
    1294      | #HPk %2 @nmk #Habs elim Habs #n #Hn cases (le_to_or_lt_eq … (proj1 … Hn))
    1295        [ #H @(absurd (∃n.n < k ∧ P n)) [ @(ex_intro … n) @conj
    1296          [ @(le_S_S_to_le … H) | @(proj2 … Hn) ] | @Hk ]
    1297        | #H @(absurd (P k)) [ <(injective_S … H) @(proj2 … Hn) | @HPk ]
    1298        ] 
    1299      ]
    1300    ]
    1301  ]
    1302 qed.
    1303 
    1304 lemma not_exists_forall:
    1305   ∀k:ℕ.∀P:ℕ → Prop.¬(∃x.x < k ∧ P x) → ∀x.x < k → ¬P x.
    1306  #k #P #Hex #x #Hx @nmk #Habs @(absurd ? ? Hex) @(ex_intro … x)
    1307  @conj [ @Hx | @Habs ]
    1308 qed.
    1309 
    1310 lemma not_forall_exists:
    1311   ∀k:ℕ.∀P:ℕ → Prop.(∀n.(P n) + (¬P n)) → ¬(∀x.x < k → P x) → ∃x.x < k ∧ ¬P x.
    1312  #k #P #Hdec elim k
    1313  [ #Hfa @⊥ @(absurd ?? Hfa) #z #Hz @⊥ @(absurd ? Hz) @not_le_Sn_O
    1314  | -k #k #Hind #Hfa cases (Hdec k)
    1315    [ #HP elim (Hind ?)
    1316      [ -Hind; #x #Hx @(ex_intro ?? x) @conj [ @le_S @(proj1 ?? Hx) | @(proj2 ?? Hx) ]
    1317      | @nmk #H @(absurd ?? Hfa) #x #Hx cases (le_to_or_lt_eq ?? Hx)
    1318        [ #H2 @H @(le_S_S_to_le … H2)
    1319        | #H2 >(injective_S … H2) @HP
    1320        ]
    1321      ]
    1322    | #HP @(ex_intro … k) @conj [ @le_n | @HP ]
    1323    ]
    1324  ]
    1325 qed.
    1326 
    13271281lemma thingie:
    13281282  ∀A:Prop.(A + ¬A) → (¬¬A) → A.
     
    13331287qed.
    13341288 
    1335 lemma dec_eq_jump_length: ∀a,b:jump_length.(a = b) + (a ≠ b).
    1336   #a #b cases a cases b /2/
    1337   %2 @nmk #H destruct (H)
    1338 qed.
     1289include "utilities/extralib.ma".
    13391290
    13401291lemma policy_not_equal_incr: ∀program:(Σl:list labelled_instruction.|l|<2^16).
     
    14411392qed.
    14421393
     1394(* these lemmas seem superfluous, but not sure how *)
    14431395lemma bla: ∀a,b:ℕ.a + a = b + b → a = b.
    14441396 #a elim a
     
    14861438qed.
    14871439
    1488 lemma eq_plus_S_to_lt:
    1489   ∀n,m,p:ℕ.n = m + (S p) → m < n.
    1490  //
    1491 qed.
    1492 
    1493 (* how to do this with a sigma-type and elimination? *)
    14941440lemma measure_special: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
    14951441  ∀policy:Σp:jump_expansion_policy.
     
    15491495qed.
    15501496
    1551 lemma dec_is_jump: ∀x.(is_jump x) + (¬is_jump x).
    1552 #x cases x #l #i cases i
    1553 [#id cases id
    1554  [1,2,3,6,7,33,34:
    1555   #x #y %2 whd in match (is_jump ?); /2 by nmk/
    1556  |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32:
    1557   #x %2 whd in match (is_jump ?); /2 by nmk/
    1558  |35,36,37: %2 whd in match (is_jump ?); /2 by nmk/
    1559  |9,10,14,15: #x %1 //
    1560  |11,12,13,16,17: #x #y %1 //
    1561  ]
    1562 |2,3: #x %2 /2 by nmk/
    1563 |4,5: #x %1 //
    1564 |6: #x #y %2 /2 by nmk/
    1565 ]
    1566 qed.
    1567  
    15681497lemma measure_zero: ∀l.∀program:Σl:list labelled_instruction.|l| < 2^16.
    15691498  |l| ≤ |program| → measure_int l (jump_expansion_internal program 0) 0 = 0.
  • src/utilities/extralib.ma

    r1523 r1593  
    1717include "basics/logic.ma".
    1818include "utilities/pair.ma".
     19include "ASM/Util.ma".
    1920
    2021lemma eq_rect_Type0_r:
     
    7576  ]
    7677] qed.
     78
     79(* some useful stuff for quantifiers *)
     80
     81lemma dec_bounded_forall:
     82  ∀P:ℕ → Prop.(∀n.(P n) + (¬P n)) → ∀k.(∀n.n < k → P n) + ¬(∀n.n < k → P n).
     83 #P #HP_dec #k elim k -k
     84 [ %1 #n #Hn @⊥ @(absurd (n < 0) Hn) @not_le_Sn_O
     85 | #k #Hind cases Hind
     86   [ #Hk cases (HP_dec k)
     87     [ #HPk %1 #n #Hn cases (le_to_or_lt_eq … Hn)
     88       [ #H @(Hk … (le_S_S_to_le … H))
     89       | #H >(injective_S … H) @HPk
     90       ]
     91     | #HPk %2 @nmk #Habs @(absurd (P k)) [ @(Habs … (le_n (S k))) | @HPk ]
     92     ]
     93   | #Hk %2 @nmk #Habs @(absurd (∀n.n<k→P n)) [ #n' #Hn' @(Habs … (le_S … Hn')) | @Hk ]
     94   ]
     95 ]
     96qed.
     97
     98lemma dec_bounded_exists:
     99  ∀P:ℕ→Prop.(∀n.(P n) + (¬P n)) → ∀k.(∃n.n < k ∧ P n) + ¬(∃n.n < k ∧ P n).
     100 #P #HP_dec #k elim k -k
     101 [ %2 @nmk #Habs elim Habs #n #Hn @(absurd (n < 0) (proj1 … Hn)) @not_le_Sn_O
     102 | #k #Hind cases Hind
     103   [ #Hk %1 elim Hk #n #Hn @(ex_intro … n) @conj [ @le_S @(proj1 … Hn) | @(proj2 … Hn) ]
     104   | #Hk cases (HP_dec k)
     105     [ #HPk %1 @(ex_intro … k) @conj [ @le_n | @HPk ]
     106     | #HPk %2 @nmk #Habs elim Habs #n #Hn cases (le_to_or_lt_eq … (proj1 … Hn))
     107       [ #H @(absurd (∃n.n < k ∧ P n)) [ @(ex_intro … n) @conj
     108         [ @(le_S_S_to_le … H) | @(proj2 … Hn) ] | @Hk ]
     109       | #H @(absurd (P k)) [ <(injective_S … H) @(proj2 … Hn) | @HPk ]
     110       ] 
     111     ]
     112   ]
     113 ]
     114qed.
     115
     116lemma not_exists_forall:
     117  ∀k:ℕ.∀P:ℕ → Prop.¬(∃x.x < k ∧ P x) → ∀x.x < k → ¬P x.
     118 #k #P #Hex #x #Hx @nmk #Habs @(absurd ? ? Hex) @(ex_intro … x)
     119 @conj [ @Hx | @Habs ]
     120qed.
     121
     122lemma not_forall_exists:
     123  ∀k:ℕ.∀P:ℕ → Prop.(∀n.(P n) + (¬P n)) → ¬(∀x.x < k → P x) → ∃x.x < k ∧ ¬P x.
     124 #k #P #Hdec elim k
     125 [ #Hfa @⊥ @(absurd ?? Hfa) #z #Hz @⊥ @(absurd ? Hz) @not_le_Sn_O
     126 | -k #k #Hind #Hfa cases (Hdec k)
     127   [ #HP elim (Hind ?)
     128     [ -Hind; #x #Hx @(ex_intro ?? x) @conj [ @le_S @(proj1 ?? Hx) | @(proj2 ?? Hx) ]
     129     | @nmk #H @(absurd ?? Hfa) #x #Hx cases (le_to_or_lt_eq ?? Hx)
     130       [ #H2 @H @(le_S_S_to_le … H2)
     131       | #H2 >(injective_S … H2) @HP
     132       ]
     133     ]
     134   | #HP @(ex_intro … k) @conj [ @le_n | @HP ]
     135   ]
     136 ]
     137qed.
  • src/utilities/extranat.ma

    r1516 r1593  
    6363] qed.
    6464
     65lemma le_S_to_le: ∀n,m:ℕ.S n ≤ m → n ≤ m.
     66 /2/ qed.
     67
     68lemma le_plus_k:
     69  ∀n,m:ℕ.n ≤ m → ∃k:ℕ.m = n + k.
     70 #n #m elim m -m;
     71 [ #Hn % [ @O | <(le_n_O_to_eq n Hn) // ]
     72 | #m #Hind #Hn cases (le_to_or_lt_eq … Hn) -Hn; #Hn
     73   [ elim (Hind (le_S_S_to_le … Hn)) #k #Hk % [ @(S k) | >Hk // ]
     74   | % [ @O | <Hn // ]
     75   ]
     76 ]
     77qed.
     78
     79lemma eq_plus_S_to_lt:
     80  ∀n,m,p:ℕ.n = m + (S p) → m < n.
     81 #n #m #p /2 by lt_plus_to_lt_l/
     82qed.
    6583
    6684(* "Fast" proofs:  some proofs get reduced during normalization (in particular,
Note: See TracChangeset for help on using the changeset viewer.