blob: 4e0a25e6aa36d4377142ad8c7bb31c5d737c0aee (
plain)
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
|
(**
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.
*)
(** * Fixed-point format *)
Require Import Raux Defs Round_pred Generic_fmt Ulp Round_NE.
Section RND_FIX.
Variable beta : radix.
Notation bpow := (bpow beta).
Variable emin : Z.
Inductive FIX_format (x : R) : Prop :=
FIX_spec (f : float beta) :
x = F2R f -> (Fexp f = emin)%Z -> FIX_format x.
Definition FIX_exp (e : Z) := emin.
(** Properties of the FIX format *)
Global Instance FIX_exp_valid : Valid_exp FIX_exp.
Proof.
intros k.
unfold FIX_exp.
split ; intros H.
now apply Zlt_le_weak.
split.
apply Z.le_refl.
now intros _ _.
Qed.
Theorem generic_format_FIX :
forall x, FIX_format x -> generic_format beta FIX_exp x.
Proof.
intros x [[xm xe] Hx1 Hx2].
rewrite Hx1.
now apply generic_format_canonical.
Qed.
Theorem FIX_format_generic :
forall x, generic_format beta FIX_exp x -> FIX_format x.
Proof.
intros x H.
rewrite H.
eexists ; repeat split.
Qed.
Theorem FIX_format_satisfies_any :
satisfies_any FIX_format.
Proof.
refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FIX_exp)).
intros x.
split.
apply FIX_format_generic.
apply generic_format_FIX.
Qed.
Global Instance FIX_exp_monotone : Monotone_exp FIX_exp.
Proof.
intros ex ey H.
apply Z.le_refl.
Qed.
Theorem ulp_FIX :
forall x, ulp beta FIX_exp x = bpow emin.
Proof.
intros x; unfold ulp.
case Req_bool_spec; intros Zx.
case (negligible_exp_spec FIX_exp).
intros T; specialize (T (emin-1)%Z); contradict T.
unfold FIX_exp; omega.
intros n _; reflexivity.
reflexivity.
Qed.
End RND_FIX.
|
