Commit 201e0da2 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Update parts of Coq realizations whose printing looks sane.

parent a9bccabd
......@@ -271,8 +271,7 @@ Defined.
(* Why3 goal *)
Lemma Nth_bw_and :
forall (v1:t) (v2:t) (n:Z),
((0%Z <= n)%Z /\ (n < size)%Z) ->
forall (v1:t) (v2:t) (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) ->
((nth (bw_and v1 v2) n) = (Init.Datatypes.andb (nth v1 n) (nth v2 n))).
symmetry.
apply nth_aux_map2 with (f := fun x y => x && y); easy.
......@@ -285,8 +284,7 @@ Defined.
(* Why3 goal *)
Lemma Nth_bw_or :
forall (v1:t) (v2:t) (n:Z),
((0%Z <= n)%Z /\ (n < size)%Z) ->
forall (v1:t) (v2:t) (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) ->
((nth (bw_or v1 v2) n) = (Init.Datatypes.orb (nth v1 n) (nth v2 n))).
symmetry.
apply nth_aux_map2; easy.
......@@ -299,8 +297,7 @@ Defined.
(* Why3 goal *)
Lemma Nth_bw_xor :
forall (v1:t) (v2:t) (n:Z),
((0%Z <= n)%Z /\ (n < size)%Z) ->
forall (v1:t) (v2:t) (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) ->
((nth (bw_xor v1 v2) n) = (Init.Datatypes.xorb (nth v1 n) (nth v2 n))).
symmetry.
apply nth_aux_map2; easy.
......@@ -313,8 +310,7 @@ Defined.
(* Why3 goal *)
Lemma Nth_bw_not :
forall (v:t) (n:Z),
((0%Z <= n)%Z /\ (n < size)%Z) ->
forall (v:t) (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) ->
((nth (bw_not v) n) = (Init.Datatypes.negb (nth v n))).
symmetry.
apply nth_aux_map; easy.
......@@ -342,17 +338,18 @@ Lemma bshiftRl_iter_nth : forall b s m,
Qed.
(* Why3 goal *)
Lemma Lsr_nth_low : forall (b:t) (n:Z) (s:Z), (0%Z <= s)%Z ->
((0%Z <= n)%Z -> (((n + s)%Z < size)%Z -> ((nth (lsr b s) n) = (nth b
(n + s)%Z)))).
Lemma Lsr_nth_low :
forall (b:t) (n:Z) (s:Z), (0%Z <= s)%Z -> (0%Z <= n)%Z ->
((n + s)%Z < size)%Z -> ((nth (lsr b s) n) = (nth b (n + s)%Z)).
intros b n s h1 h2 h3.
rewrite <-Z2Nat.id with (n := s) at 2; auto.
apply bshiftRl_iter_nth; omega.
Qed.
(* Why3 goal *)
Lemma Lsr_nth_high : forall (b:t) (n:Z) (s:Z), (0%Z <= s)%Z ->
((0%Z <= n)%Z -> ((size <= (n + s)%Z)%Z -> ((nth (lsr b s) n) = false))).
Lemma Lsr_nth_high :
forall (b:t) (n:Z) (s:Z), (0%Z <= s)%Z -> (0%Z <= n)%Z ->
(size <= (n + s)%Z)%Z -> ((nth (lsr b s) n) = false).
intros b n s h1 h2 h3.
unfold nth,lsr.
cut (nth_aux b (n + Z.of_nat (Z.to_nat s)) = false).
......@@ -445,9 +442,9 @@ Lemma BshiftRa_iter_nth_low : forall (b:t) (s:nat) (n:Z),
Qed.
(* Why3 goal *)
Lemma Asr_nth_low : forall (b:t) (n:Z) (s:Z), (0%Z <= s)%Z ->
(((0%Z <= n)%Z /\ (n < size)%Z) -> (((n + s)%Z < size)%Z -> ((nth (asr b s)
n) = (nth b (n + s)%Z)))).
Lemma Asr_nth_low :
forall (b:t) (n:Z) (s:Z), (0%Z <= s)%Z -> ((0%Z <= n)%Z /\ (n < size)%Z) ->
((n + s)%Z < size)%Z -> ((nth (asr b s) n) = (nth b (n + s)%Z)).
unfold nth, lsr.
intros.
assert ((n + s)%Z = (n + Z.of_nat (Z.to_nat s))%Z).
......@@ -491,9 +488,9 @@ Lemma BhiftRa_iter_nth_high : forall (b:t) (s:nat) (n:Z),
Qed.
(* Why3 goal *)
Lemma Asr_nth_high : forall (b:t) (n:Z) (s:Z), (0%Z <= s)%Z ->
(((0%Z <= n)%Z /\ (n < size)%Z) -> ((size <= (n + s)%Z)%Z -> ((nth (asr b
s) n) = (nth b (size - 1%Z)%Z)))).
Lemma Asr_nth_high :
forall (b:t) (n:Z) (s:Z), (0%Z <= s)%Z -> ((0%Z <= n)%Z /\ (n < size)%Z) ->
(size <= (n + s)%Z)%Z -> ((nth (asr b s) n) = (nth b (size - 1%Z)%Z)).
unfold nth, asr.
intros.
apply BhiftRa_iter_nth_high.
......@@ -529,8 +526,7 @@ Qed.
(* Why3 goal *)
Lemma Lsl_nth_high :
forall (b:t) (n:Z) (s:Z),
((0%Z <= s)%Z /\ ((s <= n)%Z /\ (n < size)%Z)) ->
forall (b:t) (n:Z) (s:Z), ((0%Z <= s)%Z /\ ((s <= n)%Z /\ (n < size)%Z)) ->
((nth (lsl b s) n) = (nth b (n - s)%Z)).
intros.
unfold lsl, nth.
......@@ -560,8 +556,8 @@ Qed.
(* Why3 goal *)
Lemma Lsl_nth_low :
forall (b:t) (n:Z) (s:Z),
((0%Z <= n)%Z /\ (n < s)%Z) -> ((nth (lsl b s) n) = false).
forall (b:t) (n:Z) (s:Z), ((0%Z <= n)%Z /\ (n < s)%Z) ->
((nth (lsl b s) n) = false).
intros.
apply Lsl_nth_low_aux.
rewrite Z2Nat.id; omega.
......@@ -1100,9 +1096,10 @@ Definition rotate_right : t -> Z -> t.
Defined.
(* Why3 goal *)
Lemma Nth_rotate_right : forall (v:t) (n:Z) (i:Z), ((0%Z <= i)%Z /\
(i < size)%Z) -> ((0%Z <= n)%Z -> ((nth (rotate_right v n) i) = (nth v
(int.EuclideanDivision.mod1 (i + n)%Z size)))).
Lemma Nth_rotate_right :
forall (v:t) (n:Z) (i:Z), ((0%Z <= i)%Z /\ (i < size)%Z) -> (0%Z <= n)%Z ->
((nth (rotate_right v n) i) =
(nth v (int.EuclideanDivision.mod1 (i + n)%Z size))).
intros v n i h1 h2.
revert h2; revert n.
apply Z_of_nat_prop.
......@@ -1123,9 +1120,10 @@ Definition rotate_left : t -> Z -> t.
Defined.
(* Why3 goal *)
Lemma Nth_rotate_left : forall (v:t) (n:Z) (i:Z), ((0%Z <= i)%Z /\
(i < size)%Z) -> ((0%Z <= n)%Z -> ((nth (rotate_left v n) i) = (nth v
(int.EuclideanDivision.mod1 (i - n)%Z size)))).
Lemma Nth_rotate_left :
forall (v:t) (n:Z) (i:Z), ((0%Z <= i)%Z /\ (i < size)%Z) -> (0%Z <= n)%Z ->
((nth (rotate_left v n) i) =
(nth v (int.EuclideanDivision.mod1 (i - n)%Z size))).
intros v n i h1 h2.
revert h2; revert n.
apply Z_of_nat_prop.
......@@ -1185,9 +1183,11 @@ Definition to_int : t -> Z.
Defined.
(* Why3 goal *)
Lemma to_int_def : forall (x:t), ((is_signed_positive x) ->
((to_int x) = (to_uint x))) /\ ((~ (is_signed_positive x)) ->
((to_int x) = (-(two_power_size - (to_uint x))%Z)%Z)).
Lemma to_int_def :
forall (x:t),
((is_signed_positive x) -> ((to_int x) = (to_uint x))) /\
(~ (is_signed_positive x) ->
((to_int x) = (-(two_power_size - (to_uint x))%Z)%Z)).
intros. split.
- unfold to_int, to_uint,is_signed_positive, twos_complement, size_nat.
intros.
......@@ -1331,8 +1331,9 @@ Qed.
(* end of to_uint helpers *)
(* Why3 goal *)
Lemma to_uint_of_int : forall (i:Z), ((0%Z <= i)%Z /\
(i < two_power_size)%Z) -> ((to_uint (of_int i)) = i).
Lemma to_uint_of_int :
forall (i:Z), ((0%Z <= i)%Z /\ (i < two_power_size)%Z) ->
((to_uint (of_int i)) = i).
intros i h1; destruct h1.
unfold to_uint, of_int.
rewrite bvec_to_nat_nat_to_bvec.
......@@ -1462,18 +1463,21 @@ Definition add : t -> t -> t.
Defined.
(* Why3 goal *)
Lemma to_uint_add : forall (v1:t) (v2:t), ((to_uint (add v1
v2)) = (int.EuclideanDivision.mod1 ((to_uint v1) + (to_uint v2))%Z
two_power_size)).
Lemma to_uint_add :
forall (v1:t) (v2:t),
((to_uint (add v1 v2)) =
(int.EuclideanDivision.mod1 ((to_uint v1) + (to_uint v2))%Z
two_power_size)).
intros v1 v2.
apply to_uint_of_int.
apply mod1_in_range2.
Qed.
(* Why3 goal *)
Lemma to_uint_add_bounded : forall (v1:t) (v2:t),
(((to_uint v1) + (to_uint v2))%Z < two_power_size)%Z -> ((to_uint (add v1
v2)) = ((to_uint v1) + (to_uint v2))%Z).
Lemma to_uint_add_bounded :
forall (v1:t) (v2:t),
(((to_uint v1) + (to_uint v2))%Z < two_power_size)%Z ->
((to_uint (add 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_add.
......@@ -1486,9 +1490,11 @@ Definition sub : t -> t -> t.
Defined.
(* Why3 goal *)
Lemma to_uint_sub : forall (v1:t) (v2:t), ((to_uint (sub v1
v2)) = (int.EuclideanDivision.mod1 ((to_uint v1) - (to_uint v2))%Z
two_power_size)).
Lemma to_uint_sub :
forall (v1:t) (v2:t),
((to_uint (sub v1 v2)) =
(int.EuclideanDivision.mod1 ((to_uint v1) - (to_uint v2))%Z
two_power_size)).
intros v1 v2.
apply to_uint_of_int, mod1_in_range2.
Qed.
......@@ -1524,9 +1530,11 @@ Definition mul : t -> t -> t.
Defined.
(* Why3 goal *)
Lemma to_uint_mul : forall (v1:t) (v2:t), ((to_uint (mul v1
v2)) = (int.EuclideanDivision.mod1 ((to_uint v1) * (to_uint v2))%Z
two_power_size)).
Lemma to_uint_mul :
forall (v1:t) (v2:t),
((to_uint (mul v1 v2)) =
(int.EuclideanDivision.mod1 ((to_uint v1) * (to_uint v2))%Z
two_power_size)).
intros v1 v2.
apply to_uint_of_int, mod1_in_range2.
Qed.
......@@ -1634,9 +1642,11 @@ Lemma lsl_bv_is_lsl :
Qed.
(* Why3 goal *)
Lemma to_uint_lsl : forall (v:t) (n:t), ((to_uint (lsl_bv v
n)) = (int.EuclideanDivision.mod1 ((to_uint v) * (bv.Pow2int.pow2 (to_uint n)))%Z
two_power_size)).
Lemma to_uint_lsl :
forall (v:t) (n:t),
((to_uint (lsl_bv v n)) =
(int.EuclideanDivision.mod1
((to_uint v) * (bv.Pow2int.pow2 (to_uint n)))%Z two_power_size)).
intros v n.
apply to_uint_lsl_aux.
Qed.
......@@ -1735,8 +1745,7 @@ Qed.
(* Why3 goal *)
Lemma Nth_bv_is_nth2 :
forall (x:t) (i:Z),
((0%Z <= i)%Z /\ (i < two_power_size)%Z) ->
forall (x:t) (i:Z), ((0%Z <= i)%Z /\ (i < two_power_size)%Z) ->
((nth_bv x (of_int i)) = (nth x i)).
intros x i h1.
rewrite <-Nth_bv_is_nth.
......
......@@ -38,8 +38,7 @@ Qed.
(* Why3 goal *)
Lemma Power_sum :
forall (n:Z) (m:Z),
((0%Z <= n)%Z /\ (0%Z <= m)%Z) ->
forall (n:Z) (m:Z), ((0%Z <= n)%Z /\ (0%Z <= m)%Z) ->
((pow2 (n + m)%Z) = ((pow2 n) * (pow2 m))%Z).
unfold pow2.
intros n m [H1 H2].
......
......@@ -67,27 +67,32 @@ Qed.
(* 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.
forall (m:floating_point.Rounding.mode) (x:R) (y:R), (x <= y)%R ->
((round m x) <= (round m y))%R.
now apply Round_monotonic.
Qed.
(* 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)).
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.
(* Why3 goal *)
Lemma Round_value : forall (m:floating_point.Rounding.mode)
(x:floating_point.DoubleFormat.double), ((round m (value x)) = (value x)).
Lemma Round_value :
forall (m:floating_point.Rounding.mode)
(x:floating_point.DoubleFormat.double),
((round m (value x)) = (value x)).
now apply Round_value.
Qed.
(* Why3 goal *)
Lemma Bounded_value : forall (x:floating_point.DoubleFormat.double),
((Reals.Rbasic_fun.Rabs (value x)) <= (9007199254740991 * 19958403095347198116563727130368385660674512604354575415025472424372118918689640657849579654926357010893424468441924952439724379883935936607391717982848314203200056729510856765175377214443629871826533567445439239933308104551208703888888552684480441575071209068757560416423584952303440099278848)%R)%R.
Lemma Bounded_value :
forall (x:floating_point.DoubleFormat.double),
((Reals.Rbasic_fun.Rabs (value x)) <=
(9007199254740991 * 19958403095347198116563727130368385660674512604354575415025472424372118918689640657849579654926357010893424468441924952439724379883935936607391717982848314203200056729510856765175377214443629871826533567445439239933308104551208703888888552684480441575071209068757560416423584952303440099278848)%R)%R.
now apply Bounded_value.
Qed.
......@@ -137,8 +142,8 @@ 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)).
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.
......
......@@ -65,7 +65,8 @@ Qed.
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.
(33554430 * 10141204801825835211973625643008)%R)%R ->
no_overflow m x.
intros m x Hx.
unfold no_overflow.
rewrite max_single_eq in *.
......@@ -74,22 +75,25 @@ Qed.
(* 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.
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.
(* 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)).
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.
(* Why3 goal *)
Lemma Round_value : forall (m:floating_point.Rounding.mode)
(x:floating_point.SingleFormat.single), ((round m (value x)) = (value x)).
Lemma Round_value :
forall (m:floating_point.Rounding.mode)
(x:floating_point.SingleFormat.single),
((round m (value x)) = (value x)).
now apply Round_value.
Qed.
......@@ -148,8 +152,8 @@ 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)).
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.
......
......@@ -50,9 +50,10 @@ Proof.
Defined.
(* Why3 goal *)
Lemma t'axiom : forall (x:t), (t'isFinite x) ->
(((-(16777215 * 20282409603651670423947251286016)%R)%R <= (t'real x))%R /\
((t'real x) <= (16777215 * 20282409603651670423947251286016)%R)%R).
Lemma t'axiom :
forall (x:t), (t'isFinite x) ->
((-(16777215 * 20282409603651670423947251286016)%R)%R <= (t'real x))%R /\
((t'real x) <= (16777215 * 20282409603651670423947251286016)%R)%R.
Proof.
intros x _.
apply Rabs_le_inv.
......@@ -237,7 +238,7 @@ Qed.
(* Why3 goal *)
Lemma is_not_finite :
forall (x:t), (~ (t'isFinite x)) <-> ((is_infinite x) \/ (is_nan x)).
forall (x:t), ~ (t'isFinite x) <-> ((is_infinite x) \/ (is_nan x)).
Proof.
apply is_not_finite.
Qed.
......@@ -333,8 +334,8 @@ Definition no_overflow (m:ieee_float.RoundingMode.mode) (x:R) : Prop :=
(* Why3 goal *)
Lemma Bounded_real_no_overflow :
forall (m:ieee_float.RoundingMode.mode) (x:R),
(in_range x) -> no_overflow m x.
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.
......@@ -343,24 +344,25 @@ Qed.
(* Why3 goal *)
Lemma Round_monotonic :
forall (m:ieee_float.RoundingMode.mode) (x:R) (y:R),
(x <= y)%R -> ((round m x) <= (round m y))%R.
forall (m:ieee_float.RoundingMode.mode) (x:R) (y:R), (x <= y)%R ->
((round m x) <= (round m y))%R.
Proof.
apply Round_monotonic.
Qed.
(* Why3 goal *)
Lemma Round_idempotent : forall (m1:ieee_float.RoundingMode.mode)
(m2:ieee_float.RoundingMode.mode) (x:R), ((round m1 (round m2
x)) = (round m2 x)).
Lemma Round_idempotent :
forall (m1:ieee_float.RoundingMode.mode) (m2:ieee_float.RoundingMode.mode)
(x:R),
((round m1 (round m2 x)) = (round m2 x)).
Proof.
apply Round_idempotent.
Qed.
(* Why3 goal *)
Lemma Round_to_real :
forall (m:ieee_float.RoundingMode.mode) (x:t),
(t'isFinite x) -> ((round m (t'real x)) = (t'real x)).
forall (m:ieee_float.RoundingMode.mode) (x:t), (t'isFinite x) ->
((round m (t'real x)) = (t'real x)).
Proof.
apply Round_to_real.
Qed.
......@@ -403,8 +405,8 @@ Definition in_safe_int_range (i:Z) : Prop :=
(* 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)).
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.
......@@ -422,8 +424,8 @@ Definition diff_sign (x:t) (y:t) : Prop :=
(* Why3 goal *)
Lemma feq_eq :
forall (x:t) (y:t),
(t'isFinite x) -> (t'isFinite y) -> ~ (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.
apply feq_eq.
Qed.
......@@ -461,25 +463,26 @@ Qed.
(* Why3 goal *)
Lemma eq_to_real_finite :
forall (x:t) (y:t),
((t'isFinite x) /\ (t'isFinite y)) ->
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.
(* Why3 goal *)
Lemma eq_special : forall (x:t) (y:t), (eq x y) -> ((is_not_nan x) /\
((is_not_nan y) /\ (((t'isFinite x) /\ (t'isFinite y)) \/ ((is_infinite
x) /\ ((is_infinite y) /\ (same_sign x y)))))).
Lemma eq_special :
forall (x:t) (y:t), (eq x y) ->
(is_not_nan x) /\
((is_not_nan y) /\
(((t'isFinite x) /\ (t'isFinite y)) \/
((is_infinite x) /\ ((is_infinite y) /\ (same_sign x y))))).
Proof.
apply eq_special.
Qed.
(* Why3 goal *)
Lemma lt_finite :
forall (x:t) (y:t),
((t'isFinite x) /\ (t'isFinite y)) ->
forall (x:t) (y:t), ((t'isFinite x) /\ (t'isFinite y)) ->
(lt x y) <-> ((t'real x) < (t'real y))%R.
Proof.
apply lt_finite.
......@@ -487,8 +490,7 @@ Qed.
(* Why3 goal *)
Lemma le_finite :
forall (x:t) (y:t),
((t'isFinite x) /\ (t'isFinite y)) ->
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.
......@@ -516,33 +518,36 @@ 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.
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.
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.
(* Why3 goal *)
Lemma le_special : forall (x:t) (y:t), (le x y) -> (((t'isFinite x) /\
(t'isFinite y)) \/ (((is_minus_infinity x) /\ (is_not_nan y)) \/
((is_not_nan x) /\ (is_plus_infinity y)))).
Lemma le_special :
forall (x:t) (y:t), (le x y) ->
((t'isFinite x) /\ (t'isFinite y)) \/
(((is_minus_infinity x) /\ (is_not_nan y)) \/
((is_not_nan x) /\ (is_plus_infinity y))).
Proof.
apply le_special.
Qed.
(* Why3 goal *)
Lemma lt_special : forall (x:t) (y:t), (lt x y) -> (((t'isFinite x) /\
(t'isFinite y)) \/ (((is_minus_infinity x) /\ ((is_not_nan y) /\
~ (is_minus_infinity y))) \/ ((is_not_nan x) /\ ((~ (is_plus_infinity
x)) /\ (is_plus_infinity y))))).
Lemma lt_special :
forall (x:t) (y:t), (lt x y) ->
((t'isFinite x) /\ (t'isFinite y)) \/
(((is_minus_infinity x) /\ ((is_not_nan y) /\ ~ (is_minus_infinity y))) \/
((is_not_nan x) /\ (~ (is_plus_infinity x) /\ (is_plus_infinity y)))).
Proof.
apply lt_special.
Qed.
......@@ -598,15 +603,18 @@ 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.
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.
(* Why3 goal *)
Lemma diff_sign_product : forall (x:t) (y:t), ((t'isFinite x) /\ ((t'isFinite
y) /\ (((t'real x) * (t'real y))%R < 0%R)%R)) -> (diff_sign x y).
Lemma diff_sign_product :
forall (x:t) (y:t),
((t'isFinite x) /\
((t'isFinite y) /\ (((t'real x) * (t'real y))%R < 0%R)%R)) ->
diff_sign x y.
Proof.
apply diff_sign_product.
Qed.
......@@ -627,18 +635,25 @@ Definition product_sign (z:t) (x:t) (y:t) : Prop :=
(* Why3 assumption *)
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) = (33554430 * 10141204801825835211973625643008)%R))) /\
((~ (is_positive x)) -> (is_infinite x))
| ieee_float.RoundingMode.RTP => ((is_positive x) -> (is_infinite x)) /\
((~ (is_positive x)) -> ((t'isFinite x) /\
((t'real x) = (-(33554430 * 10141204801825835211973625643008)%R)%R)))
| ieee_float.RoundingMode.RTZ => ((is_positive x) -> ((t'isFinite x) /\
((t'real x) = (33554430 * 10141204801825835211973625643008)%R))) /\
((~ (is_positive x)) -> ((t'isFinite x) /\
((t'real x) = (-(33554430 * 10141204801825835211973625643008)%R)%R)))
| (ieee_float.RoundingMode.RNA|ieee_float.RoundingMode.RNE) => (is_infinite
x)