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.

1 files changed, 16 insertions, 15 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.