1 files changed, 559 insertions, 0 deletions
diff --git a/flocq/Core/Float_prop.v b/flocq/Core/Float_prop.v
new file mode 100644
index 00000000..804dd397
--- /dev/null
+++ b/flocq/Core/Float_prop.v
@@ -0,0 +1,559 @@
+(**
+This file is part of the Flocq formalization of floating-point
+arithmetic in Coq: http://flocq.gforge.inria.fr/
+
+Copyright (C) 2009-2018 Sylvie Boldo
+#<br />#
+Copyright (C) 2009-2018 Guillaume Melquiond
+
+This library is free software; you can redistribute it and/or
+modify it under the terms of the GNU Lesser General Public
+License as published by the Free Software Foundation; either
+version 3 of the License, or (at your option) any later version.
+
+This library is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+COPYING file for more details.
+*)
+
+(** * Basic properties of floating-point formats: lemmas about mantissa, exponent... *)
+Require Import Raux Defs Digits.
+
+Section Float_prop.
+
+Variable beta : radix.
+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)) = Z.compare m1 m2.
+Proof.
+intros e m1 m2.
+unfold F2R. simpl.
+rewrite Rcompare_mult_r.
+apply Rcompare_IZR.
+apply bpow_gt_0.
+Qed.
+
+(** Basic facts *)
+Theorem le_F2R :
+  forall e m1 m2 : Z,
+  (F2R (Float beta m1 e) <= F2R (Float beta m2 e))%R ->
+  (m1 <= m2)%Z.
+Proof.
+intros e m1 m2 H.
+apply le_IZR.
+apply Rmult_le_reg_r with (bpow e).
+apply bpow_gt_0.
+exact H.
+Qed.
+
+Theorem F2R_le :
+  forall m1 m2 e : Z,
+  (m1 <= m2)%Z ->
+  (F2R (Float beta m1 e) <= F2R (Float beta m2 e))%R.
+Proof.
+intros m1 m2 e H.
+unfold F2R. simpl.
+apply Rmult_le_compat_r.
+apply bpow_ge_0.
+now apply IZR_le.
+Qed.
+
+Theorem lt_F2R :
+  forall e m1 m2 : Z,
+  (F2R (Float beta m1 e) < F2R (Float beta m2 e))%R ->
+  (m1 < m2)%Z.
+Proof.
+intros e m1 m2 H.
+apply lt_IZR.
+apply Rmult_lt_reg_r with (bpow e).
+apply bpow_gt_0.
+exact H.
+Qed.
+
+Theorem F2R_lt :
+  forall e m1 m2 : Z,
+  (m1 < m2)%Z ->
+  (F2R (Float beta m1 e) < F2R (Float beta m2 e))%R.
+Proof.
+intros e m1 m2 H.
+unfold F2R. simpl.
+apply Rmult_lt_compat_r.
+apply bpow_gt_0.
+now apply IZR_lt.
+Qed.
+
+Theorem F2R_eq :
+  forall e m1 m2 : Z,
+  (m1 = m2)%Z ->
+  (F2R (Float beta m1 e) = F2R (Float beta m2 e))%R.
+Proof.
+intros e m1 m2 H.
+now apply (f_equal (fun m => F2R (Float beta m e))).
+Qed.
+
+Theorem eq_F2R :
+  forall e m1 m2 : Z,
+  F2R (Float beta m1 e) = F2R (Float beta m2 e) ->
+  m1 = m2.
+Proof.
+intros e m1 m2 H.
+apply Zle_antisym ;
+  apply le_F2R with e ;
+  rewrite H ;
+  apply Rle_refl.
+Qed.
+
+Theorem F2R_Zabs:
+  forall m e : Z,
+   F2R (Float beta (Z.abs m) e) = Rabs (F2R (Float beta m e)).
+Proof.
+intros m e.
+unfold F2R.
+rewrite Rabs_mult.
+rewrite <- abs_IZR.
+simpl.
+apply f_equal.
+apply sym_eq; apply Rabs_right.
+apply Rle_ge.
+apply bpow_ge_0.
+Qed.
+
+Theorem F2R_Zopp :
+  forall m e : Z,
+  F2R (Float beta (Z.opp m) e) = Ropp (F2R (Float beta m e)).
+Proof.
+intros m e.
+unfold F2R. simpl.
+rewrite <- Ropp_mult_distr_l_reverse.
+now rewrite opp_IZR.
+Qed.
+
+Theorem F2R_cond_Zopp :
+  forall b m e,
+  F2R (Float beta (cond_Zopp b m) e) = cond_Ropp b (F2R (Float beta m e)).
+Proof.
+intros [|] m e ; unfold F2R ; simpl.
+now rewrite opp_IZR, Ropp_mult_distr_l_reverse.
+apply refl_equal.
+Qed.
+
+(** Sign facts *)
+Theorem F2R_0 :
+  forall e : Z,
+  F2R (Float beta 0 e) = 0%R.
+Proof.
+intros e.
+unfold F2R. simpl.
+apply Rmult_0_l.
+Qed.
+
+Theorem eq_0_F2R :
+  forall m e : Z,
+  F2R (Float beta m e) = 0%R ->
+  m = Z0.
+Proof.
+intros m e H.
+apply eq_F2R with e.
+now rewrite F2R_0.
+Qed.
+
+Theorem ge_0_F2R :
+  forall m e : Z,
+  (0 <= F2R (Float beta m e))%R ->
+  (0 <= m)%Z.
+Proof.
+intros m e H.
+apply le_F2R with e.
+now rewrite F2R_0.
+Qed.
+
+Theorem le_0_F2R :
+  forall m e : Z,
+  (F2R (Float beta m e) <= 0)%R ->
+  (m <= 0)%Z.
+Proof.
+intros m e H.
+apply le_F2R with e.
+now rewrite F2R_0.
+Qed.
+
+Theorem gt_0_F2R :
+  forall m e : Z,
+  (0 < F2R (Float beta m e))%R ->
+  (0 < m)%Z.
+Proof.
+intros m e H.
+apply lt_F2R with e.
+now rewrite F2R_0.
+Qed.
+
+Theorem lt_0_F2R :
+  forall m e : Z,
+  (F2R (Float beta m e) < 0)%R ->
+  (m < 0)%Z.
+Proof.
+intros m e H.
+apply lt_F2R with e.
+now rewrite F2R_0.
+Qed.
+
+Theorem F2R_ge_0 :
+  forall f : float beta,
+  (0 <= Fnum f)%Z ->
+  (0 <= F2R f)%R.
+Proof.
+intros f H.
+rewrite <- F2R_0 with (Fexp f).
+now apply F2R_le.
+Qed.
+
+Theorem F2R_le_0 :
+  forall f : float beta,
+  (Fnum f <= 0)%Z ->
+  (F2R f <= 0)%R.
+Proof.
+intros f H.
+rewrite <- F2R_0 with (Fexp f).
+now apply F2R_le.
+Qed.
+
+Theorem F2R_gt_0 :
+  forall f : float beta,
+  (0 < Fnum f)%Z ->
+  (0 < F2R f)%R.
+Proof.
+intros f H.
+rewrite <- F2R_0 with (Fexp f).
+now apply F2R_lt.
+Qed.
+
+Theorem F2R_lt_0 :
+  forall f : float beta,
+  (Fnum f < 0)%Z ->
+  (F2R f < 0)%R.
+Proof.
+intros f H.
+rewrite <- F2R_0 with (Fexp f).
+now apply F2R_lt.
+Qed.
+
+Theorem F2R_neq_0 :
+ forall f : float beta,
+  (Fnum f <> 0)%Z ->
+  (F2R f <> 0)%R.
+Proof.
+intros f H H1.
+apply H.
+now apply eq_0_F2R with (Fexp f).
+Qed.
+
+
+Lemma Fnum_ge_0: forall (f : float beta),
+  (0 <= F2R f)%R -> (0 <= Fnum f)%Z.
+Proof.
+intros f H.
+case (Zle_or_lt 0 (Fnum f)); trivial.
+intros H1; contradict H.
+apply Rlt_not_le.
+now apply F2R_lt_0.
+Qed.
+
+Lemma Fnum_le_0: forall (f : float beta),
+  (F2R f <= 0)%R -> (Fnum f <= 0)%Z.
+Proof.
+intros f H.
+case (Zle_or_lt (Fnum f) 0); trivial.
+intros H1; contradict H.
+apply Rlt_not_le.
+now apply F2R_gt_0.
+Qed.
+
+(** Floats and bpow *)
+Theorem F2R_bpow :
+  forall e : Z,
+  F2R (Float beta 1 e) = bpow e.
+Proof.
+intros e.
+unfold F2R. simpl.
+apply Rmult_1_l.
+Qed.
+
+Theorem bpow_le_F2R :
+  forall m e : Z,
+  (0 < m)%Z ->
+  (bpow e <= F2R (Float beta m e))%R.
+Proof.
+intros m e H.
+rewrite <- F2R_bpow.
+apply F2R_le.
+now apply (Zlt_le_succ 0).
+Qed.
+
+Theorem F2R_p1_le_bpow :
+  forall m e1 e2 : Z,
+  (0 < m)%Z ->
+  (F2R (Float beta m e1) < bpow e2)%R ->
+  (F2R (Float beta (m + 1) e1) <= bpow e2)%R.
+Proof.
+intros m e1 e2 Hm.
+intros H.
+assert (He : (e1 <= e2)%Z).
+(* . *)
+apply (le_bpow beta).
+apply Rle_trans with (F2R (Float beta m e1)).
+unfold F2R. simpl.
+rewrite <- (Rmult_1_l (bpow e1)) at 1.
+apply Rmult_le_compat_r.
+apply bpow_ge_0.
+apply IZR_le.
+now apply (Zlt_le_succ 0).
+now apply Rlt_le.
+(* . *)
+revert H.
+replace e2 with (e2 - e1 + e1)%Z by ring.
+rewrite bpow_plus.
+unfold F2R. simpl.
+rewrite <- (IZR_Zpower beta (e2 - e1)).
+intros H.
+apply Rmult_le_compat_r.
+apply bpow_ge_0.
+apply Rmult_lt_reg_r in H.
+apply IZR_le.
+apply Zlt_le_succ.
+now apply lt_IZR.
+apply bpow_gt_0.
+now apply Zle_minus_le_0.
+Qed.
+
+Theorem bpow_le_F2R_m1 :
+  forall m e1 e2 : Z,
+  (1 < m)%Z ->
+  (bpow e2 < F2R (Float beta m e1))%R ->
+  (bpow e2 <= F2R (Float beta (m - 1) e1))%R.
+Proof.
+intros m e1 e2 Hm.
+case (Zle_or_lt e1 e2); intros He.
+replace e2 with (e2 - e1 + e1)%Z by ring.
+rewrite bpow_plus.
+unfold F2R. simpl.
+rewrite <- (IZR_Zpower beta (e2 - e1)).
+intros H.
+apply Rmult_le_compat_r.
+apply bpow_ge_0.
+apply Rmult_lt_reg_r in H.
+apply IZR_le.
+rewrite (Zpred_succ (Zpower _ _)).
+apply Zplus_le_compat_r.
+apply Zlt_le_succ.
+now apply lt_IZR.
+apply bpow_gt_0.
+now apply Zle_minus_le_0.
+intros H.
+apply Rle_trans with (1*bpow e1)%R.
+rewrite Rmult_1_l.
+apply bpow_le.
+now apply Zlt_le_weak.
+unfold F2R. simpl.
+apply Rmult_le_compat_r.
+apply bpow_ge_0.
+apply IZR_le.
+omega.
+Qed.
+
+Theorem F2R_lt_bpow :
+  forall f : float beta, forall e',
+  (Z.abs (Fnum f) < Zpower beta (e' - Fexp f))%Z ->
+  (Rabs (F2R f) < bpow e')%R.
+Proof.
+intros (m, e) e' Hm.
+rewrite <- F2R_Zabs.
+destruct (Zle_or_lt e e') as [He|He].
+unfold F2R. simpl.
+apply Rmult_lt_reg_r with (bpow (-e)).
+apply bpow_gt_0.
+rewrite Rmult_assoc, <- 2!bpow_plus, Zplus_opp_r, Rmult_1_r.
+rewrite <-IZR_Zpower. 2: now apply Zle_left.
+now apply IZR_lt.
+elim Zlt_not_le with (1 := Hm).
+simpl.
+cut (e' - e < 0)%Z. 2: omega.
+clear.
+case (e' - e)%Z ; try easy.
+intros p _.
+apply Zabs_pos.
+Qed.
+
+Theorem F2R_change_exp :
+  forall e' m e : Z,
+  (e' <= e)%Z ->
+  F2R (Float beta m e) = F2R (Float beta (m * Zpower beta (e - e')) e').
+Proof.
+intros e' m e He.
+unfold F2R. simpl.
+rewrite mult_IZR, IZR_Zpower, Rmult_assoc.
+apply f_equal.
+pattern e at 1 ; replace e with (e - e' + e')%Z by ring.
+apply bpow_plus.
+now apply Zle_minus_le_0.
+Qed.
+
+Theorem F2R_prec_normalize :
+  forall m e e' 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.
+intros m e e' p Hm Hf.
+assert (Hp: (0 <= p)%Z).
+destruct p ; try easy.
+now elim (Zle_not_lt _ _ (Zabs_pos m)).
+(* . *)
+replace (e - e' + p)%Z with (e - (e' - p))%Z by ring.
+apply F2R_change_exp.
+cut (e' - 1 < e + p)%Z. omega.
+apply (lt_bpow beta).
+apply Rle_lt_trans with (1 := Hf).
+rewrite <- F2R_Zabs, Zplus_comm, bpow_plus.
+apply Rmult_lt_compat_r.
+apply bpow_gt_0.
+rewrite <- IZR_Zpower.
+now apply IZR_lt.
+exact Hp.
+Qed.
+
+(** Floats and mag *)
+Theorem mag_F2R_bounds :
+  forall x m e, (0 < m)%Z ->
+  (F2R (Float beta m e) <= x < F2R (Float beta (m + 1) e))%R ->
+  mag beta x = mag beta (F2R (Float beta m e)) :> Z.
+Proof.
+intros x m e Hp (Hx,Hx2).
+destruct (mag beta (F2R (Float beta m e))) as (ex, He).
+simpl.
+apply mag_unique.
+assert (Hp1: (0 < F2R (Float beta m e))%R).
+now apply F2R_gt_0.
+specialize (He (Rgt_not_eq _ _ Hp1)).
+rewrite Rabs_pos_eq in He. 2: now apply Rlt_le.
+destruct He as (He1, He2).
+assert (Hx1: (0 < x)%R).
+now apply Rlt_le_trans with (2 := Hx).
+rewrite Rabs_pos_eq. 2: now apply Rlt_le.
+split.
+now apply Rle_trans with (1 := He1).
+apply Rlt_le_trans with (1 := Hx2).
+now apply F2R_p1_le_bpow.
+Qed.
+
+Theorem mag_F2R :
+  forall m e : Z,
+  m <> Z0 ->
+  (mag beta (F2R (Float beta m e)) = mag beta (IZR m) + e :> Z)%Z.
+Proof.
+intros m e H.
+unfold F2R ; simpl.
+apply mag_mult_bpow.
+now apply IZR_neq.
+Qed.
+
+Theorem Zdigits_mag :
+  forall n,
+  n <> Z0 ->
+  Zdigits beta n = mag beta (IZR n).
+Proof.
+intros n Hn.
+destruct (mag beta (IZR n)) as (e, He) ; simpl.
+specialize (He (IZR_neq _ _ Hn)).
+rewrite <- abs_IZR in He.
+assert (Hd := Zdigits_correct beta n).
+assert (Hd' := Zdigits_gt_0 beta n).
+apply Zle_antisym ; apply (bpow_lt_bpow beta).
+apply Rle_lt_trans with (2 := proj2 He).
+rewrite <- IZR_Zpower by omega.
+now apply IZR_le.
+apply Rle_lt_trans with (1 := proj1 He).
+rewrite <- IZR_Zpower by omega.
+now apply IZR_lt.
+Qed.
+
+Theorem mag_F2R_Zdigits :
+  forall m e, m <> Z0 ->
+  (mag beta (F2R (Float beta m e)) = Zdigits beta m + e :> Z)%Z.
+Proof.
+intros m e Hm.
+rewrite mag_F2R with (1 := Hm).
+apply (f_equal (fun v => Zplus v e)).
+apply sym_eq.
+now apply Zdigits_mag.
+Qed.
+
+Theorem mag_F2R_bounds_Zdigits :
+  forall x m e, (0 < m)%Z ->
+  (F2R (Float beta m e) <= x < F2R (Float beta (m + 1) e))%R ->
+  mag beta x = (Zdigits beta m + e)%Z :> Z.
+Proof.
+intros x m e Hm Bx.
+apply mag_F2R_bounds with (1 := Hm) in Bx.
+rewrite Bx.
+apply mag_F2R_Zdigits.
+now apply Zgt_not_eq.
+Qed.
+
+Theorem float_distribution_pos :
+  forall m1 e1 m2 e2 : Z,
+  (0 < m1)%Z ->
+  (F2R (Float beta m1 e1) < F2R (Float beta m2 e2) < F2R (Float beta (m1 + 1) e1))%R ->
+  (e2 < e1)%Z /\ (e1 + mag beta (IZR m1) = e2 + mag beta (IZR m2))%Z.
+Proof.
+intros m1 e1 m2 e2 Hp1 (H12, H21).
+assert (He: (e2 < e1)%Z).
+(* . *)
+apply Znot_ge_lt.
+intros H0.
+elim Rlt_not_le with (1 := H21).
+apply Z.ge_le in H0.
+apply (F2R_change_exp e1 m2 e2) in H0.
+rewrite H0.
+apply F2R_le.
+apply Zlt_le_succ.
+apply (lt_F2R e1).
+now rewrite <- H0.
+(* . *)
+split.
+exact He.
+rewrite (Zplus_comm e1), (Zplus_comm e2).
+assert (Hp2: (0 < m2)%Z).
+apply (gt_0_F2R m2 e2).
+apply Rlt_trans with (2 := H12).
+now apply F2R_gt_0.
+rewrite <- 2!mag_F2R.
+destruct (mag beta (F2R (Float beta m1 e1))) as (e1', H1).
+simpl.
+apply sym_eq.
+apply mag_unique.
+assert (H2 : (bpow (e1' - 1) <= F2R (Float beta m1 e1) < bpow e1')%R).
+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, Z.abs_eq.
+split.
+apply Rlt_le.
+apply Rle_lt_trans with (2 := H12).
+apply H2.
+apply Rlt_le_trans with (1 := H21).
+now apply F2R_p1_le_bpow.
+now apply Zlt_le_weak.
+apply sym_not_eq.
+now apply Zlt_not_eq.
+apply sym_not_eq.
+now apply Zlt_not_eq.
+Qed.
+
+End Float_prop.