diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-11 10:21:59 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-11 10:21:59 +0200 |
| commit | 3ef3e6c78026cc1d5793ccb4e905a0232ec7bb4e (patch) | |
| tree | 2c4e87342b978883fb471559ca0c18e5f7a3cc00 /mppa_k1c/ExtValues.v | |
| parent | ae22df3c5ef0a60527ea85b83bb71e8c95a6ab9c (diff) | |
| download | compcert-kvx-3ef3e6c78026cc1d5793ccb4e905a0232ec7bb4e.tar.gz compcert-kvx-3ef3e6c78026cc1d5793ccb4e905a0232ec7bb4e.zip | |
generate multiply-sub long
Diffstat (limited to 'mppa_k1c/ExtValues.v')
| -rw-r--r-- | mppa_k1c/ExtValues.v | 33 |
1 files changed, 32 insertions, 1 deletions
diff --git a/mppa_k1c/ExtValues.v b/mppa_k1c/ExtValues.v index 0d56fd1c..735d5c3c 100644 --- a/mppa_k1c/ExtValues.v +++ b/mppa_k1c/ExtValues.v @@ -146,4 +146,35 @@ Proof. destruct x; destruct y; simpl; trivial. f_equal. apply Int.neg_mul_distr_r. -Qed.
\ No newline at end of file +Qed. + +(* pointer diff +Lemma sub_addl_negl : + forall x y, Val.subl x y = Val.addl x (Val.negl y). +Proof. + destruct x; destruct y; simpl; trivial. + + f_equal. apply Int64.sub_add_opp. + + destruct (Archi.ptr64) eqn:ARCHI64; trivial. + f_equal. rewrite Ptrofs.sub_add_opp. + pose (Ptrofs.agree64_neg ARCHI64 (Ptrofs.of_int64 i0) i0) as Hagree. + unfold Ptrofs.agree64 in Hagree. + unfold Ptrofs.add. + f_equal. f_equal. + rewrite Hagree. + pose (Ptrofs.agree64_of_int ARCHI64 (Int64.neg i0)) as Hagree2. + rewrite Hagree2. + reflexivity. + exact (Ptrofs.agree64_of_int ARCHI64 i0). + + destruct (Archi.ptr64) eqn:ARCHI64; simpl; trivial. + destruct (eq_block _ _); simpl; trivial. +Qed. + *) + +Lemma negl_mull_distr_r : + forall x y, Val.negl (Val.mull x y) = Val.mull x (Val.negl y). +Proof. + destruct x; destruct y; simpl; trivial. + f_equal. + apply Int64.neg_mul_distr_r. +Qed. + |