diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-06-04 23:16:35 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-06-04 23:16:35 +0200 |
| commit | b5352b040da8c38b371316d67c2180dbab758295 (patch) | |
| tree | d90352b59294c4521300435542d76d5b95f148ca /mppa_k1c/SelectOpproof.v | |
| parent | 68a6d0dd0ea5774529d823fb9a9ca981c1ecebb0 (diff) | |
| download | compcert-kvx-b5352b040da8c38b371316d67c2180dbab758295.tar.gz compcert-kvx-b5352b040da8c38b371316d67c2180dbab758295.zip | |
move with immediates
Diffstat (limited to 'mppa_k1c/SelectOpproof.v')
| -rw-r--r-- | mppa_k1c/SelectOpproof.v | 28 |
1 files changed, 27 insertions, 1 deletions
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v index 39ad763e..21a06857 100644 --- a/mppa_k1c/SelectOpproof.v +++ b/mppa_k1c/SelectOpproof.v @@ -1441,6 +1441,31 @@ Proof. Qed. *) +Lemma eval_neg_condition0: + forall cond0: condition0, + forall v1: val, + forall m: mem, + (eval_condition0 (negate_condition0 cond0) v1 m) = + option_map negb (eval_condition0 cond0 v1 m). +Proof. + intros. + destruct cond0; simpl; + try rewrite Val.negate_cmp_bool; + try rewrite Val.negate_cmpu_bool; + try rewrite Val.negate_cmpl_bool; + try rewrite Val.negate_cmplu_bool; + reflexivity. +Qed. + +Lemma select_neg: + forall a b c, + Val.select (option_map negb a) b c = + Val.select a c b. +Proof. + destruct a; simpl; trivial. + destruct b; simpl; trivial. +Qed. + Lemma eval_select0: forall le ty cond0 ac vc a1 v1 a2 v2, eval_expr ge sp e m le ac vc -> @@ -1454,7 +1479,8 @@ Proof. unfold select0. destruct (select0_match ty cond0 a1 a2 ac). all: InvEval; econstructor; split; - repeat (try econstructor; try eassumption). + try repeat (try econstructor; try eassumption). + all: rewrite eval_neg_condition0; rewrite select_neg; constructor. Qed. Lemma bool_cond0_ne: |