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/Prop/Fprop_Sterbenz.v       |  2 +-
 flocq/Prop/Fprop_div_sqrt_error.v |  9 ++++-----
 flocq/Prop/Fprop_plus_error.v     |  6 +++---
 flocq/Prop/Fprop_relative.v       | 13 +++++++------
 4 files changed, 15 insertions(+), 15 deletions(-)

(limited to 'flocq/Prop')

diff --git a/flocq/Prop/Fprop_Sterbenz.v b/flocq/Prop/Fprop_Sterbenz.v
index 7260d2e1..4e74f889 100644
--- a/flocq/Prop/Fprop_Sterbenz.v
+++ b/flocq/Prop/Fprop_Sterbenz.v
@@ -133,7 +133,7 @@ assert (Hy0: (0 <= y)%R).
 apply Rplus_le_reg_r with y.
 apply Rle_trans with x.
 now rewrite Rplus_0_l.
-now rewrite Rmult_plus_distr_r, Rmult_1_l in Hxy2.
+now replace (y + y)%R with (2 * y)%R by ring.
 rewrite Rabs_pos_eq with (1 := Hy0).
 rewrite Rabs_pos_eq.
 unfold Rmin.
diff --git a/flocq/Prop/Fprop_div_sqrt_error.v b/flocq/Prop/Fprop_div_sqrt_error.v
index 9d29001d..422b6b64 100644
--- a/flocq/Prop/Fprop_div_sqrt_error.v
+++ b/flocq/Prop/Fprop_div_sqrt_error.v
@@ -103,7 +103,7 @@ apply Rlt_le_trans with (Rabs x * 1)%R.
 apply Rmult_lt_compat_l.
 now apply Rabs_pos_lt.
 apply Rlt_le_trans with (1 := Heps1).
-change R1 with (bpow 0).
+change 1%R with (bpow 0).
 apply bpow_le.
 generalize (prec_gt_0 prec).
 clear ; omega.
@@ -191,7 +191,7 @@ apply Rsqr_le_abs_1.
 apply Rle_trans with (1 := Rabs_triang _ _).
 rewrite Rabs_R1.
 apply Rplus_le_reg_l with (-1)%R.
-rewrite <- Rplus_assoc, Rplus_opp_l, Rplus_0_l.
+replace (-1 + (1 + Rabs eps))%R with (Rabs eps) by ring.
 apply Rle_trans with (1 := Heps1).
 rewrite Rabs_pos_eq.
 apply Rmult_le_reg_l with 2%R.
@@ -256,8 +256,7 @@ replace (prec+(Fexp fr+Fexp fr))%Z with (Fexp fr + (prec+Fexp fr))%Z by ring.
 rewrite bpow_plus, Rmult_assoc.
 apply Rmult_lt_compat_l.
 apply bpow_gt_0.
-apply Rmult_lt_reg_l with 2%R.
-auto with real.
+apply Rmult_lt_reg_l with (1 := Rlt_0_2).
 apply Rle_lt_trans with (Rabs (F2R fr + sqrt x)).
 right; field.
 apply Rle_lt_trans with (1:=Rabs_triang _ _).
@@ -273,7 +272,7 @@ rewrite <- Hr1; auto.
 apply Rlt_le_trans with (bpow (prec + Fexp fr)+ Rabs (sqrt x))%R.
 now apply Rplus_lt_compat_r.
 (* . *)
-rewrite Rmult_plus_distr_r, Rmult_1_l.
+replace (2 * bpow (prec + Fexp fr))%R with (bpow (prec + Fexp fr) + bpow (prec + Fexp fr))%R by ring.
 apply Rplus_le_compat_l.
 assert (sqrt x <> 0)%R.
 apply Rgt_not_eq.
diff --git a/flocq/Prop/Fprop_plus_error.v b/flocq/Prop/Fprop_plus_error.v
index 950ca267..41c2f031 100644
--- a/flocq/Prop/Fprop_plus_error.v
+++ b/flocq/Prop/Fprop_plus_error.v
@@ -157,7 +157,7 @@ Lemma round_plus_eq_zero_aux :
   (canonic_exp beta fexp x <= canonic_exp beta fexp y)%Z ->
   format x -> format y ->
   (0 <= x + y)%R ->
