From 177c8fbc523a171e8c8470fa675f9a69ef7f99de Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Wed, 8 Mar 2017 08:35:29 +0100
Subject: Adapt proofs to future handling of literal constants in Coq.

This commit is mainly a squash of the relevant compatibility commits from
Flocq's master. Most of the changes are meant to make the proofs oblivious
to the way constants such as 0, 1, 2, and -1 are represented.
---
 flocq/Core/Fcore_FLT.v         |  2 +-
 flocq/Core/Fcore_FTZ.v         |  8 +++---
 flocq/Core/Fcore_Raux.v        | 56 ++++++++++++++++++++++--------------------
 flocq/Core/Fcore_float_prop.v  |  4 +--
 flocq/Core/Fcore_generic_fmt.v | 34 ++++++++++++-------------
 flocq/Core/Fcore_rnd_ne.v      |  2 +-
 flocq/Core/Fcore_ulp.v         | 21 +++-------------
 7 files changed, 58 insertions(+), 69 deletions(-)

(limited to 'flocq/Core')

diff --git a/flocq/Core/Fcore_FLT.v b/flocq/Core/Fcore_FLT.v
index 372af6ad..53dc48a7 100644
--- a/flocq/Core/Fcore_FLT.v
+++ b/flocq/Core/Fcore_FLT.v
@@ -187,7 +187,7 @@ Qed.
 
 (** Links between FLT and FIX (underflow) *)
 Theorem canonic_exp_FLT_FIX :
-  forall x, x <> R0 ->
+  forall x, x <> 0%R ->
   (Rabs x < bpow (emin + prec))%R ->
   canonic_exp beta FLT_exp x = canonic_exp beta (FIX_exp emin) x.
 Proof.
diff --git a/flocq/Core/Fcore_FTZ.v b/flocq/Core/Fcore_FTZ.v
index 2ebc7851..a2fab00b 100644
--- a/flocq/Core/Fcore_FTZ.v
+++ b/flocq/Core/Fcore_FTZ.v
@@ -217,7 +217,7 @@ Variable rnd : R -> Z.
 Context { valid_rnd : Valid_rnd rnd }.
 
 Definition Zrnd_FTZ x :=
-  if Rle_bool R1 (Rabs x) then rnd x else Z0.
+  if Rle_bool 1 (Rabs x) then rnd x else Z0.
 
 Global Instance valid_rnd_FTZ : Valid_rnd Zrnd_FTZ.
 Proof with auto with typeclass_instances.
@@ -270,7 +270,7 @@ Proof.
 intros x Hx.
 unfold round, scaled_mantissa, canonic_exp.
 destruct (ln_beta beta x) as (ex, He). simpl.
-assert (Hx0: x <> R0).
+assert (Hx0: x <> 0%R).
 intros Hx0.
 apply Rle_not_lt with (1 := Hx).
 rewrite Hx0, Rabs_R0.
@@ -286,7 +286,7 @@ rewrite Rle_bool_true.
 apply refl_equal.
 rewrite Rabs_mult.
 rewrite (Rabs_pos_eq (bpow (- FLX_exp prec ex))).
-change R1 with (bpow 0).
+change 1%R with (bpow 0).
 rewrite <- (Zplus_opp_r (FLX_exp prec ex)).
 rewrite bpow_plus.
 apply Rmult_le_compat_r.
@@ -320,7 +320,7 @@ rewrite Rle_bool_false.
 apply F2R_0.
 rewrite Rabs_mult.
 rewrite (Rabs_pos_eq (bpow (- FTZ_exp ex))).
-change R1 with (bpow 0).
+change 1%R with (bpow 0).
 rewrite <- (Zplus_opp_r (FTZ_exp ex)).
 rewrite bpow_plus.
 apply Rmult_lt_compat_r.
diff --git a/flocq/Core/Fcore_Raux.v b/flocq/Core/Fcore_Raux.v
index 939002cf..44db6c35 100644
--- a/flocq/Core/Fcore_Raux.v
+++ b/flocq/Core/Fcore_Raux.v
@@ -403,7 +403,7 @@ Definition Z2R n :=
   match n with
   | Zpos p => P2R p
   | Zneg p => Ropp (P2R p)
