Ignore:
Timestamp:
May 22, 2012, 11:15:12 AM (7 years ago)
Author:
mulligan
Message:

Changes to simplify the simpler cases of the main_lemma.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r1975 r1983  
    14351435  [ nil ⇒ eq_bv … pc final_pc = true
    14361436  | cons i tl ⇒
    1437     let fetched ≝ fetch code_memory pc in
    1438     let 〈instr_pc, ticks〉 ≝ fetched in
    1439     let 〈instr,pc'〉 ≝ instr_pc in
    1440       eq_instruction instr i = true ∧
    1441         ticks = (ticks_of_instruction i) ∧
    1442         fetch_many code_memory final_pc pc' tl
     1437      (∃pc': Word. 〈i, pc', ticks_of_instruction i〉 = fetch code_memory pc ∧
     1438        fetch_many code_memory final_pc pc' tl)
    14431439  ].
    14441440
     
    15061502    #i #tl #IH #pc #H whd
    15071503    cases (encoding_check_append ????? H) -H #H1 #H2
    1508     @pair_elim #instr_pc #ticks #fetch_refl normalize nodelta
    1509     @pair_elim #instr #pc' #instr_pc_refl normalize nodelta
    1510     lapply (fetch_assembly pc i code_memory (assembly1 i) (refl …)) whd in ⊢ (% → ?);
    1511     #H3 lapply (H3 H1) -H3 >fetch_refl >instr_pc_refl normalize nodelta
    1512     #H3 lapply (conjunction_true ?? H3) * #H4 #H5 %
    1513     [1:
    1514       lapply (conjunction_true … H4) * #B1 #B2
    1515       % try assumption @eqb_true_to_eq
    1516       <(eq_instruction_to_eq … B1) assumption
    1517     |2:
    1518       >(eq_bv_eq … H5) @IH @H2
    1519     ]
     1504    lapply (fetch_assembly pc i code_memory (assembly1 i) (refl …)) whd in ⊢ (% → ?);   
     1505    cases (fetch ??) * #instr #pc' #ticks
     1506    #H3 lapply (H3 H1) -H3 normalize nodelta #H3
     1507    lapply (conjunction_true ?? H3) * #H4 #H5
     1508    lapply (conjunction_true … H4) * #B1 #B2
     1509    %{pc'} <(eq_instruction_to_eq … B1) >(eq_bv_eq … H5)
     1510    >(eqb_true_to_refl … B2) % try % @IH @H2
    15201511  ]
    15211512qed.
Note: See TracChangeset for help on using the changeset viewer.