-  round beta fexp rnd (x + y) = R0 ->
+  round beta fexp rnd (x + y) = 0%R ->
   (x + y = 0)%R.
 Proof with auto with typeclass_instances.
 intros x y He Hx Hy Hp Hxy.
@@ -202,11 +202,11 @@ Context { valid_rnd : Valid_rnd rnd }.
 Theorem round_plus_eq_zero :
   forall x y,
   format x -> format y ->
-  round beta fexp rnd (x + y) = R0 ->
+  round beta fexp rnd (x + y) = 0%R ->
   (x + y = 0)%R.
 Proof with auto with typeclass_instances.
 intros x y Hx Hy.
-destruct (Rle_or_lt R0 (x + y)) as [H1|H1].
+destruct (Rle_or_lt 0 (x + y)) as [H1|H1].
 (* . *)
 revert H1.
 destruct (Zle_or_lt (canonic_exp beta fexp x) (canonic_exp beta fexp y)) as [H2|H2].
diff --git a/flocq/Prop/Fprop_relative.v b/flocq/Prop/Fprop_relative.v
index 585b71da..276ccd3b 100644
--- a/flocq/Prop/Fprop_relative.v
+++ b/flocq/Prop/Fprop_relative.v
@@ -44,7 +44,7 @@ Proof with auto with typeclass_instances.
 intros x b Hb0 Hxb.
 destruct (Req_dec x 0) as [Hx0|Hx0].
 (* *)
-exists R0.
+exists 0%R.
 split.
 now rewrite Rabs_R0.
 rewrite Hx0, Rmult_0_l.
@@ -71,7 +71,7 @@ Proof with auto with typeclass_instances.
 intros x b Hb0 Hxb.
 destruct (Req_dec x 0) as [Hx0|Hx0].
 (* *)
-exists R0.
+exists 0%R.
 split.
 now rewrite Rabs_R0.
 rewrite Hx0, Rmult_0_l.
@@ -588,7 +588,7 @@ rewrite Rabs_right;[assumption|apply Rle_ge; now left].
 exists eps; exists 0%R.
 split;[assumption|split].
 rewrite Rabs_R0; apply Rmult_le_pos.
-auto with real.
+apply Rlt_le, pos_half_prf.
 apply bpow_ge_0.
 split;[apply Rmult_0_r|idtac].
 now rewrite Rplus_0_r.
@@ -596,13 +596,14 @@ now rewrite Rplus_0_r.
 exists 0%R; exists (round beta (FLT_exp emin prec) (Znearest choice) x - x)%R.
 split.
 rewrite Rabs_R0; apply Rmult_le_pos.
-auto with real.
+apply Rlt_le, pos_half_prf.
 apply bpow_ge_0.
 split.
 apply Rle_trans with (/2*ulp beta (FLT_exp emin prec) x)%R.
 apply error_le_half_ulp.
 now apply FLT_exp_valid.
-apply Rmult_le_compat_l; auto with real.
+apply Rmult_le_compat_l.
+apply Rlt_le, pos_half_prf.
 rewrite ulp_neq_0.
 2: now apply Rgt_not_eq.
 apply bpow_le.
@@ -650,7 +651,7 @@ destruct (Rtotal_order x 0) as [Nx|[Zx|Px]].
   { apply (Rmult_le_reg_l 2 _ _ Rlt_0_2).
     rewrite Rmult_0_r, Rinv_r; [exact Rle_0_1|].
     apply Rgt_not_eq, Rlt_gt, Rlt_0_2. }
-  exists R0; exists R0; rewrite Zx; split; [|split; [|split]].
+  exists 0%R; exists 0%R; rewrite Zx; split; [|split; [|split]].
   { now rewrite Rabs_R0; apply Rmult_le_pos; [|apply bpow_ge_0]. }
   { now rewrite Rabs_R0; apply Rmult_le_pos; [|apply bpow_ge_0]. }
   { now rewrite Rmult_0_l. }
-- 
cgit