diff options
Diffstat (limited to 'kvx/lib/ForwardSimulationBlock.v')
| -rw-r--r-- | kvx/lib/ForwardSimulationBlock.v | 30 |
1 files changed, 15 insertions, 15 deletions
diff --git a/kvx/lib/ForwardSimulationBlock.v b/kvx/lib/ForwardSimulationBlock.v index f79814f2..61466dad 100644 --- a/kvx/lib/ForwardSimulationBlock.v +++ b/kvx/lib/ForwardSimulationBlock.v @@ -42,11 +42,11 @@ Lemma starN_split 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. + induction 1; cbn. + 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 m; destruct m as [| m']; cbn. - intros k H2; subst; repeat (eapply ex_intro); intuition eauto. - intros k H2. inversion H2. exploit (IHstarN m' k); eauto. intro. @@ -61,7 +61,7 @@ Lemma starN_tailstep 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''. Proof. - induction 1; simpl. + induction 1; cbn. + intros t t1 s0; autorewrite with trace_rewrite. intros; subst; eapply starN_step; eauto. autorewrite with trace_rewrite; auto. @@ -153,8 +153,8 @@ Definition head (s: memostate): state L1 := 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. + destruct s as [rs ms Hs]. cbn. + destruct ms as [ms|]; unfold head; cbn; auto. constructor 1. omega. cutrewrite ((dist_end_block rs - dist_end_block rs)%nat=O). @@ -198,21 +198,21 @@ Definition memoL1 := {| Lemma discr_dist_end s: {dist_end_block s = O} + {dist_end_block s <> O}. Proof. - destruct (dist_end_block s); simpl; intuition. + destruct (dist_end_block s); cbn; 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. + intros s1 t s1' H1 [rs2 ms2 Hmoi] H2. cbn in H2; subst. destruct (discr_dist_end rs2) as [H3 | H3]. - + refine (ex_intro _ {|real:=s1'; memorized:=None |} _); simpl. + + refine (ex_intro _ {|real:=s1'; memorized:=None |} _); cbn. intuition. + destruct ms2 as [s|]. - - refine (ex_intro _ {|real:=s1'; memorized:=Some s |} _); simpl. + - refine (ex_intro _ {|real:=s1'; memorized:=Some s |} _); cbn. intuition. - - refine (ex_intro _ {|real:=s1'; memorized:=Some rs2 |} _); simpl. + - refine (ex_intro _ {|real:=s1'; memorized:=Some rs2 |} _); cbn. intuition. Unshelve. * intros; discriminate. @@ -228,7 +228,7 @@ 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. + + intros s1 H; eapply ex_intro with (x:={|real:=s1; memorized:=None |}); cbn. intuition. + intros; subst; auto. + intros; exploit memo_simulation_step; eauto. @@ -239,8 +239,8 @@ Qed. Lemma forward_memo_simulation_2: forward_simulation memoL1 L2. Proof. - 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. + unfold memoL1; cbn. + apply forward_simulation_opt with (measure:=fun s => dist_end_block (real s)) (match_states:=fun s1 s2 => match_states (head s1) s2); cbn; auto. + intros s1 [H0 H1]; destruct (match_initial_states (real s1) H0). unfold head; rewrite H1. intuition eauto. @@ -254,14 +254,14 @@ Proof. - (* MidBloc *) 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. + destruct (memorized s1); cbn; auto. tauto. - (* EndBloc *) constructor 1. destruct (simu_end_block (head s1) t (real s1') s2) as (s2' & H3 & H4); auto. * 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_tailstep; eauto. - * unfold head; rewrite H2; simpl. intuition eauto. + * unfold head; rewrite H2; cbn. intuition eauto. Qed. Lemma forward_simulation_block_rel: forward_simulation L1 L2. |