Operations.v

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.
Basic operations on floats: alignment, addition, multiplication
Require Import Raux Defs Float_prop.

Set Implicit Arguments.
Set Strongly Strict Implicit.

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 :
  forall 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).beta:radix
forall f1 f2 : float beta,
let
'(m1, m2, e) := Falign f1 f2 in
 F2R f1 = F2R {| Fnum := m1; Fexp := e |} /\
 F2R f2 = F2R {| Fnum := m2; Fexp := e |}
Proof.beta:radix
forall f1 f2 : float beta,
let
'(m1, m2, e) := Falign f1 f2 in
 F2R f1 = F2R {| Fnum := m1; Fexp := e |} /\
 F2R f2 = F2R {| Fnum := m2; Fexp := e |}
unfold Falign.beta:radix
forall f1 f2 : float beta,
let
'(m1, m2, e) :=
 let
 '{| Fnum := m1; Fexp := e1 |} := f1 in
  let
  '{| Fnum := m2; Fexp := e2 |} := f2 in
   if (e1 <=? e2)%Z
   then (m1, (m2 * beta ^ (e2 - e1))%Z, e1)
   else ((m1 * beta ^ (e1 - e2))%Z, m2, e2) in
 F2R f1 = F2R {| Fnum := m1; Fexp := e |} /\
 F2R f2 = F2R {| Fnum := m2; Fexp := e |}
intros (m1, e1) (m2, e2).beta:radix
m1, e1, m2, e2:Z
let
'(m0, m3, e) :=
 if (e1 <=? e2)%Z
 then (m1, (m2 * beta ^ (e2 - e1))%Z, e1)
 else ((m1 * beta ^ (e1 - e2))%Z, m2, e2) in
 F2R {| Fnum := m1; Fexp := e1 |} =
 F2R {| Fnum := m0; Fexp := e |} /\
 F2R {| Fnum := m2; Fexp := e2 |} =
 F2R {| Fnum := m3; Fexp := e |}
generalize (Zle_cases e1 e2).beta:radix
m1, e1, m2, e2:Z
(if (e1 <=? e2)%Z then (e1 <= e2)%Z else (e1 > e2)%Z) ->
let
'(m0, m3, e) :=
 if (e1 <=? e2)%Z
 then (m1, (m2 * beta ^ (e2 - e1))%Z, e1)
 else ((m1 * beta ^ (e1 - e2))%Z, m2, e2) in
 F2R {| Fnum := m1; Fexp := e1 |} =
 F2R {| Fnum := m0; Fexp := e |} /\
 F2R {| Fnum := m2; Fexp := e2 |} =
 F2R {| Fnum := m3; Fexp := e |}
case (Zle_bool e1 e2) ; intros He ; split ; trivial.beta:radix
m1, e1, m2, e2:Z
He:(e1 <= e2)%Z
F2R {| Fnum := m2; Fexp := e2 |} =
F2R {| Fnum := m2 * beta ^ (e2 - e1); Fexp := e1 |}
beta:radix
m1, e1, m2, e2:Z
He:(e1 > e2)%Z
F2R {| Fnum := m1; Fexp := e1 |} =
F2R {| Fnum := m1 * beta ^ (e1 - e2); Fexp := e2 |}
now rewrite <- F2R_change_exp.beta:radix
m1, e1, m2, e2:Z
He:(e1 > e2)%Z
F2R {| Fnum := m1; Fexp := e1 |} =
F2R {| Fnum := m1 * beta ^ (e1 - e2); Fexp := e2 |}
rewrite <- F2R_change_exp.beta:radix
m1, e1, m2, e2:Z
He:(e1 > e2)%Z
F2R {| Fnum := m1; Fexp := e1 |} =
F2R {| Fnum := m1; Fexp := e1 |}
beta:radix
m1, e1, m2, e2:Z
He:(e1 > e2)%Z
(e2 <= e1)%Z
apply refl_equal.beta:radix
m1, e1, m2, e2:Z
He:(e1 > e2)%Z
(e2 <= e1)%Z
omega.
Qed.

Theorem Falign_spec_exp:
  forall f1 f2 : float beta,
  snd (Falign f1 f2) = Z.min (Fexp f1) (Fexp f2).beta:radix
