Ignore:
Timestamp:
Jul 17, 2012, 6:57:39 PM (8 years ago)
Author:
campbell
Message:

Start defining equivalent executions.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/labelSimulation.ma

    r2176 r2202  
    11891189
    11901190lemma not_wrong_init : ∀p.
    1191   not_wrong (exec_inf … clight_fullexec p) →
     1191  not_wrong state (exec_inf … clight_fullexec p) →
    11921192  ∃s. make_initial_state … p = OK ? s.
    1193 #p whd in ⊢ (?% → ?); change with (make_initial_state p) in match (make_initial_state ??? p);
     1193#p whd in ⊢ (??% → ?); change with (make_initial_state p) in match (make_initial_state ??? p);
    11941194cases (make_initial_state p)
    11951195[ /2/
     
    12251225  plus ge s tr s' →
    12261226  is_final s' = None ? →
    1227   steps tr (exec_inf_aux … clight_fullexec ge (exec_step ge s))
    1228            (exec_inf_aux … clight_fullexec ge (exec_step ge s')).
     1227  steps state tr
     1228    (exec_inf_aux … clight_fullexec ge (exec_step ge s))
     1229    (exec_inf_aux … clight_fullexec ge (exec_step ge s')).
    12291230#ge #s0 #tr0 #s0' #P elim P
    12301231[ #s1 #tr #s2 #EX #NF >EX >exec_inf_aux_unfold
    1231   whd in ⊢ (??%?);
     1232  whd in ⊢ (???%?);
    12321233  whd in match (is_final ?????); >NF
    12331234  %2
    12341235| #s1 #tr #s2 #tr' #s3 #EX1 #P2 #IH #NF
    12351236  >exec_inf_aux_unfold >EX1
    1236   whd in ⊢ (??%?);
     1237  whd in ⊢ (???%?);
    12371238  whd in match (is_final ?????); >(plus_not_final … P2)
    12381239  %3 @IH //
     
    12421243  plus ge s tr s' →
    12431244  is_final s' = Some ? r →
    1244   ∃tr'. steps tr (exec_inf_aux … clight_fullexec ge (exec_step ge s))
    1245                  (e_stop … tr' r s').
     1245  ∃tr'. steps state tr
     1246          (exec_inf_aux … clight_fullexec ge (exec_step ge s))
     1247          (e_stop … tr' r s').
    12461248#ge #s0 #tr0 #s0' #r #P elim P
    12471249[ #s1 #tr #s2 #EX #F >EX >exec_inf_aux_unfold
    1248   %{tr} whd in ⊢ (??%?);
     1250  %{tr} whd in ⊢ (???%?);
    12491251  whd in match (is_final ?????); >F
    12501252  %1
     
    12531255  #tr' #S' %{tr'}
    12541256  >exec_inf_aux_unfold >EX1
    1255   whd in ⊢ (??%?);
     1257  whd in ⊢ (???%?);
    12561258  whd in match (is_final ?????); >(plus_not_final … P2)
    12571259  %3 @S'
     
    12631265  (s1,s2:state)
    12641266  (S:state_with_labels s1 s2)
    1265   (NW:not_wrong (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1)))
     1267  (NW:not_wrong state (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1)))
    12661268: sim_with_labels (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1)) (exec_inf_aux … clight_fullexec ge2 (exec_step ge2 s2)) ≝
    12671269match NW return λe,NW. exec_inf_aux … clight_fullexec ?? = e → sim_with_labels e ? with
     
    12991301  #i cases (H2 i) #tr1 * #s1' * #K1 * #tr2 * #s2' * * #K2 #TR #S'
    13001302  lapply (NWk i)
    1301   @(match sym_eq … K1 with [refl ⇒ ?]) @(match sym_eq … (exec_inf_aux_unfold …) with [refl ⇒ ?]) whd in ⊢ (?% → ?%%); whd in match (is_final ?????); @(match sym_eq … (final_related … S') with [refl ⇒ ?])
     1303  @(match sym_eq … K1 with [refl ⇒ ?]) @(match sym_eq … (exec_inf_aux_unfold …) with [refl ⇒ ?]) whd in ⊢ (??% → ?%%); whd in match (is_final ?????); @(match sym_eq … (final_related … S') with [refl ⇒ ?])
    13021304  @(match sym_eq … K2 with [refl ⇒ ?]) @(match sym_eq … (exec_inf_aux_unfold ?? clight_fullexec ge2 …) with [refl ⇒ ?]) whd in ⊢ (? → ??%); whd in match (is_final ?????);
    13031305  cases (is_final s2')
    1304   [ whd in ⊢ (?% → ?%%); #NW' @(swl_steps … (steps_step …)) // @build_exec //
     1306  [ whd in ⊢ (??% → ?%%); #NW' @(swl_steps … (steps_step …)) // @build_exec //
    13051307    inversion NW'
    13061308    [ #H1 #H2 #H3 #H4 #H5 destruct
     
    13081310    | #H14 #H15 #H16 #H17 #H18 destruct
    13091311    ]
    1310   | #r whd in ⊢ (?% → ?%%); #NW' @(swl_stop … (steps_stop …)) //
     1312  | #r whd in ⊢ (??% → ?%%); #NW' @(swl_stop … (steps_stop …)) //
    13111313  ]
    13121314] qed.
     
    13431345>I2
    13441346
    1345 whd in ⊢ (?% → ? → ?%%);
     1347whd in ⊢ (??% → ? → ?%%);
    13461348>exec_inf_aux_unfold
    13471349>exec_inf_aux_unfold
    1348 whd in ⊢ (?% → ? → ?%%);
     1350whd in ⊢ (??% → ? → ?%%);
    13491351whd in match (is_final ?????);
    13501352>(initial_state_is_not_final … I1)
    13511353whd in match (is_final ?????);
    13521354>(initial_state_is_not_final … I2)
    1353 whd in ⊢ (?% → ? → ?%%);
     1355whd in ⊢ (??% → ? → ?%%);
    13541356
    13551357#NW #S
Note: See TracChangeset for help on using the changeset viewer.