Commit 14972b6d authored by Guillaume Melquiond's avatar Guillaume Melquiond

Update parts of Coq realizations whose printing looks sane.

parent 070cdf54
...@@ -1754,8 +1754,8 @@ Defined. ...@@ -1754,8 +1754,8 @@ Defined.
(* Why3 goal *) (* Why3 goal *)
Lemma eq_sub_bv_def : Lemma eq_sub_bv_def :
forall (a:t) (b:t) (i:t) (n:t), forall (a:t) (b:t) (i:t) (n:t),
let mask := (lsl_bv (sub (lsl_bv one n) one) i) in let mask := lsl_bv (sub (lsl_bv one n) one) i in
((eq_sub_bv a b i n) <-> ((bw_and b mask) = (bw_and a mask))). (eq_sub_bv a b i n) <-> ((bw_and b mask) = (bw_and a mask)).
rewrite Of_int_one. rewrite Of_int_one.
easy. easy.
Qed. Qed.
......
...@@ -61,7 +61,7 @@ Lemma Bounded_real_no_overflow : ...@@ -61,7 +61,7 @@ Lemma Bounded_real_no_overflow :
forall (m:floating_point.Rounding.mode) (x:R), forall (m:floating_point.Rounding.mode) (x:R),
((Reals.Rbasic_fun.Rabs x) <= ((Reals.Rbasic_fun.Rabs x) <=
(9007199254740991 * 19958403095347198116563727130368385660674512604354575415025472424372118918689640657849579654926357010893424468441924952439724379883935936607391717982848314203200056729510856765175377214443629871826533567445439239933308104551208703888888552684480441575071209068757560416423584952303440099278848)%R)%R -> (9007199254740991 * 19958403095347198116563727130368385660674512604354575415025472424372118918689640657849579654926357010893424468441924952439724379883935936607391717982848314203200056729510856765175377214443629871826533567445439239933308104551208703888888552684480441575071209068757560416423584952303440099278848)%R)%R ->
(no_overflow m x). no_overflow m x.
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.
......
...@@ -65,7 +65,7 @@ Qed. ...@@ -65,7 +65,7 @@ Qed.
Lemma Bounded_real_no_overflow : Lemma Bounded_real_no_overflow :
forall (m:floating_point.Rounding.mode) (x:R), forall (m:floating_point.Rounding.mode) (x:R),
((Reals.Rbasic_fun.Rabs x) <= ((Reals.Rbasic_fun.Rabs x) <=
(33554430 * 10141204801825835211973625643008)%R)%R -> (no_overflow m x). (33554430 * 10141204801825835211973625643008)%R)%R -> no_overflow m x.
intros m x Hx. intros m x Hx.
unfold no_overflow. unfold no_overflow.
rewrite max_single_eq in *. rewrite max_single_eq in *.
......
...@@ -243,13 +243,13 @@ Proof. ...@@ -243,13 +243,13 @@ Proof.
Qed. Qed.
(* Why3 goal *) (* Why3 goal *)
Lemma zeroF_is_positive : (is_positive zeroF). Lemma zeroF_is_positive : is_positive zeroF.
Proof. Proof.
apply zeroF_is_positive. apply zeroF_is_positive.
Qed. Qed.
(* Why3 goal *) (* Why3 goal *)
Lemma zeroF_is_zero : (is_zero zeroF). Lemma zeroF_is_zero : is_zero zeroF.
Proof. Proof.
apply zeroF_is_zero. apply zeroF_is_zero.
Qed. Qed.
...@@ -319,7 +319,7 @@ Definition in_int_range (i:Z) : Prop := ...@@ -319,7 +319,7 @@ Definition in_int_range (i:Z) : Prop :=
((-max_int)%Z <= i)%Z /\ (i <= max_int)%Z. ((-max_int)%Z <= i)%Z /\ (i <= max_int)%Z.
(* Why3 goal *) (* Why3 goal *)
Lemma is_finite : forall (x:t), (t'isFinite x) -> (in_range (t'real x)). Lemma is_finite : forall (x:t), (t'isFinite x) -> in_range (t'real x).
Proof. Proof.
unfold t'isFinite, in_range. unfold t'isFinite, in_range.
intros x Hx. intros x Hx.
...@@ -329,12 +329,12 @@ Qed. ...@@ -329,12 +329,12 @@ Qed.
(* Why3 assumption *) (* Why3 assumption *)
Definition no_overflow (m:ieee_float.RoundingMode.mode) (x:R) : Prop := Definition no_overflow (m:ieee_float.RoundingMode.mode) (x:R) : Prop :=
(in_range (round m x)). in_range (round m x).
(* Why3 goal *) (* Why3 goal *)
Lemma Bounded_real_no_overflow : Lemma Bounded_real_no_overflow :
forall (m:ieee_float.RoundingMode.mode) (x:R), forall (m:ieee_float.RoundingMode.mode) (x:R),
(in_range x) -> (no_overflow m x). (in_range x) -> no_overflow m x.
Proof. Proof.
unfold no_overflow, in_range. unfold no_overflow, in_range.
rewrite <- max_real_cst. rewrite <- max_real_cst.
...@@ -421,41 +421,40 @@ Definition diff_sign (x:t) (y:t) : Prop := ...@@ -421,41 +421,40 @@ Definition diff_sign (x:t) (y:t) : Prop :=
((is_negative x) /\ (is_positive y)). ((is_negative x) /\ (is_positive y)).
(* Why3 goal *) (* Why3 goal *)
Lemma feq_eq : forall (x:t) (y:t), (t'isFinite x) -> ((t'isFinite y) -> Lemma feq_eq :
((~ (is_zero x)) -> ((eq x y) -> (x = y)))). forall (x:t) (y:t),
(t'isFinite x) -> (t'isFinite y) -> ~ (is_zero x) -> (eq x y) -> (x = y).
Proof. Proof.
apply feq_eq. apply feq_eq.
Qed. Qed.
(* Why3 goal *) (* Why3 goal *)
Lemma eq_feq : Lemma eq_feq :
forall (x:t) (y:t), forall (x:t) (y:t), (t'isFinite x) -> (t'isFinite y) -> (x = y) -> eq x y.
(t'isFinite x) -> ((t'isFinite y) -> ((x = y) -> (eq x y))).
Proof. Proof.
apply eq_feq. apply eq_feq.
Qed. Qed.
(* Why3 goal *) (* Why3 goal *)
Lemma eq_refl : forall (x:t), (t'isFinite x) -> (eq x x). Lemma eq_refl : forall (x:t), (t'isFinite x) -> eq x x.
Proof. Proof.
apply eq_refl. apply eq_refl.
Qed. Qed.
(* Why3 goal *) (* Why3 goal *)
Lemma eq_sym : forall (x:t) (y:t), (eq x y) -> (eq y x). Lemma eq_sym : forall (x:t) (y:t), (eq x y) -> eq y x.
Proof. Proof.
apply eq_sym. apply eq_sym.
Qed. Qed.
(* Why3 goal *) (* Why3 goal *)
Lemma eq_trans : Lemma eq_trans : forall (x:t) (y:t) (z:t), (eq x y) -> (eq y z) -> eq x z.
forall (x:t) (y:t) (z:t), (eq x y) -> ((eq y z) -> (eq x z)).
Proof. Proof.
apply eq_trans. apply eq_trans.
Qed. Qed.
(* Why3 goal *) (* Why3 goal *)
Lemma eq_zero : (eq zeroF (neg zeroF)). Lemma eq_zero : eq zeroF (neg zeroF).
Proof. Proof.
apply eq_zero. apply eq_zero.
Qed. Qed.
...@@ -464,7 +463,7 @@ Qed. ...@@ -464,7 +463,7 @@ Qed.
Lemma eq_to_real_finite : Lemma eq_to_real_finite :
forall (x:t) (y:t), forall (x:t) (y:t),
((t'isFinite x) /\ (t'isFinite y)) -> ((t'isFinite x) /\ (t'isFinite y)) ->
((eq x y) <-> ((t'real x) = (t'real y))). (eq x y) <-> ((t'real x) = (t'real y)).
Proof. Proof.
apply eq_to_real_finite. apply eq_to_real_finite.
Qed. Qed.
...@@ -481,7 +480,7 @@ Qed. ...@@ -481,7 +480,7 @@ Qed.
Lemma lt_finite : Lemma lt_finite :
forall (x:t) (y:t), forall (x:t) (y:t),
((t'isFinite x) /\ (t'isFinite y)) -> ((t'isFinite x) /\ (t'isFinite y)) ->
((lt x y) <-> ((t'real x) < (t'real y))%R). (lt x y) <-> ((t'real x) < (t'real y))%R.
Proof. Proof.
apply lt_finite. apply lt_finite.
Qed. Qed.
...@@ -490,27 +489,27 @@ Qed. ...@@ -490,27 +489,27 @@ Qed.
Lemma le_finite : Lemma le_finite :
forall (x:t) (y:t), forall (x:t) (y:t),
((t'isFinite x) /\ (t'isFinite y)) -> ((t'isFinite x) /\ (t'isFinite y)) ->
((le x y) <-> ((t'real x) <= (t'real y))%R). (le x y) <-> ((t'real x) <= (t'real y))%R.
Proof. Proof.
apply le_finite. apply le_finite.
Qed. Qed.
(* Why3 goal *) (* Why3 goal *)
Lemma le_lt_trans : Lemma le_lt_trans :
forall (x:t) (y:t) (z:t), ((le x y) /\ (lt y z)) -> (lt x z). forall (x:t) (y:t) (z:t), ((le x y) /\ (lt y z)) -> lt x z.
Proof. Proof.
apply le_lt_trans. apply le_lt_trans.
Qed. Qed.
(* Why3 goal *) (* Why3 goal *)
Lemma lt_le_trans : Lemma lt_le_trans :
forall (x:t) (y:t) (z:t), ((lt x y) /\ (le y z)) -> (lt x z). forall (x:t) (y:t) (z:t), ((lt x y) /\ (le y z)) -> lt x z.
Proof. Proof.
apply lt_le_trans. apply lt_le_trans.
Qed. Qed.
(* Why3 goal *) (* Why3 goal *)
Lemma le_ge_asym : forall (x:t) (y:t), ((le x y) /\ (le y x)) -> (eq x y). Lemma le_ge_asym : forall (x:t) (y:t), ((le x y) /\ (le y x)) -> eq x y.
Proof. Proof.
apply le_ge_asym. apply le_ge_asym.
Qed. Qed.
...@@ -518,7 +517,7 @@ Qed. ...@@ -518,7 +517,7 @@ Qed.
(* Why3 goal *) (* Why3 goal *)
Lemma not_lt_ge : Lemma not_lt_ge :
forall (x:t) (y:t), forall (x:t) (y:t),
((~ (lt x y)) /\ ((is_not_nan x) /\ (is_not_nan y))) -> (le y x). (~ (lt x y) /\ ((is_not_nan x) /\ (is_not_nan y))) -> le y x.
Proof. Proof.
apply not_lt_ge. apply not_lt_ge.
Qed. Qed.
...@@ -526,7 +525,7 @@ Qed. ...@@ -526,7 +525,7 @@ Qed.
(* Why3 goal *) (* Why3 goal *)
Lemma not_gt_le : Lemma not_gt_le :
forall (x:t) (y:t), forall (x:t) (y:t),
((~ (lt y x)) /\ ((is_not_nan x) /\ (is_not_nan y))) -> (le x y). (~ (lt y x) /\ ((is_not_nan x) /\ (is_not_nan y))) -> le x y.
Proof. Proof.
apply not_gt_le. apply not_gt_le.
Qed. Qed.
...@@ -550,35 +549,35 @@ Qed. ...@@ -550,35 +549,35 @@ Qed.
(* Why3 goal *) (* Why3 goal *)
Lemma lt_lt_finite : Lemma lt_lt_finite :
forall (x:t) (y:t) (z:t), (lt x y) -> ((lt y z) -> (t'isFinite y)). forall (x:t) (y:t) (z:t), (lt x y) -> (lt y z) -> t'isFinite y.
Proof. Proof.
apply lt_lt_finite. apply lt_lt_finite.
Qed. Qed.
(* Why3 goal *) (* Why3 goal *)
Lemma positive_to_real : Lemma positive_to_real :
forall (x:t), (t'isFinite x) -> ((is_positive x) -> (0%R <= (t'real x))%R). forall (x:t), (t'isFinite x) -> (is_positive x) -> (0%R <= (t'real x))%R.
Proof. Proof.
apply positive_to_real. apply positive_to_real.
Qed. Qed.
(* Why3 goal *) (* Why3 goal *)
Lemma to_real_positive : Lemma to_real_positive :
forall (x:t), (t'isFinite x) -> ((0%R < (t'real x))%R -> (is_positive x)). forall (x:t), (t'isFinite x) -> (0%R < (t'real x))%R -> is_positive x.
Proof. Proof.
apply to_real_positive. apply to_real_positive.
Qed. Qed.
(* Why3 goal *) (* Why3 goal *)
Lemma negative_to_real : Lemma negative_to_real :
forall (x:t), (t'isFinite x) -> ((is_negative x) -> ((t'real x) <= 0%R)%R). forall (x:t), (t'isFinite x) -> (is_negative x) -> ((t'real x) <= 0%R)%R.
Proof. Proof.
apply negative_to_real. apply negative_to_real.
Qed. Qed.
(* Why3 goal *) (* Why3 goal *)
Lemma to_real_negative : Lemma to_real_negative :
forall (x:t), (t'isFinite x) -> (((t'real x) < 0%R)%R -> (is_negative x)). forall (x:t), (t'isFinite x) -> ((t'real x) < 0%R)%R -> is_negative x.
Proof. Proof.
apply to_real_negative. apply to_real_negative.
Qed. Qed.
...@@ -592,7 +591,7 @@ Qed. ...@@ -592,7 +591,7 @@ Qed.
(* Why3 goal *) (* Why3 goal *)
Lemma negative_or_positive : Lemma negative_or_positive :
forall (x:t), (is_not_nan x) -> ((is_positive x) \/ (is_negative x)). forall (x:t), (is_not_nan x) -> (is_positive x) \/ (is_negative x).
Proof. Proof.
apply negative_or_positive. apply negative_or_positive.
Qed. Qed.
...@@ -600,7 +599,7 @@ Qed. ...@@ -600,7 +599,7 @@ Qed.
(* Why3 goal *) (* Why3 goal *)
Lemma diff_sign_trans : Lemma diff_sign_trans :
forall (x:t) (y:t) (z:t), forall (x:t) (y:t) (z:t),
((diff_sign x y) /\ (diff_sign y z)) -> (same_sign x z). ((diff_sign x y) /\ (diff_sign y z)) -> same_sign x z.
Proof. Proof.
apply diff_sign_trans. apply diff_sign_trans.
Qed. Qed.
...@@ -623,8 +622,7 @@ Qed. ...@@ -623,8 +622,7 @@ Qed.
(* Why3 assumption *) (* Why3 assumption *)
Definition product_sign (z:t) (x:t) (y:t) : Prop := Definition product_sign (z:t) (x:t) (y:t) : Prop :=
((same_sign x y) -> (is_positive z)) /\ ((same_sign x y) -> is_positive z) /\ ((diff_sign x y) -> is_negative z).
((diff_sign x y) -> (is_negative z)).
(* Why3 assumption *) (* Why3 assumption *)
Definition overflow_value (m:ieee_float.RoundingMode.mode) (x:t) : Prop := Definition overflow_value (m:ieee_float.RoundingMode.mode) (x:t) : Prop :=
...@@ -647,8 +645,8 @@ Definition overflow_value (m:ieee_float.RoundingMode.mode) (x:t) : Prop := ...@@ -647,8 +645,8 @@ Definition overflow_value (m:ieee_float.RoundingMode.mode) (x:t) : Prop :=
Definition sign_zero_result (m:ieee_float.RoundingMode.mode) (x:t) : Prop := Definition sign_zero_result (m:ieee_float.RoundingMode.mode) (x:t) : Prop :=
(is_zero x) -> (is_zero x) ->
match m with match m with
| ieee_float.RoundingMode.RTN => (is_negative x) | ieee_float.RoundingMode.RTN => is_negative x
| _ => (is_positive x) | _ => is_positive x
end. end.
(* Why3 goal *) (* Why3 goal *)
...@@ -698,7 +696,7 @@ Qed. ...@@ -698,7 +696,7 @@ Qed.
(* Why3 goal *) (* Why3 goal *)
Lemma sub_finite_rev : Lemma sub_finite_rev :
forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t), forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
(t'isFinite (sub m x y)) -> ((t'isFinite x) /\ (t'isFinite y)). (t'isFinite (sub m x y)) -> (t'isFinite x) /\ (t'isFinite y).
Proof. Proof.
apply sub_finite_rev. apply sub_finite_rev.
Qed. Qed.
...@@ -730,7 +728,7 @@ Qed. ...@@ -730,7 +728,7 @@ Qed.
(* Why3 goal *) (* Why3 goal *)
Lemma mul_finite_rev : Lemma mul_finite_rev :
forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t), forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
(t'isFinite (mul m x y)) -> ((t'isFinite x) /\ (t'isFinite y)). (t'isFinite (mul m x y)) -> (t'isFinite x) /\ (t'isFinite y).
Proof. Proof.
apply mul_finite_rev. apply mul_finite_rev.
Qed. Qed.
...@@ -763,8 +761,8 @@ Qed. ...@@ -763,8 +761,8 @@ Qed.
Lemma div_finite_rev : Lemma div_finite_rev :
forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t), forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
(t'isFinite (div m x y)) -> (t'isFinite (div m x y)) ->
(((t'isFinite x) /\ ((t'isFinite y) /\ ~ (is_zero y))) \/ ((t'isFinite x) /\ ((t'isFinite y) /\ ~ (is_zero y))) \/
((t'isFinite x) /\ ((is_infinite y) /\ ((t'real (div m x y)) = 0%R)))). ((t'isFinite x) /\ ((is_infinite y) /\ ((t'real (div m x y)) = 0%R))).
Proof. Proof.
apply div_finite_rev. apply div_finite_rev.
Qed. Qed.
...@@ -785,7 +783,7 @@ Qed. ...@@ -785,7 +783,7 @@ Qed.
Lemma neg_finite : Lemma neg_finite :
forall (x:t), forall (x:t),
(t'isFinite x) -> (t'isFinite x) ->
((t'isFinite (neg x)) /\ ((t'real (neg x)) = (-(t'real x))%R)). (t'isFinite (neg x)) /\ ((t'real (neg x)) = (-(t'real x))%R).
Proof. Proof.
apply neg_finite. apply neg_finite.
Qed. Qed.
...@@ -794,7 +792,7 @@ Qed. ...@@ -794,7 +792,7 @@ Qed.
Lemma neg_finite_rev : Lemma neg_finite_rev :
forall (x:t), forall (x:t),
(t'isFinite (neg x)) -> (t'isFinite (neg x)) ->
((t'isFinite x) /\ ((t'real (neg x)) = (-(t'real x))%R)). (t'isFinite x) /\ ((t'real (neg x)) = (-(t'real x))%R).
Proof. Proof.
apply neg_finite_rev. apply neg_finite_rev.
Qed. Qed.
...@@ -811,7 +809,7 @@ Qed. ...@@ -811,7 +809,7 @@ Qed.
Lemma abs_finite_rev : Lemma abs_finite_rev :
forall (x:t), forall (x:t),
(t'isFinite (abs x)) -> (t'isFinite (abs x)) ->
((t'isFinite x) /\ ((t'real (abs x)) = (Reals.Rbasic_fun.Rabs (t'real x)))). (t'isFinite x) /\ ((t'real (abs x)) = (Reals.Rbasic_fun.Rabs (t'real x))).
Proof. Proof.
apply abs_finite_rev. apply abs_finite_rev.
Qed. Qed.
...@@ -954,9 +952,9 @@ Qed. ...@@ -954,9 +952,9 @@ Qed.
(* Why3 goal *) (* Why3 goal *)
Lemma neg_special : Lemma neg_special :
forall (x:t), forall (x:t),
((is_nan x) -> (is_nan (neg x))) /\ ((is_nan x) -> is_nan (neg x)) /\
(((is_infinite x) -> (is_infinite (neg x))) /\ (((is_infinite x) -> is_infinite (neg x)) /\
((~ (is_nan x)) -> (diff_sign x (neg x)))). (~ (is_nan x) -> diff_sign x (neg x))).
Proof. Proof.
apply neg_special. apply neg_special.
Qed. Qed.
...@@ -964,9 +962,9 @@ Qed. ...@@ -964,9 +962,9 @@ Qed.
(* Why3 goal *) (* Why3 goal *)
Lemma abs_special : Lemma abs_special :
forall (x:t), forall (x:t),
((is_nan x) -> (is_nan (abs x))) /\ ((is_nan x) -> is_nan (abs x)) /\
(((is_infinite x) -> (is_infinite (abs x))) /\ (((is_infinite x) -> is_infinite (abs x)) /\
((~ (is_nan x)) -> (is_positive (abs x)))). (~ (is_nan x) -> is_positive (abs x))).
Proof. Proof.
apply abs_special. apply abs_special.
Qed. Qed.
...@@ -1048,25 +1046,25 @@ Proof. ...@@ -1048,25 +1046,25 @@ Proof.
Qed. Qed.
(* Why3 goal *) (* Why3 goal *)
Lemma Min_r : forall (x:t) (y:t), (le y x) -> (eq (min x y) y). Lemma Min_r : forall (x:t) (y:t), (le y x) -> eq (min x y) y.
Proof. Proof.
apply Min_r. apply Min_r.
Qed. Qed.
(* Why3 goal *) (* Why3 goal *)
Lemma Min_l : forall (x:t) (y:t), (le x y) -> (eq (min x y) x). Lemma Min_l : forall (x:t) (y:t), (le x y) -> eq (min x y) x.
Proof. Proof.
apply Min_l. apply Min_l.
Qed. Qed.
(* Why3 goal *) (* Why3 goal *)
Lemma Max_r : forall (x:t) (y:t), (le y x) -> (eq (max x y) x). Lemma Max_r : forall (x:t) (y:t), (le y x) -> eq (max x y) x.
Proof. Proof.
apply Max_r. apply Max_r.
Qed. Qed.
(* Why3 goal *) (* Why3 goal *)
Lemma Max_l : forall (x:t) (y:t), (le x y) -> (eq (max x y) y). Lemma Max_l : forall (x:t) (y:t), (le x y) -> eq (max x y) y.
Proof. Proof.
apply Max_l. apply Max_l.
Qed. Qed.
...@@ -1078,7 +1076,7 @@ Proof. ...@@ -1078,7 +1076,7 @@ Proof.
Defined. Defined.
(* Why3 goal *) (* Why3 goal *)