forall f1 f2 : float beta,
snd (Falign f1 f2) = Z.min (Fexp f1) (Fexp f2)
Proof.beta:radix
forall f1 f2 : float beta,
snd (Falign f1 f2) = Z.min (Fexp f1) (Fexp f2)
intros (m1,e1) (m2,e2).beta:radix
m1, e1, m2, e2:Z
snd
  (Falign {| Fnum := m1; Fexp := e1 |}
     {| Fnum := m2; Fexp := e2 |}) =
Z.min (Fexp {| Fnum := m1; Fexp := e1 |})
  (Fexp {| Fnum := m2; Fexp := e2 |})
unfold Falign; simpl.beta:radix
m1, e1, m2, e2:Z
snd
  (if (e1 <=? e2)%Z
   then (m1, (m2 * beta ^ (e2 - e1))%Z, e1)
   else ((m1 * beta ^ (e1 - e2))%Z, m2, e2)) =
Z.min e1 e2
generalize (Zle_cases e1 e2);case (Zle_bool e1 e2); intros He.beta:radix
m1, e1, m2, e2:Z
He:(e1 <= e2)%Z
snd (m1, (m2 * beta ^ (e2 - e1))%Z, e1) = Z.min e1 e2
beta:radix
m1, e1, m2, e2:Z
He:(e1 > e2)%Z
snd ((m1 * beta ^ (e1 - e2))%Z, m2, e2) = Z.min e1 e2
case (Zmin_spec e1 e2); intros (H1,H2); easy.beta:radix
m1, e1, m2, e2:Z
He:(e1 > e2)%Z
snd ((m1 * beta ^ (e1 - e2))%Z, m2, e2) = Z.min e1 e2
case (Zmin_spec e1 e2); intros (H1,H2); easy.
Qed.

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

Theorem F2R_opp :
  forall f1 : float beta,
  (F2R (Fopp f1) = -F2R f1)%R.beta:radix
forall f1 : float beta, F2R (Fopp f1) = (- F2R f1)%R
intros (m1,e1).beta:radix
m1, e1:Z
F2R (Fopp {| Fnum := m1; Fexp := e1 |}) =
(- F2R {| Fnum := m1; Fexp := e1 |})%R
apply F2R_Zopp.
Qed.

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

Theorem F2R_abs :
  forall f1 : float beta,
  (F2R (Fabs f1) = Rabs (F2R f1))%R.beta:radix
forall f1 : float beta, F2R (Fabs f1) = Rabs (F2R f1)
intros (m1,e1).beta:radix
m1, e1:Z
F2R (Fabs {| Fnum := m1; Fexp := e1 |}) =
Rabs (F2R {| Fnum := m1; Fexp := e1 |})
apply F2R_Zabs.
Qed.

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

Theorem F2R_plus :
  forall f1 f2 : float beta,
  F2R (Fplus f1 f2) = (F2R f1 + F2R f2)%R.beta:radix
forall f1 f2 : float beta,
F2R (Fplus f1 f2) = (F2R f1 + F2R f2)%R
Proof.beta:radix
forall f1 f2 : float beta,
F2R (Fplus f1 f2) = (F2R f1 + F2R f2)%R
intros f1 f2.beta:radix
f1, f2:float beta
F2R (Fplus f1 f2) = (F2R f1 + F2R f2)%R
unfold Fplus.beta:radix
f1, f2:float beta
F2R
  (let
   '(m1, m2, e) := Falign f1 f2 in
    {| Fnum := m1 + m2; Fexp := e |}) =
(F2R f1 + F2R f2)%R
generalize (Falign_spec f1 f2).beta:radix
f1, f2:float beta
(let
 '(m1, m2, e) := Falign f1 f2 in
  F2R f1 = F2R {| Fnum := m1; Fexp := e |} /\
  F2R f2 = F2R {| Fnum := m2; Fexp := e |}) ->
F2R
  (let
   '(m1, m2, e) := Falign f1 f2 in
    {| Fnum := m1 + m2; Fexp := e |}) =
(F2R f1 + F2R f2)%R
destruct (Falign f1 f2) as ((m1, m2), e).beta:radix
f1, f2:float beta
m1, m2, e:Z
F2R f1 = F2R {| Fnum := m1; Fexp := e |} /\
F2R f2 = F2R {| Fnum := m2; Fexp := e |} ->
F2R {| Fnum := m1 + m2; Fexp := e |} =
(F2R f1 + F2R f2)%R
intros (H1, H2).beta:radix
f1, f2:float beta
m1, m2, e:Z
H1:F2R f1 = F2R {| Fnum := m1; Fexp := e |}
H2:F2R f2 = F2R {| Fnum := m2; Fexp := e |}
F2R {| Fnum := m1 + m2; Fexp := e |} =
(F2R f1 + F2R f2)%R
rewrite H1, H2.beta:radix
f1, f2:float beta
m1, m2, e:Z
H1:F2R f1 = F2R {| Fnum := m1; Fexp := e |}
H2:F2R f2 = F2R {| Fnum := m2; Fexp := e |}
F2R {| Fnum := m1 + m2; Fexp := e |} =
(F2R {| Fnum := m1; Fexp := e |} +
 F2R {| Fnum := m2; Fexp := e |})%R
