diff options
| -rw-r--r-- | lib/Integers.v | 28 |
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. |