Library Flocq.Calc.Operations

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.

Basic operations on floats: alignment, addition, multiplication

From Coq Require Import ZArith Reals Lia.

Require Import Zaux Raux Defs Float_prop.

Set Implicit Arguments.

Section Float_ops.

Variable beta : radix.

Notation bpow e := (bpow beta e).

Arguments Float {beta}.

Definition Falign (f1 f2 : float beta) :=
  let '(Float m1 e1) := f1 in
  let '(Float m2 e2) := f2 in
  if Zle_bool e1 e2
  then (m1, (m2 × Zpower beta (e2 - e1))%Z, e1)
  else ((m1 × Zpower beta (e1 - e2))%Z, m2, e2).

Theorem Falign_spec :
  ∀ f1 f2 : float beta,
  let '(m1, m2, e) := Falign f1 f2 in
  F2R f1 = @F2R beta (Float m1 e) ∧ F2R f2 = @F2R beta (Float m2 e).

Theorem Falign_spec_exp:
  ∀ f1 f2 : float beta,
  snd (Falign f1 f2) = Z.min (Fexp f1) (Fexp f2).

Definition Fopp (f1 : float beta) : float beta :=
  let '(Float m1 e1) := f1 in
  Float (-m1)%Z e1.

Theorem F2R_opp :
  ∀ f1 : float beta,
  (F2R (Fopp f1) = -F2R f1)%R.

Definition Fabs (f1 : float beta) : float beta :=
  let '(Float m1 e1) := f1 in
  Float (Z.abs m1)%Z e1.

Theorem F2R_abs :
  ∀ f1 : float beta,
  (F2R (Fabs f1) = Rabs (F2R f1))%R.

Definition Fplus (f1 f2 : float beta) : float beta :=
  let '(m1, m2 ,e) := Falign f1 f2 in
  Float (m1 + m2) e.

Theorem F2R_plus :
  ∀ f1 f2 : float beta,
  F2R (Fplus f1 f2) = (F2R f1 + F2R f2)%R.

Theorem Fplus_same_exp :
  ∀ m1 m2 e,
  Fplus (Float m1 e) (Float m2 e) = Float (m1 + m2) e.

Theorem Fexp_Fplus :
  ∀ f1 f2 : float beta,
  Fexp (Fplus f1 f2) = Z.min (Fexp f1) (Fexp f2).

Definition Fminus (f1 f2 : float beta) :=
  Fplus f1 (Fopp f2).

Theorem F2R_minus :
  ∀ f1 f2 : float beta,
  F2R (Fminus f1 f2) = (F2R f1 - F2R f2)%R.

Theorem Fminus_same_exp :
  ∀ m1 m2 e,
  Fminus (Float m1 e) (Float m2 e) = Float (m1 - m2) e.

Definition Fmult (f1 f2 : float beta) : float beta :=
  let '(Float m1 e1) := f1 in
  let '(Float m2 e2) := f2 in
  Float (m1 × m2) (e1 + e2).

Theorem F2R_mult :
  ∀ f1 f2 : float beta,
  F2R (Fmult f1 f2) = (F2R f1 × F2R f2)%R.

End Float_ops.