(**
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/

Copyright (C) 2010-2013 Sylvie Boldo
#<br />#
Copyright (C) 2010-2013 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.
*)

(** Basic operations on floats: alignment, addition, multiplication *)
Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Fcore_float_prop.

Section Float_ops.

Variable beta : radix.

Notation bpow e := (bpow beta e).

Arguments Float {beta} Fnum Fexp.

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).
Proof.
(* Goal: forall f1 f2 : float beta, let 'pair (pair m1 m2 as p) e := Falign f1 f2 in and (@eq R (@F2R beta f1) (@F2R beta (@Float beta m1 e))) (@eq R (@F2R beta f2) (@F2R beta (@Float beta m2 e))) *)
unfold Falign.
(* Goal: forall f1 f2 : float beta, @eq R (@F2R beta (Fmult f1 f2)) (Rmult (@F2R beta f1) (@F2R beta f2)) *)
intros (m1, e1) (m2, e2).
(* Goal: let 'pair (pair m3 m4 as p) e := if Z.leb e1 e2 then @pair (prod Z Z) Z (@pair Z Z m1 (Z.mul m2 (Z.pow (radix_val beta) (Z.sub e2 e1)))) e1 else @pair (prod Z Z) Z (@pair Z Z (Z.mul m1 (Z.pow (radix_val beta) (Z.sub e1 e2))) m2) e2 in and (@eq R (@F2R beta (@Float beta m1 e1)) (@F2R beta (@Float beta m3 e))) (@eq R (@F2R beta (@Float beta m2 e2)) (@F2R beta (@Float beta m4 e))) *)
generalize (Zle_cases e1 e2).
(* Goal: forall _ : if Z.leb e1 e2 then Z.le e1 e2 else Z.gt e1 e2, let 'pair (pair m3 m4 as p) e := if Z.leb e1 e2 then @pair (prod Z Z) Z (@pair Z Z m1 (Z.mul m2 (Z.pow (radix_val beta) (Z.sub e2 e1)))) e1 else @pair (prod Z Z) Z (@pair Z Z (Z.mul m1 (Z.pow (radix_val beta) (Z.sub e1 e2))) m2) e2 in and (@eq R (@F2R beta (@Float beta m1 e1)) (@F2R beta (@Float beta m3 e))) (@eq R (@F2R beta (@Float beta m2 e2)) (@F2R beta (@Float beta m4 e))) *)
case (Zle_bool e1 e2) ; intros He ; split ; trivial.
(* Goal: @eq R (@F2R beta (@Float beta m2 e2)) (@F2R beta (@Float beta (Z.mul m2 (Z.pow (radix_val beta) (Z.sub e2 e1))) e1)) *)
(* Goal: @eq R (@F2R beta (@Float beta m1 e1)) (@F2R beta (@Float beta (Z.mul m1 (Z.pow (radix_val beta) (Z.sub e1 e2))) e2)) *)
now rewrite <- F2R_change_exp.
(* Goal: @eq R (@F2R beta (@Float beta m1 e1)) (@F2R beta (@Float beta (Z.mul m1 (Z.pow (radix_val beta) (Z.sub e1 e2))) e2)) *)
rewrite <- F2R_change_exp.
(* Goal: @eq R (@F2R beta (@Float beta m1 e1)) (@F2R beta (@Float beta m1 e1)) *)
(* Goal: Z.le e2 e1 *)
apply refl_equal.
(* Goal: Z.le e2 e1 *)
omega.
Qed.

Theorem Falign_spec_exp:
  forall f1 f2 : float beta,
  snd (Falign f1 f2) = Zmin (Fexp f1) (Fexp f2).
Proof.
(* Goal: forall f1 f2 : float beta, @eq R (@F2R beta (Fmult f1 f2)) (Rmult (@F2R beta f1) (@F2R beta f2)) *)
intros (m1,e1) (m2,e2).
(* Goal: @eq Z (@snd (prod Z Z) Z (Falign (@Float beta m1 e1) (@Float beta m2 e2))) (Z.min (@Fexp beta (@Float beta m1 e1)) (@Fexp beta (@Float beta m2 e2))) *)
unfold Falign; simpl.
(* Goal: @eq Z (@snd (prod Z Z) Z (if Z.leb e1 e2 then @pair (prod Z Z) Z (@pair Z Z m1 (Z.mul m2 (Z.pow (radix_val beta) (Z.sub e2 e1)))) e1 else @pair (prod Z Z) Z (@pair Z Z (Z.mul m1 (Z.pow (radix_val beta) (Z.sub e1 e2))) m2) e2)) (Z.min e1 e2) *)
generalize (Zle_cases e1 e2);case (Zle_bool e1 e2); intros He.
(* Goal: @eq Z (@snd (prod Z Z) Z (@pair (prod Z Z) Z (@pair Z Z (Z.mul m1 (Z.pow (radix_val beta) (Z.sub e1 e2))) m2) e2)) (Z.min e1 e2) *)
case (Zmin_spec e1 e2); intros (H1,H2); easy.
(* Goal: @eq Z (@snd (prod Z Z) Z (@pair (prod Z Z) Z (@pair Z Z (Z.mul m1 (Z.pow (radix_val beta) (Z.sub e1 e2))) 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.
(* Goal: forall f1 : float beta, @eq R (@F2R beta (Fabs f1)) (Rabs (@F2R beta f1)) *)
intros (m1,e1).
(* Goal: @eq R (@F2R beta (Fopp (@Float beta m1 e1))) (Ropp (@F2R beta (@Float beta m1 e1))) *)
apply F2R_Zopp.
Qed.

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

Theorem F2R_abs :
  forall f1 : float beta,
  (F2R (Fabs f1) = Rabs (F2R f1))%R.
(* Goal: forall f1 : float beta, @eq R (@F2R beta (Fabs f1)) (Rabs (@F2R beta f1)) *)
intros (m1,e1).
(* Goal: @eq R (@F2R beta (Fabs (@Float beta m1 e1))) (Rabs (@F2R beta (@Float beta m1 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.
Proof.
(* Goal: forall f1 f2 : float beta, @eq Z (@Fexp beta (Fplus f1 f2)) (Z.min (@Fexp beta f1) (@Fexp beta f2)) *)
intros f1 f2.
(* Goal: @eq Z (@Fexp beta (Fplus f1 f2)) (Z.min (@Fexp beta f1) (@Fexp beta f2)) *)
unfold Fplus.
(* Goal: @eq R (@F2R beta (let 'pair (pair m1 m2 as p) e := Falign f1 f2 in @Float beta (Z.add m1 m2) e)) (Rplus (@F2R beta f1) (@F2R beta f2)) *)
generalize (Falign_spec f1 f2).
(* Goal: forall _ : let 'pair (pair m1 m2 as p) e := Falign f1 f2 in and (@eq R (@F2R beta f1) (@F2R beta (@Float beta m1 e))) (@eq R (@F2R beta f2) (@F2R beta (@Float beta m2 e))), @eq R (@F2R beta (let 'pair (pair m1 m2 as p) e := Falign f1 f2 in @Float beta (Z.add m1 m2) e)) (Rplus (@F2R beta f1) (@F2R beta f2)) *)
destruct (Falign f1 f2) as ((m1, m2), e).
(* Goal: forall _ : and (@eq R (@F2R beta f1) (@F2R beta (@Float beta m1 e))) (@eq R (@F2R beta f2) (@F2R beta (@Float beta m2 e))), @eq R (@F2R beta (@Float beta (Z.add m1 m2) e)) (Rplus (@F2R beta f1) (@F2R beta f2)) *)
intros (H1, H2).
(* Goal: @eq R (@F2R beta (@Float beta (Z.add m1 m2) e)) (Rplus (@F2R beta f1) (@F2R beta f2)) *)
rewrite H1, H2.
(* Goal: @eq R (@F2R beta (@Float beta (Z.add m1 m2) e)) (Rplus (@F2R beta (@Float beta m1 e)) (@F2R beta (@Float beta m2 e))) *)
unfold F2R. simpl.
(* Goal: @eq R (Rmult (Z2R (Z.add m1 m2)) (Fcore_Raux.bpow beta e)) (Rplus (Rmult (Z2R m1) (Fcore_Raux.bpow beta e)) (Rmult (Z2R m2) (Fcore_Raux.bpow beta e))) *)
rewrite Z2R_plus.
(* Goal: @eq R (Rmult (Rplus (Z2R m1) (Z2R m2)) (Fcore_Raux.bpow beta e)) (Rplus (Rmult (Z2R m1) (Fcore_Raux.bpow beta e)) (Rmult (Z2R m2) (Fcore_Raux.bpow beta e))) *)
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.
Proof.
(* Goal: forall m1 m2 e : Z, @eq (float beta) (Fminus (@Float beta m1 e) (@Float beta m2 e)) (@Float beta (Z.sub m1 m2) e) *)
intros m1 m2 e.
(* Goal: @eq Z (@Fexp beta (Fplus f1 f2)) (Z.min (@Fexp beta f1) (@Fexp beta f2)) *)
unfold Fplus.
(* Goal: @eq R (Rmult (Z2R (@Fnum beta (@Float beta (Z.mul m1 m2) (Z.add e1 e2)))) (Fcore_Raux.bpow beta (@Fexp beta (@Float beta (Z.mul m1 m2) (Z.add e1 e2))))) (Rmult (Rmult (Z2R (@Fnum beta (@Float beta m1 e1))) (Fcore_Raux.bpow beta (@Fexp beta (@Float beta m1 e1)))) (Rmult (Z2R (@Fnum beta (@Float beta m2 e2))) (Fcore_Raux.bpow beta (@Fexp beta (@Float beta m2 e2))))) *)
simpl.
(* Goal: @eq (float beta) (let 'pair (pair m1 m2 as p) e := if Z.leb e e then @pair (prod Z Z) Z (@pair Z Z m1 (Z.mul m2 (Z.pow (radix_val beta) (Z.sub e e)))) e else @pair (prod Z Z) Z (@pair Z Z (Z.mul m1 (Z.pow (radix_val beta) (Z.sub e e))) m2) e in @Float beta (Z.add m1 m2) e) (@Float beta (Z.add m1 m2) e) *)
now rewrite Zle_bool_refl, Zminus_diag, Zmult_1_r.
Qed.

Theorem Fexp_Fplus :
  forall f1 f2 : float beta,
  Fexp (Fplus f1 f2) = Zmin (Fexp f1) (Fexp f2).
Proof.
(* Goal: forall f1 f2 : float beta, @eq Z (@Fexp beta (Fplus f1 f2)) (Z.min (@Fexp beta f1) (@Fexp beta f2)) *)
intros f1 f2.
(* Goal: @eq Z (@Fexp beta (Fplus f1 f2)) (Z.min (@Fexp beta f1) (@Fexp beta f2)) *)
unfold Fplus.
(* Goal: @eq Z (@Fexp beta (let 'pair (pair m1 m2 as p) e := Falign f1 f2 in @Float beta (Z.add m1 m2) e)) (Z.min (@Fexp beta f1) (@Fexp beta f2)) *)
rewrite <- Falign_spec_exp.
(* Goal: @eq Z (@Fexp beta (let 'pair (pair m1 m2 as p) e := Falign f1 f2 in @Float beta (Z.add m1 m2) e)) (@snd (prod Z Z) Z (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.
Proof.
(* Goal: forall f1 f2 : float beta, @eq R (@F2R beta (Fminus f1 f2)) (Rminus (@F2R beta f1) (@F2R beta f2)) *)
intros f1 f2; unfold Fminus.
(* Goal: @eq R (@F2R beta (Fplus f1 (Fopp f2))) (Rminus (@F2R beta f1) (@F2R beta f2)) *)
rewrite F2R_plus, F2R_opp.
(* Goal: @eq R (Rmult (Rmult (Z2R m1) (Z2R m2)) (Rmult (Fcore_Raux.bpow beta e1) (Fcore_Raux.bpow beta e2))) (Rmult (Rmult (Z2R m1) (Fcore_Raux.bpow beta e1)) (Rmult (Z2R m2) (Fcore_Raux.bpow beta e2))) *)
ring.
Qed.

Theorem Fminus_same_exp :
  forall m1 m2 e,
  Fminus (Float m1 e) (Float m2 e) = Float (m1 - m2) e.
Proof.
(* Goal: forall m1 m2 e : Z, @eq (float beta) (Fminus (@Float beta m1 e) (@Float beta m2 e)) (@Float beta (Z.sub m1 m2) e) *)
intros m1 m2 e.
(* Goal: @eq (float beta) (Fminus (@Float beta m1 e) (@Float beta m2 e)) (@Float beta (Z.sub m1 m2) e) *)
unfold Fminus.
(* Goal: @eq (float beta) (Fplus (@Float beta m1 e) (Fopp (@Float beta m2 e))) (@Float beta (Z.sub m1 m2) 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.
Proof.
(* Goal: forall f1 f2 : float beta, @eq R (@F2R beta (Fmult f1 f2)) (Rmult (@F2R beta f1) (@F2R beta f2)) *)
intros (m1, e1) (m2, e2).
(* Goal: @eq R (Rmult (Z2R (@Fnum beta (@Float beta (Z.mul m1 m2) (Z.add e1 e2)))) (Fcore_Raux.bpow beta (@Fexp beta (@Float beta (Z.mul m1 m2) (Z.add e1 e2))))) (Rmult (Rmult (Z2R (@Fnum beta (@Float beta m1 e1))) (Fcore_Raux.bpow beta (@Fexp beta (@Float beta m1 e1)))) (Rmult (Z2R (@Fnum beta (@Float beta m2 e2))) (Fcore_Raux.bpow beta (@Fexp beta (@Float beta m2 e2))))) *)
unfold Fmult, F2R. simpl.
(* Goal: @eq R (Rmult (Z2R (Z.mul m1 m2)) (Fcore_Raux.bpow beta (Z.add e1 e2))) (Rmult (Rmult (Z2R m1) (Fcore_Raux.bpow beta e1)) (Rmult (Z2R m2) (Fcore_Raux.bpow beta e2))) *)
rewrite Z2R_mult, bpow_plus.
(* Goal: @eq R (Rmult (Rmult (Z2R m1) (Z2R m2)) (Rmult (Fcore_Raux.bpow beta e1) (Fcore_Raux.bpow beta e2))) (Rmult (Rmult (Z2R m1) (Fcore_Raux.bpow beta e1)) (Rmult (Z2R m2) (Fcore_Raux.bpow beta e2))) *)
ring.
Qed.

End Float_ops.
