From b2fc9b55d9c59a9c507786a650377e2f0a1ddad8 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 29 Sep 2020 16:22:18 +0200 Subject: simpl -> cbn --- kvx/abstractbb/AbstractBasicBlocksDef.v | 50 ++++++------- kvx/abstractbb/ImpSimuTest.v | 52 +++++++------- kvx/abstractbb/Parallelizability.v | 124 ++++++++++++++++---------------- kvx/abstractbb/SeqSimuTheory.v | 56 +++++++-------- 4 files changed, 141 insertions(+), 141 deletions(-) (limited to 'kvx/abstractbb') diff --git a/kvx/abstractbb/AbstractBasicBlocksDef.v b/kvx/abstractbb/AbstractBasicBlocksDef.v index 948ed660..6960f363 100644 --- a/kvx/abstractbb/AbstractBasicBlocksDef.v +++ b/kvx/abstractbb/AbstractBasicBlocksDef.v @@ -170,7 +170,7 @@ Lemma exp_equiv e old1 old2: (exp_eval e m1 old1) = (exp_eval e m2 old2). Proof. intros H1. - induction e using exp_mut with (P0:=fun l => forall m1 m2, (forall x, m1 x = m2 x) -> list_exp_eval l m1 old1 = list_exp_eval l m2 old2); simpl; try congruence; auto. + induction e using exp_mut with (P0:=fun l => forall m1 m2, (forall x, m1 x = m2 x) -> list_exp_eval l m1 old1 = list_exp_eval l m2 old2); cbn; try congruence; auto. - intros; erewrite IHe; eauto. - intros; erewrite IHe, IHe0; auto. Qed. @@ -183,38 +183,38 @@ Lemma inst_equiv_refl i old1 old2: forall m1 m2, (forall x, m1 x = m2 x) -> res_eq (inst_run i m1 old1) (inst_run i m2 old2). Proof. - intro H; induction i as [ | [x e]]; simpl; eauto. + intro H; induction i as [ | [x e]]; cbn; eauto. intros m1 m2 H1. erewrite exp_equiv; eauto. - destruct (exp_eval e m2 old2); simpl; auto. + destruct (exp_eval e m2 old2); cbn; auto. apply IHi. unfold assign; intro y. destruct (R.eq_dec x y); auto. Qed. Lemma bblock_equiv_refl p: forall m1 m2, (forall x, m1 x = m2 x) -> res_eq (run p m1) (run p m2). Proof. - induction p as [ | i p']; simpl; eauto. + induction p as [ | i p']; cbn; eauto. intros m1 m2 H; lapply (inst_equiv_refl i m1 m2); auto. intros X; lapply (X m1 m2); auto; clear X. - destruct (inst_run i m1 m1); simpl. - - intros [m3 [H1 H2]]; rewrite H1; simpl; auto. - - intros H1; rewrite H1; simpl; auto. + destruct (inst_run i m1 m1); cbn. + - intros [m3 [H1 H2]]; rewrite H1; cbn; auto. + - intros H1; rewrite H1; cbn; auto. Qed. Lemma res_eq_sym om1 om2: res_eq om1 om2 -> res_eq om2 om1. Proof. - destruct om1; simpl. - - intros [m2 [H1 H2]]; subst; simpl. eauto. - - intros; subst; simpl; eauto. + destruct om1; cbn. + - intros [m2 [H1 H2]]; subst; cbn. eauto. + - intros; subst; cbn; eauto. Qed. Lemma res_eq_trans (om1 om2 om3: option mem): (res_eq om1 om2) -> (res_eq om2 om3) -> (res_eq om1 om3). Proof. - destruct om1; simpl. - - intros [m2 [H1 H2]]; subst; simpl. - intros [m3 [H3 H4]]; subst; simpl. + destruct om1; cbn. + - intros [m2 [H1 H2]]; subst; cbn. + intros [m3 [H3 H4]]; subst; cbn. eapply ex_intro; intuition eauto. rewrite H2; auto. - - intro; subst; simpl; auto. + - intro; subst; cbn; auto. Qed. Lemma bblock_simu_alt p1 p2: bblock_simu p1 p2 <-> (forall m1 m2, (forall x, m1 x = m2 x) -> (run p1 m1)<>None -> res_eq (run p1 m1) (run p2 m2)). @@ -232,8 +232,8 @@ Lemma run_app p1: forall m1 p2, | None => None end. Proof. - induction p1; simpl; try congruence. - intros; destruct (inst_run _ _ _); simpl; auto. + induction p1; cbn; try congruence. + intros; destruct (inst_run _ _ _); cbn; auto. Qed. Lemma run_app_None p1 m1 p2: @@ -334,7 +334,7 @@ Fixpoint allvalid ge (l: list term) m : Prop := Lemma allvalid_extensionality ge (l: list term) m: allvalid ge l m <-> (forall t, List.In t l -> term_eval ge t m <> None). Proof. - induction l as [|t l]; simpl; try (tauto). + induction l as [|t l]; cbn; try (tauto). destruct l. - intuition (congruence || eauto). - rewrite IHl; clear IHl. intuition (congruence || eauto). @@ -365,7 +365,7 @@ Qed. Lemma intro_fail_correct (l: list term) (t: term) : (forall ge m, term_eval ge t m <> None <-> allvalid ge l m) -> match_pt t (intro_fail l t). Proof. - unfold match_pt; simpl; intros; intuition congruence. + unfold match_pt; cbn; intros; intuition congruence. Qed. Hint Resolve intro_fail_correct: wlp. @@ -374,7 +374,7 @@ Definition identity_fail (t: term):= intro_fail [t] t. Lemma identity_fail_correct (t: term): match_pt t (identity_fail t). Proof. - eapply intro_fail_correct; simpl; tauto. + eapply intro_fail_correct; cbn; tauto. Qed. Global Opaque identity_fail. Hint Resolve identity_fail_correct: wlp. @@ -390,11 +390,11 @@ Definition nofail (is_constant: op -> bool) (t: term):= Lemma nofail_correct (is_constant: op -> bool) t: (forall ge o, is_constant o = true -> op_eval ge o nil <> None) -> match_pt t (nofail is_constant t). Proof. - destruct t; simpl. - + intros; eapply intro_fail_correct; simpl; intuition congruence. - + intros; destruct l; simpl; auto with wlp. - destruct (is_constant o) eqn:Heqo; simpl; intuition eauto with wlp. - eapply intro_fail_correct; simpl; intuition eauto with wlp. + destruct t; cbn. + + intros; eapply intro_fail_correct; cbn; intuition congruence. + + intros; destruct l; cbn; auto with wlp. + destruct (is_constant o) eqn:Heqo; cbn; intuition eauto with wlp. + eapply intro_fail_correct; cbn; intuition eauto with wlp. Qed. Global Opaque nofail. Hint Resolve nofail_correct: wlp. @@ -425,7 +425,7 @@ Lemma app_fail_allvalid_correct l pt t1 t2: forall (V2: forall (ge : genv) (m : mem), term_eval ge t2 m <> None <-> allvalid ge (mayfail {| mayfail := t1 :: l; effect := t1 |}) m) (ge : genv) (m : mem), term_eval ge t2 m <> None <-> allvalid ge (mayfail (app_fail l pt)) m. Proof. - intros; generalize (V1 ge m) (V2 ge m); rewrite !allvalid_extensionality; simpl. clear V1 V2. + intros; generalize (V1 ge m) (V2 ge m); rewrite !allvalid_extensionality; cbn. clear V1 V2. intuition subst. + rewrite rev_append_rev, in_app_iff, <- in_rev in H3. destruct H3; eauto. + eapply H3; eauto. diff --git a/kvx/abstractbb/ImpSimuTest.v b/kvx/abstractbb/ImpSimuTest.v index 89260ddb..b1a3b985 100644 --- a/kvx/abstractbb/ImpSimuTest.v +++ b/kvx/abstractbb/ImpSimuTest.v @@ -160,13 +160,13 @@ Definition list_term_set_hid (l: list_term) (hid: hashcode): list_term := Lemma term_eval_set_hid ge t hid m: term_eval ge (term_set_hid t hid) m = term_eval ge t m. Proof. - destruct t; simpl; auto. + destruct t; cbn; auto. Qed. Lemma list_term_eval_set_hid ge l hid m: list_term_eval ge (list_term_set_hid l hid) m = list_term_eval ge l m. Proof. - destruct l; simpl; auto. + destruct l; cbn; auto. Qed. (* Local nickname *) @@ -315,7 +315,7 @@ Proof. destruct (DM0 m) as (PRE & VALID0); clear DM0. assert (VALID1: allvalid ge hd.(hpre) m -> pre d ge m). { unfold smem_valid in PRE; tauto. } assert (VALID2: allvalid ge hd.(hpre) m -> forall x : Dict.R.t, ST.term_eval ge (d x) m <> None). { unfold smem_valid in PRE; tauto. } - rewrite !allvalid_extensionality in * |- *; simpl. + rewrite !allvalid_extensionality in * |- *; cbn. intuition (subst; eauto). + eapply smem_valid_set_proof; eauto. erewrite <- EQT; eauto. @@ -323,11 +323,11 @@ Proof. intros X1; exploit smem_valid_set_decompose_2; eauto. rewrite <- EQT; eauto. + exploit smem_valid_set_decompose_1; eauto. - - clear DM0. unfold hsmem_post_eval, hsmem_post_eval in * |- *; simpl. + - clear DM0. unfold hsmem_post_eval, hsmem_post_eval in * |- *; cbn. Local Hint Resolve smem_valid_set_decompose_1: core. intros; case (R.eq_dec x x0). - + intros; subst; rewrite !Dict.set_spec_eq; simpl; eauto. - + intros; rewrite !Dict.set_spec_diff; simpl; eauto. + + intros; subst; rewrite !Dict.set_spec_eq; cbn; eauto. + + intros; rewrite !Dict.set_spec_diff; cbn; eauto. Qed. Local Hint Resolve naive_set_correct: core. @@ -404,10 +404,10 @@ Lemma hterm_append_correct l: forall lh, WHEN hterm_append l lh ~> lh' THEN (forall ge m, allvalid ge lh' m <-> (allvalid ge l m /\ allvalid ge lh m)). Proof. Local Hint Resolve eq_trans: localhint. - induction l as [|t l']; simpl; wlp_xsimplify ltac:(eauto with wlp). + induction l as [|t l']; cbn; wlp_xsimplify ltac:(eauto with wlp). - intros; rewrite! allvalid_extensionality; intuition eauto. - intros REC ge m; rewrite REC; clear IHl' REC. rewrite !allvalid_extensionality. - simpl; intuition (subst; eauto with wlp localhint). + cbn; intuition (subst; eauto with wlp localhint). Qed. (*Local Hint Resolve hterm_append_correct: wlp.*) Global Opaque hterm_append. @@ -431,8 +431,8 @@ Lemma smart_set_correct hd x ht: forall ge m y, hsmem_post_eval ge d y m = hsmem_post_eval ge (Dict.set hd x ht) y m. Proof. destruct ht; wlp_simplify. - unfold hsmem_post_eval; simpl. case (R.eq_dec x0 y). - - intros; subst. rewrite Dict.set_spec_eq, Dict.rem_spec_eq. simpl; congruence. + unfold hsmem_post_eval; cbn. case (R.eq_dec x0 y). + - intros; subst. rewrite Dict.set_spec_eq, Dict.rem_spec_eq. cbn; congruence. - intros; rewrite Dict.set_spec_diff, Dict.rem_spec_diff; auto. Qed. (*Local Hint Resolve smart_set_correct: wlp.*) @@ -456,17 +456,17 @@ Proof. generalize (hterm_append_correct _ _ _ Hexta0); intro APPEND. generalize (hterm_lift_correct _ _ Hexta1); intro LIFT. generalize (smart_set_correct _ _ _ _ Hexta3); intro SMART. - eapply equiv_hsmem_models; eauto; unfold equiv_hsmem; simpl. + eapply equiv_hsmem_models; eauto; unfold equiv_hsmem; cbn. destruct H as (VALID & EFFECT); split. - intros; rewrite APPEND, <- VALID. - rewrite !allvalid_extensionality in * |- *; simpl; intuition (subst; eauto). + rewrite !allvalid_extensionality in * |- *; cbn; intuition (subst; eauto). - intros m x0 ALLVALID; rewrite SMART. destruct (term_eval ge ht m) eqn: Hht. * case (R.eq_dec x x0). - + intros; subst. unfold hsmem_post_eval; simpl. rewrite !Dict.set_spec_eq. + + intros; subst. unfold hsmem_post_eval; cbn. rewrite !Dict.set_spec_eq. erewrite LIFT, EFFECT; eauto. - + intros; unfold hsmem_post_eval; simpl. rewrite !Dict.set_spec_diff; auto. - * rewrite allvalid_extensionality in ALLVALID; destruct (ALLVALID ht); simpl; auto. + + intros; unfold hsmem_post_eval; cbn. rewrite !Dict.set_spec_diff; auto. + * rewrite allvalid_extensionality in ALLVALID; destruct (ALLVALID ht); cbn; auto. Qed. Local Hint Resolve hsmem_set_correct: wlp. Global Opaque hsmem_set. @@ -481,7 +481,7 @@ Proof. intro H. induction e using exp_mut with (P0:=fun le => forall d hd, smem_model ge d hd -> forall m, smem_valid ge d m -> smem_valid ge od m -> list_term_eval ge (list_exp_term le hd hod) m = list_term_eval ge (list_exp_term le d od) m); - unfold smem_model in * |- * ; simpl; intuition eauto. + unfold smem_model in * |- * ; cbn; intuition eauto. - erewrite IHe; eauto. - erewrite IHe0, IHe; eauto. Qed. @@ -516,10 +516,10 @@ Lemma exp_hterm_correct_x ge e hod od: induction e using exp_mut with (P0:=fun le => forall d hd, smem_model ge d hd -> WHEN list_exp_hterm le hd hod ~> lt THEN forall m, smem_valid ge d m -> smem_valid ge od m -> list_term_eval ge lt m = ST.list_term_eval ge (list_exp_term le d od) m); - unfold smem_model, hsmem_post_eval in * |- * ; simpl; wlp_simplify. + unfold smem_model, hsmem_post_eval in * |- * ; cbn; wlp_simplify. - rewrite H1, <- H4; auto. - - rewrite H4, <- H0; simpl; auto. - - rewrite H5, <- H0, <- H4; simpl; auto. + - rewrite H4, <- H0; cbn; auto. + - rewrite H5, <- H0, <- H4; cbn; auto. Qed. Global Opaque exp_hterm. @@ -544,7 +544,7 @@ Lemma hinst_smem_correct i: forall hd hod, forall ge od d, smem_model ge od hod -> smem_model ge d hd -> (forall m, smem_valid ge d m -> smem_valid ge od m) -> smem_model ge (inst_smem i d od) hd'. Proof. Local Hint Resolve smem_valid_set_proof: core. - induction i; simpl; wlp_simplify; eauto 15 with wlp. + induction i; cbn; wlp_simplify; eauto 15 with wlp. Qed. Global Opaque hinst_smem. Local Hint Resolve hinst_smem_correct: wlp. @@ -564,7 +564,7 @@ Fixpoint bblock_hsmem_rec (p: bblock) (d: hsmem): ?? hsmem := Lemma bblock_hsmem_rec_correct p: forall hd, WHEN bblock_hsmem_rec p hd ~> hd' THEN forall ge d, smem_model ge d hd -> smem_model ge (bblock_smem_rec p d) hd'. Proof. - induction p; simpl; wlp_simplify. + induction p; cbn; wlp_simplify. Qed. Global Opaque bblock_hsmem_rec. Local Hint Resolve bblock_hsmem_rec_correct: wlp. @@ -573,8 +573,8 @@ Definition hsmem_empty: hsmem := {| hpre:= nil ; hpost := Dict.empty |}. Lemma hsmem_empty_correct ge: smem_model ge smem_empty hsmem_empty. Proof. - unfold smem_model, smem_valid, hsmem_post_eval; simpl; intuition try congruence. - rewrite !Dict.empty_spec; simpl; auto. + unfold smem_model, smem_valid, hsmem_post_eval; cbn; intuition try congruence. + rewrite !Dict.empty_spec; cbn; auto. Qed. Definition bblock_hsmem: bblock -> ?? hsmem @@ -722,7 +722,7 @@ Theorem g_bblock_simu_test_correct p1 p2: WHEN g_bblock_simu_test p1 p2 ~> b THEN b=true -> forall ge, bblock_simu ge p1 p2. Proof. wlp_simplify. - destruct exta0; simpl in * |- *; auto. + destruct exta0; cbn in * |- *; auto. Qed. Global Opaque g_bblock_simu_test. @@ -1209,8 +1209,8 @@ Lemma eq_test_correct A d1: forall (d2: t A), WHEN eq_test d1 d2 ~> b THEN b=true -> forall x, get d1 x = get d2 x. Proof. - unfold get; induction d1 as [|l1 Hl1 [x1|] r1 Hr1]; destruct d2 as [|l2 [x2|] r2]; simpl; - wlp_simplify; (discriminate || (subst; destruct x; simpl; auto)). + unfold get; induction d1 as [|l1 Hl1 [x1|] r1 Hr1]; destruct d2 as [|l2 [x2|] r2]; cbn; + wlp_simplify; (discriminate || (subst; destruct x; cbn; auto)). Qed. Global Opaque eq_test. diff --git a/kvx/abstractbb/Parallelizability.v b/kvx/abstractbb/Parallelizability.v index 79ec9038..e5d21434 100644 --- a/kvx/abstractbb/Parallelizability.v +++ b/kvx/abstractbb/Parallelizability.v @@ -50,8 +50,8 @@ Fixpoint inst_prun (i: inst) (m tmp old: mem): option mem := Lemma inst_run_prun i: forall m old, inst_run ge i m old = inst_prun i m m old. Proof. - induction i as [|[y e] i']; simpl; auto. - intros m old; destruct (exp_eval ge e m old); simpl; auto. + induction i as [|[y e] i']; cbn; auto. + intros m old; destruct (exp_eval ge e m old); cbn; auto. Qed. @@ -76,8 +76,8 @@ Lemma inst_prun_equiv i old: forall m1 m2 tmp, (forall x, m1 x = m2 x) -> res_eq (inst_prun i m1 tmp old) (inst_prun i m2 tmp old). Proof. - induction i as [|[x e] i']; simpl; eauto. - intros m1 m2 tmp H; destruct (exp_eval ge e tmp old); simpl; auto. + induction i as [|[x e] i']; cbn; eauto. + intros m1 m2 tmp H; destruct (exp_eval ge e tmp old); cbn; auto. eapply IHi'; unfold assign. intros; destruct (R.eq_dec x x0); auto. Qed. @@ -85,12 +85,12 @@ Lemma prun_iw_equiv p: forall m1 m2 old, (forall x, m1 x = m2 x) -> res_eq (prun_iw p m1 old) (prun_iw p m2 old). Proof. - induction p as [|i p']; simpl; eauto. + induction p as [|i p']; cbn; eauto. - intros m1 m2 old H. generalize (inst_prun_equiv i old m1 m2 old H); - destruct (inst_prun i m1 old old); simpl. - + intros (m3 & H3 & H4); rewrite H3; simpl; eauto. - + intros H1; rewrite H1; simpl; auto. + destruct (inst_prun i m1 old old); cbn. + + intros (m3 & H3 & H4); rewrite H3; cbn; eauto. + + intros H1; rewrite H1; cbn; auto. Qed. @@ -101,8 +101,8 @@ Lemma prun_iw_app p1: forall m1 old p2, | None => None end. Proof. - induction p1; simpl; try congruence. - intros; destruct (inst_prun _ _ _); simpl; auto. + induction p1; cbn; try congruence. + intros; destruct (inst_prun _ _ _); cbn; auto. Qed. Lemma prun_iw_app_None p1: forall m1 old p2, @@ -132,12 +132,12 @@ Fixpoint notIn {A} (x: A) (l:list A): Prop := Lemma notIn_iff A (x:A) l: (~List.In x l) <-> notIn x l. Proof. - induction l; simpl; intuition. + induction l; cbn; intuition. Qed. Lemma notIn_app A (x:A) l1: forall l2, notIn x (l1++l2) <-> (notIn x l1 /\ notIn x l2). Proof. - induction l1; simpl. + induction l1; cbn. - intuition. - intros; rewrite IHl1. intuition. Qed. @@ -145,7 +145,7 @@ Qed. Lemma In_Permutation A (l1 l2: list A): Permutation l1 l2 -> forall x, In x l1 -> In x l2. Proof. - induction 1; simpl; intuition. + induction 1; cbn; intuition. Qed. Lemma Permutation_incl A (l1 l2: list A): Permutation l1 l2 -> incl l1 l2. @@ -174,7 +174,7 @@ Qed. Lemma disjoint_cons_l A (x:A) (l1 l2: list A): disjoint (x::l1) l2 <-> (notIn x l2) /\ (disjoint l1 l2). Proof. - unfold disjoint. simpl; intuition subst; auto. + unfold disjoint. cbn; intuition subst; auto. Qed. Lemma disjoint_cons_r A (x:A) (l1 l2: list A): disjoint l1 (x::l2) <-> (notIn x l1) /\ (disjoint l1 l2). @@ -230,13 +230,13 @@ Fixpoint frame_assign m1 (f: list R.t) m2 := Lemma frame_assign_def f: forall m1 m2 x, frame_assign m1 f m2 x = if notIn_dec x f then m1 x else m2 x. Proof. - induction f as [|y f] ; simpl; auto. - - intros; destruct (notIn_dec x []); simpl in *; tauto. - - intros; rewrite IHf; destruct (notIn_dec x (y::f)); simpl in *. - + destruct (notIn_dec x f); simpl in *; intuition. + induction f as [|y f] ; cbn; auto. + - intros; destruct (notIn_dec x []); cbn in *; tauto. + - intros; rewrite IHf; destruct (notIn_dec x (y::f)); cbn in *. + + destruct (notIn_dec x f); cbn in *; intuition. rewrite assign_diff; auto. rewrite <- notIn_iff in *; intuition. - + destruct (notIn_dec x f); simpl in *; intuition subst. + + destruct (notIn_dec x f); cbn in *; intuition subst. rewrite assign_eq; auto. rewrite <- notIn_iff in *; intuition. Qed. @@ -266,7 +266,7 @@ Lemma frame_eq_list_split f1 (f2: R.t -> Prop) om1 om2: (forall m1 m2 x, om1 = Some m1 -> om2 = Some m2 -> f2 x -> notIn x f1 -> m1 x = m2 x) -> frame_eq f2 om1 om2. Proof. - unfold frame_eq; destruct om1 as [ m1 | ]; simpl; auto. + unfold frame_eq; destruct om1 as [ m1 | ]; cbn; auto. intros (m2 & H0 & H1); subst. intros H. eexists; intuition eauto. @@ -280,7 +280,7 @@ Lemma frame_eq_res_eq f om1 om2: res_eq om1 om2. Proof. intros H H0; lapply (frame_eq_list_split f (fun _ => True) om1 om2 H); eauto. - clear H H0; unfold frame_eq, res_eq. destruct om1; simpl; firstorder. + clear H H0; unfold frame_eq, res_eq. destruct om1; cbn; firstorder. Qed. *) @@ -296,9 +296,9 @@ Lemma inst_wframe_correct i m' old: forall m tmp, inst_prun ge i m tmp old = Some m' -> forall x, notIn x (inst_wframe i) -> m' x = m x. Proof. - induction i as [|[y e] i']; simpl. + induction i as [|[y e] i']; cbn. - intros m tmp H x H0; inversion_clear H; auto. - - intros m tmp H x (H1 & H2); destruct (exp_eval ge e tmp old); simpl; try congruence. + - intros m tmp H x (H1 & H2); destruct (exp_eval ge e tmp old); cbn; try congruence. cutrewrite (m x = assign m y v x); eauto. rewrite assign_diff; auto. Qed. @@ -306,9 +306,9 @@ Qed. Lemma inst_prun_fequiv i old: forall m1 m2 tmp, frame_eq (fun x => In x (inst_wframe i)) (inst_prun ge i m1 tmp old) (inst_prun ge i m2 tmp old). Proof. - induction i as [|[y e] i']; simpl. + induction i as [|[y e] i']; cbn. - intros m1 m2 tmp; eexists; intuition eauto. - - intros m1 m2 tmp. destruct (exp_eval ge e tmp old); simpl; auto. + - intros m1 m2 tmp. destruct (exp_eval ge e tmp old); cbn; auto. eapply frame_eq_list_split; eauto. clear IHi'. intros m1' m2' x H1 H2. lapply (inst_wframe_correct i' m1' old (assign m1 y v) (assign tmp y v)); eauto. @@ -323,7 +323,7 @@ Lemma inst_prun_None i m1 m2 tmp old: inst_prun ge i m2 tmp old = None. Proof. intros H; generalize (inst_prun_fequiv i old m1 m2 tmp). - rewrite H; simpl; auto. + rewrite H; cbn; auto. Qed. Lemma inst_prun_Some i m1 m2 tmp old m1': @@ -331,7 +331,7 @@ Lemma inst_prun_Some i m1 m2 tmp old m1': res_eq (Some (frame_assign m2 (inst_wframe i) m1')) (inst_prun ge i m2 tmp old). Proof. intros H; generalize (inst_prun_fequiv i old m1 m2 tmp). - rewrite H; simpl. + rewrite H; cbn. intros (m2' & H1 & H2). eexists; intuition eauto. rewrite frame_assign_def. @@ -351,7 +351,7 @@ Local Hint Resolve Permutation_app_head Permutation_app_tail Permutation_app_com Lemma bblock_wframe_Permutation p p': Permutation p p' -> Permutation (bblock_wframe p) (bblock_wframe p'). Proof. - induction 1 as [|i p p'|i1 i2 p|p1 p2 p3]; simpl; auto. + induction 1 as [|i p p'|i1 i2 p|p1 p2 p3]; cbn; auto. - rewrite! app_assoc; auto. - eapply Permutation_trans; eauto. Qed. @@ -361,11 +361,11 @@ Lemma bblock_wframe_correct p m' old: forall m, prun_iw p m old = Some m' -> forall x, notIn x (bblock_wframe p) -> m' x = m x. Proof. - induction p as [|i p']; simpl. + induction p as [|i p']; cbn. - intros m H; inversion_clear H; auto. - intros m H x; rewrite notIn_app; intros (H1 & H2). remember (inst_prun i m old old) as om. - destruct om as [m1|]; simpl. + destruct om as [m1|]; cbn. + eapply eq_trans. eapply IHp'; eauto. eapply inst_wframe_correct; eauto. @@ -375,12 +375,12 @@ Qed. Lemma prun_iw_fequiv p old: forall m1 m2, frame_eq (fun x => In x (bblock_wframe p)) (prun_iw p m1 old) (prun_iw p m2 old). Proof. - induction p as [|i p']; simpl. + induction p as [|i p']; cbn. - intros m1 m2; eexists; intuition eauto. - intros m1 m2; generalize (inst_prun_fequiv i old m1 m2 old). remember (inst_prun i m1 old old) as om. - destruct om as [m1'|]; simpl. - + intros (m2' & H1 & H2). rewrite H1; simpl. + destruct om as [m1'|]; cbn. + + intros (m2' & H1 & H2). rewrite H1; cbn. eapply frame_eq_list_split; eauto. clear IHp'. intros m1'' m2'' x H3 H4. rewrite in_app_iff. intros X X2. assert (X1: In x (inst_wframe i)). { destruct X; auto. rewrite <- notIn_iff in X2; tauto. } @@ -389,7 +389,7 @@ Proof. lapply (bblock_wframe_correct p' m2'' old m2'); eauto. intros Xm2' Xm1'. rewrite Xm1', Xm2'; auto. - + intro H; rewrite H; simpl; auto. + + intro H; rewrite H; cbn; auto. Qed. Lemma prun_iw_equiv p m1 m2 old: @@ -418,7 +418,7 @@ Fixpoint is_det (p: bblock): Prop := Lemma is_det_Permutation p p': Permutation p p' -> is_det p -> is_det p'. Proof. - induction 1; simpl; auto. + induction 1; cbn; auto. - intros; intuition. eapply disjoint_incl_r. 2: eauto. eapply Permutation_incl. eapply Permutation_sym. eapply bblock_wframe_Permutation; auto. @@ -431,20 +431,20 @@ Theorem is_det_correct p p': is_det p -> forall m old, res_eq (prun_iw ge p m old) (prun_iw ge p' m old). Proof. - induction 1 as [ | i p p' | i1 i2 p | p1 p2 p3 ]; simpl; eauto. + induction 1 as [ | i p p' | i1 i2 p | p1 p2 p3 ]; cbn; eauto. - intros [H0 H1] m old. remember (inst_prun ge i m old old) as om0. - destruct om0 as [ m0 | ]; simpl; auto. + destruct om0 as [ m0 | ]; cbn; auto. - rewrite disjoint_app_r. intros ([Z1 Z2] & Z3 & Z4) m old. remember (inst_prun ge i2 m old old) as om2. - destruct om2 as [ m2 | ]; simpl; auto. + destruct om2 as [ m2 | ]; cbn; auto. + remember (inst_prun ge i1 m old old) as om1. - destruct om1 as [ m1 | ]; simpl; auto. - * lapply (inst_prun_Some i2 m m1 old old m2); simpl; auto. - lapply (inst_prun_Some i1 m m2 old old m1); simpl; auto. + destruct om1 as [ m1 | ]; cbn; auto. + * lapply (inst_prun_Some i2 m m1 old old m2); cbn; auto. + lapply (inst_prun_Some i1 m m2 old old m1); cbn; auto. intros (m1' & Hm1' & Xm1') (m2' & Hm2' & Xm2'). - rewrite Hm1', Hm2'; simpl. + rewrite Hm1', Hm2'; cbn. eapply prun_iw_equiv. intros x; rewrite <- Xm1', <- Xm2'. clear Xm2' Xm1' Hm1' Hm2' m1' m2'. rewrite frame_assign_def. @@ -455,9 +455,9 @@ Proof. erewrite (inst_wframe_correct i1 m1 old m old); eauto. } rewrite frame_assign_notIn; auto. - * erewrite inst_prun_None; eauto. simpl; auto. + * erewrite inst_prun_None; eauto. cbn; auto. + remember (inst_prun ge i1 m old old) as om1. - destruct om1 as [ m1 | ]; simpl; auto. + destruct om1 as [ m1 | ]; cbn; auto. erewrite inst_prun_None; eauto. - intros; eapply res_eq_trans. eapply IHPermutation1; eauto. @@ -486,7 +486,7 @@ Lemma exp_frame_correct e old1 old2: (exp_eval ge e m1 old1)=(exp_eval ge e m2 old2). Proof. induction e using exp_mut with (P0:=fun l => (forall x, In x (list_exp_frame l) -> old1 x = old2 x) -> forall m1 m2, (forall x, In x (list_exp_frame l) -> m1 x = m2 x) -> - (list_exp_eval ge l m1 old1)=(list_exp_eval ge l m2 old2)); simpl; auto. + (list_exp_eval ge l m1 old1)=(list_exp_eval ge l m2 old2)); cbn; auto. - intros H1 m1 m2 H2; rewrite H2; auto. - intros H1 m1 m2 H2; erewrite IHe; eauto. - intros H1 m1 m2 H2; erewrite IHe, IHe0; eauto; @@ -501,7 +501,7 @@ Fixpoint inst_frame (i: inst): list R.t := Lemma inst_wframe_frame i x: In x (inst_wframe i) -> In x (inst_frame i). Proof. - induction i as [ | [y e] i']; simpl; intuition. + induction i as [ | [y e] i']; cbn; intuition. Qed. @@ -511,13 +511,13 @@ Lemma inst_frame_correct i wframe old1 old2: forall m tmp1 tmp2, (forall x, notIn x wframe -> tmp1 x = tmp2 x) -> inst_prun ge i m tmp1 old1 = inst_prun ge i m tmp2 old2. Proof. - induction i as [|[x e] i']; simpl; auto. + induction i as [|[x e] i']; cbn; auto. intros m tmp1 tmp2; rewrite disjoint_cons_l, disjoint_app_l. intros (H1 & H2 & H3) H6 H7. cutrewrite (exp_eval ge e tmp1 old1 = exp_eval ge e tmp2 old2). - destruct (exp_eval ge e tmp2 old2); auto. eapply IHi'; eauto. - simpl; intros x0 H0; unfold assign. destruct (R.eq_dec x x0); simpl; auto. + cbn; intros x0 H0; unfold assign. destruct (R.eq_dec x x0); cbn; auto. - unfold disjoint in H2; apply exp_frame_correct. intros;apply H6; auto. intros;apply H7; auto. @@ -535,8 +535,8 @@ Fixpoint pararec (p: bblock) (wframe: list R.t): Prop := Lemma pararec_disjoint (p: bblock): forall wframe, pararec p wframe -> disjoint (bblock_wframe p) wframe. Proof. - induction p as [|i p']; simpl. - - unfold disjoint; simpl; intuition. + induction p as [|i p']; cbn. + - unfold disjoint; cbn; intuition. - intros wframe [H0 H1]; rewrite disjoint_app_l. generalize (IHp' _ H1). rewrite disjoint_app_r. intuition. @@ -546,7 +546,7 @@ Qed. Lemma pararec_det p: forall wframe, pararec p wframe -> is_det p. Proof. - induction p as [|i p']; simpl; auto. + induction p as [|i p']; cbn; auto. intros wframe [H0 H1]. generalize (pararec_disjoint _ _ H1). rewrite disjoint_app_r. intuition. - apply disjoint_sym; auto. @@ -558,7 +558,7 @@ Lemma pararec_correct p old: forall wframe m, (forall x, notIn x wframe -> m x = old x) -> run ge p m = prun_iw ge p m old. Proof. - elim p; clear p; simpl; auto. + elim p; clear p; cbn; auto. intros i p' X wframe m [H H0] H1. erewrite inst_run_prun, inst_frame_correct; eauto. remember (inst_prun ge i m old old) as om0. @@ -646,7 +646,7 @@ Fixpoint inst_wsframe(i:inst): S.t := Lemma inst_wsframe_correct i: S.match_frame (inst_wsframe i) (inst_wframe i). Proof. - induction i; simpl; auto. + induction i; cbn; auto. Qed. Fixpoint exp_sframe (e: exp): S.t := @@ -664,7 +664,7 @@ with list_exp_sframe (le: list_exp): S.t := Lemma exp_sframe_correct e: S.match_frame (exp_sframe e) (exp_frame e). Proof. - induction e using exp_mut with (P0:=fun l => S.match_frame (list_exp_sframe l) (list_exp_frame l)); simpl; auto. + induction e using exp_mut with (P0:=fun l => S.match_frame (list_exp_sframe l) (list_exp_frame l)); cbn; auto. Qed. Fixpoint inst_sframe (i: inst): S.t := @@ -677,7 +677,7 @@ Local Hint Resolve exp_sframe_correct: core. Lemma inst_sframe_correct i: S.match_frame (inst_sframe i) (inst_frame i). Proof. - induction i as [|[y e] i']; simpl; auto. + induction i as [|[y e] i']; cbn; auto. Qed. Local Hint Resolve inst_wsframe_correct inst_sframe_correct: core. @@ -692,7 +692,7 @@ Fixpoint is_pararec (p: bblock) (wsframe: S.t): bool := Lemma is_pararec_correct (p: bblock): forall s l, S.match_frame s l -> (is_pararec p s)=true -> (pararec p l). Proof. - induction p; simpl; auto. + induction p; cbn; auto. intros s l H1 H2; rewrite lazy_andb_bool_true in H2. destruct H2 as [H2 H3]. constructor 1; eauto. Qed. @@ -739,14 +739,14 @@ Definition empty:=PositiveSet.empty. Lemma empty_match_frame: match_frame empty nil. Proof. - unfold match_frame, empty, PositiveSet.In; simpl; intuition. + unfold match_frame, empty, PositiveSet.In; cbn; intuition. Qed. Definition add: R.t -> t -> t := PositiveSet.add. Lemma add_match_frame: forall s x l, match_frame s l -> match_frame (add x s) (x::l). Proof. - unfold match_frame, add; simpl. + unfold match_frame, add; cbn. intros s x l H y. rewrite PositiveSet.add_spec, H. intuition. Qed. @@ -772,13 +772,13 @@ Fixpoint is_disjoint (s s': PositiveSet.t) : bool := Lemma is_disjoint_spec_true s: forall s', is_disjoint s s' = true -> forall x, PositiveSet.In x s -> PositiveSet.In x s' -> False. Proof. - unfold PositiveSet.In; induction s as [ |l IHl o r IHr]; simpl; try discriminate. - destruct s' as [|l' o' r']; simpl; try discriminate. + unfold PositiveSet.In; induction s as [ |l IHl o r IHr]; cbn; try discriminate. + destruct s' as [|l' o' r']; cbn; try discriminate. intros X. assert (H: ~(o = true /\ o'=true) /\ is_disjoint l l' = true /\ is_disjoint r r'=true). - { destruct o, o', (is_disjoint l l'), (is_disjoint r r'); simpl in X; intuition. } + { destruct o, o', (is_disjoint l l'), (is_disjoint r r'); cbn in X; intuition. } clear X; destruct H as (H & H1 & H2). - destruct x as [i|i|]; simpl; eauto. + destruct x as [i|i|]; cbn; eauto. Qed. Lemma is_disjoint_match_frame: forall s1 s2 l1 l2, match_frame s1 l1 -> match_frame s2 l2 -> (is_disjoint s1 s2)=true -> disjoint l1 l2. diff --git a/kvx/abstractbb/SeqSimuTheory.v b/kvx/abstractbb/SeqSimuTheory.v index a957c50a..df6b9963 100644 --- a/kvx/abstractbb/SeqSimuTheory.v +++ b/kvx/abstractbb/SeqSimuTheory.v @@ -92,13 +92,13 @@ Variable ge: genv. Lemma set_spec_eq d x t m: term_eval ge (smem_set d x t x) m = term_eval ge t m. Proof. - unfold smem_set; simpl; case (R.eq_dec x x); try congruence. + unfold smem_set; cbn; case (R.eq_dec x x); try congruence. Qed. Lemma set_spec_diff d x y t m: x <> y -> term_eval ge (smem_set d x t y) m = term_eval ge (d y) m. Proof. - unfold smem_set; simpl; case (R.eq_dec x y); try congruence. + unfold smem_set; cbn; case (R.eq_dec x y); try congruence. Qed. Fixpoint inst_smem (i: inst) (d old: smem): smem := @@ -123,15 +123,15 @@ Definition bblock_smem: bblock -> smem Lemma inst_smem_pre_monotonic i old: forall d m, (pre (inst_smem i d old) ge m) -> (pre d ge m). Proof. - induction i as [|[y e] i IHi]; simpl; auto. + induction i as [|[y e] i IHi]; cbn; auto. intros d a H; generalize (IHi _ _ H); clear H IHi. - unfold smem_set; simpl; intuition. + unfold smem_set; cbn; intuition. Qed. Lemma bblock_smem_pre_monotonic p: forall d m, (pre (bblock_smem_rec p d) ge m) -> (pre d ge m). Proof. - induction p as [|i p' IHp']; simpl; eauto. + induction p as [|i p' IHp']; cbn; eauto. intros d a H; eapply inst_smem_pre_monotonic; eauto. Qed. @@ -146,7 +146,7 @@ Proof. intro H. induction e using exp_mut with (P0:=fun l => forall (d:smem) m1, (forall x, term_eval ge (d x) m0 = Some (m1 x)) -> list_term_eval ge (list_exp_term l d od) m0 = list_exp_eval ge l m1 old); - simpl; auto. + cbn; auto. - intros; erewrite IHe; eauto. - intros. erewrite IHe, IHe0; eauto. Qed. @@ -156,12 +156,12 @@ Lemma inst_smem_abort i m0 x old: forall (d:smem), term_eval ge (d x) m0 = None -> term_eval ge (inst_smem i d old x) m0 = None. Proof. - induction i as [|[y e] i IHi]; simpl; auto. + induction i as [|[y e] i IHi]; cbn; auto. intros d VALID H; erewrite IHi; eauto. clear IHi. - unfold smem_set; simpl; destruct (R.eq_dec y x); auto. + unfold smem_set; cbn; destruct (R.eq_dec y x); auto. subst; generalize (inst_smem_pre_monotonic _ _ _ _ VALID); clear VALID. - unfold smem_set; simpl. intuition congruence. + unfold smem_set; cbn. intuition congruence. Qed. Lemma block_smem_rec_abort p m0 x: forall d, @@ -169,7 +169,7 @@ Lemma block_smem_rec_abort p m0 x: forall d, term_eval ge (d x) m0 = None -> term_eval ge (bblock_smem_rec p d x) m0 = None. Proof. - induction p; simpl; auto. + induction p; cbn; auto. intros d VALID H; erewrite IHp; eauto. clear IHp. eapply inst_smem_abort; eauto. Qed. @@ -181,13 +181,13 @@ Lemma inst_smem_Some_correct1 i m0 old (od:smem): (forall x, term_eval ge (d x) m0 = Some (m1 x)) -> forall x, term_eval ge (inst_smem i d od x) m0 = Some (m2 x). Proof. - intro X; induction i as [|[x e] i IHi]; simpl; intros m1 m2 d H. + intro X; induction i as [|[x e] i IHi]; cbn; intros m1 m2 d H. - inversion_clear H; eauto. - intros H0 x0. destruct (exp_eval ge e m1 old) eqn:Heqov; try congruence. refine (IHi _ _ _ _ _ _); eauto. clear x0; intros x0. - unfold assign, smem_set; simpl. destruct (R.eq_dec x x0); auto. + unfold assign, smem_set; cbn. destruct (R.eq_dec x x0); auto. subst; erewrite term_eval_exp; eauto. Qed. @@ -197,7 +197,7 @@ Lemma bblocks_smem_rec_Some_correct1 p m0: forall (m1 m2: mem) (d: smem), forall x, term_eval ge (bblock_smem_rec p d x) m0 = Some (m2 x). Proof. Local Hint Resolve inst_smem_Some_correct1: core. - induction p as [ | i p]; simpl; intros m1 m2 d H. + induction p as [ | i p]; cbn; intros m1 m2 d H. - inversion_clear H; eauto. - intros H0 x0. destruct (inst_run ge i m1 m1) eqn: Heqov. @@ -218,15 +218,15 @@ Lemma inst_smem_None_correct i m0 old (od: smem): (forall x, term_eval ge (d x) m0 = Some (m1 x)) -> inst_run ge i m1 old = None -> exists x, term_eval ge (inst_smem i d od x) m0 = None. Proof. - intro X; induction i as [|[x e] i IHi]; simpl; intros m1 d. + intro X; induction i as [|[x e] i IHi]; cbn; intros m1 d. - discriminate. - intros VALID H0. destruct (exp_eval ge e m1 old) eqn: Heqov. + refine (IHi _ _ _ _); eauto. - intros x0; unfold assign, smem_set; simpl. destruct (R.eq_dec x x0); auto. + intros x0; unfold assign, smem_set; cbn. destruct (R.eq_dec x x0); auto. subst; erewrite term_eval_exp; eauto. + intuition. - constructor 1 with (x:=x); simpl. + constructor 1 with (x:=x); cbn. apply inst_smem_abort; auto. rewrite set_spec_eq. erewrite term_eval_exp; eauto. @@ -241,14 +241,14 @@ Lemma inst_smem_Some_correct2 i m0 old (od: smem): res_eq (Some m2) (inst_run ge i m1 old). Proof. intro X. - induction i as [|[x e] i IHi]; simpl; intros m1 m2 d VALID H0. + induction i as [|[x e] i IHi]; cbn; intros m1 m2 d VALID H0. - intros H; eapply ex_intro; intuition eauto. generalize (H0 x); rewrite H. congruence. - intros H. destruct (exp_eval ge e m1 old) eqn: Heqov. + refine (IHi _ _ _ _ _ _); eauto. - intros x0; unfold assign, smem_set; simpl; destruct (R.eq_dec x x0); auto. + intros x0; unfold assign, smem_set; cbn; destruct (R.eq_dec x x0); auto. subst; erewrite term_eval_exp; eauto. + generalize (H x). rewrite inst_smem_abort; discriminate || auto. @@ -262,7 +262,7 @@ Lemma bblocks_smem_rec_Some_correct2 p m0: forall (m1 m2: mem) d, (forall x, term_eval ge (bblock_smem_rec p d x) m0 = Some (m2 x)) -> res_eq (Some m2) (run ge p m1). Proof. - induction p as [|i p]; simpl; intros m1 m2 d VALID H0. + induction p as [|i p]; cbn; intros m1 m2 d VALID H0. - intros H; eapply ex_intro; intuition eauto. generalize (H0 x); rewrite H. congruence. @@ -293,13 +293,13 @@ Lemma inst_valid i m0 old (od:smem): (forall x, term_eval ge (d x) m0 = Some (m1 x)) -> pre (inst_smem i d od) ge m0. Proof. - induction i as [|[x e] i IHi]; simpl; auto. + induction i as [|[x e] i IHi]; cbn; auto. intros Hold m1 m2 d VALID0 H Hm1. - destruct (exp_eval ge e m1 old) eqn: Heq; simpl; try congruence. + destruct (exp_eval ge e m1 old) eqn: Heq; cbn; try congruence. eapply IHi; eauto. - + unfold smem_set in * |- *; simpl. + + unfold smem_set in * |- *; cbn. rewrite Hm1; intuition congruence. - + intros x0. unfold assign, smem_set; simpl; destruct (R.eq_dec x x0); auto. + + intros x0. unfold assign, smem_set; cbn; destruct (R.eq_dec x x0); auto. subst; erewrite term_eval_exp; eauto. Qed. @@ -311,7 +311,7 @@ Lemma block_smem_rec_valid p m0: forall (m1 m2: mem) (d:smem), pre (bblock_smem_rec p d) ge m0. Proof. Local Hint Resolve inst_valid: core. - induction p as [ | i p]; simpl; intros m1 d H; auto. + induction p as [ | i p]; cbn; intros m1 d H; auto. intros H0 H1. destruct (inst_run ge i m1 m1) eqn: Heqov; eauto. congruence. @@ -322,7 +322,7 @@ Lemma bblock_smem_valid p m0 m1: pre (bblock_smem p) ge m0. Proof. intros; eapply block_smem_rec_valid; eauto. - unfold smem_empty; simpl. auto. + unfold smem_empty; cbn. auto. Qed. Definition smem_valid ge d m := pre d ge m /\ forall x, term_eval ge (d x) m <> None. @@ -339,7 +339,7 @@ Theorem bblock_smem_simu p1 p2: Proof. Local Hint Resolve bblock_smem_valid bblock_smem_Some_correct1: core. intros (INCL & EQUIV) m DONTFAIL; unfold smem_valid in * |-. - destruct (run ge p1 m) as [m1|] eqn: RUN1; simpl; try congruence. + destruct (run ge p1 m) as [m1|] eqn: RUN1; cbn; try congruence. assert (X: forall x, term_eval ge (bblock_smem p1 x) m = Some (m1 x)); eauto. eapply bblock_smem_Some_correct2; eauto. + destruct (INCL m); intuition eauto. @@ -371,7 +371,7 @@ Lemma smem_valid_set_proof d x t m: Proof. unfold smem_valid; intros (PRE & VALID) PREt. split. + split; auto. - + intros x0; unfold smem_set; simpl; case (R.eq_dec x x0); intros; subst; auto. + + intros x0; unfold smem_set; cbn; case (R.eq_dec x x0); intros; subst; auto. Qed. @@ -384,7 +384,7 @@ Definition smem_correct ge (d: smem) (m: mem) (om: option mem): Prop:= Lemma bblock_smem_correct ge p m: smem_correct ge (bblock_smem p) m (run ge p m). Proof. - unfold smem_correct; simpl; intros m'; split. + unfold smem_correct; cbn; intros m'; split. + intros; split. * eapply bblock_smem_valid; eauto. * eapply bblock_smem_Some_correct1; eauto. -- cgit