diff options
Diffstat (limited to 'kvx/ValueAOp.v')
-rw-r--r-- | kvx/ValueAOp.v | 28 |
1 files changed, 14 insertions, 14 deletions
diff --git a/kvx/ValueAOp.v b/kvx/ValueAOp.v index 0206352e..87554258 100644 --- a/kvx/ValueAOp.v +++ b/kvx/ValueAOp.v @@ -349,7 +349,7 @@ Proof. intros v x; intro MATCH; inversion MATCH; - simpl; + cbn; constructor. Qed. @@ -361,9 +361,9 @@ Lemma triple_op_float_sound: Proof. intros until z. intros Hax Hby Hcz. - inv Hax; simpl; try constructor; - inv Hby; simpl; try constructor; - inv Hcz; simpl; try constructor. + inv Hax; cbn; try constructor; + inv Hby; cbn; try constructor; + inv Hcz; cbn; try constructor. Qed. Lemma triple_op_single_sound: @@ -374,9 +374,9 @@ Lemma triple_op_single_sound: Proof. intros until z. intros Hax Hby Hcz. - inv Hax; simpl; try constructor; - inv Hby; simpl; try constructor; - inv Hcz; simpl; try constructor. + inv Hax; cbn; try constructor; + inv Hby; cbn; try constructor; + inv Hcz; cbn; try constructor. Qed. Lemma fmaddf_sound : @@ -420,9 +420,9 @@ Proof. intros until aargs; intros VM. inv VM. destruct cond; auto with va. inv H0. - destruct cond; simpl; eauto with va. + destruct cond; cbn; eauto with va. inv H2. - destruct cond; simpl; eauto with va. + destruct cond; cbn; eauto with va. destruct cond; auto with va. Qed. @@ -432,7 +432,7 @@ Theorem eval_static_condition0_sound: cmatch (eval_condition0 cond varg m) (eval_static_condition0 cond aarg). Proof. intros until aarg; intro VM. - destruct cond; simpl; eauto with va. + destruct cond; cbn; eauto with va. Qed. Lemma symbol_address_sound: @@ -541,8 +541,8 @@ Proof. + eauto with va. + destruct n; destruct shift; reflexivity. - (* shrx *) - inv H1; simpl; try constructor. - all: destruct Int.ltu; [simpl | constructor; fail]. + inv H1; cbn; try constructor. + all: destruct Int.ltu; [cbn | constructor; fail]. all: auto with va. - inv H1; constructor. - replace (match Val.shll a1 (Vint (int_of_shift1_4 shift)) with @@ -580,12 +580,12 @@ Proof. (* insf *) - unfold insf, eval_static_insf. destruct (is_bitfield _ _). - + inv H1; inv H0; simpl; try constructor; destruct (Int.ltu _ _); simpl; constructor. + + inv H1; inv H0; cbn; try constructor; destruct (Int.ltu _ _); cbn; constructor. + constructor. (* insfl *) - unfold insfl, eval_static_insfl. destruct (is_bitfieldl _ _). - + inv H1; inv H0; simpl; try constructor; destruct (Int.ltu _ _); simpl; constructor. + + inv H1; inv H0; cbn; try constructor; destruct (Int.ltu _ _); cbn; constructor. + constructor. (* select *) - apply select_sound; auto. eapply eval_static_condition0_sound; eauto. |