Sterbenz.v 4.38 KB
Newer Older
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1
(**
2 3 4
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/

Guillaume Melquiond's avatar
Guillaume Melquiond committed
5
Copyright (C) 2010-2018 Sylvie Boldo
BOLDO Sylvie's avatar
BOLDO Sylvie committed
6
#<br />#
Guillaume Melquiond's avatar
Guillaume Melquiond committed
7
Copyright (C) 2010-2018 Guillaume Melquiond
8 9 10 11 12 13 14 15 16 17 18 19

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.
*)

BOLDO Sylvie's avatar
BOLDO Sylvie committed
20
(** * Sterbenz conditions for exact subtraction *)
21

22
Require Import Raux Defs Generic_fmt Operations.
23 24 25 26 27 28 29

Section Fprop_Sterbenz.

Variable beta : radix.
Notation bpow e := (bpow beta e).

Variable fexp : Z -> Z.
30
Context { valid_exp : Valid_exp fexp }.
31
Context { monotone_exp : Monotone_exp fexp }.
32 33
Notation format := (generic_format beta fexp).

34 35 36
Theorem generic_format_plus :
  forall x y,
  format x -> format y ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
37
  (Rabs (x + y) <= bpow (Zmin (mag beta x) (mag beta y)))%R ->
38 39 40 41 42 43 44 45 46 47
  format (x + y)%R.
Proof.
intros x y Fx Fy Hxy.
destruct (Req_dec (x + y) 0) as [Zxy|Zxy].
rewrite Zxy.
apply generic_format_0.
destruct (Req_dec x R0) as [Zx|Zx].
now rewrite Zx, Rplus_0_l.
destruct (Req_dec y R0) as [Zy|Zy].
now rewrite Zy, Rplus_0_r.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
48
destruct Hxy as [Hxy|Hxy].
49
revert Hxy.
50
destruct (mag beta x) as (ex, Ex). simpl.
51
specialize (Ex Zx).
52
destruct (mag beta y) as (ey, Ey). simpl.
53 54 55 56 57
specialize (Ey Zy).
intros Hxy.
set (fx := Float beta (Ztrunc (scaled_mantissa beta fexp x)) (fexp ex)).
assert (Hx: x = F2R fx).
rewrite Fx at 1.
58
unfold cexp.
59
now rewrite mag_unique with (1 := Ex).
60 61 62
set (fy := Float beta (Ztrunc (scaled_mantissa beta fexp y)) (fexp ey)).
assert (Hy: y = F2R fy).
rewrite Fy at 1.
63
unfold cexp.
64
now rewrite mag_unique with (1 := Ey).
65
rewrite Hx, Hy.
66
rewrite <- F2R_plus.
67 68
apply generic_format_F2R.
intros _.
69
case_eq (Fplus fx fy).
70
intros mxy exy Pxy.
71
rewrite <- Pxy, F2R_plus, <- Hx, <- Hy.
72
unfold cexp.
73 74
replace exy with (fexp (Zmin ex ey)).
apply monotone_exp.
75
now apply mag_le_bpow.
76
replace exy with (Fexp (Fplus fx fy)) by exact (f_equal Fexp Pxy).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
77
rewrite Fexp_Fplus.
78
simpl. clear -monotone_exp.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
79
apply sym_eq.
80
destruct (Zmin_spec ex ey) as [(H1,H2)|(H1,H2)] ; rewrite H2.
81
apply Zmin_l.
82
now apply monotone_exp.
83
apply Zmin_r.
84 85 86
apply monotone_exp.
apply Zlt_le_weak.
now apply Zgt_lt.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
87 88 89 90
apply generic_format_abs_inv.
rewrite Hxy.
apply generic_format_bpow.
apply valid_exp.
91
case (Zmin_spec (mag beta x) (mag beta y)); intros (H1,H2);
BOLDO Sylvie's avatar
BOLDO Sylvie committed
92
   rewrite H2; now apply mag_generic_gt.
93 94
Qed.

95 96 97 98 99 100 101 102 103 104 105 106
Theorem generic_format_plus_weak :
  forall x y,
  format x -> format y ->
  (Rabs (x + y) <= Rmin (Rabs x) (Rabs y))%R ->
  format (x + y)%R.
Proof.
intros x y Fx Fy Hxy.
destruct (Req_dec x R0) as [Zx|Zx].
now rewrite Zx, Rplus_0_l.
destruct (Req_dec y R0) as [Zy|Zy].
now rewrite Zy, Rplus_0_r.
apply generic_format_plus ; try assumption.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
107
apply Rle_trans with (1 := Hxy).
108 109
unfold Rmin.
destruct (Rle_dec (Rabs x) (Rabs y)) as [Hxy'|Hxy'].
110
rewrite Zmin_l.
111
destruct (mag beta x) as (ex, Hx).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
112
apply Rlt_le; now apply Hx.
113
now apply mag_le_abs.
114
rewrite Zmin_r.
115
destruct (mag beta y) as (ex, Hy).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
116
apply Rlt_le; now apply Hy.
117
apply mag_le_abs.
118 119 120 121 122
exact Zy.
apply Rlt_le.
now apply Rnot_le_lt.
Qed.

123
Lemma sterbenz_aux :
124 125 126 127 128
  forall x y, format x -> format y ->
  (y <= x <= 2 * y)%R ->
  format (x - y)%R.
Proof.
intros x y Hx Hy (Hxy1, Hxy2).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
129 130 131 132 133 134 135
unfold Rminus.
apply generic_format_plus_weak.
exact Hx.
now apply generic_format_opp.
rewrite Rabs_pos_eq.
rewrite Rabs_Ropp.
rewrite Rmin_comm.
136 137 138 139
assert (Hy0: (0 <= y)%R).
apply Rplus_le_reg_r with y.
apply Rle_trans with x.
now rewrite Rplus_0_l.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
140
now replace (y + y)%R with (2 * y)%R by ring.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
141 142 143 144
rewrite Rabs_pos_eq with (1 := Hy0).
rewrite Rabs_pos_eq.
unfold Rmin.
destruct (Rle_dec y x) as [Hyx|Hyx].
145
apply Rplus_le_reg_r with y.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
146 147 148 149
now ring_simplify.
now elim Hyx.
now apply Rle_trans with y.
now apply Rle_0_minus.
150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172
Qed.

Theorem sterbenz :
  forall x y, format x -> format y ->
  (y / 2 <= x <= 2 * y)%R ->
  format (x - y)%R.
Proof.
intros x y Hx Hy (Hxy1, Hxy2).
destruct (Rle_or_lt x y) as [Hxy|Hxy].
rewrite <- Ropp_minus_distr.
apply generic_format_opp.
apply sterbenz_aux ; try easy.
split.
exact Hxy.
apply Rcompare_not_Lt_inv.
rewrite <- Rcompare_half_r.
now apply Rcompare_not_Lt.
apply sterbenz_aux ; try easy.
split.
now apply Rlt_le.
exact Hxy2.
Qed.

173
End Fprop_Sterbenz.