diff options
Diffstat (limited to 'driver/ForwardSimulationBlock.v')
-rw-r--r-- | driver/ForwardSimulationBlock.v | 57 |
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. |