-  | Z0 => R0
+  | Z0 => 0%R
   end.
 
 Theorem P2R_INR :
@@ -432,10 +432,13 @@ Theorem Z2R_IZR :
   forall n, Z2R n = IZR n.
 Proof.
 intro.
-case n ; intros ; simpl.
+case n ; intros ; unfold Z2R.
 apply refl_equal.
+rewrite <- positive_nat_Z, <- INR_IZR_INZ.
 apply P2R_INR.
+change (IZR (Zneg p)) with (Ropp (IZR (Zpos p))).
 apply Ropp_eq_compat.
+rewrite <- positive_nat_Z, <- INR_IZR_INZ.
 apply P2R_INR.
 Qed.
 
@@ -1193,7 +1196,7 @@ unfold Ztrunc.
 case Rlt_bool_spec ; intro H.
 apply refl_equal.
 rewrite (Rle_antisym _ _ Hx H).
-fold (Z2R 0).
+change 0%R with (Z2R 0).
 rewrite Zceil_Z2R.
 apply Zfloor_Z2R.
 Qed.
@@ -1304,7 +1307,7 @@ unfold Zaway.
 case Rlt_bool_spec ; intro H.
 apply refl_equal.
 rewrite (Rle_antisym _ _ Hx H).
-fold (Z2R 0).
+change 0%R with (Z2R 0).
 rewrite Zfloor_Z2R.
 apply Zceil_Z2R.
 Qed.
@@ -1456,7 +1459,7 @@ Definition bpow e :=
   match e with
   | Zpos p => Z2R (Zpower_pos r p)
   | Zneg p => Rinv (Z2R (Zpower_pos r p))
-  | Z0 => R1
+  | Z0 => 1%R
   end.
 
 Theorem Z2R_Zpower_pos :
@@ -1532,13 +1535,13 @@ Qed.
 Theorem bpow_opp :
   forall e : Z, (bpow (-e) = /bpow e)%R.
 Proof.
-intros e; destruct e.
-simpl; now rewrite Rinv_1.
-now replace (-Zpos p)%Z with (Zneg p) by reflexivity.
-replace (-Zneg p)%Z with (Zpos p) by reflexivity.
+intros [|p|p].
+apply eq_sym, Rinv_1.
+now change (-Zpos p)%Z with (Zneg p).
+change (-Zneg p)%Z with (Zpos p).
 simpl; rewrite Rinv_involutive; trivial.
-generalize (bpow_gt_0 (Zpos p)).
-simpl; auto with real.
+apply Rgt_not_eq.
+apply (bpow_gt_0 (Zpos p)).
 Qed.
 
 Theorem Z2R_Zpower_nat :
@@ -1872,7 +1875,7 @@ apply bpow_ge_0.
 Qed.
 
 Theorem ln_beta_mult_bpow :
-  forall x e, x <> R0 ->
+  forall x e, x <> 0%R ->
   (ln_beta (x * bpow e) = ln_beta x + e :>Z)%Z.
 Proof.
 intros x e Zx.
@@ -1895,7 +1898,7 @@ Qed.
 
 Theorem ln_beta_le_bpow :
   forall x e,
-  x <> R0 ->
+  x <> 0%R ->
   (Rabs x < bpow e)%R ->
   (ln_beta x <= e)%Z.
 Proof.
