Commit ef0af75d authored by Guillaume Melquiond's avatar Guillaume Melquiond

Update parts of Coq realizations whose printing looks sane.

parent fb2fc569
......@@ -53,10 +53,11 @@ Qed.
(* Why3 goal *)
Lemma xorb_def :
forall (x:bool) (y:bool),
((Init.Datatypes.xorb x y) = match x with
| false => y
| true => (Init.Datatypes.negb y)
end).
((Init.Datatypes.xorb x y) =
match x with
| false => y
| true => (Init.Datatypes.negb y)
end).
Proof.
intros x y.
destruct x; destruct y; auto.
......
......@@ -1497,8 +1497,8 @@ Qed.
Lemma to_uint_sub_bounded :
forall (v1:t) (v2:t),
((0%Z <= ((to_uint v1) - (to_uint v2))%Z)%Z /\
(((to_uint v1) - (to_uint v2))%Z < two_power_size)%Z) -> ((to_uint (sub v1
v2)) = ((to_uint v1) - (to_uint v2))%Z).
(((to_uint v1) - (to_uint v2))%Z < two_power_size)%Z) ->
((to_uint (sub v1 v2)) = ((to_uint v1) - (to_uint v2))%Z).
intros v1 v2 (h1,h2).
rewrite <-(mod1_out (to_uint v1 - to_uint v2) two_power_size) by auto.
apply to_uint_sub.
......@@ -1512,8 +1512,8 @@ Defined.
(* Why3 goal *)
Lemma to_uint_neg :
forall (v:t),
((to_uint (neg v)) = (int.EuclideanDivision.mod1 (-(to_uint v))%Z
two_power_size)).
((to_uint (neg v)) =
(int.EuclideanDivision.mod1 (-(to_uint v))%Z two_power_size)).
intros v.
apply to_uint_of_int, mod1_in_range2.
Qed.
......@@ -1532,9 +1532,10 @@ Lemma to_uint_mul : forall (v1:t) (v2:t), ((to_uint (mul v1
Qed.
(* Why3 goal *)
Lemma to_uint_mul_bounded : forall (v1:t) (v2:t),
(((to_uint v1) * (to_uint v2))%Z < two_power_size)%Z -> ((to_uint (mul v1
v2)) = ((to_uint v1) * (to_uint v2))%Z).
Lemma to_uint_mul_bounded :
forall (v1:t) (v2:t),
(((to_uint v1) * (to_uint v2))%Z < two_power_size)%Z ->
((to_uint (mul v1 v2)) = ((to_uint v1) * (to_uint v2))%Z).
intros v1 v2 h1.
rewrite <-(mod1_out (to_uint v1 * to_uint v2) two_power_size).
apply to_uint_mul.
......@@ -1549,8 +1550,10 @@ Definition udiv : t -> t -> t.
Defined.
(* Why3 goal *)
Lemma to_uint_udiv : forall (v1:t) (v2:t), ((to_uint (udiv v1
v2)) = (int.EuclideanDivision.div (to_uint v1) (to_uint v2))).
Lemma to_uint_udiv :
forall (v1:t) (v2:t),
((to_uint (udiv v1 v2)) =
(int.EuclideanDivision.div (to_uint v1) (to_uint v2))).
intros v1 v2.
apply to_uint_of_int.
case (Z.eq_dec (to_uint v2) 0); intro.
......@@ -1571,8 +1574,10 @@ Definition urem : t -> t -> t.
Defined.
(* Why3 goal *)
Lemma to_uint_urem : forall (v1:t) (v2:t), ((to_uint (urem v1
v2)) = (int.EuclideanDivision.mod1 (to_uint v1) (to_uint v2))).
Lemma to_uint_urem :
forall (v1:t) (v2:t),
((to_uint (urem v1 v2)) =
(int.EuclideanDivision.mod1 (to_uint v1) (to_uint v2))).
intros v1 v2.
apply to_uint_of_int.
case (Z.eq_dec (to_uint v2) 0); intro.
......@@ -1598,9 +1603,10 @@ Lemma lsr_bv_is_lsr :
Qed.
(* Why3 goal *)
Lemma to_uint_lsr : forall (v:t) (n:t), ((to_uint (lsr_bv v
n)) = (int.EuclideanDivision.div (to_uint v)
(bv.Pow2int.pow2 (to_uint n)))).
Lemma to_uint_lsr :
forall (v:t) (n:t),
((to_uint (lsr_bv v n)) =
(int.EuclideanDivision.div (to_uint v) (bv.Pow2int.pow2 (to_uint n)))).
intros v n.
apply to_uint_lsr_aux.
Qed.
......@@ -1688,8 +1694,9 @@ Lemma nth_bv_def_aux : forall {l} (x:Vector.t bool (S l)) (i:Z),
Qed.
(* Why3 goal *)
Lemma nth_bv_def : forall (x:t) (i:t), ((nth_bv x i) = true) <->
~ ((bw_and (lsr_bv x i) one) = zeros).
Lemma nth_bv_def :
forall (x:t) (i:t),
((nth_bv x i) = true) <-> ~ ((bw_and (lsr_bv x i) one) = zeros).
intros; unfold nth_bv.
case (Z_lt_ge_dec (to_uint i) size); intro.
rewrite <-(Zplus_0_l (to_uint i)).
......
......@@ -52,14 +52,15 @@ Definition total_error (x:floating_point.DoubleFormat.double) : R :=
(Reals.Rbasic_fun.Rabs ((value x) - (model x))%R).
(* Why3 assumption *)
Definition no_overflow (m:floating_point.Rounding.mode) (x:R): Prop :=
((Reals.Rbasic_fun.Rabs (round m
x)) <= (9007199254740991 * 19958403095347198116563727130368385660674512604354575415025472424372118918689640657849579654926357010893424468441924952439724379883935936607391717982848314203200056729510856765175377214443629871826533567445439239933308104551208703888888552684480441575071209068757560416423584952303440099278848)%R)%R.
Definition no_overflow (m:floating_point.Rounding.mode) (x:R) : Prop :=
((Reals.Rbasic_fun.Rabs (round m x)) <=
(9007199254740991 * 19958403095347198116563727130368385660674512604354575415025472424372118918689640657849579654926357010893424468441924952439724379883935936607391717982848314203200056729510856765175377214443629871826533567445439239933308104551208703888888552684480441575071209068757560416423584952303440099278848)%R)%R.
(* Why3 goal *)
Lemma Bounded_real_no_overflow :
forall (m:floating_point.Rounding.mode) (x:R),
((Reals.Rbasic_fun.Rabs x) <= (9007199254740991 * 19958403095347198116563727130368385660674512604354575415025472424372118918689640657849579654926357010893424468441924952439724379883935936607391717982848314203200056729510856765175377214443629871826533567445439239933308104551208703888888552684480441575071209068757560416423584952303440099278848)%R)%R ->
((Reals.Rbasic_fun.Rabs x) <=
(9007199254740991 * 19958403095347198116563727130368385660674512604354575415025472424372118918689640657849579654926357010893424468441924952439724379883935936607391717982848314203200056729510856765175377214443629871826533567445439239933308104551208703888888552684480441575071209068757560416423584952303440099278848)%R)%R ->
(no_overflow m x).
exact (Bounded_real_no_overflow 53 1024 (refl_equal true) (refl_equal true)).
Qed.
......@@ -91,8 +92,9 @@ now apply Bounded_value.
Qed.
(* Why3 goal *)
Lemma Exact_rounding_for_integers : forall (m:floating_point.Rounding.mode)
(i:Z), (((-9007199254740992%Z)%Z <= i)%Z /\ (i <= 9007199254740992%Z)%Z) ->
Lemma Exact_rounding_for_integers :
forall (m:floating_point.Rounding.mode) (i:Z),
(((-9007199254740992%Z)%Z <= i)%Z /\ (i <= 9007199254740992%Z)%Z) ->
((round m (BuiltIn.IZR i)) = (BuiltIn.IZR i)).
Proof.
intros m i Hi.
......@@ -112,14 +114,18 @@ now apply Round_up_ge.
Qed.
(* Why3 goal *)
Lemma Round_down_neg : forall (x:R), ((round floating_point.Rounding.Down
(-x)%R) = (-(round floating_point.Rounding.Up x))%R).
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.
(* Why3 goal *)
Lemma Round_up_neg : forall (x:R), ((round floating_point.Rounding.Up
(-x)%R) = (-(round floating_point.Rounding.Down x))%R).
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.
......
......@@ -53,7 +53,8 @@ Definition total_error (x:floating_point.SingleFormat.single) : R :=
(* Why3 assumption *)
Definition no_overflow (m:floating_point.Rounding.mode) (x:R) : Prop :=
((Reals.Rbasic_fun.Rabs (round m x)) <= (33554430 * 10141204801825835211973625643008)%R)%R.
((Reals.Rbasic_fun.Rabs (round m x)) <=
(33554430 * 10141204801825835211973625643008)%R)%R.
Lemma max_single_eq: (33554430 * 10141204801825835211973625643008 = max 24 128)%R.
unfold max, Fcore_defs.F2R; simpl.
......@@ -63,8 +64,8 @@ Qed.
(* Why3 goal *)
Lemma Bounded_real_no_overflow :
forall (m:floating_point.Rounding.mode) (x:R),
((Reals.Rbasic_fun.Rabs x) <= (33554430 * 10141204801825835211973625643008)%R)%R ->
(no_overflow m x).
((Reals.Rbasic_fun.Rabs x) <=
(33554430 * 10141204801825835211973625643008)%R)%R -> (no_overflow m x).
intros m x Hx.
unfold no_overflow.
rewrite max_single_eq in *.
......@@ -95,15 +96,17 @@ Qed.
(* Why3 goal *)
Lemma Bounded_value :
forall (x:floating_point.SingleFormat.single),
((Reals.Rbasic_fun.Rabs (value x)) <= (33554430 * 10141204801825835211973625643008)%R)%R.
((Reals.Rbasic_fun.Rabs (value x)) <=
(33554430 * 10141204801825835211973625643008)%R)%R.
rewrite max_single_eq.
now apply Bounded_value.
Qed.
(* 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
(BuiltIn.IZR i)) = (BuiltIn.IZR i)).
Lemma Exact_rounding_for_integers :
forall (m:floating_point.Rounding.mode) (i:Z),
(((-16777216%Z)%Z <= i)%Z /\ (i <= 16777216%Z)%Z) ->
((round m (BuiltIn.IZR i)) = (BuiltIn.IZR i)).
Proof.
intros m i Hi.
now apply Exact_rounding_for_integers.
......@@ -122,25 +125,30 @@ now apply Round_up_ge.
Qed.
(* Why3 goal *)
Lemma Round_down_neg : forall (x:R), ((round floating_point.Rounding.Down
(-x)%R) = (-(round floating_point.Rounding.Up x))%R).
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.
(* Why3 goal *)
Lemma Round_up_neg : forall (x:R), ((round floating_point.Rounding.Up
(-x)%R) = (-(round floating_point.Rounding.Down x))%R).
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.
(* Why3 goal *)
Definition round_logic: floating_point.Rounding.mode -> R ->
floating_point.SingleFormat.single.
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),
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.
......
This diff is collapsed.
......@@ -301,7 +301,9 @@ Proof.
Defined.
(* Why3 goal *)
Lemma max_real_int : ((9007199254740991 * 19958403095347198116563727130368385660674512604354575415025472424372118918689640657849579654926357010893424468441924952439724379883935936607391717982848314203200056729510856765175377214443629871826533567445439239933308104551208703888888552684480441575071209068757560416423584952303440099278848)%R = (BuiltIn.IZR max_int)).
Lemma max_real_int :
((9007199254740991 * 19958403095347198116563727130368385660674512604354575415025472424372118918689640657849579654926357010893424468441924952439724379883935936607391717982848314203200056729510856765175377214443629871826533567445439239933308104551208703888888552684480441575071209068757560416423584952303440099278848)%R
= (BuiltIn.IZR max_int)).
Proof.
unfold max_int.
now rewrite mult_IZR, <- !Z2R_IZR.
......@@ -330,8 +332,9 @@ Definition no_overflow (m:ieee_float.RoundingMode.mode) (x:R) : Prop :=
(in_range (round m x)).
(* Why3 goal *)
Lemma Bounded_real_no_overflow : forall (m:ieee_float.RoundingMode.mode)
(x:R), (in_range x) -> (no_overflow m x).
Lemma Bounded_real_no_overflow :
forall (m:ieee_float.RoundingMode.mode) (x:R),
(in_range x) -> (no_overflow m x).
Proof.
unfold no_overflow, in_range.
rewrite <- max_real_cst.
......@@ -339,7 +342,8 @@ Proof.
Qed.
(* Why3 goal *)
Lemma Round_monotonic : forall (m:ieee_float.RoundingMode.mode) (x:R) (y:R),
Lemma Round_monotonic :
forall (m:ieee_float.RoundingMode.mode) (x:R) (y:R),
(x <= y)%R -> ((round m x) <= (round m y))%R.
Proof.
apply Round_monotonic.
......@@ -354,7 +358,8 @@ Proof.
Qed.
(* Why3 goal *)
Lemma Round_to_real : forall (m:ieee_float.RoundingMode.mode) (x:t),
Lemma Round_to_real :
forall (m:ieee_float.RoundingMode.mode) (x:t),
(t'isFinite x) -> ((round m (t'real x)) = (t'real x)).
Proof.
apply Round_to_real.
......@@ -375,15 +380,19 @@ Proof.
Qed.
(* Why3 goal *)
Lemma Round_down_neg : forall (x:R), ((round ieee_float.RoundingMode.RTN
(-x)%R) = (-(round ieee_float.RoundingMode.RTP x))%R).
Lemma Round_down_neg :
forall (x:R),
((round ieee_float.RoundingMode.RTN (-x)%R) =
(-(round ieee_float.RoundingMode.RTP x))%R).
Proof.
apply Round_down_neg.
Qed.
(* Why3 goal *)
Lemma Round_up_neg : forall (x:R), ((round ieee_float.RoundingMode.RTP
(-x)%R) = (-(round ieee_float.RoundingMode.RTN x))%R).
Lemma Round_up_neg :
forall (x:R),
((round ieee_float.RoundingMode.RTP (-x)%R) =
(-(round ieee_float.RoundingMode.RTN x))%R).
Proof.
apply Round_up_neg.
Qed.
......@@ -393,9 +402,9 @@ Definition in_safe_int_range (i:Z) : Prop :=
((-9007199254740992%Z)%Z <= i)%Z /\ (i <= 9007199254740992%Z)%Z.
(* Why3 goal *)
Lemma Exact_rounding_for_integers : forall (m:ieee_float.RoundingMode.mode)
(i:Z), (in_safe_int_range i) -> ((round m
(BuiltIn.IZR i)) = (BuiltIn.IZR i)).
Lemma Exact_rounding_for_integers :
forall (m:ieee_float.RoundingMode.mode) (i:Z),
(in_safe_int_range i) -> ((round m (BuiltIn.IZR i)) = (BuiltIn.IZR i)).
Proof.
intros m i h1.
now apply Exact_rounding_for_integers.
......@@ -419,8 +428,9 @@ Proof.
Qed.
(* Why3 goal *)
Lemma eq_feq : forall (x:t) (y:t), (t'isFinite x) -> ((t'isFinite y) ->
((x = y) -> (eq x y))).
Lemma eq_feq :
forall (x:t) (y:t),
(t'isFinite x) -> ((t'isFinite y) -> ((x = y) -> (eq x y))).
Proof.
apply eq_feq.
Qed.
......@@ -451,8 +461,10 @@ Proof.
Qed.
(* Why3 goal *)
Lemma eq_to_real_finite : forall (x:t) (y:t), ((t'isFinite x) /\ (t'isFinite
y)) -> ((eq x y) <-> ((t'real x) = (t'real y))).
Lemma eq_to_real_finite :
forall (x:t) (y:t),
((t'isFinite x) /\ (t'isFinite y)) ->
((eq x y) <-> ((t'real x) = (t'real y))).
Proof.
apply eq_to_real_finite.
Qed.
......@@ -473,7 +485,9 @@ Proof.
Qed.
(* Why3 goal *)
Lemma le_finite : forall (x:t) (y:t), ((t'isFinite x) /\ (t'isFinite y)) ->
Lemma le_finite :
forall (x:t) (y:t),
((t'isFinite x) /\ (t'isFinite y)) ->
((le x y) <-> ((t'real x) <= (t'real y))%R).
Proof.
apply le_finite.
......@@ -500,15 +514,17 @@ Proof.
Qed.
(* Why3 goal *)
Lemma not_lt_ge : forall (x:t) (y:t), ((~ (lt x y)) /\ ((is_not_nan x) /\
(is_not_nan y))) -> (le y x).
Lemma not_lt_ge :
forall (x:t) (y:t),
((~ (lt x y)) /\ ((is_not_nan x) /\ (is_not_nan y))) -> (le y x).
Proof.
apply not_lt_ge.
Qed.
(* Why3 goal *)
Lemma not_gt_le : forall (x:t) (y:t), ((~ (lt y x)) /\ ((is_not_nan x) /\
(is_not_nan y))) -> (le x y).
Lemma not_gt_le :
forall (x:t) (y:t),
((~ (lt y x)) /\ ((is_not_nan x) /\ (is_not_nan y))) -> (le x y).
Proof.
apply not_gt_le.
Qed.
......@@ -580,8 +596,9 @@ Proof.
Qed.
(* Why3 goal *)
Lemma diff_sign_trans : forall (x:t) (y:t) (z:t), ((diff_sign x y) /\
(diff_sign y z)) -> (same_sign x z).
Lemma diff_sign_trans :
forall (x:t) (y:t) (z:t),
((diff_sign x y) /\ (diff_sign y z)) -> (same_sign x z).
Proof.
apply diff_sign_trans.
Qed.
......@@ -594,8 +611,10 @@ Proof.
Qed.
(* Why3 goal *)
Lemma same_sign_product : forall (x:t) (y:t), ((t'isFinite x) /\ ((t'isFinite
y) /\ (same_sign x y))) -> (0%R <= ((t'real x) * (t'real y))%R)%R.
Lemma same_sign_product :
forall (x:t) (y:t),
((t'isFinite x) /\ ((t'isFinite y) /\ (same_sign x y))) ->
(0%R <= ((t'real x) * (t'real y))%R)%R.
Proof.
apply same_sign_product.
Qed.
......@@ -606,7 +625,7 @@ Definition product_sign (z:t) (x:t) (y:t) : Prop :=
((diff_sign x y) -> (is_negative z)).
(* Why3 assumption *)
Definition overflow_value (m:ieee_float.RoundingMode.mode) (x:t): Prop :=
Definition overflow_value (m:ieee_float.RoundingMode.mode) (x:t) : Prop :=
match m with
| ieee_float.RoundingMode.RTN => ((is_positive x) -> ((t'isFinite x) /\
((t'real x) = (9007199254740991 * 19958403095347198116563727130368385660674512604354575415025472424372118918689640657849579654926357010893424468441924952439724379883935936607391717982848314203200056729510856765175377214443629871826533567445439239933308104551208703888888552684480441575071209068757560416423584952303440099278848)%R))) /\
......@@ -643,7 +662,8 @@ Proof.
Qed.
(* Why3 goal *)
Lemma add_finite_rev : forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
Lemma add_finite_rev :
forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
(t'isFinite (add m x y)) -> ((t'isFinite x) /\ (t'isFinite y)).
Proof.
apply add_finite_rev.
......@@ -674,7 +694,8 @@ Proof.
Qed.
(* Why3 goal *)
Lemma sub_finite_rev : forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
Lemma sub_finite_rev :
forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
(t'isFinite (sub m x y)) -> ((t'isFinite x) /\ (t'isFinite y)).
Proof.
apply sub_finite_rev.
......@@ -705,7 +726,8 @@ Proof.
Qed.
(* Why3 goal *)
Lemma mul_finite_rev : forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
Lemma mul_finite_rev :
forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
(t'isFinite (mul m x y)) -> ((t'isFinite x) /\ (t'isFinite y)).
Proof.
apply mul_finite_rev.
......@@ -757,15 +779,19 @@ Proof.
Qed.
(* Why3 goal *)
Lemma neg_finite : forall (x:t), (t'isFinite x) -> ((t'isFinite (neg x)) /\
((t'real (neg x)) = (-(t'real x))%R)).
Lemma neg_finite :
forall (x:t),
(t'isFinite x) ->
((t'isFinite (neg x)) /\ ((t'real (neg x)) = (-(t'real x))%R)).
Proof.
apply neg_finite.
Qed.
(* Why3 goal *)
Lemma neg_finite_rev : forall (x:t), (t'isFinite (neg x)) -> ((t'isFinite
x) /\ ((t'real (neg x)) = (-(t'real x))%R)).
Lemma neg_finite_rev :
forall (x:t),
(t'isFinite (neg x)) ->
((t'isFinite x) /\ ((t'real (neg x)) = (-(t'real x))%R)).
Proof.
apply neg_finite_rev.
Qed.
......@@ -805,9 +831,10 @@ Proof.
Qed.
(* Why3 goal *)
Lemma fma_finite_rev : forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t)
(z:t), (t'isFinite (fma m x y z)) -> ((t'isFinite x) /\ ((t'isFinite y) /\
(t'isFinite z))).
Lemma fma_finite_rev :
forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t) (z:t),
(t'isFinite (fma m x y z)) ->
((t'isFinite x) /\ ((t'isFinite y) /\ (t'isFinite z))).
Proof.
apply fma_finite_rev.
Qed.
......@@ -842,8 +869,8 @@ Proof.
Qed.
(* Why3 assumption *)
Definition same_sign_real (x:t) (r:R): Prop := ((is_positive x) /\
(0%R < r)%R) \/ ((is_negative x) /\ (r < 0%R)%R).
Definition same_sign_real (x:t) (r:R) : Prop :=
((is_positive x) /\ (0%R < r)%R) \/ ((is_negative x) /\ (r < 0%R)%R).
(* Why3 goal *)
Lemma add_special : forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
......@@ -920,17 +947,21 @@ Proof.
Qed.
(* Why3 goal *)
Lemma neg_special : forall (x:t), ((is_nan x) -> (is_nan (neg x))) /\
(((is_infinite x) -> (is_infinite (neg x))) /\ ((~ (is_nan x)) ->
(diff_sign x (neg x)))).
Lemma neg_special :
forall (x:t),
((is_nan x) -> (is_nan (neg x))) /\
(((is_infinite x) -> (is_infinite (neg x))) /\
((~ (is_nan x)) -> (diff_sign x (neg x)))).
Proof.
apply neg_special.
Qed.
(* Why3 goal *)
Lemma abs_special : forall (x:t), ((is_nan x) -> (is_nan (abs x))) /\
(((is_infinite x) -> (is_infinite (abs x))) /\ ((~ (is_nan x)) ->
(is_positive (abs x)))).
Lemma abs_special :
forall (x:t),
((is_nan x) -> (is_nan (abs x))) /\
(((is_infinite x) -> (is_infinite (abs x))) /\
((~ (is_nan x)) -> (is_positive (abs x)))).
Proof.
apply abs_special.
Qed.
......@@ -1048,7 +1079,8 @@ Proof.
Qed.
(* Why3 goal *)
Lemma of_int_is_int : forall (m:ieee_float.RoundingMode.mode) (x:Z),
Lemma of_int_is_int :
forall (m:ieee_float.RoundingMode.mode) (x:Z),
(in_int_range x) -> (is_int (of_int m x)).
Proof.
intros m x h1.
......@@ -1064,7 +1096,8 @@ Proof.
Qed.
(* Why3 goal *)
Lemma roundToIntegral_is_int : forall (m:ieee_float.RoundingMode.mode) (x:t),
Lemma roundToIntegral_is_int :
forall (m:ieee_float.RoundingMode.mode) (x:t),
(t'isFinite x) -> (is_int (roundToIntegral m x)).
Proof.
now apply roundToIntegral_is_int.
......
This diff is collapsed.
......@@ -32,9 +32,11 @@ apply Z.quot_rem'.
Qed.
(* Why3 goal *)
Lemma Div_bound : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) ->
Lemma Div_bound :
forall (x:Z) (y:Z),
((0%Z <= x)%Z /\ (0%Z < y)%Z) ->
((0%Z <= (ZArith.BinInt.Z.quot x y))%Z /\
((ZArith.BinInt.Z.quot x y) <= x)%Z).
((ZArith.BinInt.Z.quot x y) <= x)%Z).
intros x y (Hx,Hy).
split.
now apply Z.quot_pos.
......@@ -49,9 +51,11 @@ now rewrite <- H', Zquot_0_l.
Qed.
(* Why3 goal *)
Lemma Mod_bound : forall (x:Z) (y:Z), (~ (y = 0%Z)) ->
Lemma Mod_bound :
forall (x:Z) (y:Z),
(~ (y = 0%Z)) ->
(((-(ZArith.BinInt.Z.abs y))%Z < (ZArith.BinInt.Z.rem x y))%Z /\
((ZArith.BinInt.Z.rem x y) < (ZArith.BinInt.Z.abs y))%Z).
((ZArith.BinInt.Z.rem x y) < (ZArith.BinInt.Z.abs y))%Z).
intros x y Zy.
destruct (Zle_or_lt 0 x) as [Hx|Hx].
refine ((fun H => conj (Zlt_le_trans _ 0 _ _ (proj1 H)) (proj2 H)) _).
......@@ -136,7 +140,8 @@ Qed.
Lemma Div_mult :
forall (x:Z) (y:Z) (z:Z),
((0%Z < x)%Z /\ ((0%Z <= y)%Z /\ (0%Z <= z)%Z)) ->
((ZArith.BinInt.Z.quot ((x * y)%Z + z)%Z x) = (y + (ZArith.BinInt.Z.quot z x))%Z).
((ZArith.BinInt.Z.quot ((x * y)%Z + z)%Z x) =
(y + (ZArith.BinInt.Z.quot z x))%Z).
intros x y z (Hx&Hy&Hz).
rewrite (Zplus_comm y).
rewrite <- Z_quot_plus.
......
......@@ -74,7 +74,8 @@ Qed.
(* Why3 goal *)
Lemma Min_assoc :
forall (x:Z) (y:Z) (z:Z),
((ZArith.BinInt.Z.min (ZArith.BinInt.Z.min x y) z) = (ZArith.BinInt.Z.min x (ZArith.BinInt.Z.min y z))).
((ZArith.BinInt.Z.min (ZArith.BinInt.Z.min x y) z) =
(ZArith.BinInt.Z.min x (ZArith.BinInt.Z.min y z))).
Proof.
intros x y z.
apply eq_sym, Zmin_assoc.
......@@ -83,7 +84,8 @@ Qed.
(* Why3 goal *)
Lemma Max_assoc :
forall (x:Z) (y:Z) (z:Z),
((ZArith.BinInt.Z.max (ZArith.BinInt.Z.max x y) z) = (ZArith.BinInt.Z.max x (ZArith.BinInt.Z.max y z))).
((ZArith.BinInt.Z.max (ZArith.BinInt.Z.max x y) z) =
(ZArith.BinInt.Z.max x (ZArith.BinInt.Z.max y z))).
Proof.
intros x y z.
apply eq_sym, Zmax_assoc.
......
......@@ -65,8 +65,9 @@ Proof.
Qed.
(* Why3 goal *)
Lemma Numof_bounds : forall (p:(Z -> bool)) (a:Z) (b:Z), (a < b)%Z ->
((0%Z <= (numof p a b))%Z /\ ((numof p a b) <= (b - a)%Z)%Z).
Lemma Numof_bounds :
forall (p:(Z -> bool)) (a:Z) (b:Z),
(a < b)%Z -> ((0%Z <= (numof p a b))%Z /\ ((numof p a b) <= (b - a)%Z)%Z).
Proof.
intros p a b h1.
unfold numof.
......@@ -80,8 +81,10 @@ Proof.
Qed.
(* Why3 goal *)
Lemma Numof_append : forall (p:(Z -> bool)) (a:Z) (b:Z) (c:Z), ((a <= b)%Z /\
(b <= c)%Z) -> ((numof p a c) = ((numof p a b) + (numof p b c))%Z).
Lemma Numof_append :
forall (p:(Z -> bool)) (a:Z) (b:Z) (c:Z),
((a <= b)%Z /\ (b <= c)%Z) ->
((numof p a c) = ((numof p a b) + (numof p b c))%Z).
Proof.
intros p a b c (h1,h2).
pattern c.
......@@ -143,8 +146,10 @@ Proof.
Qed.
(* Why3 goal *)
Lemma Empty : forall (p:(Z -> bool)) (a:Z) (b:Z), (forall (n:Z),
((a <= n)%Z /\ (n < b)%Z) -> ~ ((p n) = true)) -> ((numof p a b) = 0%Z).
Lemma Empty :
forall (p:(Z -> bool)) (a:Z) (b:Z),
(forall (n:Z), ((a <= n)%Z /\ (n < b)%Z) -> ~ ((p n) = true)) ->
((numof p a b) = 0%Z).
Proof.
intros p a b.
case (Z_lt_le_dec a b); intro; [|intro; apply Numof_empty]; auto.
......@@ -226,9 +231,10 @@ apply numof_nat.
Qed.
(* Why3 goal *)
Lemma numof_strictly_increasing : forall (p:(Z -> bool)) (i:Z) (j:Z) (k:Z)
(l:Z), ((i <= j)%Z /\ ((j <= k)%Z /\ (k < l)%Z)) -> (((p k) = true) ->
((numof p i j) < (numof p i l))%Z).
Lemma numof_strictly_increasing :
forall (p:(Z -> bool)) (i:Z) (j:Z) (k:Z) (l:Z),
((i <= j)%Z /\ ((j <= k)%Z /\ (k < l)%Z)) ->
(((p k) = true) -> ((numof p i j) < (numof p i l))%Z).
Proof.
intros p i j k l (h1,(h2,h3)) h4.
rewrite (Numof_append p i j l) by omega.
......@@ -284,9 +290,11 @@ Proof.
Qed.
(* Why3 goal *)
Lemma numof_change_equiv : forall (p1:(Z -> bool)) (p2:(Z -> bool)) (a:Z)
(b:Z), (forall (j:Z), ((a <= j)%Z /\ (j < b)%Z) -> (((p1 j) = true) <->
((p2 j) = true))) -> ((numof p2 a b) = (numof p1 a b)).
Lemma numof_change_equiv :
forall (p1:(Z -> bool)) (p2:(Z -> bool)) (a:Z) (b:Z),
(forall (j:Z),
((a <= j)%Z /\ (j < b)%Z) -> (((p1 j) = true) <-> ((p2 j) = true))) ->
((numof p2 a b) = (numof p1 a b)).
Proof.
intros p1 p2 a b h1.
apply le_ge_eq.
......
......@@ -84,7 +84,9 @@ apply Power_mult ; auto with zarith.
Qed.
(* Why3 goal *)
Lemma Power_comm1 : forall (x:Z) (y:Z), ((x * y)%Z = (y * x)%Z) ->
Lemma Power_comm1 :
forall (x:Z) (y:Z),
((x * y)%Z = (y * x)%Z) ->
forall (n:Z), (0%Z <= n)%Z -> (((power x n) * y)%Z = (y * (power x n))%Z).
Proof.
intros x y h1 n h2.
......
......@@ -19,13 +19,15 @@ Require list.Length.
Require list.Mem.