Generalization of ForwardSimulationBlock

1 files changed, 24 insertions, 33 deletions

diff --git a/driver/ForwardSimulationBlock.v b/driver/ForwardSimulationBlock.v
index 43cf58c3..8c1fcb08 100644
--- a/driver/ForwardSimulationBlock.v
+++ b/driver/ForwardSimulationBlock.v
@@ -21,13 +21,6 @@ Variable L1 L2: semantics.
 
 Local Hint Resolve starN_refl starN_step.
 
-
-(* TODO: faut-il se baser sur [starN] ou un type inductif équivalent 
-  (qui ferait les step dans l'ordre ci-dessous) ?
-
-  => Voir ce qui est le plus facile pour prouver l'hypothèse [simu_end_block] ci-dessous...
-*)
-
 Lemma starN_last_step n s t1 s': 
   starN (step L1) (globalenv L1) n s t1 s' ->
   forall (t t2:trace) s'',
@@ -51,19 +44,19 @@ Hypothesis simu_mid_block:
 Hypothesis public_preserved:
   forall id, Senv.public_symbol (symbolenv L2) id = Senv.public_symbol (symbolenv L1) id.
 
-Variable build_block: state L1 -> state L2.
+Variable match_states: state L1 -> state L2 -> Prop.
 
 Hypothesis match_initial_states:
-  forall s1, initial_state L1 s1 -> initial_state L2 (build_block s1).
+  forall s1, initial_state L1 s1 -> exists s2, match_states s1 s2 /\ initial_state L2 s2.
 
 Hypothesis match_final_states:
-  forall s1 r, final_state L1 s1 r -> final_state L2 (build_block s1) r.
+  forall s1 s2 r, final_state L1 s1 r -> match_states s1 s2 -> final_state L2 s2 r.
 
 Hypothesis final_states_end_block:
   forall s1 t s1' r, Step L1 s1 t s1' -> final_state L1 s1' r -> dist_end_block s1 = 0.
 
 Hypothesis simu_end_block:
-  forall s1 t s1', starN (step L1) (globalenv L1) (S (dist_end_block s1)) s1 t s1' -> Step L2 (build_block s1) t (build_block s1').
+  forall s1 t s1' s2, starN (step L1) (globalenv L1) (S (dist_end_block s1)) s1 t s1' -> match_states s1 s2 -> exists s2', Step L2 s2 t s2' /\ match_states s1' s2'.
 
 
 (** Introduction d'une sémantique par bloc sur L1 appelée "memoL1" *)
@@ -198,31 +191,29 @@ Qed.
 
 Lemma forward_memo_simulation_2: forward_simulation memoL1 L2.
 Proof.
-  apply forward_simulation_opt with (measure:=fun s => dist_end_block (real s)) (match_states:=fun s1 s2 => s2 = (build_block (head s1))); auto.
-  + unfold memoL1; simpl. intros s1 [H0 H1]; eapply ex_intro with (x:=(build_block (real s1))).
-    unfold head. rewrite H1. intuition.
-  + intros s1 s2 r X H0. subst. unfold head. 
-    erewrite memo_final; eauto.
-    eapply H0.
-  + unfold memoL1; simpl. 
-    intros s1 t s1' [H1 H2] s H; subst.
-    destruct H2.
+  unfold memoL1; simpl.
+  apply forward_simulation_opt with (measure:=fun s => dist_end_block (real s)) (match_states:=fun s1 s2 => match_states (head s1) s2); simpl; auto.
+  + intros s1 [H0 H1]; destruct (match_initial_states (real s1) H0).
+    unfold head; rewrite H1.
+    intuition eauto.
+  + intros s1 s2 r X H0;  unfold head in X. 
+    erewrite memo_final in X; eauto.
+  + intros s1 t s1' [H1 H2] s2 H; subst.
+    destruct H2 as [ H0 H2 H3 | H0 H2 H3 | H0 H2].
     - (* StartBloc *)
-      constructor 2. destruct (simu_mid_block (real s1) t (real s1')) as [H3 H4]; auto.
-      unfold head. rewrite H0. rewrite H2. rewrite H4. intuition.
+      constructor 2. destruct (simu_mid_block (real s1) t (real s1')) as [H5 H4]; auto.
+      unfold head in * |- *. rewrite H2 in H. rewrite H3. rewrite H4. intuition.
     - (* MidBloc *)
-      constructor 2. destruct (simu_mid_block (real s1) t (real s1')) as [H3 H4]; auto.
-      unfold head. rewrite H2. rewrite H4. intuition.
-      destruct (memorized s1); simpl; auto. destruct H0; auto.
+      constructor 2. destruct (simu_mid_block (real s1) t (real s1')) as [H5 H4]; auto.
+      unfold head in * |- *. rewrite H3. rewrite H4. intuition.
+      destruct (memorized s1); simpl; auto. tauto.
     - (* EndBloc *)
-      constructor 1. 
-      eapply ex_intro; intuition eauto.
-       apply simu_end_block.
-       destruct (head_star s1) as [H2 H3].
-       cutrewrite (dist_end_block (head s1) - dist_end_block (real s1) = dist_end_block (head s1)) in H3.
-       unfold head; rewrite H0; simpl.
-       eapply starN_last_step; eauto.
-       omega.
+      constructor 1.
+      destruct (simu_end_block (head s1) t (real s1') s2) as (s2' & H3 & H4); auto.
+      * destruct (head_star s1) as [H4 H3].
+        cutrewrite (dist_end_block (head s1) - dist_end_block (real s1) = dist_end_block (head s1)) in H3; try omega.
+        eapply starN_last_step; eauto.
+      * unfold head; rewrite H2; simpl. intuition eauto. 
 Qed.
 
 Lemma forward_simulation_block: forward_simulation L1 L2.