Commit 2e202e2b authored by Xavier Leroy's avatar Xavier Leroy
Browse files

Remove useless parameters in theorems int_round_odd_bits and int_round_odd_le

IEEE754_extra: clear unused context so that none of the context is
picked up by tactics and ends as extra parameters to theorems
int_round_odd_bits and int_round_odd_le

Floats: simplify uses of int_round_odd_bits and int_round_odd_le
accordingly.
parent d4513f41
......@@ -894,7 +894,7 @@ Proof.
}
assert (EQ: Int64.signed n * 2 = int_round_odd (Int64.unsigned x) 1).
{
symmetry. apply (int_round_odd_bits 53 1024). omega.
symmetry. apply int_round_odd_bits. omega.
intros. rewrite NB2 by omega. replace i with 0 by omega. auto.
rewrite NB2 by omega. rewrite dec_eq_false by omega. rewrite dec_eq_true.
rewrite orb_comm. unfold Int64.testbit. change (2^1) with 2.
......@@ -915,7 +915,7 @@ Proof.
compute_this Int64.min_signed; compute_this Int64.max_signed;
compute_this Int64.modulus; xomega.
- assert (2^63 <= int_round_odd (Int64.unsigned x) 1).
{ change (2^63) with (int_round_odd (2^63) 1). apply (int_round_odd_le 0 0); omega. }
{ change (2^63) with (int_round_odd (2^63) 1). apply int_round_odd_le; omega. }
rewrite <- EQ in H1. compute_this (2^63). compute_this (2^53). xomega.
- omega.
Qed.
......@@ -1321,9 +1321,9 @@ Lemma of_long_round_odd:
Proof.
intros. rewrite <- (int_round_odd_plus 11) by omega.
assert (-2^64 <= int_round_odd n 11).
{ change (-2^64) with (int_round_odd (-2^64) 11). apply (int_round_odd_le 0 0); xomega. }
{ change (-2^64) with (int_round_odd (-2^64) 11). apply int_round_odd_le; xomega. }
assert (int_round_odd n 11 <= 2^64).
{ change (2^64) with (int_round_odd (2^64) 11). apply (int_round_odd_le 0 0); xomega. }
{ change (2^64) with (int_round_odd (2^64) 11). apply int_round_odd_le; xomega. }
rewrite Bconv_BofZ.
apply BofZ_round_odd with (p := 11).
omega.
......@@ -1363,10 +1363,10 @@ Proof.
set (n' := Z.land (Z.lor (Int64.unsigned n) (Z.land (Int64.unsigned n) 2047 + 2047)) (-2048)).
assert (int_round_odd (Int64.unsigned n) 11 = n') by (apply int_round_odd_plus; omega).
assert (0 <= n').
{ rewrite <- H1. change 0 with (int_round_odd 0 11). apply (int_round_odd_le 0 0); omega. }
{ rewrite <- H1. change 0 with (int_round_odd 0 11). apply int_round_odd_le; omega. }
assert (n' < Int64.modulus).
{ apply Z.le_lt_trans with (int_round_odd (Int64.modulus - 1) 11).
rewrite <- H1. apply (int_round_odd_le 0 0); omega.
rewrite <- H1. apply int_round_odd_le; omega.
compute; auto. }
rewrite <- (Int64.unsigned_repr n') by (unfold Int64.max_unsigned; omega).
f_equal. Int64.bit_solve. rewrite Int64.testbit_repr by auto. unfold n'.
......@@ -1409,10 +1409,10 @@ Proof.
set (n' := Z.land (Z.lor (Int64.signed n) (Z.land (Int64.signed n) 2047 + 2047)) (-2048)).
assert (int_round_odd (Int64.signed n) 11 = n') by (apply int_round_odd_plus; omega).
assert (Int64.min_signed <= n').
{ rewrite <- H1. change Int64.min_signed with (int_round_odd Int64.min_signed 11). apply (int_round_odd_le 0 0); omega. }
{ rewrite <- H1. change Int64.min_signed with (int_round_odd Int64.min_signed 11). apply int_round_odd_le; omega. }
assert (n' <= Int64.max_signed).
{ apply Z.le_trans with (int_round_odd Int64.max_signed 11).
rewrite <- H1. apply (int_round_odd_le 0 0); omega.
rewrite <- H1. apply int_round_odd_le; omega.
compute; intuition congruence. }
rewrite <- (Int64.signed_repr n') by omega.
f_equal. Int64.bit_solve. rewrite Int64.testbit_repr by auto. unfold n'.
......
......@@ -545,7 +545,7 @@ Lemma Zrnd_odd_int:
Zrnd_odd (IZR n * bpow radix2 (-p)) * 2^p =
int_round_odd n p.
Proof.
intros.
clear. intros.
assert (0 < 2^p) by (apply (Zpower_gt_0 radix2); omega).
assert (n = (n / 2^p) * 2^p + n mod 2^p) by (rewrite Z.mul_comm; apply Z.div_mod; omega).
assert (0 <= n mod 2^p < 2^p) by (apply Z_mod_lt; omega).
......@@ -586,7 +586,7 @@ Lemma int_round_odd_le:
forall p x y, 0 <= p ->
x <= y -> int_round_odd x p <= int_round_odd y p.
Proof.
intros.
clear. intros.
assert (Zrnd_odd (IZR x * bpow radix2 (-p)) <= Zrnd_odd (IZR y * bpow radix2 (-p))).
{ apply Zrnd_le. apply valid_rnd_odd. apply Rmult_le_compat_r. apply bpow_ge_0.
apply IZR_le; auto. }
......@@ -598,7 +598,7 @@ Lemma int_round_odd_exact:
forall p x, 0 <= p ->
(2^p | x) -> int_round_odd x p = x.
Proof.
intros. unfold int_round_odd. apply Znumtheory.Zdivide_mod in H0.
clear. intros. unfold int_round_odd. apply Znumtheory.Zdivide_mod in H0.
rewrite H0. simpl. rewrite Z.mul_comm. symmetry. apply Z_div_exact_2.
apply Z.lt_gt. apply (Zpower_gt_0 radix2). auto. auto.
Qed.
......@@ -644,7 +644,7 @@ Lemma int_round_odd_shifts:
int_round_odd x p =
Z.shiftl (if Z.eqb (x mod 2^p) 0 then Z.shiftr x p else Z.lor (Z.shiftr x p) 1) p.
Proof.
intros.
clear. intros.
unfold int_round_odd. rewrite Z.shiftl_mul_pow2 by auto. f_equal.
rewrite Z.shiftr_div_pow2 by auto.
destruct (x mod 2^p =? 0) eqn:E. auto.
......@@ -662,7 +662,7 @@ Lemma int_round_odd_bits:
(forall i, p < i -> Z.testbit y i = Z.testbit x i) ->
int_round_odd x p = y.
Proof.
intros until p; intros PPOS BELOW AT ABOVE.
clear. intros until p; intros PPOS BELOW AT ABOVE.
rewrite int_round_odd_shifts by auto.
apply Z.bits_inj'. intros.
generalize (Zcompare_spec n p); intros SPEC; inversion SPEC.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment