Fcalc_ops.v 2.67 KB
Newer Older
1 2 3
Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Fcore_float_prop.
4

5
Section Float_ops.
6 7 8

Variable beta : radix.

9
Notation bpow e := (bpow beta e).
10 11 12 13 14

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

Theorem Falign_spec :
  forall f1 f2 : float beta,
20
  let '(m1, m2, e) := Falign f1 f2 in
21 22 23 24 25 26 27 28 29 30 31 32
  F2R f1 = F2R (Float beta m1 e) /\ F2R f2 = F2R (Float beta m2 e).
Proof.
unfold Falign.
intros (m1, e1) (m2, e2).
generalize (Zle_cases e1 e2).
case (Zle_bool e1 e2) ; intros He ; split ; trivial.
now rewrite <- F2R_change_exp.
rewrite <- F2R_change_exp.
apply refl_equal.
omega.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
33 34
Theorem Falign_spec_exp:
  forall f1 f2 : float beta,
35 36 37
  snd (Falign f1 f2) = Zmin (Fexp f1) (Fexp f2).
Proof.
intros (m1,e1) (m2,e2).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
38 39 40 41 42 43 44
unfold Falign; simpl.
generalize (Zle_cases e1 e2);case (Zle_bool e1 e2); intros He.
case (Zmin_spec e1 e2); intros (H1,H2); easy.
case (Zmin_spec e1 e2); intros (H1,H2); easy.
Qed.

Definition Fopp (f1: float beta) :=
45 46
  let '(Float m1 e1) := f1 in
  Float beta (-m1)%Z e1.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
47 48 49 50 51

Theorem Fopp_F2R :
  forall f1 : float beta,
  (F2R (Fopp f1) = -F2R f1)%R.
unfold Fopp, F2R; intros (m1,e1).
52
simpl; rewrite Z2R_opp; ring.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
53 54
Qed.

55
Definition Fabs (f1: float beta) :=
56 57
  let '(Float m1 e1) := f1 in
  Float beta (Zabs m1)%Z e1.
58 59 60 61 62 63 64 65

Theorem Fabs_F2R :
  forall f1 : float beta,
  (F2R (Fabs f1) = Rabs (F2R f1))%R.
intros (m1,e1).
now rewrite abs_F2R.
Qed.

66 67 68 69 70 71 72 73 74 75 76 77 78 79 80
Definition Fplus (f1 f2 : float beta) :=
  let '(m1, m2 ,e) := Falign f1 f2 in
  Float beta (m1 + m2) e.

Theorem plus_F2R :
  forall f1 f2 : float beta,
  F2R (Fplus f1 f2) = (F2R f1 + F2R f2)%R.
Proof.
intros f1 f2.
unfold Fplus.
generalize (Falign_spec f1 f2).
destruct (Falign f1 f2) as ((m1, m2), e).
intros (H1, H2).
rewrite H1, H2.
unfold F2R. simpl.
81
rewrite Z2R_plus.
82 83 84
apply Rmult_plus_distr_r.
Qed.

85 86 87 88 89 90 91 92 93
Theorem Fexp_Fplus :
  forall f1 f2 : float beta,
  Fexp (Fplus f1 f2) = Zmin (Fexp f1) (Fexp f2).
Proof.
intros f1 f2.
unfold Fplus.
rewrite <- Falign_spec_exp.
now destruct (Falign f1 f2) as ((p,q),e).
Qed.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
94 95 96 97 98 99 100 101 102 103 104 105 106

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

Theorem minus_F2R :
  forall f1 f2 : float beta,
  F2R (Fminus f1 f2) = (F2R f1 - F2R f2)%R.
Proof.
intros f1 f2; unfold Fminus.
rewrite plus_F2R, Fopp_F2R.
ring.
Qed.

107 108 109 110 111 112 113 114 115 116 117
Definition Fmult (f1 f2 : float beta) :=
  let '(Float m1 e1) := f1 in
  let '(Float m2 e2) := f2 in
  Float beta (m1 * m2) (e1 + e2).

Theorem mult_F2R :
  forall f1 f2 : float beta,
  F2R (Fmult f1 f2) = (F2R f1 * F2R f2)%R.
Proof.
intros (m1, e1) (m2, e2).
unfold Fmult, F2R. simpl.
118
rewrite Z2R_mult, bpow_plus.
119 120 121
ring.
Qed.

122
End Float_ops.