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/Asmvliw.v | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'kvx/Asmvliw.v') diff --git a/kvx/Asmvliw.v b/kvx/Asmvliw.v index 296963a7..66b468d7 100644 --- a/kvx/Asmvliw.v +++ b/kvx/Asmvliw.v @@ -849,7 +849,7 @@ Lemma Val_cmpu_correct (m:mem) (cmp: comparison) (v1 v2: val): Proof. unfold Val.cmpu, Val_cmpu. remember (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) as ob. - destruct ob; simpl. + destruct ob; cbn. - erewrite Val_cmpu_bool_correct; eauto. econstructor. - econstructor. @@ -873,9 +873,9 @@ Lemma Val_cmplu_correct (m:mem) (cmp: comparison) (v1 v2: val): Proof. unfold Val.cmplu, Val_cmplu. remember (Val.cmplu_bool (Mem.valid_pointer m) cmp v1 v2) as ob. - destruct ob as [b|]; simpl. + destruct ob as [b|]; cbn. - erewrite Val_cmplu_bool_correct; eauto. - simpl. econstructor. + cbn. econstructor. - econstructor. Qed. @@ -1426,13 +1426,13 @@ Definition is_label (lbl: label) (bb: bblock) : bool := Lemma is_label_correct_true lbl bb: List.In lbl (header bb) <-> is_label lbl bb = true. Proof. - unfold is_label; destruct (in_dec lbl (header bb)); simpl; intuition. + unfold is_label; destruct (in_dec lbl (header bb)); cbn; intuition. Qed. Lemma is_label_correct_false lbl bb: ~(List.In lbl (header bb)) <-> is_label lbl bb = false. Proof. - unfold is_label; destruct (in_dec lbl (header bb)); simpl; intuition. + unfold is_label; destruct (in_dec lbl (header bb)); cbn; intuition. Qed. @@ -1667,7 +1667,7 @@ Proof. constructor 1. - rewrite app_nil_r; auto. - unfold parexec_wio_bblock. - destruct (parexec_wio f _ _ _); simpl; auto. + destruct (parexec_wio f _ _ _); cbn; auto. Qed. @@ -1739,7 +1739,7 @@ Ltac Det_WIO X := exploit det_parexec_write_in_order; [ eapply H | idtac]; clear H; intro X | _ => idtac end. - intros; constructor; simpl. + intros; constructor; cbn. - (* determ *) intros s t1 s1 t2 s2 H H0. inv H; Det_WIO X1; inv H0; Det_WIO X2; Equalities. + split. constructor. auto. @@ -1754,7 +1754,7 @@ Ltac Det_WIO X := exploit external_call_determ. eexact H3. eexact H8. intros [A B]. split. auto. intros. destruct B; auto. subst. auto. - (* trace length *) - red; intros. inv H; simpl. + red; intros. inv H; cbn. omega. eapply external_call_trace_length; eauto. eapply external_call_trace_length; eauto. -- cgit