diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2020-12-29 14:44:33 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2020-12-29 14:46:49 +0100 |
| commit | 2e202e2b17cc3ae909628b7b3ae0b8ede3117d82 (patch) | |
| tree | 5e567139c9e681bf8f72413c71022eb71b41dedd /lib/IEEE754_extra.v | |
| parent | d4513f41c54869c9b4ba96ab79d50933a1d5c25a (diff) | |
| download | compcert-kvx-2e202e2b17cc3ae909628b7b3ae0b8ede3117d82.tar.gz compcert-kvx-2e202e2b17cc3ae909628b7b3ae0b8ede3117d82.zip | |
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.
Diffstat (limited to 'lib/IEEE754_extra.v')
| -rw-r--r-- | lib/IEEE754_extra.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v index 18313ec1..5e35a191 100644 --- a/lib/IEEE754_extra.v +++ b/lib/IEEE754_extra.v @@ -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. |