Single.v 6.67 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2018   --   Inria - CNRS - Paris-Sud University  *)
5 6 7 8 9 10 11
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)

12 13 14 15 16 17 18 19 20 21 22
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below    *)
Require Import BuiltIn.
Require Reals.Rbasic_fun.
Require BuiltIn.
Require int.Int.
Require real.Real.
Require real.Abs.
Require real.FromInt.
Require floating_point.Rounding.
Require floating_point.SingleFormat.
23

24
Require Import floating_point.GenFloat.
25

26 27 28 29 30 31
(* Why3 goal *)
Definition round: floating_point.Rounding.mode -> R -> R.
exact (round 24 128).
Defined.

(* Why3 goal *)
32
Definition value: floating_point.SingleFormat.single -> R.
33 34 35 36
exact (value 24 128).
Defined.

(* Why3 goal *)
37
Definition exact: floating_point.SingleFormat.single -> R.
38 39 40 41
exact (exact 24 128).
Defined.

(* Why3 goal *)
42
Definition model: floating_point.SingleFormat.single -> R.
43 44 45 46
exact (model 24 128).
Defined.

(* Why3 assumption *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
47
Definition round_error (x:floating_point.SingleFormat.single): R :=
Guillaume Melquiond's avatar
Guillaume Melquiond committed
48
  (Reals.Rbasic_fun.Rabs ((value x) - (exact x))%R).
49

50
(* Why3 assumption *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
51
Definition total_error (x:floating_point.SingleFormat.single): R :=
Guillaume Melquiond's avatar
Guillaume Melquiond committed
52
  (Reals.Rbasic_fun.Rabs ((value x) - (model x))%R).
53

54
(* Why3 assumption *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
55
Definition no_overflow (m:floating_point.Rounding.mode) (x:R): Prop :=
Guillaume Melquiond's avatar
Guillaume Melquiond committed
56 57
  ((Reals.Rbasic_fun.Rabs (round m
  x)) <= (33554430 * 10141204801825835211973625643008)%R)%R.
58 59 60 61 62 63

Lemma max_single_eq: (33554430 * 10141204801825835211973625643008 = max 24 128)%R.
unfold max, Fcore_defs.F2R; simpl.
ring.
Qed.

64
(* Why3 goal *)
65
Lemma Bounded_real_no_overflow : forall (m:floating_point.Rounding.mode)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
66 67
  (x:R),
  ((Reals.Rbasic_fun.Rabs x) <= (33554430 * 10141204801825835211973625643008)%R)%R ->
68 69 70 71 72 73 74
  (no_overflow m x).
intros m x Hx.
unfold no_overflow.
rewrite max_single_eq in *.
exact (Bounded_real_no_overflow 24 128 (refl_equal true) (refl_equal true) m x Hx).
Qed.

75
(* Why3 goal *)
76 77 78 79 80 81
Lemma Round_monotonic : forall (m:floating_point.Rounding.mode) (x:R) (y:R),
  (x <= y)%R -> ((round m x) <= (round m y))%R.
apply Round_monotonic.
easy.
Qed.

82
(* Why3 goal *)
83 84 85 86 87 88
Lemma Round_idempotent : forall (m1:floating_point.Rounding.mode)
  (m2:floating_point.Rounding.mode) (x:R), ((round m1 (round m2
  x)) = (round m2 x)).
now apply Round_idempotent.
Qed.

89
(* Why3 goal *)
90 91
Lemma Round_value : forall (m:floating_point.Rounding.mode)
  (x:floating_point.SingleFormat.single), ((round m (value x)) = (value x)).
92 93 94
now apply Round_value.
Qed.

95
(* Why3 goal *)
96
Lemma Bounded_value : forall (x:floating_point.SingleFormat.single),
Guillaume Melquiond's avatar
Guillaume Melquiond committed
97
  ((Reals.Rbasic_fun.Rabs (value x)) <= (33554430 * 10141204801825835211973625643008)%R)%R.
98 99 100 101
rewrite max_single_eq.
now apply Bounded_value.
Qed.

102
(* Why3 goal *)
103 104
Lemma Exact_rounding_for_integers : forall (m:floating_point.Rounding.mode)
  (i:Z), (((-16777216%Z)%Z <= i)%Z /\ (i <= 16777216%Z)%Z) -> ((round m
Guillaume Melquiond's avatar
Guillaume Melquiond committed
105 106
  (BuiltIn.IZR i)) = (BuiltIn.IZR i)).
Proof.
107 108 109 110
intros m i Hi.
now apply Exact_rounding_for_integers.
Qed.

111
(* Why3 goal *)
112 113 114 115 116
Lemma Round_down_le : forall (x:R), ((round floating_point.Rounding.Down
  x) <= x)%R.
now apply Round_down_le.
Qed.

117
(* Why3 goal *)
118 119 120 121 122
Lemma Round_up_ge : forall (x:R), (x <= (round floating_point.Rounding.Up
  x))%R.
now apply Round_up_ge.
Qed.

123
(* Why3 goal *)
124 125 126 127 128
Lemma Round_down_neg : forall (x:R), ((round floating_point.Rounding.Down
  (-x)%R) = (-(round floating_point.Rounding.Up x))%R).
now apply Round_down_neg.
Qed.

129
(* Why3 goal *)
130 131 132 133
Lemma Round_up_neg : forall (x:R), ((round floating_point.Rounding.Up
  (-x)%R) = (-(round floating_point.Rounding.Down x))%R).
now apply Round_up_neg.
Qed.
134

135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150
(* Why3 goal *)
Definition round_logic: floating_point.Rounding.mode -> R ->
  floating_point.SingleFormat.single.
exact (round_logic 24 128 (refl_equal true) (refl_equal true)).
Defined.

(* Why3 goal *)
Lemma Round_logic_def : forall (m:floating_point.Rounding.mode) (x:R),
  (no_overflow m x) -> ((value (round_logic m x)) = (round m x)).
Proof.
intros m x.
unfold no_overflow.
rewrite max_single_eq.
exact (Round_logic_def 24 128 (refl_equal true) (refl_equal true) m x).
Qed.

151
(* Why3 assumption *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
152
Definition of_real_post (m:floating_point.Rounding.mode) (x:R)
153 154 155 156
  (res:floating_point.SingleFormat.single): Prop := ((value res) = (round m
  x)) /\ (((exact res) = x) /\ ((model res) = x)).

(* Why3 assumption *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
157
Definition add_post (m:floating_point.Rounding.mode)
158 159 160
  (x:floating_point.SingleFormat.single)
  (y:floating_point.SingleFormat.single)
  (res:floating_point.SingleFormat.single): Prop := ((value res) = (round m
161 162 163 164 165
  ((value x) + (value y))%R)) /\
  (((exact res) = ((exact x) + (exact y))%R) /\
  ((model res) = ((model x) + (model y))%R)).

(* Why3 assumption *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
166
Definition sub_post (m:floating_point.Rounding.mode)
167 168 169
  (x:floating_point.SingleFormat.single)
  (y:floating_point.SingleFormat.single)
  (res:floating_point.SingleFormat.single): Prop := ((value res) = (round m
170 171 172 173 174
  ((value x) - (value y))%R)) /\
  (((exact res) = ((exact x) - (exact y))%R) /\
  ((model res) = ((model x) - (model y))%R)).

(* Why3 assumption *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
175
Definition mul_post (m:floating_point.Rounding.mode)
176 177 178
  (x:floating_point.SingleFormat.single)
  (y:floating_point.SingleFormat.single)
  (res:floating_point.SingleFormat.single): Prop := ((value res) = (round m
179 180 181 182 183
  ((value x) * (value y))%R)) /\
  (((exact res) = ((exact x) * (exact y))%R) /\
  ((model res) = ((model x) * (model y))%R)).

(* Why3 assumption *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
184
Definition div_post (m:floating_point.Rounding.mode)
185 186 187
  (x:floating_point.SingleFormat.single)
  (y:floating_point.SingleFormat.single)
  (res:floating_point.SingleFormat.single): Prop := ((value res) = (round m
Guillaume Melquiond's avatar
Guillaume Melquiond committed
188 189 190
  ((value x) / (value y))%R)) /\
  (((exact res) = ((exact x) / (exact y))%R) /\
  ((model res) = ((model x) / (model y))%R)).
191 192

(* Why3 assumption *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
193
Definition neg_post (x:floating_point.SingleFormat.single)
194
  (res:floating_point.SingleFormat.single): Prop :=
195 196 197 198
  ((value res) = (-(value x))%R) /\ (((exact res) = (-(exact x))%R) /\
  ((model res) = (-(model x))%R)).

(* Why3 assumption *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
199
Definition lt (x:floating_point.SingleFormat.single)
200
  (y:floating_point.SingleFormat.single): Prop := ((value x) < (value y))%R.
201 202

(* Why3 assumption *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
203
Definition gt (x:floating_point.SingleFormat.single)
204
  (y:floating_point.SingleFormat.single): Prop := ((value y) < (value x))%R.
205