Commit 0293fa40 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Update some additional Coq realizations.

parent 4a8c0479
......@@ -981,7 +981,7 @@ clean::
update-coq: bin/why3 drivers/coq-realizations.aux
for f in $(COQLIBS_INT_FILES); do bin/why3 --realize -D drivers/coq-realize.drv -T int.$$f -o lib/coq/int/; done
for f in $(COQLIBS_REAL_FILES); do bin/why3 --realize -D drivers/coq-realize.drv -T real.$$f -o lib/coq/real/; done
#for f in $(COQLIBS_FP_FILES); do bin/why3 --realize -D drivers/coq-realize.drv -T floating_point.$$f -o lib/coq/floating_point/; done
for f in $(COQLIBS_FP_FILES); do bin/why3 --realize -D drivers/coq-realize.drv -T floating_point.$$f -o lib/coq/floating_point/; done
else
......
......@@ -8,32 +8,51 @@ Require real.Real.
Require real.Abs.
Require real.FromInt.
Require floating_point.Rounding.
Require Import floating_point.GenFloat.
Definition double : Type := t 53 1024.
Definition round: floating_point.Rounding.mode -> R -> R := round 53 1024.
Definition round_logic: floating_point.Rounding.mode -> R -> double := round_logic 53 1024 (refl_equal true) (refl_equal true).
Definition value: double -> R := value 53 1024.
Definition exact: double -> R := exact 53 1024.
Definition model: double -> R := model 53 1024.
Require Import floating_point.GenFloat.
(* Why3 goal *)
Definition double : Type.
exact (t 53 1024).
Defined.
(* Why3 goal *)
Definition round: floating_point.Rounding.mode -> R -> R.
exact (round 53 1024).
Defined.
(* Why3 goal *)
Definition round_logic: floating_point.Rounding.mode -> R -> double.
exact (round_logic 53 1024 (refl_equal true) (refl_equal true)).
Defined.
(* Why3 goal *)
Definition value: double -> R.
exact (value 53 1024).
Defined.
(* Why3 goal *)
Definition exact: double -> R.
exact (exact 53 1024).
Defined.
(* Why3 goal *)
Definition model: double -> R.
exact (model 53 1024).
Defined.
(* Why3 assumption *)
Definition round_error(x:double): R := (Rabs ((value x) - (exact x))%R).
(* Why3 assumption *)
Definition total_error(x:double): R := (Rabs ((value x) - (model x))%R).
(* Why3 assumption *)
Definition no_overflow(m:floating_point.Rounding.mode) (x:R): Prop :=
((Rabs (round m
x)) <= (9007199254740991 * 19958403095347198116563727130368385660674512604354575415025472424372118918689640657849579654926357010893424468441924952439724379883935936607391717982848314203200056729510856765175377214443629871826533567445439239933308104551208703888888552684480441575071209068757560416423584952303440099278848)%R)%R.
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Bounded_real_no_overflow : forall (m:floating_point.Rounding.mode)
(x:R),
((Rabs x) <= (9007199254740991 * 19958403095347198116563727130368385660674512604354575415025472424372118918689640657849579654926357010893424468441924952439724379883935936607391717982848314203200056729510856765175377214443629871826533567445439239933308104551208703888888552684480441575071209068757560416423584952303440099278848)%R)%R ->
......@@ -41,106 +60,62 @@ Lemma Bounded_real_no_overflow : forall (m:floating_point.Rounding.mode)
(* YOU MAY EDIT THE PROOF BELOW *)
exact (Bounded_real_no_overflow 53 1024 (refl_equal true) (refl_equal true)).
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Round_monotonic : forall (m:floating_point.Rounding.mode) (x:R) (y:R),
(x <= y)%R -> ((round m x) <= (round m y))%R.
(* YOU MAY EDIT THE PROOF BELOW *)
now apply Round_monotonic.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Round_idempotent : forall (m1:floating_point.Rounding.mode)
(m2:floating_point.Rounding.mode) (x:R), ((round m1 (round m2
x)) = (round m2 x)).
(* YOU MAY EDIT THE PROOF BELOW *)
now apply Round_idempotent.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Round_value : forall (m:floating_point.Rounding.mode) (x:double),
((round m (value x)) = (value x)).
(* YOU MAY EDIT THE PROOF BELOW *)
now apply Round_value.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Bounded_value : forall (x:double),
((Rabs (value x)) <= (9007199254740991 * 19958403095347198116563727130368385660674512604354575415025472424372118918689640657849579654926357010893424468441924952439724379883935936607391717982848314203200056729510856765175377214443629871826533567445439239933308104551208703888888552684480441575071209068757560416423584952303440099278848)%R)%R.
(* YOU MAY EDIT THE PROOF BELOW *)
now apply Bounded_value.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Exact_rounding_for_integers : forall (m:floating_point.Rounding.mode)
(i:Z), (((-9007199254740992%Z)%Z <= i)%Z /\ (i <= 9007199254740992%Z)%Z) ->
((round m (IZR i)) = (IZR i)).
(* YOU MAY EDIT THE PROOF BELOW *)
intros m i Hi.
now apply Exact_rounding_for_integers.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Round_down_le : forall (x:R), ((round floating_point.Rounding.Down
x) <= x)%R.
(* YOU MAY EDIT THE PROOF BELOW *)
now apply Round_down_le.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Round_up_ge : forall (x:R), (x <= (round floating_point.Rounding.Up
x))%R.
(* YOU MAY EDIT THE PROOF BELOW *)
now apply Round_up_ge.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Round_down_neg : forall (x:R), ((round floating_point.Rounding.Down
(-x)%R) = (-(round floating_point.Rounding.Up x))%R).
(* YOU MAY EDIT THE PROOF BELOW *)
now apply Round_down_neg.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Round_up_neg : forall (x:R), ((round floating_point.Rounding.Up
(-x)%R) = (-(round floating_point.Rounding.Down x))%R).
(* YOU MAY EDIT THE PROOF BELOW *)
now apply Round_up_neg.
Qed.
(* DO NOT EDIT BELOW *)
......@@ -8,25 +8,46 @@ Require real.Real.
Require real.Abs.
Require real.FromInt.
Require floating_point.Rounding.
Require Import floating_point.GenFloat.
Definition single : Type := t 24 128.
Definition round: floating_point.Rounding.mode -> R -> R := round 24 128.
Definition round_logic: floating_point.Rounding.mode -> R -> single := round_logic 24 128 (refl_equal true) (refl_equal true).
Definition value: single -> R := value 24 128.
Definition exact: single -> R := exact 24 128.
Definition model: single -> R := model 24 128.
Require Import floating_point.GenFloat.
(* Why3 goal *)
Definition single : Type.
exact (t 24 128).
Defined.
(* Why3 goal *)
Definition round: floating_point.Rounding.mode -> R -> R.
exact (round 24 128).
Defined.
(* Why3 goal *)
Definition round_logic: floating_point.Rounding.mode -> R -> single.
exact (round_logic 24 128 (refl_equal true) (refl_equal true)).
Defined.
(* Why3 goal *)
Definition value: single -> R.
exact (value 24 128).
Defined.
(* Why3 goal *)
Definition exact: single -> R.
exact (exact 24 128).
Defined.
(* Why3 goal *)
Definition model: single -> R.
exact (model 24 128).
Defined.
(* Why3 assumption *)
Definition round_error(x:single): R := (Rabs ((value x) - (exact x))%R).
(* Why3 assumption *)
Definition total_error(x:single): R := (Rabs ((value x) - (model x))%R).
(* Why3 assumption *)
Definition no_overflow(m:floating_point.Rounding.mode) (x:R): Prop :=
((Rabs (round m x)) <= (33554430 * 10141204801825835211973625643008)%R)%R.
......@@ -35,11 +56,7 @@ unfold max, Fcore_defs.F2R; simpl.
ring.
Qed.
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Bounded_real_no_overflow : forall (m:floating_point.Rounding.mode)
(x:R), ((Rabs x) <= (33554430 * 10141204801825835211973625643008)%R)%R ->
(no_overflow m x).
......@@ -49,108 +66,64 @@ 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.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Round_monotonic : forall (m:floating_point.Rounding.mode) (x:R) (y:R),
(x <= y)%R -> ((round m x) <= (round m y))%R.
(* YOU MAY EDIT THE PROOF BELOW *)
apply Round_monotonic.
easy.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Round_idempotent : forall (m1:floating_point.Rounding.mode)
(m2:floating_point.Rounding.mode) (x:R), ((round m1 (round m2
x)) = (round m2 x)).
(* YOU MAY EDIT THE PROOF BELOW *)
now apply Round_idempotent.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Round_value : forall (m:floating_point.Rounding.mode) (x:single),
((round m (value x)) = (value x)).
(* YOU MAY EDIT THE PROOF BELOW *)
now apply Round_value.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Bounded_value : forall (x:single),
((Rabs (value x)) <= (33554430 * 10141204801825835211973625643008)%R)%R.
(* YOU MAY EDIT THE PROOF BELOW *)
rewrite max_single_eq.
now apply Bounded_value.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
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)).
(* YOU MAY EDIT THE PROOF BELOW *)
intros m i Hi.
now apply Exact_rounding_for_integers.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Round_down_le : forall (x:R), ((round floating_point.Rounding.Down
x) <= x)%R.
(* YOU MAY EDIT THE PROOF BELOW *)
now apply Round_down_le.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Round_up_ge : forall (x:R), (x <= (round floating_point.Rounding.Up
x))%R.
(* YOU MAY EDIT THE PROOF BELOW *)
now apply Round_up_ge.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Round_down_neg : forall (x:R), ((round floating_point.Rounding.Down
(-x)%R) = (-(round floating_point.Rounding.Up x))%R).
(* YOU MAY EDIT THE PROOF BELOW *)
now apply Round_down_neg.
Qed.
(* DO NOT EDIT BELOW *)
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Lemma Round_up_neg : forall (x:R), ((round floating_point.Rounding.Up
(-x)%R) = (-(round floating_point.Rounding.Down x))%R).
(* YOU MAY EDIT THE PROOF BELOW *)
now apply Round_up_neg.
Qed.
(* DO NOT EDIT BELOW *)
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment