Changeset 925


Ignore:
Timestamp:
Jun 9, 2011, 4:42:50 PM (8 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r924 r925  
    16171617  [ cases (code_memory … ps) #preamble #instr_list whd in ⊢ (???% → ?) #EQ >EQ #H
    16181618    #abs @⊥ normalize in abs; destruct (abs) ]
    1619  * #labels #costs cases (code_memory … ps) #preamble #instr_list normalize nodelta;
     1619 * #labels #costs generalize in match (refl … (code_memory … ps))
     1620 cases (code_memory … ps) in ⊢ (???% → %) #preamble #instr_list #EQ normalize nodelta;
    16201621 generalize in ⊢ (???(match % with [_ ⇒ ? | _ ⇒ ?]) → ?) *; normalize nodelta;
    16211622  [ #EQ >EQ #_ #abs @⊥ normalize in abs; destruct (abs) ]
     
    16311632 whd in match (\snd 〈final_pc,assembled〉) in H;
    16321633 -s s'' labels costs final_ppc final_pc;
     1634 letin ps' ≝ (execute_1_pseudo_instruction ticks_of ps)
    16331635 (* NICE STATEMENT HERE *)
     1636 generalize in match (refl … ps') generalize in ⊢ (??%? → ?) normalize nodelta; -ps'; #ps'
     1637 whd in ⊢ (???% → ?) generalize in match (H (program_counter … ps)) >EQ normalize nodelta;
     1638 cases (fetch_pseudo_instruction instr_list (program_counter … ps))
     1639 #pi #newppc normalize nodelta; * #instructions *
     1640 cases pi normalize nodelta;
     1641  [ (* Instruction *)
     1642  | (* Comment *) #comment #H1 #H2 #EQ normalize in H1 generalize in match (option_destruct_Some ??? H1) #K1
     1643    >K1 in H2 whd in ⊢ (% → ?) #H2 whd in ⊢ (??%?)
     1644  | (* Cost *)
     1645  | (* Jmp *)
     1646  | (* Call *)
     1647  | (* Mov *)
     1648  ]
     1649qed.
Note: See TracChangeset for help on using the changeset viewer.