Move Z definitions out of Integers and into Zbits

The module Integers.Make contained lots of definitions and theorems
about Z integers that were independent of the word size.  These
definitions and theorems are useful outside Integers.Make, but
it felt unnatural to fetch them from modules Int or Int64.

This commit moves the word-size-independent definitions and theorems
to a new module, lib/Zbits.v, and fixes their uses in the code base.

3 files changed, 21 insertions, 20 deletions

diff --git a/backend/NeedDomain.v b/backend/NeedDomain.v
index 692b4f9b..5d19e8f6 100644
--- a/backend/NeedDomain.v
+++ b/backend/NeedDomain.v
@@ -16,6 +16,7 @@ Require Import Coqlib.
 Require Import Maps.
 Require Import IntvSets.
 Require Import AST.
+Require Import Zbits.
 Require Import Integers.
 Require Import Floats.
 Require Import Values.
@@ -300,13 +301,13 @@ Proof.
   rewrite Int.bits_ror.
   replace (((i - Int.unsigned amount) mod Int.zwordsize + Int.unsigned amount)
    mod Int.zwordsize) with i. auto.
-  apply Int.eqmod_small_eq with Int.zwordsize; auto.
-  apply Int.eqmod_trans with ((i - Int.unsigned amount) + Int.unsigned amount).
-  apply Int.eqmod_refl2; omega.
-  eapply Int.eqmod_trans. 2: apply Int.eqmod_mod; auto.
-  apply Int.eqmod_add.
-  apply Int.eqmod_mod; auto.
-  apply Int.eqmod_refl.
+  apply eqmod_small_eq with Int.zwordsize; auto.
+  apply eqmod_trans with ((i - Int.unsigned amount) + Int.unsigned amount).
+  apply eqmod_refl2; omega.
+  eapply eqmod_trans. 2: apply eqmod_mod; auto.
+  apply eqmod_add.
+  apply eqmod_mod; auto.
+  apply eqmod_refl.
   apply Z_mod_lt; auto.
   apply Z_mod_lt; auto.
 Qed.
@@ -324,7 +325,7 @@ Qed.
 
 Lemma eqmod_iagree:
   forall m x y,
-  Int.eqmod (two_p (Int.size m)) x y ->
+  eqmod (two_p (Int.size m)) x y ->
   iagree (Int.repr x) (Int.repr y) m.
 Proof.
   intros. set (p := Z.to_nat (Int.size m)).
@@ -333,7 +334,7 @@ Proof.
   rewrite EQ in H; rewrite <- two_power_nat_two_p in H.
   red; intros. rewrite ! Int.testbit_repr by auto.
   destruct (zlt i (Int.size m)).
-  eapply Int.same_bits_eqmod; eauto. omega.
+  eapply same_bits_eqmod; eauto. omega.
   assert (Int.testbit m i = false) by (eapply Int.bits_size_2; omega).
   congruence.
 Qed.
@@ -343,13 +344,13 @@ Definition complete_mask (m: int) := Int.zero_ext (Int.size m) Int.mone.
 Lemma iagree_eqmod:
   forall x y m,
   iagree x y (complete_mask m) ->
-  Int.eqmod (two_p (Int.size m)) (Int.unsigned x) (Int.unsigned y).
+  eqmod (two_p (Int.size m)) (Int.unsigned x) (Int.unsigned y).
 Proof.
   intros. set (p := Z.to_nat (Int.size m)).
   generalize (Int.size_range m); intros RANGE.
   assert (EQ: Int.size m = Z.of_nat p). { symmetry; apply Z2Nat.id. omega. }
   rewrite EQ; rewrite <- two_power_nat_two_p.
-  apply Int.eqmod_same_bits. intros. apply H. omega.
+  apply eqmod_same_bits. intros. apply H. omega.
   unfold complete_mask. rewrite Int.bits_zero_ext by omega.
   rewrite zlt_true by omega. rewrite Int.bits_mone by omega. auto.
 Qed.
@@ -362,7 +363,7 @@ Proof.
 + assert (Int.unsigned m <> 0).
   { red; intros; elim n. rewrite <- (Int.repr_unsigned m). rewrite H; auto. }
   assert (0 < Int.size m).
