diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-16 19:47:03 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-16 19:47:03 +0100 |
| commit | 7ab24b18b1c9a08b0d092c2c8144ee7b3a029c1d (patch) | |
| tree | 626ffb1662cdb76fcf2979291c7adda9bacbe63f /mppa_k1c/SelectLongproof.v | |
| parent | 2227019e15866870f87488630f17cbb0797d1786 (diff) | |
| download | compcert-kvx-7ab24b18b1c9a08b0d092c2c8144ee7b3a029c1d.tar.gz compcert-kvx-7ab24b18b1c9a08b0d092c2c8144ee7b3a029c1d.zip | |
long nand, nor, nxor
Diffstat (limited to 'mppa_k1c/SelectLongproof.v')
| -rw-r--r-- | mppa_k1c/SelectLongproof.v | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v index 44846a6f..a8a6bc9c 100644 --- a/mppa_k1c/SelectLongproof.v +++ b/mppa_k1c/SelectLongproof.v @@ -441,8 +441,16 @@ Qed. Theorem eval_notl: unary_constructor_sound notl Val.notl. Proof. - unfold notl; destruct Archi.splitlong. apply SplitLongproof.eval_notl. - red; intros. rewrite Val.notl_xorl. apply eval_xorlimm; auto. + assert (forall v, Val.lessdef (Val.notl (Val.notl v)) v). + destruct v; simpl; auto. rewrite Int64.not_involutive; auto. + unfold notl; red; intros until x; case (notl_match a); intros; InvEval. + - TrivialExists; simpl; congruence. + - TrivialExists; simpl; congruence. + - TrivialExists; simpl; congruence. + - TrivialExists; simpl; congruence. + - TrivialExists; simpl; congruence. + - TrivialExists; simpl; congruence. + - apply eval_xorlimm; assumption. Qed. Theorem eval_divls_base: partial_binary_constructor_sound divls_base Val.divls. |