diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-12 11:06:32 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-12 11:06:32 +0200 |
| commit | 7e921e5ac243b453e6ec856abd5af2eed810226d (patch) | |
| tree | 1f09a81f55074984a756d39a23cf5db82ead2150 | |
| parent | 552147109492793cd811d37c3c7e310090bb5476 (diff) | |
| download | compcert-kvx-7e921e5ac243b453e6ec856abd5af2eed810226d.tar.gz compcert-kvx-7e921e5ac243b453e6ec856abd5af2eed810226d.zip | |
more simplifications
| -rw-r--r-- | mppa_k1c/SelectOp.vp | 2 | ||||
| -rw-r--r-- | mppa_k1c/SelectOpproof.v | 4 |
2 files changed, 6 insertions, 0 deletions
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp index 71e0eff3..c5a86ac1 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -353,6 +353,8 @@ Nondetfunction notint (e: expr) := | Eop (Oorimm n) (e1:::Enil) => Eop (Onorimm n) (e1:::Enil) | Eop Oxor (e1:::e2:::Enil) => Eop Onxor (e1:::e2:::Enil) | Eop (Oxorimm n) (e1:::Enil) => Eop (Onxorimm n) (e1:::Enil) + | Eop Onot (e1:::Enil) => e1 + | Eop (Ointconst k) Enil => Eop (Ointconst (Int.not k)) Enil | _ => Eop Onot (e:::Enil) end. diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v index 4af5ccfa..65038038 100644 --- a/mppa_k1c/SelectOpproof.v +++ b/mppa_k1c/SelectOpproof.v @@ -679,6 +679,10 @@ Proof. - TrivialExists; simpl; congruence. - TrivialExists; simpl; congruence. - TrivialExists; simpl; congruence. + - rewrite <- H0. + exists v1. + split; auto. + - TrivialExists. - TrivialExists. Qed. |