unfold F2R.beta:radix
f1, f2:float beta
m1, m2, e:Z
H1:F2R f1 = F2R {| Fnum := m1; Fexp := e |}
H2:F2R f2 = F2R {| Fnum := m2; Fexp := e |}
(IZR (Fnum {| Fnum := m1 + m2; Fexp := e |}) *
 bpow (Fexp {| Fnum := m1 + m2; Fexp := e |}))%R =
(IZR (Fnum {| Fnum := m1; Fexp := e |}) *
 bpow (Fexp {| Fnum := m1; Fexp := e |}) +
 IZR (Fnum {| Fnum := m2; Fexp := e |}) *
 bpow (Fexp {| Fnum := m2; Fexp := e |}))%R simpl.beta:radix
f1, f2:float beta
m1, m2, e:Z
H1:F2R f1 = F2R {| Fnum := m1; Fexp := e |}
H2:F2R f2 = F2R {| Fnum := m2; Fexp := e |}
(IZR (m1 + m2) * bpow e)%R =
(IZR m1 * bpow e + IZR m2 * bpow e)%R
rewrite plus_IZR.beta:radix
f1, f2:float beta
m1, m2, e:Z
H1:F2R f1 = F2R {| Fnum := m1; Fexp := e |}
H2:F2R f2 = F2R {| Fnum := m2; Fexp := e |}
((IZR m1 + IZR m2) * bpow e)%R =
(IZR m1 * bpow e + IZR m2 * bpow e)%R
apply Rmult_plus_distr_r.
Qed.

Theorem Fplus_same_exp :
  forall m1 m2 e,
  Fplus (Float m1 e) (Float m2 e) = Float (m1 + m2) e.beta:radix
forall m1 m2 e : Z,
Fplus {| Fnum := m1; Fexp := e |}
  {| Fnum := m2; Fexp := e |} =
{| Fnum := m1 + m2; Fexp := e |}
Proof.beta:radix
forall m1 m2 e : Z,
Fplus {| Fnum := m1; Fexp := e |}
  {| Fnum := m2; Fexp := e |} =
{| Fnum := m1 + m2; Fexp := e |}
intros m1 m2 e.beta:radix
m1, m2, e:Z
Fplus {| Fnum := m1; Fexp := e |}
  {| Fnum := m2; Fexp := e |} =
{| Fnum := m1 + m2; Fexp := e |}
unfold Fplus.beta:radix
m1, m2, e:Z
(let
 '(m0, m3, e0) :=
  Falign {| Fnum := m1; Fexp := e |}
    {| Fnum := m2; Fexp := e |} in
  {| Fnum := m0 + m3; Fexp := e0 |}) =
{| Fnum := m1 + m2; Fexp := e |}
simpl.beta:radix
m1, m2, e:Z
(let
 '(m0, m3, e0) :=
  if (e <=? e)%Z
  then (m1, (m2 * beta ^ (e - e))%Z, e)
  else ((m1 * beta ^ (e - e))%Z, m2, e) in
  {| Fnum := m0 + m3; Fexp := e0 |}) =
{| Fnum := m1 + m2; Fexp := e |}
now rewrite Zle_bool_refl, Zminus_diag, Zmult_1_r.
Qed.

Theorem Fexp_Fplus :
  forall f1 f2 : float beta,
  Fexp (Fplus f1 f2) = Z.min (Fexp f1) (Fexp f2).beta:radix
forall f1 f2 : float beta,
Fexp (Fplus f1 f2) = Z.min (Fexp f1) (Fexp f2)
Proof.beta:radix
forall f1 f2 : float beta,
Fexp (Fplus f1 f2) = Z.min (Fexp f1) (Fexp f2)
intros f1 f2.beta:radix
f1, f2:float beta
Fexp (Fplus f1 f2) = Z.min (Fexp f1) (Fexp f2)
unfold Fplus.beta:radix
f1, f2:float beta
Fexp
  (let
   '(m1, m2, e) := Falign f1 f2 in
    {| Fnum := m1 + m2; Fexp := e |}) =
