More properties on mul/div/mod

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1918 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 39 insertions, 0 deletions

diff --git a/lib/Integers.v b/lib/Integers.v
index 1e58c2d..0dc7997 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -910,6 +910,15 @@ Proof.
   apply repr_unsigned.
 Qed.
 
+Theorem mul_mone: forall x, mul x mone = neg x.
+Proof.
+  intros; unfold mul, neg. rewrite unsigned_mone. 
+  apply eqm_samerepr.
+  replace (-unsigned x) with (0 - unsigned x) by omega.
+  replace (unsigned x * (modulus - 1)) with (unsigned x * modulus - unsigned x) by ring.
+  apply eqm_sub. exists (unsigned x). omega. apply eqm_refl.
+Qed.
+
 Theorem mul_assoc: forall x y z, mul (mul x y) z = mul x (mul y z).
 Proof.
   intros; unfold mul.
@@ -1007,6 +1016,36 @@ Proof.
   apply eqm_mult. auto with ints. apply eqm_signed_unsigned.
 Qed.
 
+Theorem divu_one:
+  forall x, divu x one = x.
+Proof.
+  unfold divu; intros. rewrite unsigned_one. rewrite Zdiv_1_r. apply repr_unsigned.
+Qed.
+
+Theorem modu_one:
+  forall x, modu x one = zero.
+Proof.
+  intros. rewrite modu_divu. rewrite divu_one. rewrite mul_one. apply sub_idem.
+  apply one_not_zero.
+Qed.
+
+Theorem divs_mone:
+  forall x, divs x mone = neg x.
+Proof.
+  unfold divs, neg; intros. 
+  rewrite signed_mone. replace (Zdiv_round (signed x) (-1)) with (- (signed x)). 
+  apply eqm_samerepr. apply eqm_neg. apply eqm_signed_unsigned. 
+  unfold Zdiv_round. destruct (zlt (signed x) 0).
+  simpl. rewrite Zdiv_1_r. auto. simpl. rewrite Zdiv_1_r. auto. 
+Qed.
+
+Theorem mods_mone:
+  forall x, mods x mone = zero.
+Proof.
+  intros. rewrite mods_divs. rewrite divs_mone. 
+  rewrite <- neg_mul_distr_l. rewrite mul_mone. rewrite neg_involutive. apply sub_idem. 
+Qed.
+
 (** ** Properties of binary decompositions *)
 
 Lemma Z_shift_add_bin_decomp: