Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.
This file is part of the Flocq formalization of floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/
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.
Sterbenz conditions for exact subtraction

Require Import Raux Defs Generic_fmt Operations.

Section Fprop_Sterbenz.

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

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

Theorem generic_format_plus :
  forall x y,
  format x -> format y ->
  (Rabs (x + y) <= bpow (Z.min (mag beta x) (mag beta y)))%R ->
  format (x + y)%R.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
forall x y : R,
format x ->
format y ->
(Rabs (x + y) <=
 bpow (Z.min (mag beta x) (mag beta y)))%R ->
format (x + y)
Proof.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
forall x y : R,
format x ->
format y ->
(Rabs (x + y) <=
 bpow (Z.min (mag beta x) (mag beta y)))%R ->
format (x + y)
intros x y Fx Fy Hxy.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:(Rabs (x + y) <=
 bpow (Z.min (mag beta x) (mag beta y)))%R
format (x + y)
destruct (Req_dec (x + y) 0) as [Zxy|Zxy].beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:(Rabs (x + y) <=
 bpow (Z.min (mag beta x) (mag beta y)))%R
Zxy:(x + y)%R = 0%R
format (x + y)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:(Rabs (x + y) <=
 bpow (Z.min (mag beta x) (mag beta y)))%R
Zxy:(x + y)%R <> 0%R
format (x + y)
rewrite Zxy.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:(Rabs (x + y) <=
 bpow (Z.min (mag beta x) (mag beta y)))%R
Zxy:(x + y)%R = 0%R
format 0
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:(Rabs (x + y) <=
 bpow (Z.min (mag beta x) (mag beta y)))%R
Zxy:(x + y)%R <> 0%R
format (x + y)
apply generic_format_0.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:(Rabs (x + y) <=
 bpow (Z.min (mag beta x) (mag beta y)))%R
Zxy:(x + y)%R <> 0%R
format (x + y)
destruct (Req_dec x R0) as [Zx|Zx].beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:(Rabs (x + y) <=
 bpow (Z.min (mag beta x) (mag beta y)))%R
Zxy:(x + y)%R <> 0%R
Zx:x = R0
format (x + y)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:(Rabs (x + y) <=
 bpow (Z.min (mag beta x) (mag beta y)))%R
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
format (x + y)
now rewrite Zx, Rplus_0_l.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:(Rabs (x + y) <=
 bpow (Z.min (mag beta x) (mag beta y)))%R
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
format (x + y)
destruct (Req_dec y R0) as [Zy|Zy].beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:(Rabs (x + y) <=
 bpow (Z.min (mag beta x) (mag beta y)))%R
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y = R0
format (x + y)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:(Rabs (x + y) <=
 bpow (Z.min (mag beta x) (mag beta y)))%R
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
format (x + y)
now rewrite Zy, Rplus_0_r.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:(Rabs (x + y) <=
 bpow (Z.min (mag beta x) (mag beta y)))%R
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
format (x + y)
destruct Hxy as [Hxy|Hxy].beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:(Rabs (x + y) <
 bpow (Z.min (mag beta x) (mag beta y)))%R
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
format (x + y)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:Rabs (x + y) =
bpow (Z.min (mag beta x) (mag beta y))
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
format (x + y)
revert Hxy.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
(Rabs (x + y) < bpow (Z.min (mag beta x) (mag beta y)))%R ->
format (x + y)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:Rabs (x + y) =
bpow (Z.min (mag beta x) (mag beta y))
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
format (x + y)
destruct (mag beta x) as (ex, Ex).beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
ex:Z
Ex:x <> 0%R -> (bpow (ex - 1) <= Rabs x < bpow ex)%R
(Rabs (x + y) <
 bpow
   (Z.min (Build_mag_prop beta x ex Ex) (mag beta y)))%R ->
format (x + y)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:Rabs (x + y) =
bpow (Z.min (mag beta x) (mag beta y))
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
format (x + y) simpl.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
ex:Z
Ex:x <> 0%R -> (bpow (ex - 1) <= Rabs x < bpow ex)%R
(Rabs (x + y) < bpow (Z.min ex (mag beta y)))%R ->
format (x + y)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:Rabs (x + y) =
bpow (Z.min (mag beta x) (mag beta y))
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
format (x + y)
specialize (Ex Zx).beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
ex:Z
Ex:(bpow (ex - 1) <= Rabs x < bpow ex)%R
(Rabs (x + y) < bpow (Z.min ex (mag beta y)))%R ->
format (x + y)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:Rabs (x + y) =
bpow (Z.min (mag beta x) (mag beta y))
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
format (x + y)
destruct (mag beta y) as (ey, Ey).beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
ex:Z
Ex:(bpow (ex - 1) <= Rabs x < bpow ex)%R
ey:Z
Ey:y <> 0%R -> (bpow (ey - 1) <= Rabs y < bpow ey)%R
(Rabs (x + y) <
 bpow (Z.min ex (Build_mag_prop beta y ey Ey)))%R ->
