Flocq_defs.v 3.65 KB
Newer Older
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1
2
3
4
5
Require Import Flocq_Raux.

Section Def.

Record float (beta : radix) := Float { Fnum : Z ; Fexp : Z }.
6

BOLDO Sylvie's avatar
BOLDO Sylvie committed
7
8
9
Implicit Arguments Fnum [[beta]].
Implicit Arguments Fexp [[beta]].

10
11
12
13
Variable beta : radix.

Definition F2R (f : float beta) :=
  (Z2R (Fnum f) * epow beta (Fexp f))%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
14
15
16
17
18
19

(* A rounding mode will be a function, ie a R -> R                         *)
(* It will then have to satisfy a number of properties on a given domain D *)
(*    The domain will be used to formalize Overflow, flush to zero...      *)


BOLDO Sylvie's avatar
BOLDO Sylvie committed
20
21
22
Definition MonotoneP (rnd : R -> R) :=
  forall x y : R,
  (x <= y)%R -> (rnd x <= rnd y)%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
23

24

Guillaume Melquiond's avatar
Guillaume Melquiond committed
25
Definition IdempotentP (F : R -> Prop) (rnd : R -> R) :=
BOLDO Sylvie's avatar
BOLDO Sylvie committed
26
27
    (forall x : R, F (rnd x))
        /\ (forall x : R, F x -> rnd x = x). 
BOLDO Sylvie's avatar
BOLDO Sylvie committed
28

BOLDO Sylvie's avatar
BOLDO Sylvie committed
29
Definition Rounding_for_Format (F : R -> Prop) (rnd : R -> R) :=
Guillaume Melquiond's avatar
Guillaume Melquiond committed
30
   MonotoneP rnd /\ IdempotentP F rnd.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47

(* unbounded floating-point format *)
Definition FLX_format (prec : Z) (x : R) :=
  exists f : float beta,
  x = F2R f /\ (Zabs (Fnum f) < Zpower (radix_val beta) prec)%Z.

(* floating-point format with gradual underflow *)
Definition FLT_format (emin prec : Z) (x : R) :=
  exists f : float beta,
  x = F2R f /\ (Zabs (Fnum f) < Zpower (radix_val beta) prec)%Z /\ (emin <= Fexp f)%Z.

(* fixed-point format *)
Definition FIX_format (emin : Z) (x : R) :=
  exists f : float beta,
  x = F2R f /\ (Fexp f = emin)%Z.

Definition FLX_RoundingModeP (prec : Z) (rnd : R -> R):=
BOLDO Sylvie's avatar
BOLDO Sylvie committed
48
  Rounding_for_Format (FLX_format prec) rnd.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
49
50

Definition FLT_RoundingModeP (emin prec : Z) (rnd : R -> R):=
BOLDO Sylvie's avatar
BOLDO Sylvie committed
51
  Rounding_for_Format (FLT_format emin prec) rnd.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
52
53

Definition FIX_RoundingModeP (emin : Z) (rnd : R -> R):=
BOLDO Sylvie's avatar
BOLDO Sylvie committed
54
  Rounding_for_Format (FIX_format emin) rnd.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
55
56
57

End Def.

58
59
60
61
Implicit Arguments Fnum [[beta]].
Implicit Arguments Fexp [[beta]].
Implicit Arguments F2R [[beta]].

BOLDO Sylvie's avatar
BOLDO Sylvie committed
62
63
64
Section RND.

(* property of being a rounding toward -inf *)
65
66
67
Definition Rnd_DN_pt (F : R -> Prop) (x f : R) :=
  F f /\ (f <= x)%R /\
  forall g : R, F g -> (g <= x)%R -> (g <= f)%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
68

BOLDO Sylvie's avatar
BOLDO Sylvie committed
69
70
Definition Rnd_DN (F : R -> Prop) (rnd : R -> R) :=
  forall x : R, Rnd_DN_pt F x (rnd x).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
71
72

(* property of being a rounding toward +inf *)
73
74
75
76
Definition Rnd_UP_pt (F : R -> Prop) (x f : R) :=
  F f /\ (x <= f)%R /\
  forall g : R, F g -> (x <= g)%R -> (f <= g)%R.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
77
78
Definition Rnd_UP (F : R -> Prop) (rnd : R -> R) :=
  forall x : R, Rnd_UP_pt F x (rnd x).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
79
80

(* property of being a rounding toward zero *)
BOLDO Sylvie's avatar
BOLDO Sylvie committed
81
82
83
84
85
86
87
88
89
90
91
92
93
Definition Rnd_ZR_pt (F : R -> Prop) (x f : R) :=
  ( (0 <= x)%R -> Rnd_DN_pt F x f ) /\
  ( (x <= 0)%R -> Rnd_UP_pt F x f ).

Definition Rnd_ZR (F : R -> Prop) (rnd : R -> R) :=
  forall x : R, Rnd_ZR_pt F x (rnd x).

Theorem toto :
  forall (F : R -> Prop) (rnd: R-> R), 
  Rnd_ZR F rnd ->
  forall x : R,  (Rabs (rnd x) <= Rabs x)%R.
Proof.
intros F rnd H x.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
94
95
assert (F 0%R).
replace 0%R with (rnd 0%R).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
96
97
98
eapply H.
apply Rle_refl.
destruct (H 0%R) as (H1, H2).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
99
apply Rle_antisym.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
100
101
102
103
104
apply H1.
apply Rle_refl.
apply H2.
apply Rle_refl.
(* . *)
BOLDO Sylvie's avatar
BOLDO Sylvie committed
105
106
107
108
destruct (Rle_or_lt 0 x).
(* positive *)
rewrite Rabs_right.
rewrite Rabs_right; auto with real.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
109
now apply (proj1 (H x)).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
110
apply Rle_ge.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
111
now apply (proj1 (H x)).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
112
113
114
115
(* negative *)
rewrite Rabs_left1.
rewrite Rabs_left1 ; auto with real.
apply Ropp_le_contravar.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
116
apply (proj2 (H x)).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
117
auto with real.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
118
apply (proj2 (H x)) ; auto with real.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
119
120
121
Qed.

(* property of being a rounding to nearest *)
122
123
124
Definition Rnd_N_pt (F : R -> Prop) (x f : R) :=
  F f /\
  forall g : R, F g -> (Rabs (f - x) <= Rabs (g - x))%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
125

BOLDO Sylvie's avatar
BOLDO Sylvie committed
126
127
Definition Rnd_N (F : R -> Prop) (rnd : R -> R) :=
  forall x : R, Rnd_N_pt F x (rnd x).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
128

BOLDO Sylvie's avatar
BOLDO Sylvie committed
129
130
131
132
Definition Rnd_NA_pt (F : R -> Prop) (x f : R) :=
  Rnd_N_pt F x f /\
  forall f2 : R, Rnd_N_pt F x f2 ->
  (Rabs f2 <= Rabs f)%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
133

BOLDO Sylvie's avatar
BOLDO Sylvie committed
134
135
Definition Rnd_NA (F : R -> Prop) (rnd : R -> R) :=
  forall x : R, Rnd_NA_pt F x (rnd x).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
136
137

End RND.