Z.min (Fexp f1) (Fexp f2)
rewrite <- Falign_spec_exp.beta:radix
f1, f2:float beta
Fexp
  (let
   '(m1, m2, e) := Falign f1 f2 in
    {| Fnum := m1 + m2; Fexp := e |}) =
snd (Falign f1 f2)
now destruct (Falign f1 f2) as ((p,q),e).
Qed.

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

Theorem F2R_minus :
  forall f1 f2 : float beta,
  F2R (Fminus f1 f2) = (F2R f1 - F2R f2)%R.beta:radix
forall f1 f2 : float beta,
F2R (Fminus f1 f2) = (F2R f1 - F2R f2)%R
Proof.beta:radix
forall f1 f2 : float beta,
F2R (Fminus f1 f2) = (F2R f1 - F2R f2)%R
intros f1 f2; unfold Fminus.beta:radix
f1, f2:float beta
F2R (Fplus f1 (Fopp f2)) = (F2R f1 - F2R f2)%R
rewrite F2R_plus, F2R_opp.beta:radix
f1, f2:float beta
(F2R f1 + - F2R f2)%R = (F2R f1 - F2R f2)%R
ring.
Qed.

Theorem Fminus_same_exp :
  forall m1 m2 e,
  Fminus (Float m1 e) (Float m2 e) = Float (m1 - m2) e.beta:radix
forall m1 m2 e : Z,
Fminus {| Fnum := m1; Fexp := e |}
  {| Fnum := m2; Fexp := e |} =
{| Fnum := m1 - m2; Fexp := e |}
Proof.beta:radix
forall m1 m2 e : Z,
Fminus {| Fnum := m1; Fexp := e |}
  {| Fnum := m2; Fexp := e |} =
{| Fnum := m1 - m2; Fexp := e |}
intros m1 m2 e.beta:radix
m1, m2, e:Z
Fminus {| Fnum := m1; Fexp := e |}
  {| Fnum := m2; Fexp := e |} =
{| Fnum := m1 - m2; Fexp := e |}
unfold Fminus.beta:radix
m1, m2, e:Z
Fplus {| Fnum := m1; Fexp := e |}
  (Fopp {| Fnum := m2; Fexp := e |}) =
{| Fnum := m1 - m2; Fexp := e |}
apply Fplus_same_exp.
Qed.

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 :
  forall f1 f2 : float beta,
  F2R (Fmult f1 f2) = (F2R f1 * F2R f2)%R.beta:radix
forall f1 f2 : float beta,
F2R (Fmult f1 f2) = (F2R f1 * F2R f2)%R
Proof.beta:radix
forall f1 f2 : float beta,
F2R (Fmult f1 f2) = (F2R f1 * F2R f2)%R
intros (m1, e1) (m2, e2).beta:radix
m1, e1, m2, e2:Z
F2R
  (Fmult {| Fnum := m1; Fexp := e1 |}
     {| Fnum := m2; Fexp := e2 |}) =
(F2R {| Fnum := m1; Fexp := e1 |} *
 F2R {| Fnum := m2; Fexp := e2 |})%R
unfold Fmult, F2R.beta:radix
m1, e1, m2, e2:Z
(IZR (Fnum {| Fnum := m1 * m2; Fexp := e1 + e2 |}) *
 bpow (Fexp {| Fnum := m1 * m2; Fexp := e1 + e2 |}))%R =
(IZR (Fnum {| Fnum := m1; Fexp := e1 |}) *
 bpow (Fexp {| Fnum := m1; Fexp := e1 |}) *
 (IZR (Fnum {| Fnum := m2; Fexp := e2 |}) *
  bpow (Fexp {| Fnum := m2; Fexp := e2 |})))%R simpl.beta:radix
m1, e1, m2, e2:Z
(IZR (m1 * m2) * bpow (e1 + e2))%R =
(IZR m1 * bpow e1 * (IZR m2 * bpow e2))%R
rewrite mult_IZR, bpow_plus.beta:radix
m1, e1, m2, e2:Z
(IZR m1 * IZR m2 * (bpow e1 * bpow e2))%R =
(IZR m1 * bpow e1 * (IZR m2 * bpow e2))%R
ring.
Qed.

End Float_ops.