format (x + y)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:Rabs (x + y) =
bpow (Z.min (mag beta x) (mag beta y))
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
format (x + y) simpl.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
ex:Z
Ex:(bpow (ex - 1) <= Rabs x < bpow ex)%R
ey:Z
Ey:y <> 0%R -> (bpow (ey - 1) <= Rabs y < bpow ey)%R
(Rabs (x + y) < bpow (Z.min ex ey))%R ->
format (x + y)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:Rabs (x + y) =
bpow (Z.min (mag beta x) (mag beta y))
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
format (x + y)
specialize (Ey Zy).beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
ex:Z
Ex:(bpow (ex - 1) <= Rabs x < bpow ex)%R
ey:Z
Ey:(bpow (ey - 1) <= Rabs y < bpow ey)%R
(Rabs (x + y) < bpow (Z.min ex ey))%R ->
format (x + y)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:Rabs (x + y) =
bpow (Z.min (mag beta x) (mag beta y))
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
format (x + y)
intros Hxy.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
ex:Z
Ex:(bpow (ex - 1) <= Rabs x < bpow ex)%R
ey:Z
Ey:(bpow (ey - 1) <= Rabs y < bpow ey)%R
Hxy:(Rabs (x + y) < bpow (Z.min ex ey))%R
format (x + y)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:Rabs (x + y) =
bpow (Z.min (mag beta x) (mag beta y))
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
format (x + y)
set (fx := Float beta (Ztrunc (scaled_mantissa beta fexp x)) (fexp ex)).beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
ex:Z
Ex:(bpow (ex - 1) <= Rabs x < bpow ex)%R
ey:Z
Ey:(bpow (ey - 1) <= Rabs y < bpow ey)%R
Hxy:(Rabs (x + y) < bpow (Z.min ex ey))%R
fx:={|
Fnum := Ztrunc (scaled_mantissa beta fexp x);
Fexp := fexp ex |}:float beta
format (x + y)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:Rabs (x + y) =
bpow (Z.min (mag beta x) (mag beta y))
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
format (x + y)
assert (Hx: x = F2R fx).beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
ex:Z
Ex:(bpow (ex - 1) <= Rabs x < bpow ex)%R
ey:Z
Ey:(bpow (ey - 1) <= Rabs y < bpow ey)%R
Hxy:(Rabs (x + y) < bpow (Z.min ex ey))%R
fx:={|
Fnum := Ztrunc (scaled_mantissa beta fexp x);
Fexp := fexp ex |}:float beta
x = F2R fx
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
ex:Z
Ex:(bpow (ex - 1) <= Rabs x < bpow ex)%R
ey:Z
Ey:(bpow (ey - 1) <= Rabs y < bpow ey)%R
Hxy:(Rabs (x + y) < bpow (Z.min ex ey))%R
fx:={|
Fnum := Ztrunc (scaled_mantissa beta fexp x);
Fexp := fexp ex |}:float beta
Hx:x = F2R fx
format (x + y)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:Rabs (x + y) =
bpow (Z.min (mag beta x) (mag beta y))
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
format (x + y)
rewrite Fx at 1.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
ex:Z
Ex:(bpow (ex - 1) <= Rabs x < bpow ex)%R
ey:Z
Ey:(bpow (ey - 1) <= Rabs y < bpow ey)%R
Hxy:(Rabs (x + y) < bpow (Z.min ex ey))%R
fx:={|
Fnum := Ztrunc (scaled_mantissa beta fexp x);
Fexp := fexp ex |}:float beta
F2R
  {|
  Fnum := Ztrunc (scaled_mantissa beta fexp x);
  Fexp := cexp beta fexp x |} = F2R fx
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
ex:Z
Ex:(bpow (ex - 1) <= Rabs x < bpow ex)%R
ey:Z
Ey:(bpow (ey - 1) <= Rabs y < bpow ey)%R
Hxy:(Rabs (x + y) < bpow (Z.min ex ey))%R
fx:={|
Fnum := Ztrunc (scaled_mantissa beta fexp x);
Fexp := fexp ex |}:float beta
Hx:x = F2R fx
format (x + y)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:Rabs (x + y) =
bpow (Z.min (mag beta x) (mag beta y))
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
format (x + y)
unfold cexp.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
ex:Z
Ex:(bpow (ex - 1) <= Rabs x < bpow ex)%R
ey:Z
Ey:(bpow (ey - 1) <= Rabs y < bpow ey)%R
Hxy:(Rabs (x + y) < bpow (Z.min ex ey))%R
fx:={|
Fnum := Ztrunc (scaled_mantissa beta fexp x);
Fexp := fexp ex |}:float beta
F2R
  {|
  Fnum := Ztrunc (scaled_mantissa beta fexp x);
  Fexp := fexp (mag beta x) |} = F2R fx
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
ex:Z
Ex:(bpow (ex - 1) <= Rabs x < bpow ex)%R
ey:Z
Ey:(bpow (ey - 1) <= Rabs y < bpow ey)%R
Hxy:(Rabs (x + y) < bpow (Z.min ex ey))%R
fx:={|
Fnum := Ztrunc (scaled_mantissa beta fexp x);
Fexp := fexp ex |}:float beta
Hx:x = F2R fx
format (x + y)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:Rabs (x + y) =
bpow (Z.min (mag beta x) (mag beta y))
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
format (x + y)
now rewrite mag_unique with (1 := Ex).beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
ex:Z
Ex:(bpow (ex - 1) <= Rabs x < bpow ex)%R
ey:Z
Ey:(bpow (ey - 1) <= Rabs y < bpow ey)%R
Hxy:(Rabs (x + y) < bpow (Z.min ex ey))%R
fx:={|
Fnum := Ztrunc (scaled_mantissa beta fexp x);
Fexp := fexp ex |}:float beta
Hx:x = F2R fx
format (x + y)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:Rabs (x + y) =
bpow (Z.min (mag beta x) (mag beta y))
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
format (x + y)
set (fy := Float beta (Ztrunc (scaled_mantissa beta fexp y)) (fexp ey)).beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
ex:Z
Ex:(bpow (ex - 1) <= Rabs x < bpow ex)%R
ey:Z
Ey:(bpow (ey - 1) <= Rabs y < bpow ey)%R
Hxy:(Rabs (x + y) < bpow (Z.min ex ey))%R
fx:={|
Fnum := Ztrunc (scaled_mantissa beta fexp x);
Fexp := fexp ex |}:float beta
Hx:x = F2R fx
fy:={|
Fnum := Ztrunc (scaled_mantissa beta fexp y);
Fexp := fexp ey |}:float beta
format (x + y)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:Rabs (x + y) =
bpow (Z.min (mag beta x) (mag beta y))
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
format (x + y)
assert (Hy: y = F2R fy).beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
ex:Z
Ex:(bpow (ex - 1) <= Rabs x < bpow ex)%R
ey:Z
Ey:(bpow (ey - 1) <= Rabs y < bpow ey)%R
Hxy:(Rabs (x + y) < bpow (Z.min ex ey))%R
fx:={|
Fnum := Ztrunc (scaled_mantissa beta fexp x);
Fexp := fexp ex |}:float beta
Hx:x = F2R fx
fy:={|
Fnum := Ztrunc (scaled_mantissa beta fexp y);
Fexp := fexp ey |}:float beta
y = F2R fy
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
ex:Z
Ex:(bpow (ex - 1) <= Rabs x < bpow ex)%R
ey:Z
Ey:(bpow (ey - 1) <= Rabs y < bpow ey)%R
Hxy:(Rabs (x + y) < bpow (Z.min ex ey))%R
fx:={|
Fnum := Ztrunc (scaled_mantissa beta fexp x);
Fexp := fexp ex |}:float beta
Hx:x = F2R fx
fy:={|
Fnum := Ztrunc (scaled_mantissa beta fexp y);
Fexp := fexp ey |}:float beta
Hy:y = F2R fy
format (x + y)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:Rabs (x + y) =
bpow (Z.min (mag beta x) (mag beta y))
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
format (x + y)
rewrite Fy at 1.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
ex:Z
Ex:(bpow (ex - 1) <= Rabs x < bpow ex)%R
ey:Z
Ey:(bpow (ey - 1) <= Rabs y < bpow ey)%R
Hxy:(Rabs (x + y) < bpow (Z.min ex ey))%R
fx:={|
Fnum := Ztrunc (scaled_mantissa beta fexp x);
Fexp := fexp ex |}:float beta
Hx:x = F2R fx
fy:={|
Fnum := Ztrunc (scaled_mantissa beta fexp y);
Fexp := fexp ey |}:float beta
F2R
  {|
  Fnum := Ztrunc (scaled_mantissa beta fexp y);
  Fexp := cexp beta fexp y |} = F2R fy
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
ex:Z
Ex:(bpow (ex - 1) <= Rabs x < bpow ex)%R
ey:Z
Ey:(bpow (ey - 1) <= Rabs y < bpow ey)%R
Hxy:(Rabs (x + y) < bpow (Z.min ex ey))%R
fx:={|
Fnum := Ztrunc (scaled_mantissa beta fexp x);
Fexp := fexp ex |}:float beta
Hx:x = F2R fx
fy:={|
Fnum := Ztrunc (scaled_mantissa beta fexp y);
Fexp := fexp ey |}:float beta
Hy:y = F2R fy
format (x + y)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:Rabs (x + y) =
bpow (Z.min (mag beta x) (mag beta y))
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
format (x + y)
unfold cexp.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
ex:Z
Ex:(bpow (ex - 1) <= Rabs x < bpow ex)%R
ey:Z
Ey:(bpow (ey - 1) <= Rabs y < bpow ey)%R
Hxy:(Rabs (x + y) < bpow (Z.min ex ey))%R
fx:={|
Fnum := Ztrunc (scaled_mantissa beta fexp x);
Fexp := fexp ex |}:float beta
Hx:x = F2R fx
fy:={|
Fnum := Ztrunc (scaled_mantissa beta fexp y);
Fexp := fexp ey |}:float beta
F2R
  {|
  Fnum := Ztrunc (scaled_mantissa beta fexp y);
  Fexp := fexp (mag beta y) |} = F2R fy
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
ex:Z
Ex:(bpow (ex - 1) <= Rabs x < bpow ex)%R
ey:Z
Ey:(bpow (ey - 1) <= Rabs y < bpow ey)%R
Hxy:(Rabs (x + y) < bpow (Z.min ex ey))%R
fx:={|
Fnum := Ztrunc (scaled_mantissa beta fexp x);
Fexp := fexp ex |}:float beta
Hx:x = F2R fx
fy:={|
Fnum := Ztrunc (scaled_mantissa beta fexp y);
Fexp := fexp ey |}:float beta
Hy:y = F2R fy
format (x + y)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:Rabs (x + y) =
bpow (Z.min (mag beta x) (mag beta y))
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
format (x + y)
now rewrite mag_unique with (1 := Ey).beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
ex:Z
Ex:(bpow (ex - 1) <= Rabs x < bpow ex)%R
ey:Z
Ey:(bpow (ey - 1) <= Rabs y < bpow ey)%R
Hxy:(Rabs (x + y) < bpow (Z.min ex ey))%R
fx:={|
Fnum := Ztrunc (scaled_mantissa beta fexp x);
Fexp := fexp ex |}:float beta
Hx:x = F2R fx
fy:={|
Fnum := Ztrunc (scaled_mantissa beta fexp y);
Fexp := fexp ey |}:float beta
Hy:y = F2R fy
format (x + y)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:Rabs (x + y) =
bpow (Z.min (mag beta x) (mag beta y))
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
format (x + y)
rewrite Hx, Hy.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
ex:Z
Ex:(bpow (ex - 1) <= Rabs x < bpow ex)%R
ey:Z
Ey:(bpow (ey - 1) <= Rabs y < bpow ey)%R
Hxy:(Rabs (x + y) < bpow (Z.min ex ey))%R
fx:={|
Fnum := Ztrunc (scaled_mantissa beta fexp x);
Fexp := fexp ex |}:float beta
Hx:x = F2R fx
fy:={|
Fnum := Ztrunc (scaled_mantissa beta fexp y);
Fexp := fexp ey |}:float beta
Hy:y = F2R fy
format (F2R fx + F2R fy)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:Rabs (x + y) =
bpow (Z.min (mag beta x) (mag beta y))
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
format (x + y)
rewrite <- F2R_plus.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
ex:Z
Ex:(bpow (ex - 1) <= Rabs x < bpow ex)%R
ey:Z
Ey:(bpow (ey - 1) <= Rabs y < bpow ey)%R
Hxy:(Rabs (x + y) < bpow (Z.min ex ey))%R
fx:={|
Fnum := Ztrunc (scaled_mantissa beta fexp x);
Fexp := fexp ex |}:float beta
Hx:x = F2R fx
fy:={|
Fnum := Ztrunc (scaled_mantissa beta fexp y);
Fexp := fexp ey |}:float beta
Hy:y = F2R fy
format (F2R (Fplus fx fy))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:Rabs (x + y) =
bpow (Z.min (mag beta x) (mag beta y))
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
format (x + y)
apply generic_format_F2R.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
ex:Z
Ex:(bpow (ex - 1) <= Rabs x < bpow ex)%R
ey:Z
Ey:(bpow (ey - 1) <= Rabs y < bpow ey)%R
Hxy:(Rabs (x + y) < bpow (Z.min ex ey))%R
fx:={|
Fnum := Ztrunc (scaled_mantissa beta fexp x);
Fexp := fexp ex |}:float beta
Hx:x = F2R fx
fy:={|
Fnum := Ztrunc (scaled_mantissa beta fexp y);
Fexp := fexp ey |}:float beta
Hy:y = F2R fy
(let (Fnum, _) := Fplus fx fy in Fnum) <> 0%Z ->
(cexp beta fexp
   (F2R
      {|
      Fnum := let (Fnum, _) := Fplus fx fy in Fnum;
      Fexp := let (_, Fexp) := Fplus fx fy in Fexp |}) <=
 (let (_, Fexp) := Fplus fx fy in Fexp))%Z
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:Rabs (x + y) =
bpow (Z.min (mag beta x) (mag beta y))
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
format (x + y)
intros _.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
ex:Z
Ex:(bpow (ex - 1) <= Rabs x < bpow ex)%R
ey:Z
Ey:(bpow (ey - 1) <= Rabs y < bpow ey)%R
Hxy:(Rabs (x + y) < bpow (Z.min ex ey))%R
fx:={|
Fnum := Ztrunc (scaled_mantissa beta fexp x);
Fexp := fexp ex |}:float beta
Hx:x = F2R fx
fy:={|
Fnum := Ztrunc (scaled_mantissa beta fexp y);
Fexp := fexp ey |}:float beta
Hy:y = F2R fy
(cexp beta fexp
   (F2R
      {|
      Fnum := let (Fnum, _) := Fplus fx fy in Fnum;
      Fexp := let (_, Fexp) := Fplus fx fy in Fexp |}) <=
 (let (_, Fexp) := Fplus fx fy in Fexp))%Z
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:Rabs (x + y) =
bpow (Z.min (mag beta x) (mag beta y))
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
format (x + y)
case_eq (Fplus fx fy).beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
ex:Z
Ex:(bpow (ex - 1) <= Rabs x < bpow ex)%R
ey:Z
Ey:(bpow (ey - 1) <= Rabs y < bpow ey)%R
Hxy:(Rabs (x + y) < bpow (Z.min ex ey))%R
fx:={|
Fnum := Ztrunc (scaled_mantissa beta fexp x);
Fexp := fexp ex |}:float beta
Hx:x = F2R fx
fy:={|
Fnum := Ztrunc (scaled_mantissa beta fexp y);
Fexp := fexp ey |}:float beta
Hy:y = F2R fy
forall Fnum Fexp : Z,
Fplus fx fy = {| Fnum := Fnum; Fexp := Fexp |} ->
(cexp beta fexp (F2R {| Fnum := Fnum; Fexp := Fexp |}) <=
 Fexp)%Z
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:Rabs (x + y) =
bpow (Z.min (mag beta x) (mag beta y))
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
format (x + y)
intros mxy exy Pxy.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
ex:Z
Ex:(bpow (ex - 1) <= Rabs x < bpow ex)%R
ey:Z
Ey:(bpow (ey - 1) <= Rabs y < bpow ey)%R
Hxy:(Rabs (x + y) < bpow (Z.min ex ey))%R
fx:={|
Fnum := Ztrunc (scaled_mantissa beta fexp x);
Fexp := fexp ex |}:float beta
Hx:x = F2R fx
fy:={|
Fnum := Ztrunc (scaled_mantissa beta fexp y);
Fexp := fexp ey |}:float beta
Hy:y = F2R fy
mxy, exy:Z
Pxy:Fplus fx fy = {| Fnum := mxy; Fexp := exy |}
(cexp beta fexp (F2R {| Fnum := mxy; Fexp := exy |}) <=
 exy)%Z
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:Rabs (x + y) =
bpow (Z.min (mag beta x) (mag beta y))
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
format (x + y)
rewrite <- Pxy, F2R_plus, <- Hx, <- Hy.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
ex:Z
Ex:(bpow (ex - 1) <= Rabs x < bpow ex)%R
ey:Z
Ey:(bpow (ey - 1) <= Rabs y < bpow ey)%R
Hxy:(Rabs (x + y) < bpow (Z.min ex ey))%R
fx:={|
Fnum := Ztrunc (scaled_mantissa beta fexp x);
Fexp := fexp ex |}:float beta
Hx:x = F2R fx
fy:={|
Fnum := Ztrunc (scaled_mantissa beta fexp y);
Fexp := fexp ey |}:float beta
Hy:y = F2R fy
mxy, exy:Z
Pxy:Fplus fx fy = {| Fnum := mxy; Fexp := exy |}
(cexp beta fexp (x + y) <= exy)%Z
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:Rabs (x + y) =
bpow (Z.min (mag beta x) (mag beta y))
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
format (x + y)
unfold cexp.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
ex:Z
Ex:(bpow (ex - 1) <= Rabs x < bpow ex)%R
ey:Z
Ey:(bpow (ey - 1) <= Rabs y < bpow ey)%R
Hxy:(Rabs (x + y) < bpow (Z.min ex ey))%R
fx:={|
Fnum := Ztrunc (scaled_mantissa beta fexp x);
Fexp := fexp ex |}:float beta
Hx:x = F2R fx
fy:={|
Fnum := Ztrunc (scaled_mantissa beta fexp y);
Fexp := fexp ey |}:float beta
Hy:y = F2R fy
mxy, exy:Z
Pxy:Fplus fx fy = {| Fnum := mxy; Fexp := exy |}
(fexp (mag beta (x + y)) <= exy)%Z
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:Rabs (x + y) =
bpow (Z.min (mag beta x) (mag beta y))
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
format (x + y)
replace exy with (fexp (Z.min ex ey)).beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
ex:Z
Ex:(bpow (ex - 1) <= Rabs x < bpow ex)%R
ey:Z
Ey:(bpow (ey - 1) <= Rabs y < bpow ey)%R
Hxy:(Rabs (x + y) < bpow (Z.min ex ey))%R
fx:={|
Fnum := Ztrunc (scaled_mantissa beta fexp x);
Fexp := fexp ex |}:float beta
Hx:x = F2R fx
fy:={|
Fnum := Ztrunc (scaled_mantissa beta fexp y);
Fexp := fexp ey |}:float beta
Hy:y = F2R fy
mxy, exy:Z
Pxy:Fplus fx fy = {| Fnum := mxy; Fexp := exy |}
(fexp (mag beta (x + y)) <= fexp (Z.min ex ey))%Z
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
ex:Z
Ex:(bpow (ex - 1) <= Rabs x < bpow ex)%R
ey:Z
Ey:(bpow (ey - 1) <= Rabs y < bpow ey)%R
Hxy:(Rabs (x + y) < bpow (Z.min ex ey))%R
fx:={|
Fnum := Ztrunc (scaled_mantissa beta fexp x);
Fexp := fexp ex |}:float beta
Hx:x = F2R fx
fy:={|
Fnum := Ztrunc (scaled_mantissa beta fexp y);
Fexp := fexp ey |}:float beta
Hy:y = F2R fy
mxy, exy:Z
Pxy:Fplus fx fy = {| Fnum := mxy; Fexp := exy |}
fexp (Z.min ex ey) = exy
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:Rabs (x + y) =
bpow (Z.min (mag beta x) (mag beta y))
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
format (x + y)
apply monotone_exp.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
ex:Z
Ex:(bpow (ex - 1) <= Rabs x < bpow ex)%R
ey:Z
Ey:(bpow (ey - 1) <= Rabs y < bpow ey)%R
Hxy:(Rabs (x + y) < bpow (Z.min ex ey))%R
fx:={|
Fnum := Ztrunc (scaled_mantissa beta fexp x);
Fexp := fexp ex |}:float beta
Hx:x = F2R fx
fy:={|
Fnum := Ztrunc (scaled_mantissa beta fexp y);
Fexp := fexp ey |}:float beta
Hy:y = F2R fy
mxy, exy:Z
Pxy:Fplus fx fy = {| Fnum := mxy; Fexp := exy |}
(mag beta (x + y) <= Z.min ex ey)%Z
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
ex:Z
Ex:(bpow (ex - 1) <= Rabs x < bpow ex)%R
ey:Z
Ey:(bpow (ey - 1) <= Rabs y < bpow ey)%R
Hxy:(Rabs (x + y) < bpow (Z.min ex ey))%R
fx:={|
Fnum := Ztrunc (scaled_mantissa beta fexp x);
Fexp := fexp ex |}:float beta
Hx:x = F2R fx
fy:={|
Fnum := Ztrunc (scaled_mantissa beta fexp y);
Fexp := fexp ey |}:float beta
Hy:y = F2R fy
mxy, exy:Z
Pxy:Fplus fx fy = {| Fnum := mxy; Fexp := exy |}
fexp (Z.min ex ey) = exy
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:Rabs (x + y) =
bpow (Z.min (mag beta x) (mag beta y))
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
format (x + y)
now apply mag_le_bpow.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
ex:Z
Ex:(bpow (ex - 1) <= Rabs x < bpow ex)%R
ey:Z
Ey:(bpow (ey - 1) <= Rabs y < bpow ey)%R
Hxy:(Rabs (x + y) < bpow (Z.min ex ey))%R
fx:={|
Fnum := Ztrunc (scaled_mantissa beta fexp x);
Fexp := fexp ex |}:float beta
Hx:x = F2R fx
fy:={|
Fnum := Ztrunc (scaled_mantissa beta fexp y);
Fexp := fexp ey |}:float beta
Hy:y = F2R fy
mxy, exy:Z
Pxy:Fplus fx fy = {| Fnum := mxy; Fexp := exy |}
fexp (Z.min ex ey) = exy
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:Rabs (x + y) =
bpow (Z.min (mag beta x) (mag beta y))
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
format (x + y)
replace exy with (Fexp (Fplus fx fy)) by exact (f_equal Fexp Pxy).beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
ex:Z
Ex:(bpow (ex - 1) <= Rabs x < bpow ex)%R
ey:Z
Ey:(bpow (ey - 1) <= Rabs y < bpow ey)%R
Hxy:(Rabs (x + y) < bpow (Z.min ex ey))%R
fx:={|
Fnum := Ztrunc (scaled_mantissa beta fexp x);
Fexp := fexp ex |}:float beta
Hx:x = F2R fx
fy:={|
Fnum := Ztrunc (scaled_mantissa beta fexp y);
Fexp := fexp ey |}:float beta
Hy:y = F2R fy
mxy, exy:Z
Pxy:Fplus fx fy = {| Fnum := mxy; Fexp := exy |}
fexp (Z.min ex ey) = Fexp (Fplus fx fy)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:Rabs (x + y) =
bpow (Z.min (mag beta x) (mag beta y))
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
format (x + y)
rewrite Fexp_Fplus.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
ex:Z
Ex:(bpow (ex - 1) <= Rabs x < bpow ex)%R
ey:Z
Ey:(bpow (ey - 1) <= Rabs y < bpow ey)%R
Hxy:(Rabs (x + y) < bpow (Z.min ex ey))%R
fx:={|
Fnum := Ztrunc (scaled_mantissa beta fexp x);
Fexp := fexp ex |}:float beta
Hx:x = F2R fx
fy:={|
Fnum := Ztrunc (scaled_mantissa beta fexp y);
Fexp := fexp ey |}:float beta
Hy:y = F2R fy
mxy, exy:Z
Pxy:Fplus fx fy = {| Fnum := mxy; Fexp := exy |}
fexp (Z.min ex ey) = Z.min (Fexp fx) (Fexp fy)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:Rabs (x + y) =
bpow (Z.min (mag beta x) (mag beta y))
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
format (x + y)
simpl.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
ex:Z
Ex:(bpow (ex - 1) <= Rabs x < bpow ex)%R
ey:Z
Ey:(bpow (ey - 1) <= Rabs y < bpow ey)%R
Hxy:(Rabs (x + y) < bpow (Z.min ex ey))%R
fx:={|
Fnum := Ztrunc (scaled_mantissa beta fexp x);
Fexp := fexp ex |}:float beta
Hx:x = F2R fx
fy:={|
Fnum := Ztrunc (scaled_mantissa beta fexp y);
Fexp := fexp ey |}:float beta
Hy:y = F2R fy
mxy, exy:Z
Pxy:Fplus fx fy = {| Fnum := mxy; Fexp := exy |}
fexp (Z.min ex ey) = Z.min (fexp ex) (fexp ey)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:Rabs (x + y) =
bpow (Z.min (mag beta x) (mag beta y))
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
format (x + y) clear -monotone_exp.fexp:Z -> Z
monotone_exp:Monotone_exp fexp
ex, ey:Z
fexp (Z.min ex ey) = Z.min (fexp ex) (fexp ey)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:Rabs (x + y) =
bpow (Z.min (mag beta x) (mag beta y))
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
format (x + y)
apply sym_eq.fexp:Z -> Z
monotone_exp:Monotone_exp fexp
ex, ey:Z
Z.min (fexp ex) (fexp ey) = fexp (Z.min ex ey)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:Rabs (x + y) =
bpow (Z.min (mag beta x) (mag beta y))
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
format (x + y)
destruct (Zmin_spec ex ey) as [(H1,H2)|(H1,H2)] ; rewrite H2.fexp:Z -> Z
monotone_exp:Monotone_exp fexp
ex, ey:Z
H1:(ex <= ey)%Z
H2:Z.min ex ey = ex
Z.min (fexp ex) (fexp ey) = fexp ex
fexp:Z -> Z
monotone_exp:Monotone_exp fexp
ex, ey:Z
H1:(ex > ey)%Z
H2:Z.min ex ey = ey
Z.min (fexp ex) (fexp ey) = fexp ey
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:Rabs (x + y) =
bpow (Z.min (mag beta x) (mag beta y))
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
format (x + y)
apply Z.min_l.fexp:Z -> Z
monotone_exp:Monotone_exp fexp
ex, ey:Z
H1:(ex <= ey)%Z
H2:Z.min ex ey = ex
(fexp ex <= fexp ey)%Z
fexp:Z -> Z
monotone_exp:Monotone_exp fexp
ex, ey:Z
H1:(ex > ey)%Z
H2:Z.min ex ey = ey
Z.min (fexp ex) (fexp ey) = fexp ey
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:Rabs (x + y) =
bpow (Z.min (mag beta x) (mag beta y))
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
format (x + y)
now apply monotone_exp.fexp:Z -> Z
monotone_exp:Monotone_exp fexp
ex, ey:Z
H1:(ex > ey)%Z
H2:Z.min ex ey = ey
Z.min (fexp ex) (fexp ey) = fexp ey
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:Rabs (x + y) =
bpow (Z.min (mag beta x) (mag beta y))
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
format (x + y)
apply Z.min_r.fexp:Z -> Z
monotone_exp:Monotone_exp fexp
ex, ey:Z
H1:(ex > ey)%Z
H2:Z.min ex ey = ey
(fexp ey <= fexp ex)%Z
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:Rabs (x + y) =
bpow (Z.min (mag beta x) (mag beta y))
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
format (x + y)
apply monotone_exp.fexp:Z -> Z
monotone_exp:Monotone_exp fexp
ex, ey:Z
H1:(ex > ey)%Z
H2:Z.min ex ey = ey
(ey <= ex)%Z
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:Rabs (x + y) =
bpow (Z.min (mag beta x) (mag beta y))
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
format (x + y)
apply Zlt_le_weak.fexp:Z -> Z
monotone_exp:Monotone_exp fexp
ex, ey:Z
H1:(ex > ey)%Z
H2:Z.min ex ey = ey
(ey < ex)%Z
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:Rabs (x + y) =
bpow (Z.min (mag beta x) (mag beta y))
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
format (x + y)
now apply Z.gt_lt.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:Rabs (x + y) =
bpow (Z.min (mag beta x) (mag beta y))
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
format (x + y)
apply generic_format_abs_inv.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:Rabs (x + y) =
bpow (Z.min (mag beta x) (mag beta y))
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
format (Rabs (x + y))
rewrite Hxy.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:Rabs (x + y) =
bpow (Z.min (mag beta x) (mag beta y))
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
format (bpow (Z.min (mag beta x) (mag beta y)))
apply generic_format_bpow.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:Rabs (x + y) =
bpow (Z.min (mag beta x) (mag beta y))
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
(fexp (Z.min (mag beta x) (mag beta y) + 1) <=
 Z.min (mag beta x) (mag beta y))%Z
