diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-12 12:38:48 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-12 12:38:48 +0200 |
| commit | af3bf7d993ebccd93577bc0986a6ab45729fdc1d (patch) | |
| tree | 798e66dd365b6b08a3da4fb5cae01039efca3f66 | |
| parent | 56249c0fa5aa96767ce3fd9be76b8a9e7bef0231 (diff) | |
| download | compcert-kvx-af3bf7d993ebccd93577bc0986a6ab45729fdc1d.tar.gz compcert-kvx-af3bf7d993ebccd93577bc0986a6ab45729fdc1d.zip | |
some more simplification
| -rw-r--r-- | mppa_k1c/SelectOp.vp | 1 | ||||
| -rw-r--r-- | mppa_k1c/SelectOpproof.v | 6 |
2 files changed, 7 insertions, 0 deletions
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp index 019de37d..da0049fe 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -365,6 +365,7 @@ Nondetfunction notint (e: expr) := | Eop Onxor (e1:::e2:::Enil) => Eop Oxor (e1:::e2:::Enil) | Eop (Onxorimm n) (e1:::Enil) => Eop (Oxorimm n) (e1:::Enil) | Eop Oandn (e1:::e2:::Enil) => Eop Oorn (e2:::e1:::Enil) + | Eop Oorn (e1:::e2:::Enil) => Eop Oandn (e2:::e1:::Enil) | Eop Onot (e1:::Enil) => e1 | Eop (Ointconst k) Enil => Eop (Ointconst (Int.not k)) Enil | _ => Eop Onot (e:::Enil) diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v index 76cfdafe..49980c51 100644 --- a/mppa_k1c/SelectOpproof.v +++ b/mppa_k1c/SelectOpproof.v @@ -704,6 +704,12 @@ Proof. rewrite Int.not_and_or_not. rewrite Int.not_involutive. apply Int.or_commut. + - subst x. TrivialExists. simpl. + destruct v0; destruct v1; simpl; trivial. + f_equal. f_equal. + rewrite Int.not_or_and_not. + rewrite Int.not_involutive. + apply Int.and_commut. - subst x. exists v1; split; trivial. - TrivialExists. - TrivialExists. |