diff options
Diffstat (limited to 'mppa_k1c/SelectOpproof.v')
| -rw-r--r-- | mppa_k1c/SelectOpproof.v | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v index 26df4fc7..c81f6fb5 100644 --- a/mppa_k1c/SelectOpproof.v +++ b/mppa_k1c/SelectOpproof.v @@ -430,6 +430,7 @@ Proof. red; intros until y; unfold and; case (and_match a b); intros; InvEval. - rewrite Val.and_commut. apply eval_andimm; auto. - apply eval_andimm; auto. + - (*andn*) TrivialExists; simpl; congruence. - TrivialExists. Qed. @@ -493,6 +494,7 @@ Proof. destruct (same_expr_pure t1 t2) eqn:?; auto. InvEval. exploit eval_same_expr; eauto. intros [EQ1 EQ2]; subst. exists (Val.ror v1 (Vint n2)); split. EvalOp. rewrite Val.or_commut. apply ROR; auto. + - (*orn*) TrivialExists; simpl; congruence. - apply DEFAULT. Qed. @@ -526,14 +528,14 @@ Theorem eval_notint: unary_constructor_sound notint Val.notint. Proof. assert (forall v, Val.lessdef (Val.notint (Val.notint v)) v). destruct v; simpl; auto. rewrite Int.not_involutive; auto. - unfold notint; red; intros until x; case (notint_match a); intros; InvEval. - - TrivialExists; simpl; congruence. - - TrivialExists; simpl; congruence. - - TrivialExists; simpl; congruence. - - TrivialExists; simpl; congruence. - - TrivialExists; simpl; congruence. - - TrivialExists; simpl; congruence. - - TrivialExists. + unfold notint; red; intros until x; case (notint_match a); intros; InvEval. + - TrivialExists; simpl; congruence. + - TrivialExists; simpl; congruence. + - TrivialExists; simpl; congruence. + - TrivialExists; simpl; congruence. + - TrivialExists; simpl; congruence. + - TrivialExists; simpl; congruence. + - TrivialExists. Qed. Theorem eval_divs_base: |