Ignore:
Timestamp:
Jun 9, 2011, 3:51:07 PM (9 years ago)
Author:
sacerdot
Message:

Main theorem made nice... but unprovable at the moment.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r921 r923  
    15921592  status_of_pseudo_status (execute_1_pseudo_instruction ticks_of ps) = Some … s'' →
    15931593   execute_1 s = s''.
    1594  #ticks_of #ps #s #s'' whd in ⊢ (??%? → ??%? → ?)
     1594 #ticks_of #ps #s #s''
     1595 generalize in match (fetch_assembly_pseudo2 (code_memory … ps))
     1596 whd in ⊢ (? → ??%? → ??%? → ?)
    15951597 >execute_1_pseudo_instruction_preserves_code_memory
    1596  cases (assembly (code_memory … ps)) [#abs @⊥ normalize in abs; destruct (abs)]
    1597  * #assembled #costs whd in ⊢ (??%? → ??%? → ?)
     1598 generalize in match (refl … (assembly (code_memory … ps)))
     1599 generalize in match (assembly (code_memory … ps)) in ⊢ (??%? → %) #ASS whd in ⊢ (???% → ?)
     1600 cases (build_maps (code_memory … ps))
     1601  [ cases (code_memory … ps) #preamble #instr_list whd in ⊢ (???% → ?) #EQ >EQ #H
     1602    #abs @⊥ normalize in abs; destruct (abs) ]
     1603 * #labels #costs cases (code_memory … ps) #preamble #instr_list normalize nodelta;
     1604 generalize in ⊢ (???(match % with [_ ⇒ ? | _ ⇒ ?]) → ?) *; normalize nodelta;
     1605  [ #EQ >EQ #_ #abs @⊥ normalize in abs; destruct (abs) ]
     1606 * #final_ppc * #final_pc #assembled #EQ >EQ -EQ ASS; normalize nodelta;
     1607 #H generalize in match (H ??? (refl …) (refl …)) -H; #H;
    15981608 #H1 generalize in match (option_destruct_Some ??? H1) -H1; #H1 <H1 -H1;
    15991609 #H2 generalize in match (option_destruct_Some ??? H2) -H2; #H2 <H2 -H2;
     
    16011611  (execute_1 (set_program_counter ? (set_code_memory ?? ps (load_code_memory assembled)) ?)
    16021612   = set_program_counter ? (set_code_memory ?? (execute_1_pseudo_instruction ticks_of ps) (load_code_memory assembled)) ?)
     1613 whd in match (\snd 〈preamble,instr_list〉) in H;
     1614 whd in match (\fst 〈preamble,instr_list〉) in H;
     1615 whd in match (\snd 〈final_pc,assembled〉) in H;
     1616 -s s'' labels costs final_ppc final_pc;
Note: See TracChangeset for help on using the changeset viewer.