Flocq_defs.v 2.61 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

BOLDO Sylvie's avatar
BOLDO Sylvie committed
15
16
17
Definition MonotoneP (rnd : R -> R) :=
  forall x y : R,
  (x <= y)%R -> (rnd x <= rnd y)%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
18

Guillaume Melquiond's avatar
Guillaume Melquiond committed
19
Definition IdempotentP (F : R -> Prop) (rnd : R -> R) :=
BOLDO Sylvie's avatar
BOLDO Sylvie committed
20
21
    (forall x : R, F (rnd x))
        /\ (forall x : R, F x -> rnd x = x). 
BOLDO Sylvie's avatar
BOLDO Sylvie committed
22

BOLDO Sylvie's avatar
BOLDO Sylvie committed
23
Definition Rounding_for_Format (F : R -> Prop) (rnd : R -> R) :=
Guillaume Melquiond's avatar
Guillaume Melquiond committed
24
   MonotoneP rnd /\ IdempotentP F rnd.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
25
26
27

End Def.

28
29
30
31
Implicit Arguments Fnum [[beta]].
Implicit Arguments Fexp [[beta]].
Implicit Arguments F2R [[beta]].

BOLDO Sylvie's avatar
BOLDO Sylvie committed
32
33
34
Section RND.

(* property of being a rounding toward -inf *)
35
36
37
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
38

BOLDO Sylvie's avatar
BOLDO Sylvie committed
39
40
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
41
42

(* property of being a rounding toward +inf *)
43
44
45
46
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
47
48
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
49
50

(* property of being a rounding toward zero *)
BOLDO Sylvie's avatar
BOLDO Sylvie committed
51
52
53
54
55
56
57
58
59
60
61
62
63
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
64
65
assert (F 0%R).
replace 0%R with (rnd 0%R).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
66
67
68
eapply H.
apply Rle_refl.
destruct (H 0%R) as (H1, H2).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
69
apply Rle_antisym.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
70
71
72
73
74
apply H1.
apply Rle_refl.
apply H2.
apply Rle_refl.
(* . *)
BOLDO Sylvie's avatar
BOLDO Sylvie committed
75
76
77
78
destruct (Rle_or_lt 0 x).
(* positive *)
rewrite Rabs_right.
rewrite Rabs_right; auto with real.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
79
now apply (proj1 (H x)).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
80
apply Rle_ge.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
81
now apply (proj1 (H x)).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
82
83
84
85
(* negative *)
rewrite Rabs_left1.
rewrite Rabs_left1 ; auto with real.
apply Ropp_le_contravar.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
86
apply (proj2 (H x)).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
87
auto with real.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
88
apply (proj2 (H x)) ; auto with real.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
89
90
91
Qed.

(* property of being a rounding to nearest *)
92
93
94
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
95

BOLDO Sylvie's avatar
BOLDO Sylvie committed
96
97
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
98

BOLDO Sylvie's avatar
BOLDO Sylvie committed
99
100
101
102
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
103

BOLDO Sylvie's avatar
BOLDO Sylvie committed
104
105
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
106
107

End RND.