1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
|
(**
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2010-2011 Sylvie Boldo
#<br />#
Copyright (C) 2010-2011 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).
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 (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.
Theorem Falign_spec_exp:
forall f1 f2 : float beta,
snd (Falign f1 f2) = Zmin (Fexp f1) (Fexp f2).
Proof.
intros (m1,e1) (m2,e2).
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) :=
let '(Float m1 e1) := f1 in
Float beta (-m1)%Z e1.
Theorem F2R_opp :
forall f1 : float beta,
(F2R (Fopp f1) = -F2R f1)%R.
intros (m1,e1).
apply F2R_Zopp.
Qed.
Definition Fabs (f1: float beta) :=
let '(Float m1 e1) := f1 in
Float beta (Zabs m1)%Z e1.
Theorem F2R_abs :
forall f1 : float beta,
(F2R (Fabs f1) = Rabs (F2R f1))%R.
intros (m1,e1).
apply F2R_Zabs.
Qed.
Definition Fplus (f1 f2 : float beta) :=
let '(m1, m2 ,e) := Falign f1 f2 in
Float beta (m1 + m2) e.
Theorem F2R_plus :
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.
rewrite Z2R_plus.
apply Rmult_plus_distr_r.
Qed.
Theorem Fplus_same_exp :
forall m1 m2 e,
Fplus (Float beta m1 e) (Float beta m2 e) = Float beta (m1 + m2) e.
Proof.
intros m1 m2 e.
unfold Fplus.
simpl.
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.
intros f1 f2.
unfold Fplus.
rewrite <- Falign_spec_exp.
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.
intros f1 f2; unfold Fminus.
rewrite F2R_plus, F2R_opp.
ring.
Qed.
Theorem Fminus_same_exp :
forall m1 m2 e,
Fminus (Float beta m1 e) (Float beta m2 e) = Float beta (m1 - m2) e.
Proof.
intros m1 m2 e.
unfold Fminus.
apply Fplus_same_exp.
Qed.
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 F2R_mult :
forall f1 f2 : float beta,
F2R (Fmult f1 f2) = (F2R f1 * F2R f2)%R.
Proof.
intros (m1, e1) (m2, e2).
unfold Fmult, F2R. simpl.
rewrite Z2R_mult, bpow_plus.
ring.
Qed.
End Float_ops.
|
