...
 
Commits (49)
Sylvie Boldo <sylvie.boldo@inria.fr> Sylvie Boldo <sboldo@quetsche.inria.fr>
Pierre Roux <pierre@roux01.fr> Pierre Roux <proux@lri.fr>
Sylvie Boldo <sylvie.boldo@inria.fr> <sboldo@quetsche.inria.fr>
Xavier Leroy <xavier.leroy@college-de-france.fr> <xavier.leroy@inria.fr>
Pierre Roux <pierre.roux@onera.fr> <pierre@roux01.fr>
Pierre Roux <pierre.roux@onera.fr> <proux@lri.fr>
......@@ -4,7 +4,7 @@ Installation instructions
Prerequisites
-------------
You will need the [Coq proof assistant](https://coq.inria.fr/) (>= 8.4)
You will need the [Coq proof assistant](https://coq.inria.fr/) (>= 8.7)
with the `Reals` theory compiled in.
The `.tar.gz` file is distributed with a working set of configure files. They
......
Version 3.2.0
-------------
* added function `Bfma`
* ensured compatibility from Coq 8.7 to 8.10
Version 3.1.0
-------------
* changed matching order in `Bcompare`
* improved behavior of `Binary.v` functions with respect to NaNs
* ensured compatibility from Coq 8.7 to 8.9
* added functions `Bpred` and `Bsucc`
* added theorems on optimal relative error bounds for plus and square root
* made installation also install source files
Version 3.0.0
-------------
* stripped the `F*_` prefix from all the file names, renamed some files:
- `Definitions -> Defs`
- `Appli -> IEEE754`
* renamed `ln_beta` into `mag`
* renamed `canonic_exp` into `cexp`, `canonic` into `canonical`
* renamed all theorems ending with `unicity` by `unique`
* changed `FLX_`, `FIX_`, `FLT_`, `FLXN_`, `FTZ_format` into inductive types
......
......@@ -8,7 +8,7 @@ multi-precision fixed- and floating-point arithmetic for the
PROJECT HOME
------------
Homepage: http://flocg.gforge.inria.fr/
Homepage: http://flocq.gforge.inria.fr/
Repository: https://gitlab.inria.fr/flocq/flocq
......
......@@ -28,6 +28,7 @@ FILES = \
Prop/Double_rounding.v \
IEEE754/Binary.v \
IEEE754/Bits.v \
@PRIM_FLOAT@ \
Pff/Pff.v \
Pff/Pff2FlocqAux.v \
Pff/Pff2Flocq.v
......@@ -85,7 +86,7 @@ html/index.html: $(OBJS)
rm -rf html
mkdir -p html
@COQDOC@ -toc -interpolate -utf8 -html -g -R src Flocq -d html \
--coqlib http://coq.inria.fr/distrib/current/stdlib/ \
--coqlib http://coq.inria.fr/distrib/current/stdlib \
$(addprefix src/,$(FILES))
for f in html/*.html; do
sed -e 's;<a href="index.html">Index</a>;Go back to the <a href="../index.html">Main page</a> or <a href="index.html">Index</a>.;' -i $f
......@@ -116,7 +117,7 @@ deps.png: deps.dot
dot -T png deps.dot > deps.png
deps.map: deps.dot
dot -T cmap deps.dot > deps.map
dot -T cmap deps.dot | sed -e 's,>$,/>,' > deps.map
doc: html/index.html
......@@ -125,8 +126,9 @@ install:
prefix=@prefix@
exec_prefix=@exec_prefix@
mkdir -p @libdir@
for d in Core Calc Prop IEEE754 Pff; do mkdir -p @libdir@/$d; done
for d in Core Calc Prop IEEE754 Pff PrimitiveFloats; do mkdir -p @libdir@/$d; done
for f in $(OBJS); do cp $f @libdir@/${f#src/}; done
for f in $(FILES); do cp src/$f @libdir@/$f; done
( cd src && find . -type d -name ".coq-native" -exec cp -RT "{}" "@libdir@/{}" \; )
EXTRA_DIST = \
......
-R src Flocq
AC_INIT([Flocq], [3.0.0],
AC_INIT([Flocq], [3.2.0],
[Sylvie Boldo <sylvie.boldo@inria.fr>, Guillaume Melquiond <guillaume.melquiond@inria.fr>],
[flocq])
......@@ -15,6 +15,8 @@ m4_divert_pop([HELP_ENABLE])
AC_PROG_CXX
AC_DEFUN([AX_VERSION_GE], [AS_VERSION_COMPARE([$1],[$2],[$4],[$3],[$3])])
AC_ARG_VAR(COQBIN, [path to Coq executables [empty]])
if test ${COQBIN##*/}; then COQBIN=$COQBIN/; fi
......@@ -29,6 +31,17 @@ if test ! "$COQC"; then
fi
AC_MSG_RESULT([$COQC])
AC_MSG_CHECKING(Coq version)
coq_version=`$COQC -v | grep version | sed -e 's/^.*version \([[0-9.]]*\).*$/\1/'`
AX_VERSION_GE([$coq_version], 8.7, [],
[AC_MSG_ERROR([must be at least 8.7 (you have version $coq_version).])])
AC_MSG_RESULT($coq_version)
AX_VERSION_GE([$coq_version], 8.11,
[PRIM_FLOAT="PrimitiveFloats/SpecLayer.v PrimitiveFloats/NativeLayer.v"],
[PRIM_FLOAT=""])
AC_SUBST(PRIM_FLOAT)
AC_ARG_VAR(COQDEP, [Coq dependency analyzer command [coqdep]])
AC_MSG_CHECKING([for coqdep])
if test ! "$COQDEP"; then
......@@ -51,7 +64,7 @@ fi
AC_MSG_RESULT([$COQDOC])
if test "$libdir" = '${exec_prefix}/lib'; then
libdir="`$COQC -where`/user-contrib/Flocq"
libdir="`$COQC -where | tr -d '\r' | tr '\\\\' '/'`/user-contrib/Flocq"
fi
AC_MSG_NOTICE([building remake...])
......
......@@ -15,7 +15,7 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)
Require Import Reals Fourier Psatz.
Require Import Reals Psatz.
From Flocq Require Import Core Plus_error.
Open Scope R_scope.
......@@ -74,7 +74,7 @@ rewrite H1; unfold F2R; simpl.
rewrite bpow_plus, bpow_1.
simpl;ring.
easy.
apply Zle_trans with (1:=H3).
apply Z.le_trans with (1:=H3).
apply Zle_succ.
Qed.
......@@ -128,8 +128,7 @@ apply Rle_lt_trans with (1:=Hz).
now apply He.
unfold cexp, FLT_exp.
replace ((mag radix2 (z/2))-prec)%Z with ((mag radix2 z -1) -prec)%Z.
rewrite Z.max_l; try omega.
rewrite Z.max_l; try omega.
rewrite Z.max_l; lia.
apply Zplus_eq_compat; try reflexivity.
apply sym_eq, mag_unique.
destruct (mag radix2 z) as (e,He); simpl.
......@@ -271,7 +270,7 @@ rewrite <- (Rmult_1_l (ulp_flt f)) at 2.
apply Rmult_lt_compat_r.
rewrite ulp_neq_0; try now apply Rgt_not_eq.
apply bpow_gt_0.
fourier.
lra.
rewrite <- (round_UP_plus_eps_pos radix2 (FLT_exp emin prec) f) with (eps:=h); try assumption.
apply round_UP_pt...
now left.
......@@ -280,7 +279,7 @@ apply Rle_trans with (1:=Hh).
rewrite <- (Rmult_1_l (ulp_flt f)) at 2.
apply Rmult_le_compat_r.
apply ulp_ge_0.
fourier.
lra.
apply Rplus_lt_reg_l with (-f); ring_simplify.
apply Rlt_le_trans with (/2*ulp_flt f).
2: right; field.
......@@ -288,7 +287,7 @@ apply Rle_lt_trans with (1:=Hh).
apply Rmult_lt_compat_r.
rewrite ulp_neq_0; try now apply Rgt_not_eq.
apply bpow_gt_0.
fourier.
lra.
(* h = 0 *)
rewrite <- H, Rplus_0_r.
apply round_generic...
......@@ -433,13 +432,13 @@ apply Rle_trans with (1:=Hh).
apply Rle_trans with (/2*ulp_flt f).
apply Rmult_le_compat_r.
apply ulp_ge_0.
fourier.
lra.
case H0.
intros Y; rewrite Y.
rewrite <- (Rmult_1_l (ulp_flt f)) at 2.
apply Rmult_le_compat_r.
apply ulp_ge_0.
fourier.
lra.
intros Y; rewrite (proj1 Y); now right.
replace (f+h) with (pred_flt f + (f-pred_flt f+h)) by ring.
pattern f at 4; rewrite <- (round_UP_pred_plus_eps_pos radix2 (FLT_exp emin prec) f) with (eps:=(f - pred_flt f + h)); try assumption.
......@@ -453,12 +452,12 @@ rewrite Y.
rewrite <- (Rmult_1_l (ulp_flt f)) at 2.
apply Rmult_lt_compat_r.
rewrite ulp_neq_0;[apply bpow_gt_0|now apply Rgt_not_eq].
fourier.
lra.
apply Rlt_le_trans with (1:=Y2).
rewrite Y1.
apply Rmult_le_compat_r.
apply ulp_ge_0.
fourier.
lra.
apply Rplus_le_reg_l with (-ulp_flt (pred_flt f)); ring_simplify.
now left.
rewrite pred_eq_pos; try now left.
......@@ -479,7 +478,7 @@ apply Rle_lt_trans with (1:=Hh).
rewrite Y.
apply Rmult_lt_compat_r.
rewrite ulp_neq_0; try apply bpow_gt_0; now apply Rgt_not_eq.
fourier.
lra.
apply Rlt_le_trans with (1:=Y2).
rewrite Y1.
right; field.
......@@ -503,19 +502,19 @@ auto with real.
rewrite T3, T1.
apply Rmult_le_compat_r.
apply ulp_ge_0.
fourier.
lra.
assert (round radix2 (FLT_exp emin prec) Zceil (f+h) = f).
replace (f+h) with (pred_flt f + /2*ulp_flt (pred_flt f)).
apply round_UP_pred_plus_eps_pos...
split.
apply Rmult_lt_0_compat.
fourier.
lra.
rewrite ulp_neq_0; try now apply Rgt_not_eq.
apply bpow_gt_0.
rewrite <- (Rmult_1_l (ulp_flt (pred_flt f))) at 2.
apply Rmult_le_compat_r.
apply ulp_ge_0.
fourier.
lra.
rewrite T1, H0, <- T2.
replace h with (--h) by ring; rewrite T3.
replace (bpow (mag radix2 f - 1 - prec)) with (/2*ulp_flt f).
......@@ -544,11 +543,11 @@ rewrite bpow_opp.
rewrite <- ulp_neq_0; try now apply Rgt_not_eq.
rewrite T1.
rewrite Rinv_mult_distr.
2: apply Rgt_not_eq; fourier.
2: apply Rgt_not_eq; lra.
2: apply Rgt_not_eq; rewrite ulp_neq_0; try apply bpow_gt_0.
2: now apply Rgt_not_eq.
rewrite Rinv_involutive.
2: apply Rgt_not_eq; fourier.
2: apply Rgt_not_eq; lra.
rewrite T2 at 2.
rewrite ulp_bpow.
rewrite <- bpow_opp.
......@@ -795,9 +794,9 @@ unfold Rdiv; rewrite Rabs_mult.
unfold Zminus; rewrite bpow_plus.
simpl; rewrite (Rabs_pos_eq (/2)).
apply (Rmult_le_compat_r (/2)).
fourier.
lra.
now left.
fourier.
lra.
assert (K2:bpow (prec+emin-1) <= / 4 * ulp_flt (x / 2)).
assert (Z: x/2 <> 0).
intros K; contradict H0.
......@@ -817,9 +816,9 @@ unfold Rdiv; rewrite Rabs_mult.
unfold Zminus; rewrite bpow_plus.
simpl; rewrite (Rabs_right (/2)).
apply Rmult_le_compat_r.
fourier.
lra.
exact Hx.
fourier.
lra.
apply He; trivial.
rewrite Z.max_l.
omega.
......@@ -1391,7 +1390,7 @@ now apply IZR_le.
rewrite ulp_neq_0.
2: apply Rmult_integral_contrapositive_currified.
2: apply Rgt_not_eq, bpow_gt_0.
2: apply Rinv_neq_0_compat, Rgt_not_eq; fourier.
2: apply Rinv_neq_0_compat, Rgt_not_eq; lra.
apply bpow_le.
unfold cexp, FLT_exp.
apply Z.le_max_r.
......@@ -1427,7 +1426,7 @@ now apply IZR_le.
rewrite ulp_neq_0.
2: apply Rmult_integral_contrapositive_currified.
2: apply Rgt_not_eq, bpow_gt_0.
2: apply Rinv_neq_0_compat, Rgt_not_eq; fourier.
2: apply Rinv_neq_0_compat, Rgt_not_eq; lra.
apply bpow_le.
unfold cexp, FLT_exp.
apply Z.le_max_r.
......
......@@ -55,7 +55,7 @@ Qed.
Definition plus (x y : float beta) :=
let (m, e) := Fplus x y in
let s := Zlt_bool m 0 in
let '(m', e', l) := truncate beta fexp (Zabs m, e, loc_Exact) in
let '(m', e', l) := truncate beta fexp (Z.abs m, e, loc_Exact) in
Float beta (cond_Zopp s (choice s m' l)) e'.
Theorem plus_correct :
......@@ -66,7 +66,7 @@ intros x y.
unfold plus.
rewrite <- F2R_plus.
destruct (Fplus x y) as [m e].
rewrite (round_trunc_sign_any_correct beta fexp rnd choice rnd_choice _ (Zabs m) e loc_Exact).
rewrite (round_trunc_sign_any_correct beta fexp rnd choice rnd_choice _ (Z.abs m) e loc_Exact).
3: now right.
destruct truncate as [[m' e'] l'].
apply (f_equal (fun s => F2R (Float beta (cond_Zopp s (choice s _ _)) _))).
......@@ -78,7 +78,7 @@ Qed.
Definition mult (x y : float beta) :=
let (m, e) := Fmult x y in
let s := Zlt_bool m 0 in
let '(m', e', l) := truncate beta fexp (Zabs m, e, loc_Exact) in
let '(m', e', l) := truncate beta fexp (Z.abs m, e, loc_Exact) in
Float beta (cond_Zopp s (choice s m' l)) e'.
Theorem mult_correct :
......@@ -89,7 +89,7 @@ intros x y.
unfold mult.
rewrite <- F2R_mult.
destruct (Fmult x y) as [m e].
rewrite (round_trunc_sign_any_correct beta fexp rnd choice rnd_choice _ (Zabs m) e loc_Exact).
rewrite (round_trunc_sign_any_correct beta fexp rnd choice rnd_choice _ (Z.abs m) e loc_Exact).
3: now right.
destruct truncate as [[m' e'] l'].
apply (f_equal (fun s => F2R (Float beta (cond_Zopp s (choice s _ _)) _))).
......
......@@ -72,13 +72,13 @@ Lemma midpoint_beta_odd_remains_pos :
Proof.
intros x Px ex1 ex2 Hf2.
set (z := (ex1 - ex2)%Z).
assert (Hz : Z_of_nat (Zabs_nat z) = z).
assert (Hz : Z_of_nat (Z.abs_nat z) = z).
{ rewrite Zabs2Nat.id_abs.
rewrite <- cond_Zopp_Zlt_bool; unfold cond_Zopp.
assert (H : (z <? 0)%Z = false); [|now rewrite H].
apply Zlt_bool_false; unfold z; omega. }
revert Hz.
generalize (Zabs_nat z); intro n.
generalize (Z.abs_nat z); intro n.
unfold z; clear z; revert ex1 ex2 Hf2.
induction n.
- simpl.
......
......@@ -99,8 +99,8 @@ Qed.
Lemma FLXN_le_exp: forall f1 f2:float beta,
((Zpower beta (prec - 1) <= Zabs (Fnum f1) < Zpower beta prec)%Z) ->
((Zpower beta (prec - 1) <= Zabs (Fnum f2) < Zpower beta prec))%Z ->
((Zpower beta (prec - 1) <= Z.abs (Fnum f1) < Zpower beta prec)%Z) ->
((Zpower beta (prec - 1) <= Z.abs (Fnum f2) < Zpower beta prec))%Z ->
0 <= F2R f1 -> F2R f1 <= F2R f2 -> (Fexp f1 <= Fexp f2)%Z.
Proof.
intros f1 f2 H1 H2 H3 H4.
......@@ -132,7 +132,7 @@ apply Rmult_le_compat_r.
apply bpow_ge_0.
rewrite <- IZR_Zpower.
apply IZR_le.
apply Zle_trans with (1:=proj1 H1).
apply Z.le_trans with (1:=proj1 H1).
rewrite Z.abs_eq.
auto with zarith.
apply le_IZR.
......@@ -2177,7 +2177,7 @@ apply Rmult_le_compat_r.
apply bpow_ge_0.
rewrite <- IZR_Zpower.
left; apply IZR_lt.
replace (Fnum (Fabs f)) with (Zabs (Fnum f)).
replace (Fnum (Fabs f)) with (Z.abs (Fnum f)).
assumption.
destruct f; unfold Fabs; reflexivity.
omega.
......
This diff is collapsed.
......@@ -375,7 +375,7 @@ rewrite <- mult_IZR.
apply Rcompare_not_Lt.
apply IZR_le.
rewrite Hk.
apply Zle_refl.
apply Z.le_refl.
exact Hstep.
Qed.
......@@ -403,7 +403,7 @@ Definition new_location_even k l :=
match l with loc_Exact => l | _ => loc_Inexact Lt end
else
loc_Inexact
match Zcompare (2 * k) nb_steps with
match Z.compare (2 * k) nb_steps with
| Lt => Lt
| Eq => match l with loc_Exact => Eq | _ => Gt end
| Gt => Gt
......@@ -460,7 +460,7 @@ Definition new_location_odd k l :=
match l with loc_Exact => l | _ => loc_Inexact Lt end
else
loc_Inexact
match Zcompare (2 * k + 1) nb_steps with
match Z.compare (2 * k + 1) nb_steps with
| Lt => Lt
| Eq => match l with loc_Inexact l => l | loc_Exact => Lt end
| Gt => Gt
......@@ -513,7 +513,7 @@ Theorem new_location_correct :
Proof.
intros x k l Hk Hx.
unfold new_location.
generalize (refl_equal nb_steps) (Zle_lt_trans _ _ _ (proj1 Hk) (proj2 Hk)).
generalize (refl_equal nb_steps) (Z.le_lt_trans _ _ _ (proj1 Hk) (proj2 Hk)).
pattern nb_steps at 2 3 5 ; case nb_steps.
now intros _.
(* . *)
......@@ -603,7 +603,7 @@ Theorem inbetween_float_new_location :
forall x m e l k,
(0 < k)%Z ->
inbetween_float m e x l ->
inbetween_float (Zdiv m (Zpower beta k)) (e + k) x (new_location (Zpower beta k) (Zmod m (Zpower beta k)) l).
inbetween_float (Z.div m (Zpower beta k)) (e + k) x (new_location (Zpower beta k) (Zmod m (Zpower beta k)) l).
Proof.
intros x m e l k Hk Hx.
unfold inbetween_float in *.
......@@ -614,7 +614,7 @@ apply (f_equal (fun r => F2R (Float beta (m * Zpower _ r) e))).
ring.
omega.
assert (Hp: (Zpower beta k > 0)%Z).
apply Zlt_gt.
apply Z.lt_gt.
apply Zpower_gt_0.
now apply Zlt_le_weak.
(* . *)
......@@ -634,7 +634,7 @@ Qed.
Theorem inbetween_float_new_location_single :
forall x m e l,
inbetween_float m e x l ->
inbetween_float (Zdiv m beta) (e + 1) x (new_location beta (Zmod m beta) l).
inbetween_float (Z.div m beta) (e + 1) x (new_location beta (Zmod m beta) l).
Proof.
intros x m e l Hx.
replace (radix_val beta) with (Zpower beta 1).
......
......@@ -62,7 +62,7 @@ Definition Fdiv_core m1 e1 m2 e2 e :=
if Zle_bool e (e1 - e2)%Z
then (m1 * Zpower beta (e1 - e2 - e), m2)%Z
else (m1, m2 * Zpower beta (e - (e1 - e2)))%Z in
let '(q, r) := Zdiv_eucl m1' m2' in
let '(q, r) := Z.div_eucl m1' m2' in
(q, new_location m2' r loc_Exact).
Theorem Fdiv_core_correct :
......@@ -96,7 +96,7 @@ assert ((F2R (Float beta m1 e1) / F2R (Float beta m2 e2) = IZR m1' / IZR m2' * b
now apply IZR_neq, Zgt_not_eq. }
clearbody m12 ; clear Hm Hm1 Hm2.
generalize (Z_div_mod m1' m2' (Z.lt_gt _ _ Hm2')).
destruct (Zdiv_eucl m1' m2') as (q, r).
destruct (Z.div_eucl m1' m2') as (q, r).
intros (Hq, Hr).
rewrite Hf.
unfold inbetween_float, F2R. simpl.
......@@ -123,7 +123,7 @@ Definition Fdiv (x y : float beta) :=
let (m1, e1) := x in
let (m2, e2) := y in
let e' := ((Zdigits beta m1 + e1) - (Zdigits beta m2 + e2))%Z in
let e := Zmin (Zmin (fexp e') (fexp (e' + 1))) (e1 - e2) in
let e := Z.min (Z.min (fexp e') (fexp (e' + 1))) (e1 - e2) in
let '(m, l) := Fdiv_core m1 e1 m2 e2 e in
(m, e, l).
......@@ -140,19 +140,19 @@ apply gt_0_F2R in Hm2.
unfold Fdiv.
generalize (mag_div_F2R m1 e1 m2 e2 Hm1 Hm2).
set (e := Zminus _ _).
set (e' := Zmin (Zmin (fexp e) (fexp (e + 1))) (e1 - e2)).
set (e' := Z.min (Z.min (fexp e) (fexp (e + 1))) (e1 - e2)).
intros [H1 H2].
generalize (Fdiv_core_correct m1 e1 m2 e2 e' Hm1 Hm2).
destruct Fdiv_core as [m' l].
apply conj.
apply Zle_trans with (1 := Zle_min_l _ _).
apply Z.le_trans with (1 := Z.le_min_l _ _).
unfold cexp.
destruct (Zle_lt_or_eq _ _ H1) as [H|H].
- replace (fexp (mag _ _)) with (fexp (e + 1)).
apply Zle_min_r.
apply Z.le_min_r.
clear -H1 H2 H ; apply f_equal ; omega.
- replace (fexp (mag _ _)) with (fexp e).
apply Zle_min_l.
apply Z.le_min_l.
clear -H1 H2 H ; apply f_equal ; omega.
Qed.
......
......@@ -55,7 +55,7 @@ Qed.
Theorem Falign_spec_exp:
forall f1 f2 : float beta,
snd (Falign f1 f2) = Zmin (Fexp f1) (Fexp f2).
snd (Falign f1 f2) = Z.min (Fexp f1) (Fexp f2).
Proof.
intros (m1,e1) (m2,e2).
unfold Falign; simpl.
......@@ -77,7 +77,7 @@ Qed.
Definition Fabs (f1 : float beta) : float beta :=
let '(Float m1 e1) := f1 in
Float (Zabs m1)%Z e1.
Float (Z.abs m1)%Z e1.
Theorem F2R_abs :
forall f1 : float beta,
......@@ -117,7 +117,7 @@ Qed.
Theorem Fexp_Fplus :
forall f1 f2 : float beta,
Fexp (Fplus f1 f2) = Zmin (Fexp f1) (Fexp f2).
Fexp (Fplus f1 f2) = Z.min (Fexp f1) (Fexp f2).
Proof.
intros f1 f2.
unfold Fplus.
......
......@@ -60,9 +60,9 @@ simpl in He |- *.
clear Bx.
destruct He as [He|He].
- apply eq_sym, valid_exp with (2 := He).
now apply Zle_trans with e.
now apply Z.le_trans with e.
- apply valid_exp with (1 := He).
now apply Zle_trans with e.
now apply Z.le_trans with e.
Qed.
Theorem cexp_inbetween_float_loc_Exact :
......@@ -296,7 +296,7 @@ rewrite H.
apply Zceil_IZR.
apply Zceil_imp.
split.
change (m + 1 - 1)%Z with (Zpred (Zsucc m)).
change (m + 1 - 1)%Z with (Z.pred (Z.succ m)).
now rewrite <- Zpred_succ.
now apply Rlt_le.
now apply Rge_le.
......@@ -591,7 +591,7 @@ Qed.
Definition truncate_aux t k :=
let '(m, e, l) := t in
let p := Zpower beta k in
(Zdiv m p, (e + k)%Z, new_location p (Zmod m p) l).
(Z.div m p, (e + k)%Z, new_location p (Zmod m p) l).
Theorem truncate_aux_comp :
forall t k1 k2,
......@@ -656,17 +656,17 @@ rewrite Zdigits_div_Zpower with (1 := Hm).
replace (Zdigits beta m - k + (e + k))%Z with (Zdigits beta m + e)%Z by ring.
unfold k.
ring_simplify.
apply Zle_refl.
apply Z.le_refl.
split.
now apply Zlt_le_weak.
apply Znot_gt_le.
contradict Hd.
apply Zdiv_small.
apply conj with (1 := Hm).
rewrite <- Zabs_eq with (1 := Hm).
rewrite <- Z.abs_eq with (1 := Hm).
apply Zpower_gt_Zdigits.
apply Zlt_le_weak.
now apply Zgt_lt.
now apply Z.gt_lt.
(* *)
destruct (Zle_lt_or_eq _ _ Hm) as [Hm'|Hm'].
apply generic_format_F2R.
......@@ -953,7 +953,7 @@ now apply Rge_le.
(* *)
destruct (Rlt_bool_spec x 0) as [Zx|Zx].
(* . *)
apply Zopp_inj.
apply Z.opp_inj.
change (- m = cond_Zopp true (choice true m loc_Exact))%Z.
rewrite <- (Zrnd_IZR rnd (-m)) at 1.
assert (IZR (-m) < 0)%R.
......@@ -1125,7 +1125,7 @@ Definition truncate_FIX t :=
let k := (emin - e)%Z in
if Zlt_bool 0 k then
let p := Zpower beta k in
(Zdiv m p, (e + k)%Z, new_location p (Zmod m p) l)
(Z.div m p, (e + k)%Z, new_location p (Zmod m p) l)
else t.
Theorem truncate_FIX_correct :
......
......@@ -51,7 +51,7 @@ Complexity is fine as long as p1 <= 2p-1.
Lemma mag_sqrt_F2R :
forall m1 e1,
(0 < m1)%Z ->
mag beta (sqrt (F2R (Float beta m1 e1))) = Zdiv2 (Zdigits beta m1 + e1 + 1) :> Z.
mag beta (sqrt (F2R (Float beta m1 e1))) = Z.div2 (Zdigits beta m1 + e1 + 1) :> Z.
Proof.
intros m1 e1 Hm1.
rewrite <- (mag_F2R_Zdigits beta m1 e1) by now apply Zgt_not_eq.
......@@ -170,7 +170,7 @@ Qed.
Definition Fsqrt (x : float beta) :=
let (m1, e1) := x in
let e' := (Zdigits beta m1 + e1 + 1)%Z in
let e := Zmin (fexp (Z.div2 e')) (Z.div2 e1) in
let e := Z.min (fexp (Z.div2 e')) (Z.div2 e1) in
let '(m, l) := Fsqrt_core m1 e1 e in
(m, e, l).
......@@ -184,18 +184,18 @@ Proof.
intros [m1 e1] Hm1.
apply gt_0_F2R in Hm1.
unfold Fsqrt.
set (e := Zmin _ _).
set (e := Z.min _ _).
assert (2 * e <= e1)%Z as He.
{ assert (e <= Zdiv2 e1)%Z by apply Zle_min_r.
{ assert (e <= Z.div2 e1)%Z by apply Z.le_min_r.
rewrite (Zdiv2_odd_eqn e1).
destruct Z.odd ; omega. }
generalize (Fsqrt_core_correct m1 e1 e Hm1 He).
destruct Fsqrt_core as [m l].
apply conj.
apply Zle_trans with (1 := Zle_min_l _ _).
apply Z.le_trans with (1 := Z.le_min_l _ _).
unfold cexp.
rewrite (mag_sqrt_F2R m1 e1 Hm1).
apply Zle_refl.
apply Z.le_refl.
Qed.
End Fcalc_sqrt.
This diff is collapsed.
......@@ -43,7 +43,7 @@ unfold FIX_exp.
split ; intros H.
now apply Zlt_le_weak.
split.
apply Zle_refl.
apply Z.le_refl.
now intros _ _.
Qed.
......@@ -76,7 +76,7 @@ Qed.
Global Instance FIX_exp_monotone : Monotone_exp FIX_exp.
Proof.
intros ex ey H.
apply Zle_refl.
apply Z.le_refl.
Qed.
Theorem ulp_FIX :
......
......@@ -20,6 +20,7 @@ COPYING file for more details.
(** * Floating-point format with gradual underflow *)
Require Import Raux Defs Round_pred Generic_fmt Float_prop.
Require Import FLX FIX Ulp Round_NE.
Require Import Psatz.
Section RND_FLT.
......@@ -33,10 +34,10 @@ Context { prec_gt_0_ : Prec_gt_0 prec }.
Inductive FLT_format (x : R) : Prop :=
FLT_spec (f : float beta) :
x = F2R f -> (Zabs (Fnum f) < Zpower beta prec)%Z ->
x = F2R f -> (Z.abs (Fnum f) < Zpower beta prec)%Z ->
(emin <= Fexp f)%Z -> FLT_format x.
Definition FLT_exp e := Zmax (e - prec) emin.
Definition FLT_exp e := Z.max (e - prec) emin.
(** Properties of the FLT format *)
Global Instance FLT_exp_valid : Valid_exp FLT_exp.
......@@ -59,7 +60,7 @@ apply generic_format_F2R.
intros Zmx.
unfold cexp, FLT_exp.
rewrite mag_F2R with (1 := Zmx).
apply Zmax_lub with (2 := H3).
apply Z.max_lub with (2 := H3).
apply Zplus_le_reg_r with (prec - ex)%Z.
ring_simplify.
now apply mag_le_Zpower.
......@@ -80,7 +81,7 @@ rewrite IZR_Zpower. 2: now apply Zlt_le_weak.
apply Rmult_lt_reg_r with (bpow ex).
apply bpow_gt_0.
rewrite <- bpow_plus.
change (F2R (Float beta (Zabs mx) ex) < bpow (prec + ex))%R.
change (F2R (Float beta (Z.abs mx) ex) < bpow (prec + ex))%R.
rewrite F2R_Zabs.
rewrite <- Hx.
destruct (Req_dec x 0) as [Hx0|Hx0].
......@@ -94,8 +95,8 @@ apply Rlt_le_trans with (1 := proj2 He).
apply bpow_le.
cut (ex' - prec <= ex)%Z. omega.
unfold ex, FLT_exp.
apply Zle_max_l.
apply Zle_max_r.
apply Z.le_max_l.
apply Z.le_max_r.
Qed.
......@@ -167,7 +168,7 @@ apply generic_format_F2R.
intros _.
rewrite <- Hx.
unfold cexp, FLX_exp, FLT_exp.
apply Zle_max_l.
apply Z.le_max_l.
Qed.
Theorem round_FLT_FLX : forall rnd x,
......@@ -208,7 +209,7 @@ rewrite Hx.
apply generic_format_F2R.
intros _.
rewrite <- Hx.
apply Zle_max_r.
apply Z.le_max_r.
Qed.
Theorem generic_format_FLT_FIX :
......@@ -220,9 +221,37 @@ Proof with auto with typeclass_instances.
apply generic_inclusion_le...
intros e He.
unfold FIX_exp.
apply Zmax_lub.
apply Z.max_lub.
omega.
apply Zle_refl.
apply Z.le_refl.
Qed.
Lemma negligible_exp_FLT :
exists n, negligible_exp FLT_exp = Some n /\ (n <= emin)%Z.
Proof.
case (negligible_exp_spec FLT_exp).
{ intro H; exfalso; specialize (H emin); revert H.
apply Zle_not_lt, Z.le_max_r. }
intros n Hn; exists n; split; [now simpl|].
destruct (Z.max_spec (n - prec) emin) as [(Hm, Hm')|(Hm, Hm')].
{ now revert Hn; unfold FLT_exp; rewrite Hm'. }
revert Hn prec_gt_0_; unfold FLT_exp, Prec_gt_0; rewrite Hm'; lia.
Qed.
Theorem generic_format_FLT_1 (Hemin : (emin <= 0)%Z) :
generic_format beta FLT_exp 1.
Proof.
unfold generic_format, scaled_mantissa, cexp, F2R; simpl.
rewrite Rmult_1_l, (mag_unique beta 1 1).
{ unfold FLT_exp.
destruct (Z.max_spec_le (1 - prec) emin) as [(H,Hm)|(H,Hm)]; rewrite Hm;
(rewrite <- IZR_Zpower; [|unfold Prec_gt_0 in prec_gt_0_; omega]);
(rewrite Ztrunc_IZR, IZR_Zpower, <-bpow_plus;
[|unfold Prec_gt_0 in prec_gt_0_; omega]);
now replace (_ + _)%Z with Z0 by ring. }
rewrite Rabs_R1; simpl; split; [now right|].
rewrite IZR_Zpower_pos; simpl; rewrite Rmult_1_r; apply IZR_lt.
apply (Z.lt_le_trans _ 2); [omega|]; apply Zle_bool_imp_le, beta.
Qed.
Theorem ulp_FLT_small: forall x, (Rabs x < bpow (emin+prec))%R ->
......@@ -234,7 +263,7 @@ unfold ulp; case Req_bool_spec; intros Hx2.
case (negligible_exp_spec FLT_exp).
intros T; specialize (T (emin-1)%Z); contradict T.
apply Zle_not_lt; unfold FLT_exp.
apply Zle_trans with (2:=Z.le_max_r _ _); omega.
apply Z.le_trans with (2:=Z.le_max_r _ _); omega.
assert (V:FLT_exp emin = emin).
unfold FLT_exp; apply Z.max_r.
unfold Prec_gt_0 in prec_gt_0_; omega.
......@@ -293,7 +322,58 @@ apply bpow_le.
apply Z.le_max_l.
Qed.
Lemma ulp_FLT_exact_shift :
forall x e,
(x <> 0)%R ->
(emin + prec <= mag beta x)%Z ->
(emin + prec - mag beta x <= e)%Z ->
(ulp beta FLT_exp (x * bpow e) = ulp beta FLT_exp x * bpow e)%R.
Proof.
intros x e Nzx Hmx He.
unfold ulp; rewrite Req_bool_false;
[|now intro H; apply Nzx, (Rmult_eq_reg_r (bpow e));
[rewrite Rmult_0_l|apply Rgt_not_eq, Rlt_gt, bpow_gt_0]].
rewrite (Req_bool_false _ _ Nzx), <- bpow_plus; f_equal; unfold cexp, FLT_exp.
rewrite (mag_mult_bpow _ _ _ Nzx), !Z.max_l; omega.
Qed.
Lemma succ_FLT_exact_shift_pos :
forall x e,
(0 < x)%R ->
(emin + prec <= mag beta x)%Z ->
(emin + prec - mag beta x <= e)%Z ->
(succ beta FLT_exp (x * bpow e) = succ beta FLT_exp x * bpow e)%R.
Proof.
intros x e Px Hmx He.
rewrite succ_eq_pos; [|now apply Rlt_le, Rmult_lt_0_compat, bpow_gt_0].
rewrite (succ_eq_pos _ _ _ (Rlt_le _ _ Px)).
now rewrite Rmult_plus_distr_r; f_equal; apply ulp_FLT_exact_shift; [lra| |].
Qed.
Lemma succ_FLT_exact_shift :
forall x e,
(x <> 0)%R ->
(emin + prec + 1 <= mag beta x)%Z ->
(emin + prec - mag beta x + 1 <= e)%Z ->
(succ beta FLT_exp (x * bpow e) = succ beta FLT_exp x * bpow e)%R.
Proof.
intros x e Nzx Hmx He.
destruct (Rle_or_lt 0 x) as [Px|Nx].
{ now apply succ_FLT_exact_shift_pos; [lra|lia|lia]. }
unfold succ.
rewrite Rle_bool_false; [|assert (H := bpow_gt_0 beta e); nra].
rewrite Rle_bool_false; [|now simpl].
rewrite Ropp_mult_distr_l_reverse, <-Ropp_mult_distr_l_reverse; f_equal.
unfold pred_pos.
rewrite mag_mult_bpow; [|lra].
replace (_ - 1)%Z with (mag beta (- x) - 1 + e)%Z; [|ring]; rewrite bpow_plus.
unfold Req_bool; rewrite Rcompare_mult_r; [|now apply bpow_gt_0].
fold (Req_bool (-x) (bpow (mag beta (-x) - 1))); case Req_bool.
{ rewrite mag_opp; unfold FLT_exp; do 2 (rewrite Z.max_l; [|lia]).
replace (_ - _)%Z with (mag beta x - 1 - prec + e)%Z; [|ring].
rewrite bpow_plus; ring. }
rewrite ulp_FLT_exact_shift; [ring|lra| |]; rewrite mag_opp; lia.
Qed.
(** FLT is a nice format: it has a monotone exponent... *)
Global Instance FLT_exp_monotone : Monotone_exp FLT_exp.
......
......@@ -20,6 +20,7 @@ COPYING file for more details.
(** * Floating-point format without underflow *)
Require Import Raux Defs Round_pred Generic_fmt Float_prop.
Require Import FIX Ulp Round_NE.
Require Import Psatz.
Section RND_FLX.
......@@ -36,7 +37,7 @@ Context { prec_gt_0_ : Prec_gt_0 }.
Inductive FLX_format (x : R) : Prop :=
FLX_spec (f : float beta) :
x = F2R f -> (Zabs (Fnum f) < Zpower beta prec)%Z -> FLX_format x.
x = F2R f -> (Z.abs (Fnum f) < Zpower beta prec)%Z -> FLX_format x.
Definition FLX_exp (e : Z) := (e - prec)%Z.
......@@ -127,14 +128,14 @@ apply FLX_format_generic.
apply generic_format_FIX in Fx.
revert Fx.
apply generic_inclusion with (e := e)...
apply Zle_refl.
apply Z.le_refl.
Qed.
(** unbounded floating-point format with normal mantissas *)
Inductive FLXN_format (x : R) : Prop :=
FLXN_spec (f : float beta) :
x = F2R f ->
(x <> 0%R -> Zpower beta (prec - 1) <= Zabs (Fnum f) < Zpower beta prec)%Z ->
(x <> 0%R -> Zpower beta (prec - 1) <= Z.abs (Fnum f) < Zpower beta prec)%Z ->
FLXN_format x.
Theorem generic_format_FLXN :
......@@ -214,12 +215,38 @@ intros n H2; contradict H2.
unfold FLX_exp; unfold Prec_gt_0 in prec_gt_0_; omega.
Qed.
Theorem generic_format_FLX_1 :
generic_format beta FLX_exp 1.
Proof.
unfold generic_format, scaled_mantissa, cexp, F2R; simpl.
rewrite Rmult_1_l, (mag_unique beta 1 1).
{ unfold FLX_exp.
rewrite <- IZR_Zpower; [|unfold Prec_gt_0 in prec_gt_0_; omega].
rewrite Ztrunc_IZR, IZR_Zpower; [|unfold Prec_gt_0 in prec_gt_0_; omega].
rewrite <- bpow_plus.
now replace (_ + _)%Z with Z0 by ring. }
rewrite Rabs_R1; simpl; split; [now right|].
unfold Z.pow_pos; simpl; rewrite Zmult_1_r; apply IZR_lt.
assert (H := Zle_bool_imp_le _ _ (radix_prop beta)); omega.
Qed.
Theorem ulp_FLX_0: (ulp beta FLX_exp 0 = 0)%R.
Proof.
unfold ulp; rewrite Req_bool_true; trivial.
rewrite negligible_exp_FLX; easy.
Qed.
Lemma ulp_FLX_1 : ulp beta FLX_exp 1 = bpow (-prec + 1).
Proof.
unfold ulp, FLX_exp, cexp; rewrite Req_bool_false; [|apply R1_neq_R0].
rewrite mag_1; f_equal; ring.
Qed.
Lemma succ_FLX_1 : (succ beta FLX_exp 1 = 1 + bpow (-prec + 1))%R.
Proof.
now unfold succ; rewrite Rle_bool_true; [|apply Rle_0_1]; rewrite ulp_FLX_1.
Qed.
Theorem eq_0_round_0_FLX :
forall rnd {Vr: Valid_rnd rnd} x,
round beta FLX_exp rnd x = 0%R -> x = 0%R.
......@@ -274,6 +301,45 @@ apply bpow_ge_0.
left; now apply bpow_mag_gt.
Qed.
Lemma ulp_FLX_exact_shift :
forall x e,
(ulp beta FLX_exp (x * bpow e) = ulp beta FLX_exp x * bpow e)%R.
Proof.
intros x e.
destruct (Req_dec x 0) as [Hx|Hx].
{ unfold ulp.
now rewrite !Req_bool_true, negligible_exp_FLX; rewrite ?Hx, ?Rmult_0_l. }
unfold ulp; rewrite Req_bool_false;
[|now intro H; apply Hx, (Rmult_eq_reg_r (bpow e));
[rewrite Rmult_0_l|apply Rgt_not_eq, Rlt_gt, bpow_gt_0]].
rewrite (Req_bool_false _ _ Hx), <- bpow_plus; f_equal; unfold cexp, FLX_exp.
now rewrite mag_mult_bpow; [ring|].
Qed.
Lemma succ_FLX_exact_shift :
forall x e,
(succ beta FLX_exp (x * bpow e) = succ beta FLX_exp x * bpow e)%R.
Proof.
intros x e.
destruct (Rle_or_lt 0 x) as [Px|Nx].
{ rewrite succ_eq_pos; [|now apply Rmult_le_pos, bpow_ge_0].
rewrite (succ_eq_pos _ _ _ Px).
now rewrite Rmult_plus_distr_r; f_equal; apply ulp_FLX_exact_shift. }
unfold succ.
rewrite Rle_bool_false; [|assert (H := bpow_gt_0 beta e); nra].
rewrite Rle_bool_false; [|now simpl].
rewrite Ropp_mult_distr_l_reverse, <-Ropp_mult_distr_l_reverse; f_equal.
unfold pred_pos.
rewrite mag_mult_bpow; [|lra].
replace (_ - 1)%Z with (mag beta (- x) - 1 + e)%Z; [|ring]; rewrite bpow_plus.
unfold Req_bool; rewrite Rcompare_mult_r; [|now apply bpow_gt_0].
fold (Req_bool (-x) (bpow (mag beta (-x) - 1))); case Req_bool.
{ unfold FLX_exp.
replace (_ - _)%Z with (mag beta (- x) - 1 - prec + e)%Z; [|ring].
rewrite bpow_plus; ring. }
rewrite ulp_FLX_exact_shift; ring.
Qed.
(** FLX is a nice format: it has a monotone exponent... *)
Global Instance FLX_exp_monotone : Monotone_exp FLX_exp.
Proof.
......
......@@ -34,7 +34,7 @@ Context { prec_gt_0_ : Prec_gt_0 prec }.
Inductive FTZ_format (x : R) : Prop :=
FTZ_spec (f : float beta) :
x = F2R f ->
(x <> 0%R -> Zpower beta (prec - 1) <= Zabs (Fnum f) < Zpower beta prec)%Z ->
(x <> 0%R -> Zpower beta (prec - 1) <= Z.abs (Fnum f) < Zpower beta prec)%Z ->
(emin <= Fexp f)%Z ->
FTZ_format x.
......@@ -91,7 +91,7 @@ rewrite Hx1, Zx.
apply F2R_0.
unfold FTZ_exp, FLX_exp.
rewrite Zlt_bool_false.
apply Zle_refl.
apply Z.le_refl.
rewrite Hx1, mag_F2R with (1 := Zxm).
cut (prec - 1 < mag beta (IZR xm))%Z.
clear -Hx3 ; omega.
......@@ -110,7 +110,7 @@ exists (Float beta 0 emin).
apply sym_eq, F2R_0.
intros H.
now elim H.
apply Zle_refl.
apply Z.le_refl.
unfold generic_format, scaled_mantissa, cexp, FTZ_exp in Hx.
destruct (mag beta x) as (ex, Hx4).
simpl in Hx.
......@@ -131,7 +131,7 @@ apply lt_IZR.
apply Rmult_lt_reg_r with (bpow (emin + prec - 1)).
apply bpow_gt_0.
rewrite Rmult_0_l.
change (0 < F2R (Float beta (Zabs (Ztrunc (x * bpow (- (emin + prec - 1))))) (emin + prec - 1)))%R.
change (0 < F2R (Float beta (Z.abs (Ztrunc (x * bpow (- (emin + prec - 1))))) (emin + prec - 1)))%R.
rewrite F2R_Zabs, <- Hx2.
now apply Rabs_pos_lt.
apply bpow_le.
......@@ -144,7 +144,7 @@ apply Rmult_le_reg_r with (bpow (ex - prec)).
apply bpow_gt_0.
rewrite <- bpow_plus.
replace (prec - 1 + (ex - prec))%Z with (ex - 1)%Z by ring.
change (bpow (ex - 1) <= F2R (Float beta (Zabs (Ztrunc (x * bpow (- (ex - prec))))) (ex - prec)))%R.
change (bpow (ex - 1) <= F2R (Float beta (Z.abs (Ztrunc (x * bpow (- (ex - prec))))) (ex - prec)))%R.
rewrite F2R_Zabs, <- Hx2.
apply Hx4.
apply Zle_minus_le_0.
......@@ -155,11 +155,11 @@ apply Rmult_lt_reg_r with (bpow (ex - prec)).
apply bpow_gt_0.
rewrite <- bpow_plus.
replace (prec + (ex - prec))%Z with ex by ring.
change (F2R (Float beta (Zabs (Ztrunc (x * bpow (- (ex - prec))))) (ex - prec)) < bpow ex)%R.
change (F2R (Float beta (Z.abs (Ztrunc (x * bpow (- (ex - prec))))) (ex - prec)) < bpow ex)%R.
rewrite F2R_Zabs, <- Hx2.
apply Hx4.
now apply Zlt_le_weak.
now apply Zge_le.
now apply Z.ge_le.
Qed.
Theorem FTZ_format_satisfies_any :
......@@ -185,7 +185,7 @@ apply generic_inclusion_ge.
intros e He.
unfold FTZ_exp.
rewrite Zlt_bool_false.
apply Zle_refl.
apply Z.le_refl.
omega.
Qed.
......@@ -326,7 +326,7 @@ unfold FTZ_exp.
generalize (Zlt_cases (ex - prec) emin).
case Zlt_bool.
intros _.
apply Zle_refl.
apply Z.le_refl.
intros He'.
elim Rlt_not_le with (1 := Hx).
apply Rle_trans with (2 := proj1 He).
......
......@@ -27,7 +27,7 @@ Notation bpow e := (bpow beta e).
Theorem Rcompare_F2R :
forall e m1 m2 : Z,
Rcompare (F2R (Float beta m1 e)) (F2R (Float beta m2 e)) = Zcompare m1 m2.
Rcompare (F2R (Float beta m1 e)) (F2R (Float beta m2 e)) = Z.compare m1 m2.
Proof.
intros e m1 m2.
unfold F2R. simpl.
......@@ -108,7 +108,7 @@ Qed.
Theorem F2R_Zabs:
forall m e : Z,
F2R (Float beta (Zabs m) e) = Rabs (F2R (Float beta m e)).
F2R (Float beta (Z.abs m) e) = Rabs (F2R (Float beta m e)).
Proof.
intros m e.
unfold F2R.
......@@ -123,7 +123,7 @@ Qed.
Theorem F2R_Zopp :
forall m e : Z,
F2R (Float beta (Zopp m) e) = Ropp (F2R (Float beta m e)).
F2R (Float beta (Z.opp m) e) = Ropp (F2R (Float beta m e)).
Proof.
intros m e.
unfold F2R. simpl.
......@@ -365,7 +365,7 @@ Qed.
Theorem F2R_lt_bpow :
forall f : float beta, forall e',
(Zabs (Fnum f) < Zpower beta (e' - Fexp f))%Z ->
(Z.abs (Fnum f) < Zpower beta (e' - Fexp f))%Z ->
(Rabs (F2R f) < bpow e')%R.
Proof.
intros (m, e) e' Hm.
......@@ -402,7 +402,7 @@ Qed.
Theorem F2R_prec_normalize :
forall m e e' p : Z,
(Zabs m < Zpower beta p)%Z ->
(Z.abs m < Zpower beta p)%Z ->
(bpow (e' - 1)%Z <= Rabs (F2R (Float beta m e)))%R ->
F2R (Float beta m e) = F2R (Float beta (m * Zpower beta (e - e' + p)) (e' - p)).
Proof.
......@@ -514,7 +514,7 @@ assert (He: (e2 < e1)%Z).
apply Znot_ge_lt.
intros H0.
elim Rlt_not_le with (1 := H21).
apply Zge_le in H0.
apply Z.ge_le in H0.
apply (F2R_change_exp e1 m2 e2) in H0.
rewrite H0.
apply F2R_le.
......@@ -535,14 +535,14 @@ simpl.
apply sym_eq.
apply mag_unique.
assert (H2 : (bpow (e1' - 1) <= F2R (Float beta m1 e1) < bpow e1')%R).
rewrite <- (Zabs_eq m1), F2R_Zabs.
rewrite <- (Z.abs_eq m1), F2R_Zabs.
apply H1.
apply Rgt_not_eq.
apply Rlt_gt.
now apply F2R_gt_0.
now apply Zlt_le_weak.
clear H1.
rewrite <- F2R_Zabs, Zabs_eq.
rewrite <- F2R_Zabs, Z.abs_eq.
split.
apply Rlt_le.
apply Rle_lt_trans with (2 := H12).
......
......@@ -50,7 +50,7 @@ Proof.
intros k l Hk H.
apply Znot_ge_lt.
intros Hl.
apply Zge_le in Hl.
apply Z.ge_le in Hl.
assert (H' := proj2 (proj2 (valid_exp l) Hl) k).
omega.
Qed.
......@@ -63,8 +63,8 @@ Proof.
intros k l Hk H.
apply Znot_ge_lt.
intros H'.
apply Zge_le in H'.
assert (Hl := Zle_trans _ _ _ H H').
apply Z.ge_le in H'.
assert (Hl := Z.le_trans _ _ _ H H').
apply valid_exp in Hl.
assert (H1 := proj2 Hl k H').
omega.
......@@ -150,7 +150,7 @@ now apply valid_exp_.
rewrite <- H.
apply valid_exp.
rewrite H.
apply Zle_refl.
apply Z.le_refl.
Qed.
Theorem generic_format_F2R :
......@@ -159,7 +159,7 @@ Theorem generic_format_F2R :
generic_format (F2R (Float beta m e)).
Proof.
intros m e.
destruct (Z_eq_dec m 0) as [Zm|Zm].
destruct (Z.eq_dec m 0) as [Zm|Zm].
intros _.
rewrite Zm, F2R_0.
apply generic_format_0.
......@@ -204,7 +204,7 @@ Qed.
Theorem canonical_abs :
forall m e,
canonical (Float beta m e) ->
canonical (Float beta (Zabs m) e).
canonical (Float beta (Z.abs m) e).
Proof.
intros m e H.
unfold canonical.
......@@ -386,7 +386,7 @@ simpl.
specialize (Ex' Zx).
apply (mantissa_small_pos _ _ Ex').
assert (ex' <= fexp ex)%Z.
apply Zle_trans with (2 := He).
apply Z.le_trans with (2 := He).
apply bpow_lt_bpow with beta.
now apply Rle_lt_trans with (2 := Ex).
now rewrite (proj2 (proj2 (valid_exp _) He)).
......@@ -404,7 +404,7 @@ apply Rlt_le_trans with (1 := bpow_mag_gt beta _).
apply bpow_le.
unfold scaled_mantissa.
rewrite mag_mult_bpow with (1 := Zx).
apply Zle_refl.
apply Z.le_refl.
Qed.
Theorem mag_generic_gt :
......@@ -418,13 +418,13 @@ unfold cexp.
destruct (mag beta x) as (ex,Ex) ; simpl.
specialize (Ex Zx).
intros H.
apply Zge_le in H.
apply Z.ge_le in H.
generalize (scaled_mantissa_lt_1 x ex (proj2 Ex) H).
contradict Zx.
rewrite Gx.
replace (Ztrunc (scaled_mantissa x)) with Z0.
apply F2R_0.
cut (Zabs (Ztrunc (scaled_mantissa x)) < 1)%Z.
cut (Z.abs (Ztrunc (scaled_mantissa x)) < 1)%Z.
clear ; zify ; omega.
apply lt_IZR.
rewrite abs_IZR.
......@@ -591,7 +591,7 @@ omega.
intros H.
rewrite <- H in Hx.
rewrite Zfloor_IZR, Zrnd_IZR in Hx.
apply Zlt_irrefl with (1 := Hx).
apply Z.lt_irrefl with (1 := Hx).
Qed.
Theorem Zrnd_ZR_or_AW :
......@@ -727,7 +727,7 @@ assert (Heq: fexp ex = fexp ey -> (round x <= round y)%R).
destruct (Zle_or_lt ey (fexp ey)) as [Hy1|Hy1].
apply Heq.
apply valid_exp with (1 := Hy1).
now apply Zle_trans with ey.
now apply Z.le_trans with ey.
destruct (Zle_lt_or_eq _ _ He) as [He'|He'].
2: now apply Heq, f_equal.
apply Rle_trans with (bpow (ey - 1)).
......@@ -827,7 +827,7 @@ Section Zround_opp.
Variable rnd : R -> Z.
Context { valid_rnd : Valid_rnd rnd }.
Definition Zrnd_opp x := Zopp (rnd (-x)).
Definition Zrnd_opp x := Z.opp (rnd (-x)).
Global Instance valid_rnd_opp : Valid_rnd Zrnd_opp.
Proof with auto with typeclass_instances.
......@@ -836,14 +836,14 @@ split.
intros x y Hxy.
unfold Zrnd_opp.
apply Zopp_le_cancel.
rewrite 2!Zopp_involutive.
rewrite 2!Z.opp_involutive.
apply Zrnd_le...
now apply Ropp_le_contravar.
(* *)
intros n.
unfold Zrnd_opp.
rewrite <- opp_IZR, Zrnd_IZR...
apply Zopp_involutive.
apply Z.opp_involutive.
Qed.
Theorem round_opp :
......@@ -855,7 +855,7 @@ unfold round.
rewrite <- F2R_Zopp, cexp_opp, scaled_mantissa_opp.
apply F2R_eq.
apply sym_eq.
exact (Zopp_involutive _).
exact (Z.opp_involutive _).
Qed.
End Zround_opp.
......@@ -1077,7 +1077,7 @@ unfold round.
rewrite scaled_mantissa_opp.
rewrite <- F2R_Zopp.
unfold Zceil.
rewrite Zopp_involutive.
rewrite Z.opp_involutive.
now rewrite cexp_opp.
Qed.
......@@ -1422,7 +1422,7 @@ Theorem mag_round :
forall rnd {Hrnd : Valid_rnd rnd} x,
(round rnd x <> 0)%R ->
(mag beta (round rnd x) = mag beta x :> Z) \/
Rabs (round rnd x) = bpow (Zmax (mag beta x) (fexp (mag beta x))).
Rabs (round rnd x) = bpow (Z.max (mag beta x) (fexp (mag beta x))).
Proof with auto with typeclass_instances.
intros rnd Hrnd x.
destruct (round_ZR_or_AW rnd x) as [Hr|Hr] ; rewrite Hr ; clear Hr rnd Hrnd.
......@@ -1437,7 +1437,7 @@ rewrite <- mag_abs.
rewrite <- round_AW_abs.
destruct (Zle_or_lt ex (fexp ex)) as [He|He].
right.
rewrite Zmax_r with (1 := He).
rewrite Z.max_r with (1 := He).
rewrite round_AW_UP with (1 := Rabs_pos _).
now apply round_UP_small_pos.
destruct (round_bounded_large_pos Zaway _ ex He Ex) as (H1,[H2|H2]).
......@@ -1446,7 +1446,7 @@ apply mag_unique.
rewrite <- round_AW_abs, Rabs_Rabsolu.
now split.
right.
now rewrite Zmax_l with (1 := Zlt_le_weak _ _ He).
now rewrite Z.max_l with (1 := Zlt_le_weak _ _ He).
Qed.
Theorem mag_DN :
......@@ -1588,7 +1588,7 @@ Proof with auto with typeclass_instances.
intros x.
destruct (round_ZR_or_AW rnd x) as [H|H] ; rewrite H ; clear H ; intros Zr.
rewrite mag_round_ZR with (1 := Zr).
apply Zle_refl.
apply Z.le_refl.
apply mag_le_abs.
contradict Zr.
rewrite Zr.
......@@ -1644,7 +1644,7 @@ Theorem Znearest_ge_floor :
Proof.
intros x.
destruct (Znearest_DN_or_UP x) as [Hx|Hx] ; rewrite Hx.
apply Zle_refl.
apply Z.le_refl.
apply le_IZR.
apply Rle_trans with x.
apply Zfloor_lb.
......@@ -1661,7 +1661,7 @@ apply le_IZR.
apply Rle_trans with x.
apply Zfloor_lb.
apply Zceil_ub.
apply Zle_refl.
apply Z.le_refl.
Qed.
Global Instance valid_rnd_N : Valid_rnd Znearest.
......@@ -1670,8 +1670,8 @@ split.
(* *)
intros x y Hxy.
destruct (Rle_or_lt (IZR (Zceil x)) y) as [H|H].
apply Zle_trans with (1 := Znearest_le_ceil x).
apply Zle_trans with (2 := Znearest_ge_floor y).