From 0236781c3ff798b60c5c8171a0f9b6cd569f7995 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Thu, 24 May 2018 15:06:18 +0200 Subject: Machblock: Mach language with basic blocks --- driver/ForwardSimulationBlock.v | 236 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 236 insertions(+) create mode 100644 driver/ForwardSimulationBlock.v (limited to 'driver/ForwardSimulationBlock.v') diff --git a/driver/ForwardSimulationBlock.v b/driver/ForwardSimulationBlock.v new file mode 100644 index 00000000..43cf58c3 --- /dev/null +++ b/driver/ForwardSimulationBlock.v @@ -0,0 +1,236 @@ +(*** + +Variante de Forward Simulation pour les blocks. + +***) + +Require Import Relations. +Require Import Wellfounded. +Require Import Coqlib. +Require Import Events. +Require Import Globalenvs. +Require Import Smallstep. + + +Local Open Scope nat_scope. + + +Section ForwardSimuBlock. + +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'', + Step L1 s' t2 s'' -> t = t1 ** t2 -> starN (step L1) (globalenv L1) (S n) s t s''. +Proof. + induction 1; simpl. + + intros t t1 s0; autorewrite with trace_rewrite. + intros; subst; eapply starN_step; eauto. + autorewrite with trace_rewrite; auto. + + intros. eapply starN_step; eauto. + intros; subst; autorewrite with trace_rewrite; auto. +Qed. + +(** Hypothèses de la preuve *) + +Variable dist_end_block: state L1 -> nat. + +Hypothesis simu_mid_block: + forall s1 t s1', Step L1 s1 t s1' -> (dist_end_block s1)<>0 -> t = E0 /\ dist_end_block s1=S (dist_end_block s1'). + +Hypothesis public_preserved: + forall id, Senv.public_symbol (symbolenv L2) id = Senv.public_symbol (symbolenv L1) id. + +Variable build_block: state L1 -> state L2. + +Hypothesis match_initial_states: + forall s1, initial_state L1 s1 -> initial_state L2 (build_block s1). + +Hypothesis match_final_states: + forall s1 r, final_state L1 s1 r -> final_state L2 (build_block s1) 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'). + + +(** Introduction d'une sémantique par bloc sur L1 appelée "memoL1" *) + +Definition star_in_block (head current: state L1): Prop := + dist_end_block head >= dist_end_block current + /\ starN (step L1) (globalenv L1) (minus (dist_end_block head) (dist_end_block current)) head E0 current. + +Lemma star_in_block_step (head previous next: state L1): + forall t, star_in_block head previous -> Step L1 previous t next -> (dist_end_block previous)<>0 -> star_in_block head next. +Proof. + intros t [H1 H2] H3 H4. + destruct (simu_mid_block _ _ _ H3 H4) as [H5 H6]; subst. + constructor 1. + + omega. + + cutrewrite (dist_end_block head - dist_end_block next = S (dist_end_block head - dist_end_block previous)). + - eapply starN_last_step; eauto. + - omega. +Qed. + +Lemma star_in_block_init (head current: state L1): + forall t, Step L1 head t current -> (dist_end_block head)<>0 -> star_in_block head current. +Proof. + intros t H3 H4. + destruct (simu_mid_block _ _ _ H3 H4) as [H5 H6]; subst. + constructor 1. + + omega. + + cutrewrite (dist_end_block head - dist_end_block current = 1). + - eapply starN_last_step; eauto. + - omega. +Qed. + + +Record memostate := { + real: state L1; + memorized: option (state L1); + memo_star: forall head, memorized = Some head -> star_in_block head real; + memo_final: forall r, final_state L1 real r -> memorized = None +}. + +Definition head (s: memostate): state L1 := + match memorized s with + | None => real s + | Some s' => s' + end. + +Lemma head_star (s: memostate): star_in_block (head s) (real s). +Proof. + destruct s as [rs ms Hs]. simpl. + destruct ms as [ms|]; unfold head; simpl; auto. + constructor 1. + omega. + cutrewrite ((dist_end_block rs - dist_end_block rs)%nat=O). + + apply starN_refl; auto. + + omega. +Qed. + +Inductive is_well_memorized (s s': memostate): Prop := + | StartBloc: + dist_end_block (real s) <> O -> + memorized s = None -> + memorized s' = Some (real s) -> + is_well_memorized s s' + | MidBloc: + dist_end_block (real s) <> O -> + memorized s <> None -> + memorized s' = memorized s -> + is_well_memorized s s' + | ExitBloc: + dist_end_block (real s) = O -> + memorized s' = None -> + is_well_memorized s s'. + +Local Hint Resolve StartBloc MidBloc ExitBloc. + +Definition memoL1 := {| + state := memostate; + genvtype := genvtype L1; + step := fun ge s t s' => + step L1 ge (real s) t (real s') + /\ is_well_memorized s s' ; + initial_state := fun s => initial_state L1 (real s) /\ memorized s = None; + final_state := fun s r => final_state L1 (real s) r; + globalenv:= globalenv L1; + symbolenv:= symbolenv L1 +|}. + + +(** Preuve des 2 forward simulations: L1 -> memoL1 et memoL1 -> L2 *) + +Lemma discr_dist_end s: + {dist_end_block s = O} + {dist_end_block s <> O}. +Proof. + destruct (dist_end_block s); simpl; intuition. +Qed. + +Lemma memo_simulation_step: + forall s1 t s1', Step L1 s1 t s1' -> + forall s2, s1 = (real s2) -> exists s2', Step memoL1 s2 t s2' /\ s1' = (real s2'). +Proof. + intros s1 t s1' H1 [rs2 ms2 Hmoi] H2. simpl in H2; subst. + destruct (discr_dist_end rs2) as [H3 | H3]. + + refine (ex_intro _ {|real:=s1'; memorized:=None |} _); simpl. + intuition. + + destruct ms2 as [s|]. + - refine (ex_intro _ {|real:=s1'; memorized:=Some s |} _); simpl. + intuition. + - refine (ex_intro _ {|real:=s1'; memorized:=Some rs2 |} _); simpl. + intuition. + Unshelve. + * intros; discriminate. + * intros; auto. + * intros head X; injection X; clear X; intros; subst. + eapply star_in_block_step; eauto. + * intros r X; erewrite final_states_end_block in H3; intuition eauto. + * intros head X; injection X; clear X; intros; subst. + eapply star_in_block_init; eauto. + * intros r X; erewrite final_states_end_block in H3; intuition eauto. +Qed. + +Lemma forward_memo_simulation_1: forward_simulation L1 memoL1. +Proof. + apply forward_simulation_step with (match_states:=fun s1 s2 => s1 = (real s2)); auto. + + intros s1 H; eapply ex_intro with (x:={|real:=s1; memorized:=None |}); simpl. + intuition. + + intros; subst; auto. + + intros; exploit memo_simulation_step; eauto. + Unshelve. + * intros; discriminate. + * auto. +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. + - (* 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. + - (* 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. + - (* 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. +Qed. + +Lemma forward_simulation_block: forward_simulation L1 L2. +Proof. + eapply compose_forward_simulations. + eapply forward_memo_simulation_1. + apply forward_memo_simulation_2. +Qed. + + +End ForwardSimuBlock. \ No newline at end of file -- cgit From cb6627f0d3668a6d641f491a3e58f3eb36f741e6 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Tue, 26 Jun 2018 10:59:29 +0200 Subject: Generalization of ForwardSimulationBlock --- driver/ForwardSimulationBlock.v | 57 +++++++++++++++++------------------------ 1 file changed, 24 insertions(+), 33 deletions(-) (limited to 'driver/ForwardSimulationBlock.v') 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. -- cgit From 2e93b668df554edbfec0c23de7b14caf95a48b1d Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Thu, 28 Jun 2018 10:38:26 +0200 Subject: Machblock: adaptation to the generalized ForwardSimulationBlock --- driver/ForwardSimulationBlock.v | 111 +++++++++++++++++++++++++++++++++++++--- 1 file changed, 103 insertions(+), 8 deletions(-) (limited to 'driver/ForwardSimulationBlock.v') diff --git a/driver/ForwardSimulationBlock.v b/driver/ForwardSimulationBlock.v index 8c1fcb08..a9569e08 100644 --- a/driver/ForwardSimulationBlock.v +++ b/driver/ForwardSimulationBlock.v @@ -1,6 +1,7 @@ (*** -Variante de Forward Simulation pour les blocks. +Auxiliary lemmas on starN and forward_simulation +in order to prove the forward simulation of Mach -> Machblock. ***) @@ -15,16 +16,36 @@ Require Import Smallstep. Local Open Scope nat_scope. -Section ForwardSimuBlock. +(** Auxiliary lemma on starN *) +Section starN_lemma. -Variable L1 L2: semantics. +Variable L: semantics. -Local Hint Resolve starN_refl starN_step. +Local Hint Resolve starN_refl starN_step Eapp_assoc. + +Lemma starN_split n s t s': + starN (step L) (globalenv L) n s t s' -> + forall m k, n=m+k -> + exists (t1 t2:trace) s0, starN (step L) (globalenv L) m s t1 s0 /\ starN (step L) (globalenv L) k s0 t2 s' /\ t=t1**t2. +Proof. + induction 1; simpl. + + intros m k H; assert (X: m=0); try omega. + assert (X0: k=0); try omega. + subst; repeat (eapply ex_intro); intuition eauto. + + intros m; destruct m as [| m']; simpl. + - intros k H2; subst; repeat (eapply ex_intro); intuition eauto. + - intros k H2. inversion H2. + exploit (IHstarN m' k); eauto. intro. + destruct H3 as (t5 & t6 & s0 & H5 & H6 & H7). + repeat (eapply ex_intro). + instantiate (1 := t6); instantiate (1 := t1 ** t5); instantiate (1 := s0). + intuition eauto. subst. auto. +Qed. Lemma starN_last_step n s t1 s': - starN (step L1) (globalenv L1) n s t1 s' -> + starN (step L) (globalenv L) n s t1 s' -> forall (t t2:trace) s'', - Step L1 s' t2 s'' -> t = t1 ** t2 -> starN (step L1) (globalenv L1) (S n) s t s''. + Step L s' t2 s'' -> t = t1 ** t2 -> starN (step L) (globalenv L) (S n) s t s''. Proof. induction 1; simpl. + intros t t1 s0; autorewrite with trace_rewrite. @@ -34,6 +55,17 @@ Proof. intros; subst; autorewrite with trace_rewrite; auto. Qed. +End starN_lemma. + + + +(** General scheme from a "match_states" relation *) + +Section ForwardSimuBlock_REL. + +Variable L1 L2: semantics. + + (** Hypothèses de la preuve *) Variable dist_end_block: state L1 -> nat. @@ -61,6 +93,8 @@ Hypothesis simu_end_block: (** Introduction d'une sémantique par bloc sur L1 appelée "memoL1" *) +Local Hint Resolve starN_refl starN_step. + Definition star_in_block (head current: state L1): Prop := dist_end_block head >= dist_end_block current /\ starN (step L1) (globalenv L1) (minus (dist_end_block head) (dist_end_block current)) head E0 current. @@ -216,7 +250,7 @@ Proof. * unfold head; rewrite H2; simpl. intuition eauto. Qed. -Lemma forward_simulation_block: forward_simulation L1 L2. +Lemma forward_simulation_block_rel: forward_simulation L1 L2. Proof. eapply compose_forward_simulations. eapply forward_memo_simulation_1. @@ -224,4 +258,65 @@ Proof. Qed. -End ForwardSimuBlock. \ No newline at end of file +End ForwardSimuBlock_REL. + + + +(* An instance of the previous scheme, when there is a translation from L1 states to L2 states + +Here, we do not require that the sequence of S2 states does exactly match the sequence of L1 states by trans_state. +This is because the exact matching is broken in Machblock on "goto" instruction (due to the find_label). + +However, the Machblock state after a goto remains "equivalent" to the trans_state of the Mach state in the sense of "equiv_on_next_step" below... + +*) + +Section ForwardSimuBlock_TRANS. + +Variable L1 L2: semantics. + +Variable trans_state: state L1 -> state L2. + +Definition equiv_on_next_step (P Q: Prop) s2_a s2_b: Prop := + (P -> (forall t s', Step L2 s2_a t s' <-> Step L2 s2_b t s')) /\ (Q -> (forall r, (final_state L2 s2_a r) <-> (final_state L2 s2_b r))). + +Definition match_states s1 s2: Prop := + equiv_on_next_step (exists t s1', Step L1 s1 t s1') (exists r, final_state L1 s1 r) s2 (trans_state s1). + +Lemma match_states_trans_state s1: match_states s1 (trans_state s1). +Proof. + unfold match_states, equiv_on_next_step. intuition. +Qed. + +Variable dist_end_block: state L1 -> nat. + +Hypothesis simu_mid_block: + forall s1 t s1', Step L1 s1 t s1' -> (dist_end_block s1)<>0 -> t = E0 /\ dist_end_block s1=S (dist_end_block s1'). + +Hypothesis public_preserved: + forall id, Senv.public_symbol (symbolenv L2) id = Senv.public_symbol (symbolenv L1) id. + +Hypothesis match_initial_states: + 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 (trans_state s1) 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' -> exists s2', Step L2 (trans_state s1) t s2' /\ match_states s1' s2'. + +Lemma forward_simulation_block_trans: forward_simulation L1 L2. +Proof. + eapply forward_simulation_block_rel with (dist_end_block:=dist_end_block) (match_states:=match_states); try tauto. + + (* final_states *) intros s1 s2 r H1 [H2 H3]. rewrite H3; eauto. + + (* simu_end_block *) + intros s1 t s1' s2 H1 [H2a H2b]. exploit simu_end_block; eauto. + intros (s2' & H3 & H4); econstructor 1; intuition eauto. + rewrite H2a; auto. + inversion_clear H1. eauto. +Qed. + +End ForwardSimuBlock_TRANS. \ No newline at end of file -- cgit From edb93401b3621e8e9731c0a50afdbcc441d7f495 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Thu, 12 Jul 2018 14:58:06 +0200 Subject: Machblock: some renaming and proof simplifications --- driver/ForwardSimulationBlock.v | 30 +++++++++++++++--------------- 1 file changed, 15 insertions(+), 15 deletions(-) (limited to 'driver/ForwardSimulationBlock.v') diff --git a/driver/ForwardSimulationBlock.v b/driver/ForwardSimulationBlock.v index a9569e08..dc8beb29 100644 --- a/driver/ForwardSimulationBlock.v +++ b/driver/ForwardSimulationBlock.v @@ -42,7 +42,7 @@ Proof. intuition eauto. subst. auto. Qed. -Lemma starN_last_step n s t1 s': +Lemma starN_tailstep n s t1 s': starN (step L) (globalenv L) n s t1 s' -> forall (t t2:trace) s'', Step L s' t2 s'' -> t = t1 ** t2 -> starN (step L) (globalenv L) (S n) s t s''. @@ -95,31 +95,31 @@ Hypothesis simu_end_block: Local Hint Resolve starN_refl starN_step. -Definition star_in_block (head current: state L1): Prop := +Definition follows_in_block (head current: state L1): Prop := dist_end_block head >= dist_end_block current /\ starN (step L1) (globalenv L1) (minus (dist_end_block head) (dist_end_block current)) head E0 current. -Lemma star_in_block_step (head previous next: state L1): - forall t, star_in_block head previous -> Step L1 previous t next -> (dist_end_block previous)<>0 -> star_in_block head next. +Lemma follows_in_block_step (head previous next: state L1): + forall t, follows_in_block head previous -> Step L1 previous t next -> (dist_end_block previous)<>0 -> follows_in_block head next. Proof. intros t [H1 H2] H3 H4. destruct (simu_mid_block _ _ _ H3 H4) as [H5 H6]; subst. constructor 1. + omega. + cutrewrite (dist_end_block head - dist_end_block next = S (dist_end_block head - dist_end_block previous)). - - eapply starN_last_step; eauto. + - eapply starN_tailstep; eauto. - omega. Qed. -Lemma star_in_block_init (head current: state L1): - forall t, Step L1 head t current -> (dist_end_block head)<>0 -> star_in_block head current. +Lemma follows_in_block_init (head current: state L1): + forall t, Step L1 head t current -> (dist_end_block head)<>0 -> follows_in_block head current. Proof. intros t H3 H4. destruct (simu_mid_block _ _ _ H3 H4) as [H5 H6]; subst. constructor 1. + omega. + cutrewrite (dist_end_block head - dist_end_block current = 1). - - eapply starN_last_step; eauto. + - eapply starN_tailstep; eauto. - omega. Qed. @@ -127,7 +127,7 @@ Qed. Record memostate := { real: state L1; memorized: option (state L1); - memo_star: forall head, memorized = Some head -> star_in_block head real; + memo_star: forall head, memorized = Some head -> follows_in_block head real; memo_final: forall r, final_state L1 real r -> memorized = None }. @@ -137,7 +137,7 @@ Definition head (s: memostate): state L1 := | Some s' => s' end. -Lemma head_star (s: memostate): star_in_block (head s) (real s). +Lemma head_followed (s: memostate): follows_in_block (head s) (real s). Proof. destruct s as [rs ms Hs]. simpl. destruct ms as [ms|]; unfold head; simpl; auto. @@ -204,10 +204,10 @@ Proof. * intros; discriminate. * intros; auto. * intros head X; injection X; clear X; intros; subst. - eapply star_in_block_step; eauto. + eapply follows_in_block_step; eauto. * intros r X; erewrite final_states_end_block in H3; intuition eauto. * intros head X; injection X; clear X; intros; subst. - eapply star_in_block_init; eauto. + eapply follows_in_block_init; eauto. * intros r X; erewrite final_states_end_block in H3; intuition eauto. Qed. @@ -244,9 +244,9 @@ Proof. - (* EndBloc *) constructor 1. destruct (simu_end_block (head s1) t (real s1') s2) as (s2' & H3 & H4); auto. - * destruct (head_star s1) as [H4 H3]. + * destruct (head_followed 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. + eapply starN_tailstep; eauto. * unfold head; rewrite H2; simpl. intuition eauto. Qed. @@ -319,4 +319,4 @@ Proof. inversion_clear H1. eauto. Qed. -End ForwardSimuBlock_TRANS. \ No newline at end of file +End ForwardSimuBlock_TRANS. -- cgit