Library Flocq.Calc.Plus

This file is part of the Flocq formalization of floating-point arithmetic in Coq: https://flocq.gitlabpages.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.

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.