apply valid_exp.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:Rabs (x + y) =
bpow (Z.min (mag beta x) (mag beta y))
Zxy:(x + y)%R <> 0%R
Zx:x <> R0
Zy:y <> R0
(fexp (Z.min (mag beta x) (mag beta y)) <
 Z.min (mag beta x) (mag beta y))%Z
case (Zmin_spec (mag beta x) (mag beta y)); intros (H1,H2);
   rewrite H2; now apply mag_generic_gt.
Qed.

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.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
forall x y : R,
format x ->
format y ->
(Rabs (x + y) <= Rmin (Rabs x) (Rabs y))%R ->
format (x + y)
Proof.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
forall x y : R,
format x ->
format y ->
(Rabs (x + y) <= Rmin (Rabs x) (Rabs y))%R ->
format (x + y)
intros x y Fx Fy Hxy.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:(Rabs (x + y) <= Rmin (Rabs x) (Rabs y))%R
format (x + y)
destruct (Req_dec x R0) as [Zx|Zx].beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:(Rabs (x + y) <= Rmin (Rabs x) (Rabs y))%R
Zx:x = R0
format (x + y)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:(Rabs (x + y) <= Rmin (Rabs x) (Rabs y))%R
Zx:x <> R0
format (x + y)
now rewrite Zx, Rplus_0_l.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:(Rabs (x + y) <= Rmin (Rabs x) (Rabs y))%R
Zx:x <> R0
format (x + y)
destruct (Req_dec y R0) as [Zy|Zy].beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:(Rabs (x + y) <= Rmin (Rabs x) (Rabs y))%R
Zx:x <> R0
Zy:y = R0
format (x + y)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:(Rabs (x + y) <= Rmin (Rabs x) (Rabs y))%R
Zx:x <> R0
Zy:y <> R0
format (x + y)
now rewrite Zy, Rplus_0_r.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:(Rabs (x + y) <= Rmin (Rabs x) (Rabs y))%R
Zx:x <> R0
Zy:y <> R0
format (x + y)
apply generic_format_plus ; try assumption.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:(Rabs (x + y) <= Rmin (Rabs x) (Rabs y))%R
Zx:x <> R0
Zy:y <> R0
(Rabs (x + y) <=
 bpow (Z.min (mag beta x) (mag beta y)))%R