@@ -2044,20 +2047,19 @@ destruct Hex as (Hex0,Hex1); [now apply Rgt_not_eq|].
 assert (Haxy : (Rabs (x + y) < bpow (ex + 1))%R).
 { rewrite bpow_plus1.
   apply Rlt_le_trans with (2 * bpow ex)%R.
-  - apply Rle_lt_trans with (2 * Rabs x)%R.
-    + rewrite Rabs_right.
-      { apply Rle_trans with (x + x)%R; [now apply Rplus_le_compat_l|].
-        rewrite Rabs_right.
-        { rewrite Rmult_plus_distr_r.
-          rewrite Rmult_1_l.
-          now apply Rle_refl. }
-        now apply Rgt_ge. }
-      apply Rgt_ge.
-      rewrite <- (Rplus_0_l 0).
-      now apply Rplus_gt_compat.
-    + now apply Rmult_lt_compat_l; intuition.
-  - apply Rmult_le_compat_r; [now apply bpow_ge_0|].
-    now change 2%R with (Z2R 2); apply Z2R_le. }
+  - rewrite Rabs_pos_eq.
+    apply Rle_lt_trans with (2 * Rabs x)%R.
+    + rewrite Rabs_pos_eq.
+      replace (2 * x)%R with (x + x)%R by ring.
+      now apply Rplus_le_compat_l.
+      now apply Rlt_le.
+    + apply Rmult_lt_compat_l with (2 := Hex1).
+      exact Rlt_0_2.
+    + rewrite <- (Rplus_0_l 0).
+      now apply Rlt_le, Rplus_lt_compat.
+  - apply Rmult_le_compat_r.
+    now apply bpow_ge_0.
+    now apply (Z2R_le 2). }
 assert (Haxy2 : (bpow (ex - 1) <= Rabs (x + y))%R).
 { apply (Rle_trans _ _ _ Hex0).
   rewrite Rabs_right; [|now apply Rgt_ge].
diff --git a/flocq/Core/Fcore_float_prop.v b/flocq/Core/Fcore_float_prop.v
index 8199ede6..a183bf0a 100644
--- a/flocq/Core/Fcore_float_prop.v
+++ b/flocq/Core/Fcore_float_prop.v
@@ -136,7 +136,7 @@ Qed.
 (** Sign facts *)
 Theorem F2R_0 :
   forall e : Z,
-  F2R (Float beta 0 e) = R0.
+  F2R (Float beta 0 e) = 0%R.
 Proof.
 intros e.
 unfold F2R. simpl.
@@ -145,7 +145,7 @@ Qed.
 
 Theorem F2R_eq_0_reg :
   forall m e : Z,
-  F2R (Float beta m e) = R0 ->
+  F2R (Float beta m e) = 0%R ->
   m = Z0.
 Proof.
 intros m e H.
diff --git a/flocq/Core/Fcore_generic_fmt.v b/flocq/Core/Fcore_generic_fmt.v
index 21e51890..668b4da2 100644
--- a/flocq/Core/Fcore_generic_fmt.v
+++ b/flocq/Core/Fcore_generic_fmt.v
@@ -252,7 +252,7 @@ apply Rmult_1_r.
 Qed.
 
 Theorem scaled_mantissa_0 :
-  scaled_mantissa 0 = R0.
+  scaled_mantissa 0 = 0%R.
 Proof.
 apply Rmult_0_l.
 Qed.
@@ -667,7 +667,7 @@ Theorem round_bounded_small_pos :
   forall x ex,
   (ex <= fexp ex)%Z ->
   (bpow (ex - 1) <= x < bpow ex)%R ->
-  round x = R0 \/ round x = bpow (fexp ex).
+  round x = 0%R \/ round x = bpow (fexp ex).
 Proof.
 intros x ex He Hx.
 unfold round, scaled_mantissa.
@@ -751,19 +751,19 @@ now apply sym_eq.
 Qed.
 
 Theorem round_0 :
-  round 0 = R0.
+  round 0 = 0%R.
 Proof.
 unfold round, scaled_mantissa.
 rewrite Rmult_0_l.
-fold (Z2R 0).
+change 0%R with (Z2R 0).
 rewrite Zrnd_Z2R.
 apply F2R_0.
 Qed.
 
 Theorem exp_small_round_0_pos :
   forall x ex,
- (bpow (ex - 1) <= x < bpow ex)%R ->
-   round x =R0 -> (ex <= fexp ex)%Z .
+  (bpow (ex - 1) <= x < bpow ex)%R ->
+  round x = 0%R -> (ex <= fexp ex)%Z .
 Proof.
 intros x ex H H1.
 case (Zle_or_lt ex (fexp ex)); trivial; intros V.
@@ -771,7 +771,7 @@ contradict H1.
 apply Rgt_not_eq.
 apply Rlt_le_trans with (bpow (ex-1)).
 apply bpow_gt_0.
-apply  (round_bounded_large_pos); assumption.
+apply (round_bounded_large_pos); assumption.
 Qed.
 
 Theorem generic_format_round_pos :
@@ -931,7 +931,7 @@ rewrite <- Ropp_0.
 now apply Ropp_lt_contravar.
 now apply Ropp_le_contravar.
 (* . 0 <= y *)
-apply Rle_trans with R0.
+apply Rle_trans with 0%R.
 apply F2R_le_0_compat. simpl.
 rewrite <- (Zrnd_Z2R rnd 0).
 apply Zrnd_le...
@@ -1020,7 +1020,7 @@ Qed.
 Theorem exp_small_round_0 :
   forall rnd {Hr : Valid_rnd rnd} x ex,
   (bpow (ex - 1) <= Rabs x < bpow ex)%R ->
-   round rnd x =R0 -> (ex <= fexp ex)%Z .
+   round rnd x = 0%R -> (ex <= fexp ex)%Z .
 Proof.
 intros rnd Hr x ex H1 H2.
 generalize Rabs_R0.
@@ -1177,7 +1177,7 @@ rewrite <- (Rmult_0_l (bpow (- canonic_exp x))).
 apply Rmult_le_compat_r with (2 := Hx).
 apply bpow_ge_0.
 rewrite <- H.
-change R0 with (Z2R 0).
+change 0%R with (Z2R 0).
 now rewrite Zfloor_Z2R, Zceil_Z2R.
 Qed.
 
@@ -1212,7 +1212,7 @@ rewrite <- (Rmult_0_l (bpow (- canonic_exp x))).
 apply Rmult_le_compat_r with (2 := Hx).
 apply bpow_ge_0.
 rewrite <- H.
-change R0 with (Z2R 0).
+change 0%R with (Z2R 0).
 now rewrite Zfloor_Z2R, Zceil_Z2R.
 Qed.
 
@@ -1296,7 +1296,7 @@ Theorem round_DN_small_pos :
   forall x ex,
   (bpow (ex - 1) <= x < bpow ex)%R ->
   (ex <= fexp ex)%Z ->
-  round Zfloor x = R0.
+  round Zfloor x = 0%R.
 Proof.
 intros x ex Hx He.
 rewrite <- (F2R_0 beta (canonic_exp x)).
@@ -1552,7 +1552,7 @@ Qed.
 
 Lemma canonic_exp_le_bpow :
   forall (x : R) (e : Z),
-  x <> R0 ->
+  x <> 0%R ->
   (Rabs x < bpow e)%R ->
   (canonic_exp x <= fexp e)%Z.
 Proof.
@@ -1578,7 +1578,7 @@ Context { valid_rnd : Valid_rnd rnd }.
 
 Theorem ln_beta_round_ge :
   forall x,
-  round rnd x <> R0 ->
+  round rnd x <> 0%R ->
   (ln_beta beta x <= ln_beta beta (round rnd x))%Z.
 Proof with auto with typeclass_instances.
 intros x.
@@ -1597,7 +1597,7 @@ Qed.
 
 Theorem canonic_exp_round_ge :
   forall x,
-  round rnd x <> R0 ->
+  round rnd x <> 0%R ->
   (canonic_exp x <= canonic_exp (round rnd x))%Z.
 Proof with auto with typeclass_instances.
 intros x Zr.
@@ -1807,7 +1807,7 @@ rewrite Zceil_floor_neq.
 rewrite Z2R_plus.
 simpl.
 apply Ropp_lt_cancel.
-apply Rplus_lt_reg_l with R1.
+apply Rplus_lt_reg_l with 1%R.
 replace (1 + -/2)%R with (/2)%R by field.
 now replace (1 + - (Z2R (Zfloor x) + 1 - x))%R with (x - Z2R (Zfloor x))%R by ring.
 apply Rlt_not_eq.
@@ -1866,7 +1866,7 @@ rewrite Z2R_abs, Z2R_minus.
 replace (Z2R (Znearest x) - Z2R n)%R with (- (x - Z2R (Znearest x)) + (x - Z2R n))%R by ring.
 apply Rle_lt_trans with (1 := Rabs_triang _ _).
 simpl.
-replace R1 with (/2 + /2)%R by field.
+replace 1%R with (/2 + /2)%R by field.
 apply Rplus_le_lt_compat with (2 := Hd).
 rewrite Rabs_Ropp.
 apply Znearest_N.
diff --git a/flocq/Core/Fcore_rnd_ne.v b/flocq/Core/Fcore_rnd_ne.v
index 1f265406..2d67e709 100644
--- a/flocq/Core/Fcore_rnd_ne.v
+++ b/flocq/Core/Fcore_rnd_ne.v
@@ -370,7 +370,7 @@ destruct (Rle_or_lt (round beta fexp Zfloor x) 0) as [Hr|Hr].
 rewrite (Rle_antisym _ _ Hr).
 unfold scaled_mantissa.
 rewrite Rmult_0_l.
-change R0 with (Z2R 0).
+change 0%R with (Z2R 0).
 now rewrite (Ztrunc_Z2R 0).
 rewrite <- (round_0 beta fexp Zfloor).
 apply round_le...
diff --git a/flocq/Core/Fcore_ulp.v b/flocq/Core/Fcore_ulp.v
index 28d2bc35..3bc0eac3 100644
--- a/flocq/Core/Fcore_ulp.v
+++ b/flocq/Core/Fcore_ulp.v
@@ -18,6 +18,7 @@ COPYING file for more details.
 *)
 
 (** * Unit in the Last Place: our definition using fexp and its properties, successor and predecessor *)
