Library Flocq.Calc.Plus

This file is part of the Flocq formalization of floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2010-2021 Sylvie Boldo
Copyright (C) 2010-2021 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.

Helper function and theorem for computing the rounded sum of two floating-point numbers.


From Coq Require Import ZArith Reals Lia.

Require Import Core Bracket Operations Round.

Section Plus.

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

Variable fexp : Z Z.

Context { monotone_exp : Monotone_exp fexp }.

Definition Fplus_core m1 e1 m2 e2 e :=
  let k := (e - e2)%Z in
  let '(m2', _, l) :=
    if Zlt_bool 0 k then truncate_aux beta (m2, e2, loc_Exact) k
    else (m2 × Zpower beta (-k), e, loc_Exact)%Z in
  let m1' := (m1 × Zpower beta (e1 - e))%Z in
  (m1' + m2', l)%Z.

Theorem Fplus_core_correct :
   m1 e1 m2 e2 e,
  (e e1)%Z
  let '(m, l) := Fplus_core m1 e1 m2 e2 e in
  inbetween_float beta m e (F2R (Float beta m1 e1) + F2R (Float beta m2 e2)) l.

Definition Fplus (f1 f2 : float beta) :=
  let (m1, e1) := f1 in
  let (m2, e2) := f2 in
  if Zeq_bool m1 0 then
    (m2, e2, loc_Exact)
  else if Zeq_bool m2 0 then
    (m1, e1, loc_Exact)
  else
  let p1 := (Zdigits beta m1 + e1)%Z in
  let p2 := (Zdigits beta m2 + e2)%Z in
  if Zle_bool 2 (Z.abs (p1 - p2)) then
    let e := Z.min (Z.max e1 e2) (fexp (Z.max p1 p2 - 1)) in
    let (m, l) :=
      if Zlt_bool e1 e then
        Fplus_core m2 e2 m1 e1 e
      else
        Fplus_core m1 e1 m2 e2 e in
    (m, e, l)
  else
    let (m, e) := Fplus f1 f2 in
    (m, e, loc_Exact).

Theorem Fplus_correct :
   x y,
  let '(m, e, l) := Fplus x y in
  (l = loc_Exact e cexp beta fexp (F2R x + F2R y))%Z
  inbetween_float beta m e (F2R x + F2R y) l.

End Plus.