Single.v 5.6 KB
Newer Older
1 2
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below    *)
3
Require Import BuiltIn.
4
Require Import Rbasic_fun.
5
Require BuiltIn.
6 7 8 9 10
Require int.Int.
Require real.Real.
Require real.Abs.
Require real.FromInt.
Require floating_point.Rounding.
11
Require floating_point.SingleFormat.
12

13
Require Import floating_point.GenFloat.
14

15 16 17 18 19 20
(* Why3 goal *)
Definition round: floating_point.Rounding.mode -> R -> R.
exact (round 24 128).
Defined.

(* Why3 goal *)
21 22
Definition round_logic: floating_point.Rounding.mode -> R ->
  floating_point.SingleFormat.single.
23 24 25 26
exact (round_logic 24 128 (refl_equal true) (refl_equal true)).
Defined.

(* Why3 goal *)
27
Definition value: floating_point.SingleFormat.single -> R.
28 29 30 31
exact (value 24 128).
Defined.

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

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

(* Why3 assumption *)
42 43
Definition round_error(x:floating_point.SingleFormat.single): R :=
  (Rabs ((value x) - (exact x))%R).
44

45
(* Why3 assumption *)
46 47
Definition total_error(x:floating_point.SingleFormat.single): R :=
  (Rabs ((value x) - (model x))%R).
48

49
(* Why3 assumption *)
50 51 52 53 54 55 56 57
Definition no_overflow(m:floating_point.Rounding.mode) (x:R): Prop :=
  ((Rabs (round m x)) <= (33554430 * 10141204801825835211973625643008)%R)%R.

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

58
(* Why3 goal *)
59 60 61 62 63 64 65 66 67 68
Lemma Bounded_real_no_overflow : forall (m:floating_point.Rounding.mode)
  (x:R), ((Rabs x) <= (33554430 * 10141204801825835211973625643008)%R)%R ->
  (no_overflow m x).
(* YOU MAY EDIT THE PROOF BELOW *)
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.

69
(* Why3 goal *)
70 71 72 73 74 75
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.

76
(* Why3 goal *)
77 78 79 80 81 82
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.

83
(* Why3 goal *)
84 85
Lemma Round_value : forall (m:floating_point.Rounding.mode)
  (x:floating_point.SingleFormat.single), ((round m (value x)) = (value x)).
86 87 88
now apply Round_value.
Qed.

89
(* Why3 goal *)
90
Lemma Bounded_value : forall (x:floating_point.SingleFormat.single),
91 92 93 94 95
  ((Rabs (value x)) <= (33554430 * 10141204801825835211973625643008)%R)%R.
rewrite max_single_eq.
now apply Bounded_value.
Qed.

96
(* Why3 goal *)
97 98 99 100 101 102 103
Lemma Exact_rounding_for_integers : forall (m:floating_point.Rounding.mode)
  (i:Z), (((-16777216%Z)%Z <= i)%Z /\ (i <= 16777216%Z)%Z) -> ((round m
  (IZR i)) = (IZR i)).
intros m i Hi.
now apply Exact_rounding_for_integers.
Qed.

104
(* Why3 goal *)
105 106 107 108 109
Lemma Round_down_le : forall (x:R), ((round floating_point.Rounding.Down
  x) <= x)%R.
now apply Round_down_le.
Qed.

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

116
(* Why3 goal *)
117 118 119 120 121
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.

122
(* Why3 goal *)
123 124 125 126
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.
127

128
(* Why3 assumption *)
129 130 131 132 133 134 135 136 137
Definition of_real_post(m:floating_point.Rounding.mode) (x:R)
  (res:floating_point.SingleFormat.single): Prop := ((value res) = (round m
  x)) /\ (((exact res) = x) /\ ((model res) = x)).

(* Why3 assumption *)
Definition add_post(m:floating_point.Rounding.mode)
  (x:floating_point.SingleFormat.single)
  (y:floating_point.SingleFormat.single)
  (res:floating_point.SingleFormat.single): Prop := ((value res) = (round m
138 139 140 141 142
  ((value x) + (value y))%R)) /\
  (((exact res) = ((exact x) + (exact y))%R) /\
  ((model res) = ((model x) + (model y))%R)).

(* Why3 assumption *)
143 144 145 146
Definition sub_post(m:floating_point.Rounding.mode)
  (x:floating_point.SingleFormat.single)
  (y:floating_point.SingleFormat.single)
  (res:floating_point.SingleFormat.single): Prop := ((value res) = (round m
147 148 149 150 151
  ((value x) - (value y))%R)) /\
  (((exact res) = ((exact x) - (exact y))%R) /\
  ((model res) = ((model x) - (model y))%R)).

(* Why3 assumption *)
152 153 154 155
Definition mul_post(m:floating_point.Rounding.mode)
  (x:floating_point.SingleFormat.single)
  (y:floating_point.SingleFormat.single)
  (res:floating_point.SingleFormat.single): Prop := ((value res) = (round m
156 157 158 159 160
  ((value x) * (value y))%R)) /\
  (((exact res) = ((exact x) * (exact y))%R) /\
  ((model res) = ((model x) * (model y))%R)).

(* Why3 assumption *)
161 162 163 164
Definition div_post(m:floating_point.Rounding.mode)
  (x:floating_point.SingleFormat.single)
  (y:floating_point.SingleFormat.single)
  (res:floating_point.SingleFormat.single): Prop := ((value res) = (round m
165 166 167 168 169
  (Rdiv (value x) (value y))%R)) /\
  (((exact res) = (Rdiv (exact x) (exact y))%R) /\
  ((model res) = (Rdiv (model x) (model y))%R)).

(* Why3 assumption *)
170 171
Definition neg_post(x:floating_point.SingleFormat.single)
  (res:floating_point.SingleFormat.single): Prop :=
172 173 174 175
  ((value res) = (-(value x))%R) /\ (((exact res) = (-(exact x))%R) /\
  ((model res) = (-(model x))%R)).

(* Why3 assumption *)
176 177
Definition lt(x:floating_point.SingleFormat.single)
  (y:floating_point.SingleFormat.single): Prop := ((value x) < (value y))%R.
178 179

(* Why3 assumption *)
180 181
Definition gt(x:floating_point.SingleFormat.single)
  (y:floating_point.SingleFormat.single): Prop := ((value y) < (value x))%R.
182

183