+Require Import Reals Psatz.
 Require Import Fcore_Raux.
 Require Import Fcore_defs.
 Require Import Fcore_rnd.
@@ -2002,7 +2003,7 @@ rewrite Hx in Hfx; contradict Hfx; auto with real.
 intros H.
 apply Rle_trans with (1:=error_le_half_ulp _ _).
 apply Rmult_le_compat_l.
-auto with real.
+apply Rlt_le, pos_half_prf.
 apply ulp_le.
 rewrite Hx; rewrite (Rabs_left1 x), Rabs_left; try assumption.
 apply Ropp_le_contravar.
@@ -2018,7 +2019,7 @@ case (Rle_or_lt 0 (round beta fexp Zceil x)).
 intros H; destruct H.
 apply Rle_trans with (1:=error_le_half_ulp _ _).
 apply Rmult_le_compat_l.
-auto with real.
+apply Rlt_le, pos_half_prf.
 apply ulp_le_pos; trivial.
 case (Rle_or_lt 0 x); trivial.
 intros H1; contradict H.
@@ -2234,21 +2235,7 @@ apply generic_format_0.
 left; apply Rlt_le_trans with (1:=H).
 rewrite V1,V2; right; field.
 (* *)
-assert (T: (u < (u + succ u) / 2 < succ u)%R).
-split.
-apply Rmult_lt_reg_l with 2%R.
-now auto with real.
-apply Rplus_lt_reg_l with (-u)%R.
-apply Rle_lt_trans with u;[right; ring|idtac].
-apply Rlt_le_trans with (1:=V).
-right; field.
-apply Rmult_lt_reg_l with 2%R.
-now auto with real.
-apply Rplus_lt_reg_l with (-succ u)%R.
-apply Rle_lt_trans with u;[right; field|idtac].
-apply Rlt_le_trans with (1:=V).
-right; ring.
-(* *)
+assert (T: (u < (u + succ u) / 2 < succ u)%R) by lra.
 destruct T as (T1,T2).
 apply Rnd_N_pt_monotone with F v ((u + succ u) / 2)%R...
 apply round_N_pt...
-- 
cgit