apply Rle_trans with (1 := Hxy).beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:(Rabs (x + y) <= Rmin (Rabs x) (Rabs y))%R
Zx:x <> R0
Zy:y <> R0
(Rmin (Rabs x) (Rabs y) <=
 bpow (Z.min (mag beta x) (mag beta y)))%R
unfold Rmin.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:(Rabs (x + y) <= Rmin (Rabs x) (Rabs y))%R
Zx:x <> R0
Zy:y <> R0
((if Rle_dec (Rabs x) (Rabs y) then Rabs x else Rabs y) <=
 bpow (Z.min (mag beta x) (mag beta y)))%R
destruct (Rle_dec (Rabs x) (Rabs y)) as [Hxy'|Hxy'].beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:(Rabs (x + y) <= Rmin (Rabs x) (Rabs y))%R
Zx:x <> R0
Zy:y <> R0
Hxy':(Rabs x <= Rabs y)%R
(Rabs x <= bpow (Z.min (mag beta x) (mag beta y)))%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:(Rabs (x + y) <= Rmin (Rabs x) (Rabs y))%R
Zx:x <> R0
Zy:y <> R0
Hxy':~ (Rabs x <= Rabs y)%R
(Rabs y <= bpow (Z.min (mag beta x) (mag beta y)))%R
rewrite Z.min_l.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:(Rabs (x + y) <= Rmin (Rabs x) (Rabs y))%R
Zx:x <> R0
Zy:y <> R0
Hxy':(Rabs x <= Rabs y)%R
(Rabs x <= bpow (mag beta x))%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:(Rabs (x + y) <= Rmin (Rabs x) (Rabs y))%R
Zx:x <> R0
Zy:y <> R0
Hxy':(Rabs x <= Rabs y)%R
(mag beta x <= mag beta y)%Z
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:(Rabs (x + y) <= Rmin (Rabs x) (Rabs y))%R
Zx:x <> R0
Zy:y <> R0
Hxy':~ (Rabs x <= Rabs y)%R
(Rabs y <= bpow (Z.min (mag beta x) (mag beta y)))%R
destruct (mag beta x) as (ex, Hx).beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:(Rabs (x + y) <= Rmin (Rabs x) (Rabs y))%R
Zx:x <> R0
Zy:y <> R0
Hxy':(Rabs x <= Rabs y)%R
ex:Z
Hx:x <> 0%R -> (bpow (ex - 1) <= Rabs x < bpow ex)%R
(Rabs x <= bpow (Build_mag_prop beta x ex Hx))%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:(Rabs (x + y) <= Rmin (Rabs x) (Rabs y))%R
Zx:x <> R0
Zy:y <> R0
Hxy':(Rabs x <= Rabs y)%R
(mag beta x <= mag beta y)%Z
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:(Rabs (x + y) <= Rmin (Rabs x) (Rabs y))%R
Zx:x <> R0
Zy:y <> R0
Hxy':~ (Rabs x <= Rabs y)%R
(Rabs y <= bpow (Z.min (mag beta x) (mag beta y)))%R
apply Rlt_le; now apply Hx.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:(Rabs (x + y) <= Rmin (Rabs x) (Rabs y))%R
Zx:x <> R0
Zy:y <> R0
Hxy':(Rabs x <= Rabs y)%R
(mag beta x <= mag beta y)%Z
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:(Rabs (x + y) <= Rmin (Rabs x) (Rabs y))%R
Zx:x <> R0
Zy:y <> R0
Hxy':~ (Rabs x <= Rabs y)%R
(Rabs y <= bpow (Z.min (mag beta x) (mag beta y)))%R
now apply mag_le_abs.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:(Rabs (x + y) <= Rmin (Rabs x) (Rabs y))%R
Zx:x <> R0
Zy:y <> R0
Hxy':~ (Rabs x <= Rabs y)%R
(Rabs y <= bpow (Z.min (mag beta x) (mag beta y)))%R
rewrite Z.min_r.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:(Rabs (x + y) <= Rmin (Rabs x) (Rabs y))%R
Zx:x <> R0
Zy:y <> R0
Hxy':~ (Rabs x <= Rabs y)%R
(Rabs y <= bpow (mag beta y))%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:(Rabs (x + y) <= Rmin (Rabs x) (Rabs y))%R
Zx:x <> R0
Zy:y <> R0
Hxy':~ (Rabs x <= Rabs y)%R
(mag beta y <= mag beta x)%Z
destruct (mag beta y) as (ex, Hy).beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:(Rabs (x + y) <= Rmin (Rabs x) (Rabs y))%R
Zx:x <> R0
Zy:y <> R0
Hxy':~ (Rabs x <= Rabs y)%R
ex:Z
Hy:y <> 0%R -> (bpow (ex - 1) <= Rabs y < bpow ex)%R
(Rabs y <= bpow (Build_mag_prop beta y ex Hy))%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:(Rabs (x + y) <= Rmin (Rabs x) (Rabs y))%R
Zx:x <> R0
Zy:y <> R0
Hxy':~ (Rabs x <= Rabs y)%R
(mag beta y <= mag beta x)%Z
apply Rlt_le; now apply Hy.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:(Rabs (x + y) <= Rmin (Rabs x) (Rabs y))%R
Zx:x <> R0
Zy:y <> R0
Hxy':~ (Rabs x <= Rabs y)%R
(mag beta y <= mag beta x)%Z
apply mag_le_abs.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:(Rabs (x + y) <= Rmin (Rabs x) (Rabs y))%R
Zx:x <> R0
Zy:y <> R0
Hxy':~ (Rabs x <= Rabs y)%R
y <> 0%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:(Rabs (x + y) <= Rmin (Rabs x) (Rabs y))%R
Zx:x <> R0
Zy:y <> R0
Hxy':~ (Rabs x <= Rabs y)%R
(Rabs y <= Rabs x)%R
exact Zy.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:(Rabs (x + y) <= Rmin (Rabs x) (Rabs y))%R
Zx:x <> R0
Zy:y <> R0
Hxy':~ (Rabs x <= Rabs y)%R
(Rabs y <= Rabs x)%R
apply Rlt_le.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Fx:format x
Fy:format y
Hxy:(Rabs (x + y) <= Rmin (Rabs x) (Rabs y))%R
Zx:x <> R0
Zy:y <> R0
Hxy':~ (Rabs x <= Rabs y)%R
(Rabs y < Rabs x)%R
now apply Rnot_le_lt.
Qed.

