summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--lib/Integers.v28
1 files changed, 19 insertions, 9 deletions
diff --git a/lib/Integers.v b/lib/Integers.v
index 4464d26..a3ff520 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -421,7 +421,7 @@ Qed.
Remark half_modulus_modulus: modulus = 2 * half_modulus.
Proof.
rewrite half_modulus_power. rewrite modulus_power.
- rewrite <- two_p_S. decEq. omega.
+ rewrite <- two_p_S. apply f_equal. omega.
generalize wordsize_pos; omega.
Qed.
@@ -1016,8 +1016,6 @@ Proof.
rewrite unsigned_zero. apply Zmod_unique with 0. omega. omega.
Qed.
-
-
(** ** Properties of multiplication *)
Theorem mul_commut: forall x y, mul x y = mul y x.
@@ -2057,7 +2055,7 @@ Qed.
Lemma ltu_iwordsize_inv:
forall x, ltu x iwordsize = true -> 0 <= unsigned x < zwordsize.
Proof.
- intros. exploit ltu_inv; eauto. rewrite unsigned_repr_wordsize. auto.
+ intros. generalize (ltu_inv _ _ H). rewrite unsigned_repr_wordsize. auto.
Qed.
Theorem shl_shl:
@@ -2331,7 +2329,7 @@ Theorem shl_rolm:
ltu n iwordsize = true ->
shl x n = rolm x n (shl mone n).
Proof.
- intros. exploit ltu_inv; eauto. rewrite unsigned_repr_wordsize; intros.
+ intros. generalize (ltu_inv _ _ H). rewrite unsigned_repr_wordsize; intros.
unfold rolm. apply same_bits_eq; intros.
rewrite bits_and; auto. rewrite !bits_shl; auto. rewrite bits_rol; auto.
destruct (zlt i (unsigned n)).
@@ -2347,7 +2345,7 @@ Theorem shru_rolm:
ltu n iwordsize = true ->
shru x n = rolm x (sub iwordsize n) (shru mone n).
Proof.
- intros. exploit ltu_inv; eauto. rewrite unsigned_repr_wordsize; intros.
+ intros. generalize (ltu_inv _ _ H). rewrite unsigned_repr_wordsize; intros.
unfold rolm. apply same_bits_eq; intros.
rewrite bits_and; auto. rewrite !bits_shru; auto. rewrite bits_rol; auto.
destruct (zlt (i + unsigned n) zwordsize).
@@ -2852,7 +2850,7 @@ Proof.
intros.
set (uy := unsigned y).
assert (0 <= uy < zwordsize - 1).
- exploit ltu_inv; eauto. rewrite unsigned_repr. auto.
+ generalize (ltu_inv _ _ H). rewrite unsigned_repr. auto.
generalize wordsize_pos wordsize_max_unsigned; omega.
rewrite shr_div_two_p. unfold shrx. unfold divs.
assert (shl one y = repr (two_p uy)).
@@ -2896,7 +2894,7 @@ Proof.
- set (uy := unsigned y).
generalize (unsigned_range y); fold uy; intros.
assert (0 <= uy < zwordsize - 1).
- exploit ltu_inv; eauto. rewrite unsigned_repr. auto.
+ generalize (ltu_inv _ _ H). rewrite unsigned_repr. auto.
generalize wordsize_pos wordsize_max_unsigned; omega.
assert (two_p uy < modulus).
rewrite modulus_power. apply two_p_monotone_strict. omega.
@@ -2937,7 +2935,7 @@ Proof.
2: rewrite add_zero; auto.
set (uy := unsigned y).
assert (0 <= uy < zwordsize - 1).
- exploit ltu_inv; eauto. rewrite unsigned_repr. auto.
+ generalize (ltu_inv _ _ H). rewrite unsigned_repr. auto.
generalize wordsize_pos wordsize_max_unsigned; omega.
assert (shl one y = repr (two_p uy)).
rewrite shl_mul_two_p. rewrite mul_commut. apply mul_one.
@@ -3828,8 +3826,12 @@ Module Wordsize_32.
Proof. unfold wordsize; congruence. Qed.
End Wordsize_32.
+Strategy opaque [Wordsize_32.wordsize].
+
Module Int := Make(Wordsize_32).
+Strategy 0 [Wordsize_32.wordsize].
+
Notation int := Int.int.
Remark int_wordsize_divides_modulus:
@@ -3844,8 +3846,12 @@ Module Wordsize_8.
Proof. unfold wordsize; congruence. Qed.
End Wordsize_8.
+Strategy opaque [Wordsize_8.wordsize].
+
Module Byte := Make(Wordsize_8).
+Strategy 0 [Wordsize_8.wordsize].
+
Notation byte := Byte.int.
Module Wordsize_64.
@@ -3854,6 +3860,8 @@ Module Wordsize_64.
Proof. unfold wordsize; congruence. Qed.
End Wordsize_64.
+Strategy opaque [Wordsize_64.wordsize].
+
Module Int64.
Include Make(Wordsize_64).
@@ -4423,6 +4431,8 @@ Qed.
End Int64.
+Strategy 0 [Wordsize_64.wordsize].
+
Notation int64 := Int64.int.
Global Opaque Int.repr Int64.repr Byte.repr.