-  { apply Int.Zsize_pos'. generalize (Int.unsigned_range m); omega. }
+  { apply Zsize_pos'. generalize (Int.unsigned_range m); omega. }
   generalize (Int.size_range m); intros.
   f_equal. apply Int.bits_size_4. tauto.
   rewrite Int.bits_zero_ext by omega. rewrite zlt_true by omega.
@@ -610,7 +611,7 @@ Proof.
   unfold modarith; intros. destruct x; simpl in *.
 - auto.
 - unfold Val.add; InvAgree.
-  apply eqmod_iagree. apply Int.eqmod_add; apply iagree_eqmod; auto.
+  apply eqmod_iagree. apply eqmod_add; apply iagree_eqmod; auto.
 - inv H; auto. inv H0; auto. destruct w1; auto.
 Qed.
 
@@ -626,7 +627,7 @@ Lemma mul_sound:
 Proof.
   unfold mul, add; intros. destruct x; simpl in *.
 - auto.
-- unfold Val.mul; InvAgree. apply eqmod_iagree. apply Int.eqmod_mult; apply iagree_eqmod; auto.
+- unfold Val.mul; InvAgree. apply eqmod_iagree. apply eqmod_mult; apply iagree_eqmod; auto.
 - inv H; auto. inv H0; auto. destruct w1; auto.
 Qed.
 
@@ -638,7 +639,7 @@ Proof.
   intros; destruct x; simpl in *.
 - auto.
 - unfold Val.neg; InvAgree.
-  apply eqmod_iagree. apply Int.eqmod_neg. apply iagree_eqmod; auto.
+  apply eqmod_iagree. apply eqmod_neg. apply iagree_eqmod; auto.
 - inv H; simpl; auto.
 Qed.
 
diff --git a/backend/SelectDivproof.v b/backend/SelectDivproof.v
index e660677a..f4ff2c86 100644
--- a/backend/SelectDivproof.v
+++ b/backend/SelectDivproof.v
@@ -12,7 +12,7 @@
 
 (** Correctness of instruction selection for integer division *)
 
-Require Import Zquot Coqlib.
+Require Import Zquot Coqlib Zbits.
 Require Import AST Integers Floats Values Memory Globalenvs Events.
 Require Import Cminor Op CminorSel.
 Require Import SelectOp SelectOpproof SplitLong SplitLongproof SelectLong SelectLongproof SelectDiv.
@@ -378,7 +378,7 @@ Qed.
 Remark int64_shr'_div_two_p:
   forall x y, Int64.shr' x y = Int64.repr (Int64.signed x / two_p (Int.unsigned y)).
 Proof.
-  intros; unfold Int64.shr'. rewrite Int64.Zshiftr_div_two_p; auto. generalize (Int.unsigned_range y); omega.
+  intros; unfold Int64.shr'. rewrite Zshiftr_div_two_p; auto. generalize (Int.unsigned_range y); omega.
 Qed.
 
 Lemma divls_mul_shift_gen:
@@ -453,7 +453,7 @@ Qed.
 Remark int64_shru'_div_two_p:
   forall x y, Int64.shru' x y = Int64.repr (Int64.unsigned x / two_p (Int.unsigned y)).
 Proof.
-  intros; unfold Int64.shru'. rewrite Int64.Zshiftr_div_two_p; auto. generalize (Int.unsigned_range y); omega.
+  intros; unfold Int64.shru'. rewrite Zshiftr_div_two_p; auto. generalize (Int.unsigned_range y); omega.
 Qed.
 
 Theorem divlu_mul_shift:
diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v
index 47b87bfb..3ba2a35b 100644
--- a/backend/ValueDomain.v
+++ b/backend/ValueDomain.v
@@ -11,7 +11,7 @@
 (* *********************************************************************)
 
 Require Import FunInd.
-Require Import Zwf Coqlib Maps Integers Floats Lattice.
+Require Import Zwf Coqlib Maps Zbits Integers Floats Lattice.
 Require Import Compopts AST.
 Require Import Values Memory Globalenvs Events.
 Require Import Registers RTL.
@@ -1670,7 +1670,7 @@ Proof.
   assert (UNS: forall i j, j <> Int.zero -> is_uns (usize j) (Int.modu i j)).
   {
     intros. apply is_uns_mon with (usize (Int.modu i j)); auto with va.
-    unfold usize, Int.size. apply Int.Zsize_monotone.
+    unfold usize, Int.size. apply Zsize_monotone.
     generalize (Int.unsigned_range_2 j); intros RANGE.
     assert (Int.unsigned j <> 0).
     { red; intros; elim H. rewrite <- (Int.repr_unsigned j). rewrite H0. auto. }