Lemma sterbenz_aux :
  forall x y, format x -> format y ->
  (y <= x <= 2 * y)%R ->
  format (x - y)%R.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
forall x y : R,
format x ->
format y -> (y <= x <= 2 * y)%R -> format (x - y)
Proof.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
forall x y : R,
format x ->
format y -> (y <= x <= 2 * y)%R -> format (x - y)
intros x y Hx Hy (Hxy1, Hxy2).beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Hx:format x
Hy:format y
Hxy1:(y <= x)%R
Hxy2:(x <= 2 * y)%R
format (x - y)
unfold Rminus.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Hx:format x
Hy:format y
Hxy1:(y <= x)%R
Hxy2:(x <= 2 * y)%R
format (x + - y)
apply generic_format_plus_weak.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Hx:format x
Hy:format y
Hxy1:(y <= x)%R
Hxy2:(x <= 2 * y)%R
format x
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Hx:format x
Hy:format y
Hxy1:(y <= x)%R
Hxy2:(x <= 2 * y)%R
format (- y)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Hx:format x
Hy:format y
Hxy1:(y <= x)%R
Hxy2:(x <= 2 * y)%R
(Rabs (x + - y) <= Rmin (Rabs x) (Rabs (- y)))%R
exact Hx.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Hx:format x
Hy:format y
Hxy1:(y <= x)%R
Hxy2:(x <= 2 * y)%R
format (- y)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Hx:format x
Hy:format y
Hxy1:(y <= x)%R
Hxy2:(x <= 2 * y)%R
(Rabs (x + - y) <= Rmin (Rabs x) (Rabs (- y)))%R
now apply generic_format_opp.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Hx:format x
Hy:format y
Hxy1:(y <= x)%R
Hxy2:(x <= 2 * y)%R
(Rabs (x + - y) <= Rmin (Rabs x) (Rabs (- y)))%R
rewrite Rabs_pos_eq.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Hx:format x
Hy:format y
Hxy1:(y <= x)%R
Hxy2:(x <= 2 * y)%R
(x + - y <= Rmin (Rabs x) (Rabs (- y)))%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Hx:format x
Hy:format y
Hxy1:(y <= x)%R
Hxy2:(x <= 2 * y)%R
(0 <= x + - y)%R
rewrite Rabs_Ropp.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Hx:format x
Hy:format y
Hxy1:(y <= x)%R
Hxy2:(x <= 2 * y)%R
(x + - y <= Rmin (Rabs x) (Rabs y))%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Hx:format x
Hy:format y
Hxy1:(y <= x)%R
Hxy2:(x <= 2 * y)%R
(0 <= x + - y)%R
rewrite Rmin_comm.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Hx:format x
Hy:format y
Hxy1:(y <= x)%R
Hxy2:(x <= 2 * y)%R
(x + - y <= Rmin (Rabs y) (Rabs x))%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Hx:format x
Hy:format y
Hxy1:(y <= x)%R
Hxy2:(x <= 2 * y)%R
(0 <= x + - y)%R
assert (Hy0: (0 <= y)%R).beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Hx:format x
Hy:format y
Hxy1:(y <= x)%R
Hxy2:(x <= 2 * y)%R
(0 <= y)%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Hx:format x
Hy:format y
Hxy1:(y <= x)%R
Hxy2:(x <= 2 * y)%R
Hy0:(0 <= y)%R
(x + - y <= Rmin (Rabs y) (Rabs x))%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Hx:format x
Hy:format y
Hxy1:(y <= x)%R
Hxy2:(x <= 2 * y)%R
(0 <= x + - y)%R
apply Rplus_le_reg_r with y.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Hx:format x
Hy:format y
Hxy1:(y <= x)%R
Hxy2:(x <= 2 * y)%R
(0 + y <= y + y)%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Hx:format x
Hy:format y
Hxy1:(y <= x)%R
Hxy2:(x <= 2 * y)%R
Hy0:(0 <= y)%R
(x + - y <= Rmin (Rabs y) (Rabs x))%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Hx:format x
Hy:format y
Hxy1:(y <= x)%R
Hxy2:(x <= 2 * y)%R
(0 <= x + - y)%R
apply Rle_trans with x.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Hx:format x
Hy:format y
Hxy1:(y <= x)%R
Hxy2:(x <= 2 * y)%R
(0 + y <= x)%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Hx:format x
Hy:format y
Hxy1:(y <= x)%R
Hxy2:(x <= 2 * y)%R
(x <= y + y)%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Hx:format x
Hy:format y
Hxy1:(y <= x)%R
Hxy2:(x <= 2 * y)%R
Hy0:(0 <= y)%R
(x + - y <= Rmin (Rabs y) (Rabs x))%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Hx:format x
Hy:format y
Hxy1:(y <= x)%R
Hxy2:(x <= 2 * y)%R
(0 <= x + - y)%R
now rewrite Rplus_0_l.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Hx:format x
Hy:format y
Hxy1:(y <= x)%R
Hxy2:(x <= 2 * y)%R
(x <= y + y)%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Hx:format x
Hy:format y
Hxy1:(y <= x)%R
Hxy2:(x <= 2 * y)%R
Hy0:(0 <= y)%R
(x + - y <= Rmin (Rabs y) (Rabs x))%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Hx:format x
Hy:format y
Hxy1:(y <= x)%R
Hxy2:(x <= 2 * y)%R
(0 <= x + - y)%R
now replace (y + y)%R with (2 * y)%R by ring.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Hx:format x
Hy:format y
Hxy1:(y <= x)%R
Hxy2:(x <= 2 * y)%R
Hy0:(0 <= y)%R
(x + - y <= Rmin (Rabs y) (Rabs x))%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Hx:format x
Hy:format y
Hxy1:(y <= x)%R
Hxy2:(x <= 2 * y)%R
(0 <= x + - y)%R
rewrite Rabs_pos_eq with (1 := Hy0).beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Hx:format x
Hy:format y
Hxy1:(y <= x)%R
Hxy2:(x <= 2 * y)%R
Hy0:(0 <= y)%R
(x + - y <= Rmin y (Rabs x))%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Hx:format x
Hy:format y
Hxy1:(y <= x)%R
Hxy2:(x <= 2 * y)%R
(0 <= x + - y)%R
rewrite Rabs_pos_eq.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Hx:format x
Hy:format y
Hxy1:(y <= x)%R
Hxy2:(x <= 2 * y)%R
Hy0:(0 <= y)%R
(x + - y <= Rmin y x)%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Hx:format x
Hy:format y
Hxy1:(y <= x)%R
Hxy2:(x <= 2 * y)%R
Hy0:(0 <= y)%R
(0 <= x)%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Hx:format x
Hy:format y
Hxy1:(y <= x)%R
Hxy2:(x <= 2 * y)%R
(0 <= x + - y)%R
unfold Rmin.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Hx:format x
Hy:format y
Hxy1:(y <= x)%R
Hxy2:(x <= 2 * y)%R
Hy0:(0 <= y)%R
(x + - y <= (if Rle_dec y x then y else x))%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Hx:format x
Hy:format y
Hxy1:(y <= x)%R
Hxy2:(x <= 2 * y)%R
Hy0:(0 <= y)%R
(0 <= x)%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Hx:format x
Hy:format y
Hxy1:(y <= x)%R
Hxy2:(x <= 2 * y)%R
(0 <= x + - y)%R
destruct (Rle_dec y x) as [Hyx|Hyx].beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Hx:format x
Hy:format y
Hxy1:(y <= x)%R
Hxy2:(x <= 2 * y)%R
Hy0:(0 <= y)%R
Hyx:(y <= x)%R
(x + - y <= y)%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Hx:format x
Hy:format y
Hxy1:(y <= x)%R
Hxy2:(x <= 2 * y)%R
Hy0:(0 <= y)%R
Hyx:~ (y <= x)%R
(x + - y <= x)%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Hx:format x
Hy:format y
Hxy1:(y <= x)%R
Hxy2:(x <= 2 * y)%R
Hy0:(0 <= y)%R
(0 <= x)%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Hx:format x
Hy:format y
Hxy1:(y <= x)%R
Hxy2:(x <= 2 * y)%R
(0 <= x + - y)%R
apply Rplus_le_reg_r with y.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Hx:format x
Hy:format y
Hxy1:(y <= x)%R
Hxy2:(x <= 2 * y)%R
Hy0:(0 <= y)%R
Hyx:(y <= x)%R
(x + - y + y <= y + y)%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Hx:format x
Hy:format y
Hxy1:(y <= x)%R
Hxy2:(x <= 2 * y)%R
Hy0:(0 <= y)%R
Hyx:~ (y <= x)%R
(x + - y <= x)%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Hx:format x
Hy:format y
Hxy1:(y <= x)%R
Hxy2:(x <= 2 * y)%R
Hy0:(0 <= y)%R
(0 <= x)%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Hx:format x
Hy:format y
Hxy1:(y <= x)%R
Hxy2:(x <= 2 * y)%R
(0 <= x + - y)%R
now ring_simplify.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Hx:format x
Hy:format y
Hxy1:(y <= x)%R
Hxy2:(x <= 2 * y)%R
Hy0:(0 <= y)%R
Hyx:~ (y <= x)%R
(x + - y <= x)%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Hx:format x
Hy:format y
Hxy1:(y <= x)%R
Hxy2:(x <= 2 * y)%R
Hy0:(0 <= y)%R
(0 <= x)%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Hx:format x
Hy:format y
Hxy1:(y <= x)%R
Hxy2:(x <= 2 * y)%R
(0 <= x + - y)%R
now elim Hyx.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Hx:format x
Hy:format y
Hxy1:(y <= x)%R
Hxy2:(x <= 2 * y)%R
Hy0:(0 <= y)%R
(0 <= x)%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Hx:format x
Hy:format y
Hxy1:(y <= x)%R
Hxy2:(x <= 2 * y)%R
(0 <= x + - y)%R
now apply Rle_trans with y.beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
monotone_exp:Monotone_exp fexp
x, y:R
Hx:format x
Hy:format y
Hxy1:(y <= x)%R
Hxy2:(x <= 2 * y)%R
(0 <= x + - y)%R
now apply Rle_0_minus.
Qed.

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

End Fprop_Sterbenz.