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
162
163
164
165
166
|
(**
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2009-2018 Sylvie Boldo
#<br />#
Copyright (C) 2009-2018 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 *)
From Coq Require Import Lia.
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).
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.
lia.
Qed.
Theorem Falign_spec_exp:
forall f1 f2 : float beta,
snd (Falign f1 f2) = Z.min (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) : 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.
intros (m1,e1).
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.
intros (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.
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 plus_IZR.
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.
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) = Z.min (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 m1 e) (Float m2 e) = Float (m1 - m2) e.
Proof.
intros m1 m2 e.
unfold Fminus.
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.
intros (m1, e1) (m2, e2).
unfold Fmult, F2R. simpl.
rewrite mult_IZR, bpow_plus.
ring.
Qed.
End Float_ops.
|
