Changeset 2202 for src/Clight/labelSimulation.ma

Timestamp:

Jul 17, 2012, 6:57:39 PM (8 years ago)

Author:

campbell

Message:

Start defining equivalent executions.

File:

• src/Clight/labelSimulation.ma (modified) (8 diffs)

src/Clight/labelSimulation.ma

@@ -1189 +1189 @@
 
 lemma not_wrong_init : ∀p.
-  not_wrong (exec_inf … clight_fullexec p) →
+  not_wrong state (exec_inf … clight_fullexec p) →
   ∃s. make_initial_state … p = OK ? s.
-#p whd in ⊢ (?% → ?); change with (make_initial_state p) in match (make_initial_state ??? p);
+#p whd in ⊢ (??% → ?); change with (make_initial_state p) in match (make_initial_state ??? p);
 cases (make_initial_state p)
 [ /2/
@@ -1225 +1225 @@
   plus ge s tr s' →
   is_final s' = None ? →
-  steps tr (exec_inf_aux … clight_fullexec ge (exec_step ge s))
-           (exec_inf_aux … clight_fullexec ge (exec_step ge s')).
+  steps state tr
+    (exec_inf_aux … clight_fullexec ge (exec_step ge s))
+    (exec_inf_aux … clight_fullexec ge (exec_step ge s')).
 #ge #s0 #tr0 #s0' #P elim P
 [ #s1 #tr #s2 #EX #NF >EX >exec_inf_aux_unfold
-  whd in ⊢ (??%?);
+  whd in ⊢ (???%?);
   whd in match (is_final ?????); >NF
   %2
 | #s1 #tr #s2 #tr' #s3 #EX1 #P2 #IH #NF
   >exec_inf_aux_unfold >EX1
-  whd in ⊢ (??%?);
+  whd in ⊢ (???%?);
   whd in match (is_final ?????); >(plus_not_final … P2)
   %3 @IH //
@@ -1242 +1243 @@
   plus ge s tr s' →
   is_final s' = Some ? r →
-  ∃tr'. steps tr (exec_inf_aux … clight_fullexec ge (exec_step ge s))
-                 (e_stop … tr' r s').
+  ∃tr'. steps state tr
+          (exec_inf_aux … clight_fullexec ge (exec_step ge s))
+          (e_stop … tr' r s').
 #ge #s0 #tr0 #s0' #r #P elim P
 [ #s1 #tr #s2 #EX #F >EX >exec_inf_aux_unfold
-  %{tr} whd in ⊢ (??%?);
+  %{tr} whd in ⊢ (???%?);
   whd in match (is_final ?????); >F
   %1
@@ -1253 +1255 @@
   #tr' #S' %{tr'}
   >exec_inf_aux_unfold >EX1
-  whd in ⊢ (??%?);
+  whd in ⊢ (???%?);
   whd in match (is_final ?????); >(plus_not_final … P2)
   %3 @S'
@@ -1263 +1265 @@
   (s1,s2:state)
   (S:state_with_labels s1 s2)
-  (NW:not_wrong (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1)))
+  (NW:not_wrong state (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1)))
 : sim_with_labels (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1)) (exec_inf_aux … clight_fullexec ge2 (exec_step ge2 s2)) ≝ 
 match NW return λe,NW. exec_inf_aux … clight_fullexec ?? = e → sim_with_labels e ? with
@@ -1299 +1301 @@
   #i cases (H2 i) #tr1 * #s1' * #K1 * #tr2 * #s2' * * #K2 #TR #S'
   lapply (NWk i)
-  @(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 ⇒ ?])
+  @(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 ⇒ ?])
   @(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 ?????);
   cases (is_final s2')
-  [ whd in ⊢ (?% → ?%%); #NW' @(swl_steps … (steps_step …)) // @build_exec //
+  [ whd in ⊢ (??% → ?%%); #NW' @(swl_steps … (steps_step …)) // @build_exec //
     inversion NW'
     [ #H1 #H2 #H3 #H4 #H5 destruct
@@ -1308 +1310 @@
     | #H14 #H15 #H16 #H17 #H18 destruct
     ]
-  | #r whd in ⊢ (?% → ?%%); #NW' @(swl_stop … (steps_stop …)) //
+  | #r whd in ⊢ (??% → ?%%); #NW' @(swl_stop … (steps_stop …)) //
   ]
 ] qed.
@@ -1343 +1345 @@
 >I2
 
-whd in ⊢ (?% → ? → ?%%);
+whd in ⊢ (??% → ? → ?%%);
 >exec_inf_aux_unfold
 >exec_inf_aux_unfold
-whd in ⊢ (?% → ? → ?%%);
+whd in ⊢ (??% → ? → ?%%);
 whd in match (is_final ?????);
 >(initial_state_is_not_final … I1)
 whd in match (is_final ?????);
 >(initial_state_is_not_final … I2)
-whd in ⊢ (?% → ? → ?%%);
+whd in ⊢ (??% → ? → ?%%);
 
 #NW #S