Fcalc_ops.v 2.67 KB
 Guillaume Melquiond committed Feb 24, 2010 1 2 3 ``````Require Import Fcore_Raux. Require Import Fcore_defs. Require Import Fcore_float_prop. `````` Guillaume Melquiond committed Oct 02, 2009 4 `````` `````` Guillaume Melquiond committed Feb 24, 2010 5 ``````Section Float_ops. `````` Guillaume Melquiond committed Oct 02, 2009 6 7 8 `````` Variable beta : radix. `````` Guillaume Melquiond committed Oct 29, 2009 9 ``````Notation bpow e := (bpow beta e). `````` Guillaume Melquiond committed Oct 02, 2009 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 `````` Guillaume Melquiond committed Oct 01, 2010 15 16 `````` then (m1, (m2 * Zpower beta (e2 - e1))%Z, e1) else ((m1 * Zpower beta (e1 - e2))%Z, m2, e2). `````` Guillaume Melquiond committed Oct 02, 2009 17 18 19 `````` Theorem Falign_spec : forall f1 f2 : float beta, `````` Guillaume Melquiond committed Sep 17, 2010 20 `````` let '(m1, m2, e) := Falign f1 f2 in `````` Guillaume Melquiond committed Oct 02, 2009 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 committed Sep 06, 2010 33 34 ``````Theorem Falign_spec_exp: forall f1 f2 : float beta, `````` Guillaume Melquiond committed Sep 17, 2010 35 36 37 `````` snd (Falign f1 f2) = Zmin (Fexp f1) (Fexp f2). Proof. intros (m1,e1) (m2,e2). `````` BOLDO Sylvie committed Sep 06, 2010 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) := `````` Guillaume Melquiond committed Sep 17, 2010 45 46 `````` let '(Float m1 e1) := f1 in Float beta (-m1)%Z e1. `````` BOLDO Sylvie committed Sep 06, 2010 47 48 49 50 51 `````` Theorem Fopp_F2R : forall f1 : float beta, (F2R (Fopp f1) = -F2R f1)%R. unfold Fopp, F2R; intros (m1,e1). `````` Guillaume Melquiond committed Oct 01, 2010 52 ``````simpl; rewrite Z2R_opp; ring. `````` BOLDO Sylvie committed Sep 06, 2010 53 54 ``````Qed. `````` BOLDO Sylvie committed Sep 16, 2010 55 ``````Definition Fabs (f1: float beta) := `````` Guillaume Melquiond committed Sep 17, 2010 56 57 `````` let '(Float m1 e1) := f1 in Float beta (Zabs m1)%Z e1. `````` BOLDO Sylvie committed Sep 16, 2010 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. `````` Guillaume Melquiond committed Oct 02, 2009 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. `````` Guillaume Melquiond committed Oct 01, 2010 81 ``````rewrite Z2R_plus. `````` Guillaume Melquiond committed Oct 02, 2009 82 83 84 ``````apply Rmult_plus_distr_r. Qed. `````` Guillaume Melquiond committed Sep 17, 2010 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 committed Sep 06, 2010 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. `````` Guillaume Melquiond committed Oct 02, 2009 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. `````` Guillaume Melquiond committed Oct 01, 2010 118 ``````rewrite Z2R_mult, bpow_plus. `````` Guillaume Melquiond committed Oct 02, 2009 119 120 121 ``````ring. Qed. `````` Guillaume Melquiond committed Feb 24, 2010 122 ``End Float_ops.``