Commit c7756ed4 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Realize axiom Round_logic_def in Coq.

parent 5fa2b7df
...@@ -17,12 +17,6 @@ Definition round: floating_point.Rounding.mode -> R -> R. ...@@ -17,12 +17,6 @@ Definition round: floating_point.Rounding.mode -> R -> R.
exact (round 53 1024). exact (round 53 1024).
Defined. Defined.
(* Why3 goal *)
Definition round_logic: floating_point.Rounding.mode -> R ->
floating_point.DoubleFormat.double.
exact (round_logic 53 1024 (refl_equal true) (refl_equal true)).
Defined.
(* Why3 goal *) (* Why3 goal *)
Definition value: floating_point.DoubleFormat.double -> R. Definition value: floating_point.DoubleFormat.double -> R.
exact (value 53 1024). exact (value 53 1024).
...@@ -56,7 +50,6 @@ Lemma Bounded_real_no_overflow : forall (m:floating_point.Rounding.mode) ...@@ -56,7 +50,6 @@ Lemma Bounded_real_no_overflow : forall (m:floating_point.Rounding.mode)
(x:R), (x:R),
((Rabs x) <= (9007199254740991 * 19958403095347198116563727130368385660674512604354575415025472424372118918689640657849579654926357010893424468441924952439724379883935936607391717982848314203200056729510856765175377214443629871826533567445439239933308104551208703888888552684480441575071209068757560416423584952303440099278848)%R)%R -> ((Rabs x) <= (9007199254740991 * 19958403095347198116563727130368385660674512604354575415025472424372118918689640657849579654926357010893424468441924952439724379883935936607391717982848314203200056729510856765175377214443629871826533567445439239933308104551208703888888552684480441575071209068757560416423584952303440099278848)%R)%R ->
(no_overflow m x). (no_overflow m x).
(* YOU MAY EDIT THE PROOF BELOW *)
exact (Bounded_real_no_overflow 53 1024 (refl_equal true) (refl_equal true)). exact (Bounded_real_no_overflow 53 1024 (refl_equal true) (refl_equal true)).
Qed. Qed.
...@@ -117,6 +110,19 @@ Lemma Round_up_neg : forall (x:R), ((round floating_point.Rounding.Up ...@@ -117,6 +110,19 @@ Lemma Round_up_neg : forall (x:R), ((round floating_point.Rounding.Up
now apply Round_up_neg. now apply Round_up_neg.
Qed. Qed.
(* Why3 goal *)
Definition round_logic: floating_point.Rounding.mode -> R ->
floating_point.DoubleFormat.double.
exact (round_logic 53 1024 (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.
exact (Round_logic_def 53 1024 (refl_equal true) (refl_equal true)).
Qed.
(* Why3 assumption *) (* Why3 assumption *)
Definition of_real_post (m:floating_point.Rounding.mode) (x:R) Definition of_real_post (m:floating_point.Rounding.mode) (x:R)
(res:floating_point.DoubleFormat.double): Prop := ((value res) = (round m (res:floating_point.DoubleFormat.double): Prop := ((value res) = (round m
......
...@@ -188,11 +188,6 @@ Definition round: floating_point.Rounding.mode -> R -> R. ...@@ -188,11 +188,6 @@ Definition round: floating_point.Rounding.mode -> R -> R.
exact (fun m => round radix2 fexp (round_mode (rnd_of_mode m))). exact (fun m => round radix2 fexp (round_mode (rnd_of_mode m))).
Defined. Defined.
(* Why3 goal *)
Definition round_logic: floating_point.Rounding.mode -> R -> t.
exact (fun m r => r_to_fp_aux m r r r).
Defined.
(* Why3 assumption *) (* Why3 assumption *)
Definition round_error(x:t): R := (Rabs ((value x) - (exact x))%R). Definition round_error(x:t): R := (Rabs ((value x) - (exact x))%R).
...@@ -387,4 +382,30 @@ rewrite Round_down_neg. ...@@ -387,4 +382,30 @@ rewrite Round_down_neg.
now rewrite Ropp_involutive. now rewrite Ropp_involutive.
Qed. Qed.
(* Why3 goal *)
Definition round_logic: floating_point.Rounding.mode -> R -> t.
exact (fun m r => r_to_fp_aux m r r r).
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 h1.
unfold value, round_logic.
simpl.
apply r_to_fp_correct.
apply Rle_lt_trans with (1 := h1).
replace emax with (prec + (emax - prec))%Z by ring.
rewrite bpow_plus.
apply Rmult_lt_compat_r.
apply bpow_gt_0.
simpl.
rewrite <- Z2R_Zpower.
apply Z2R_lt.
apply Zlt_pred.
apply Zlt_le_weak.
exact Hprec'.
Qed.
End GenFloat. End GenFloat.
...@@ -17,12 +17,6 @@ Definition round: floating_point.Rounding.mode -> R -> R. ...@@ -17,12 +17,6 @@ Definition round: floating_point.Rounding.mode -> R -> R.
exact (round 24 128). exact (round 24 128).
Defined. Defined.
(* 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 *) (* Why3 goal *)
Definition value: floating_point.SingleFormat.single -> R. Definition value: floating_point.SingleFormat.single -> R.
exact (value 24 128). exact (value 24 128).
...@@ -59,7 +53,6 @@ Qed. ...@@ -59,7 +53,6 @@ Qed.
Lemma Bounded_real_no_overflow : forall (m:floating_point.Rounding.mode) Lemma Bounded_real_no_overflow : forall (m:floating_point.Rounding.mode)
(x:R), ((Rabs x) <= (33554430 * 10141204801825835211973625643008)%R)%R -> (x:R), ((Rabs x) <= (33554430 * 10141204801825835211973625643008)%R)%R ->
(no_overflow m x). (no_overflow m x).
(* YOU MAY EDIT THE PROOF BELOW *)
intros m x Hx. intros m x Hx.
unfold no_overflow. unfold no_overflow.
rewrite max_single_eq in *. rewrite max_single_eq in *.
...@@ -125,6 +118,22 @@ Lemma Round_up_neg : forall (x:R), ((round floating_point.Rounding.Up ...@@ -125,6 +118,22 @@ Lemma Round_up_neg : forall (x:R), ((round floating_point.Rounding.Up
now apply Round_up_neg. now apply Round_up_neg.
Qed. Qed.
(* 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.
(* Why3 assumption *) (* Why3 assumption *)
Definition of_real_post (m:floating_point.Rounding.mode) (x:R) Definition of_real_post (m:floating_point.Rounding.mode) (x:R)
(res:floating_point.SingleFormat.single): Prop := ((value res) = (round m (res:floating_point.SingleFormat.single): Prop := ((value res) = (round m
......
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