Commit 8e2ef3b8 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Adapt to Coq 8.7.

parent 109ba0d4
......@@ -826,7 +826,7 @@ COQPDEP = $(addsuffix .dep, $(COQPMODULES))
COQPCMO = $(addsuffix .cmo, $(COQPMODULES))
COQPCMX = $(addsuffix .cmx, $(COQPMODULES))
COQPTREES = engine interp intf kernel lib library ltac parsing pretyping printing proofs tactics toplevel
COQPTREES = engine interp intf kernel lib library ltac parsing pretyping printing proofs tactics toplevel vernac plugins/ltac
COQPINCLUDES = -I src/coq-tactic -I $(COQCAMLPLIB) $(addprefix -I @COQLIB@/, $(COQPTREES)) @ZIPINCLUDE@
$(COQPDEP): DEPFLAGS += -I src/coq-tactic
......@@ -857,6 +857,9 @@ COQRTAC = -R lib/coq-tactic Why3 -R lib/coq Why3
ifeq (@coq_compat_version@,COQ86)
COQRTAC += -I lib/coq-tactic
endif
ifeq (@coq_compat_version@,COQ87)
COQRTAC += -I lib/coq-tactic
endif
src/coq-tactic/.why3-vo-byte: lib/coq-tactic/Why3.v lib/coq/BuiltIn.vo lib/coq-tactic/why3tac.cma
$(SHOW) 'Coqc $<'
......
......@@ -527,11 +527,16 @@ if test "$enable_coq_support" = yes; then
COQPPLIBS="$OCAMLLIB/unix.cma $OCAMLLIB/threads/threads.cma $COQLIB/grammar/grammar.cma"
AC_MSG_RESULT($COQVERSION)
;;
8.6*|trunk)
8.6*)
coq_compat_version="COQ86"
COQPPLIBS="$OCAMLLIB/unix.cma $OCAMLLIB/threads/threads.cma $COQLIB/grammar/grammar.cma"
AC_MSG_RESULT($COQVERSION)
;;
8.7*)
coq_compat_version="COQ87"
COQPPLIBS="$OCAMLLIB/unix.cma $OCAMLLIB/threads/threads.cma $COQLIB/grammar/grammar.cma"
AC_MSG_RESULT($COQVERSION)
;;
*)
enable_coq_support=no
AC_MSG_WARN(You need Coq 8.4 or later; Coq discarded)
......
......@@ -218,7 +218,7 @@ end
theory real.FromInt
syntax function from_int "(Reals.Raxioms.IZR %1)"
syntax function from_int "(BuiltIn.IZR %1)"
remove prop Zero
remove prop One
......@@ -273,6 +273,12 @@ theory real.PowerInt
end
theory real.PowerReal
syntax function pow "(Reals.Rpower.Rpower %1 %2)"
end
theory real.Trigonometry
prelude "Require Reals.Rtrigo_def."
......
......@@ -20,6 +20,7 @@ Class WhyType T := {
}.
Notation int := Z.
Notation IZR := IZR (only parsing).
Global Instance int_WhyType : WhyType int.
Proof.
......
......@@ -92,7 +92,8 @@ 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) ->
((round m (Reals.Raxioms.IZR i)) = (Reals.Raxioms.IZR i)).
((round m (BuiltIn.IZR i)) = (BuiltIn.IZR i)).
Proof.
intros m i Hi.
now apply Exact_rounding_for_integers.
Qed.
......
......@@ -102,7 +102,8 @@ 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
(Reals.Raxioms.IZR i)) = (Reals.Raxioms.IZR i)).
(BuiltIn.IZR i)) = (BuiltIn.IZR i)).
Proof.
intros m i Hi.
now apply Exact_rounding_for_integers.
Qed.
......
......@@ -859,7 +859,8 @@ Lemma max_int1 : (max_int = ((bv.Pow2int.pow2 (bv.Pow2int.pow2 (eb - 1%Z)%Z)) -
Qed.
(* Why3 goal *)
Lemma max_real_int : (max_real = (Reals.Raxioms.IZR max_int)).
Lemma max_real_int : (max_real = (BuiltIn.IZR max_int)).
Proof.
unfold max_int.
rewrite <-Z2R_IZR, Z2R_minus.
change 2%Z with (radix_val radix2).
......@@ -1129,7 +1130,7 @@ Qed.
(* Why3 goal *)
Lemma Exact_rounding_for_integers : forall (m:mode) (i:Z), (in_safe_int_range
i) -> ((round m (Reals.Raxioms.IZR i)) = (Reals.Raxioms.IZR i)).
i) -> ((round m (BuiltIn.IZR i)) = (BuiltIn.IZR i)).
Proof with auto with typeclass_instances.
intros m z Hz.
apply round_generic...
......@@ -3310,10 +3311,12 @@ Lemma Bmax_rep_int_is_int: is_int Bmax_rep_int.
Qed.
Lemma B754_zero_is_int : forall {b}, (is_int (B754_zero b)).
Proof.
split;auto.
rewrite B754_zero_to_real.
unfold is_intR.
rewrite <-FromInt.Zero, Floor_int; reflexivity.
change 0%R with (Z2R 0).
now rewrite Zfloor_Z2R.
Qed.
Lemma max_value_is_int : is_int max_value.
......@@ -3362,7 +3365,8 @@ Lemma of_int_is_int : forall (m:mode) (x:Z), (in_int_range x) -> (is_int
Qed.
Lemma int_to_real_ : forall {m:mode} {x:t}, (is_int x) ->
((to_real x) = (Reals.Raxioms.IZR (to_int m x))).
((to_real x) = (BuiltIn.IZR (to_int m x))).
Proof.
intros m x h1.
destruct h1.
assert (is_intR (to_real x)) by assumption.
......@@ -3376,7 +3380,6 @@ case m; rewrite <-Z2R_IZR;
destruct valid_rnd_DN|
destruct valid_rnd_ZR]; rewrite H0;
rewrite Zrnd_Z2R; easy.
apply Rabs_lt.
rewrite Rminus_diag_eq.
split; fourier.
......@@ -3519,6 +3522,7 @@ Qed.
(* Why3 goal *)
Lemma roundToIntegral_is_int : forall (m:mode) (x:t), (is_finite x) ->
(is_int (roundToIntegral m x)).
Proof.
intros m x h1.
destruct x; try easy.
+ apply zeroF_is_int.
......@@ -3526,7 +3530,8 @@ Lemma roundToIntegral_is_int : forall (m:mode) (x:t), (is_finite x) ->
destruct Z.eq_dec.
split;[apply h1|].
simpl; unfold is_intR.
rewrite <-FromInt.Zero, Floor_int; reflexivity.
change 0 with (Z2R 0).
now rewrite Zfloor_Z2R.
change (is_int (of_int RTZ (to_int m (B754_finite b m0 e e0)))).
apply of_int_is_int.
apply is_finite_to_int2.
......@@ -3690,14 +3695,16 @@ Qed.
(* Why3 goal *)
Lemma int_to_real : forall (m:mode) (x:t), (is_int x) ->
((to_real x) = (Reals.Raxioms.IZR (to_int m x))).
((to_real x) = (BuiltIn.IZR (to_int m x))).
Proof.
intros m x.
apply int_to_real_.
Qed.
Lemma of_int_to_real : forall (m:mode) (x:Z), (no_overflow m
(Reals.Raxioms.IZR x)) -> ((to_real (of_int m x)) = (round m
(Reals.Raxioms.IZR x))).
(BuiltIn.IZR x)) -> ((to_real (of_int m x)) = (round m
(BuiltIn.IZR x))).
Proof.
intros m x h1.
apply (of_int_correct h1).
Qed.
......@@ -3830,7 +3837,8 @@ Qed.
(* Why3 goal *)
Lemma ceil_to_real : forall (x:t), (is_finite x) ->
((to_real (roundToIntegral RTP
x)) = (Reals.Raxioms.IZR (real.Truncate.ceil (to_real x)))).
x)) = (BuiltIn.IZR (real.Truncate.ceil (to_real x)))).
Proof.
intros x h.
rewrite to_real_roundToIntegral; auto.
unfold to_int.
......@@ -3882,7 +3890,8 @@ Qed.
(* Why3 goal *)
Lemma floor_to_real : forall (x:t), (is_finite x) ->
((to_real (roundToIntegral RTN
x)) = (Reals.Raxioms.IZR (real.Truncate.floor (to_real x)))).
x)) = (BuiltIn.IZR (real.Truncate.floor (to_real x)))).
Proof.
intros x h.
rewrite to_real_roundToIntegral; auto.
unfold to_int.
......@@ -4151,49 +4160,50 @@ Qed.
Lemma RTN_not_far_opp: forall x,
is_finite x -> to_real x <= -/2 ->
2 * to_real (roundToIntegral RTN x) <= to_real x <= to_real (roundToIntegral RTN x) / 2.
Proof.
intros x h h1.
rewrite floor_to_real; auto.
pose proof (Zfloor_lb (to_real x));
pose proof (Zfloor_ub (to_real x)).
rewrite <-Z2R_IZR.
rewrite <- (Z2R_IZR (floor _)).
split; try fourier.
destruct (Rle_lt_dec (to_real x) (-1)); try fourier.
assert (Z2R(floor (to_real x)) = -1).
{ assert (Z2R(floor(to_real x)) < Z2R 0) by (simpl Z2R; fourier).
assert (Z2R(-2) < Z2R(floor(to_real x))) by (simpl Z2R; fourier).
apply lt_Z2R in H1; apply lt_Z2R in H2.
replace (-1) with (Z2R(-1)) by auto; f_equal.
auto with zarith. }
now replace (floor (to_real x)) with (-1)%Z by omega. }
fourier.
Qed.
Lemma RTP_not_far: forall x,
is_finite x -> /2 <= to_real x ->
to_real x / 2 <= to_real (roundToIntegral RTP x) <= 2 * to_real x.
Proof.
intros x h h1.
rewrite ceil_to_real; auto.
pose proof (ceil_lb (to_real x));
pose proof (Zceil_ub (to_real x)).
rewrite <-Z2R_IZR.
rewrite <- (Z2R_IZR (ceil _)).
split; try fourier.
destruct (Rle_lt_dec 1 (to_real x) ); try fourier.
assert (Z2R (ceil (to_real x)) = 1).
{ assert (Z2R 0 < Z2R(ceil(to_real x))) by (simpl Z2R; fourier).
assert (Z2R(ceil(to_real x)) < Z2R(2)) by (simpl Z2R; fourier).
apply lt_Z2R in H1; apply lt_Z2R in H2.
replace 1 with (Z2R 1) by auto; f_equal.
auto with zarith. }
now replace (ceil (to_real x)) with 1%Z by omega. }
fourier.
Qed.
Lemma RTP_not_far_opp: forall x,
is_finite x -> to_real x <= -1 ->
2 * to_real x <= to_real (roundToIntegral RTP x) <= to_real x / 2.
Proof.
intros x h h1.
rewrite ceil_to_real; auto.
pose proof (ceil_lb (to_real x));
pose proof (Zceil_ub (to_real x)).
rewrite <-Z2R_IZR.
rewrite <- (Z2R_IZR (ceil _)).
split; try fourier.
apply Rmult_le_reg_r with (r:=2); try fourier.
replace (to_real x / 2 * 2) with (to_real x) by field.
......@@ -4201,11 +4211,9 @@ Lemma RTP_not_far_opp: forall x,
apply Rle_lt_trans with (r2:=(Z2R (ceil (to_real x)) - 1)); auto.
assert (Z2R (ceil (to_real x)) <= -1).
{ pose proof (Rlt_le_trans _ _ _ H h1).
change 1 with (Z2R 1) in *.
rewrite <-Z2R_minus,<-Z2R_opp in H1.
apply lt_Z2R in H1.
rewrite <-Z2R_opp in *.
apply Z2R_le.
rewrite <- (Z2R_minus _ 1) in H1.
apply (lt_Z2R _ (-1)) in H1.
apply (Z2R_le _ (-1)).
auto with zarith. }
fourier.
Qed.
......@@ -4344,7 +4352,7 @@ Lemma eq_diff_floor_ceil: forall {x}, eq (sub RNE x (roundToIntegral RTN x)) (su
unfold to_int in h.
rewrite H0 in *.
simpl Z2R in *.
replace (_--1) with (to_real x+1) in * by ring.
replace (to_real x - -(1)) with (to_real x+1) in * by ring.
pose proof (Rplus_lt_compat_r 1 _ _ r1).
apply Rlt_le in H2.
replace (-/2+1) with (5/10) in H2 by field.
......@@ -4352,7 +4360,7 @@ Lemma eq_diff_floor_ceil: forall {x}, eq (sub RNE x (roundToIntegral RTN x)) (su
apply (Round_monotonic RNE) in H2.
rewrite Round_to_real in H2 by easy.
rewrite half_to_real in H2.
assert false by fourier; easy. }
fourier. }
* assert (floor (to_real x) = 0%Z) by
(apply Zfloor_imp; simpl Z2R; split; fourier).
assert (ceil (to_real x) = 0%Z) by
......
......@@ -17,45 +17,51 @@ Require int.Int.
Require real.Real.
(* Why3 comment *)
(* from_int is replaced with (Reals.Raxioms.IZR x) by the coq driver *)
(* from_int is replaced with (BuiltIn.IZR x) by the coq driver *)
(* Why3 goal *)
Lemma Zero : ((Reals.Raxioms.IZR 0%Z) = 0%R).
Lemma Zero : ((BuiltIn.IZR 0%Z) = 0%R).
Proof.
split.
Qed.
(* Why3 goal *)
Lemma One : ((Reals.Raxioms.IZR 1%Z) = 1%R).
Lemma One : ((BuiltIn.IZR 1%Z) = 1%R).
Proof.
split.
Qed.
(* Why3 goal *)
Lemma Add : forall (x:Z) (y:Z),
((Reals.Raxioms.IZR (x + y)%Z) = ((Reals.Raxioms.IZR x) + (Reals.Raxioms.IZR y))%R).
((BuiltIn.IZR (x + y)%Z) = ((BuiltIn.IZR x) + (BuiltIn.IZR y))%R).
Proof.
exact plus_IZR.
Qed.
(* Why3 goal *)
Lemma Sub : forall (x:Z) (y:Z),
((Reals.Raxioms.IZR (x - y)%Z) = ((Reals.Raxioms.IZR x) - (Reals.Raxioms.IZR y))%R).
((BuiltIn.IZR (x - y)%Z) = ((BuiltIn.IZR x) - (BuiltIn.IZR y))%R).
Proof.
exact minus_IZR.
Qed.
(* Why3 goal *)
Lemma Mul : forall (x:Z) (y:Z),
((Reals.Raxioms.IZR (x * y)%Z) = ((Reals.Raxioms.IZR x) * (Reals.Raxioms.IZR y))%R).
((BuiltIn.IZR (x * y)%Z) = ((BuiltIn.IZR x) * (BuiltIn.IZR y))%R).
Proof.
exact mult_IZR.
Qed.
(* Why3 goal *)
Lemma Neg : forall (x:Z),
((Reals.Raxioms.IZR (-x)%Z) = (-(Reals.Raxioms.IZR x))%R).
Lemma Neg : forall (x:Z), ((BuiltIn.IZR (-x)%Z) = (-(BuiltIn.IZR x))%R).
Proof.
exact opp_IZR.
Qed.
(* Why3 goal *)
Lemma Monotonic : forall (x:Z) (y:Z), (x <= y)%Z ->
((Reals.Raxioms.IZR x) <= (Reals.Raxioms.IZR y))%R.
((BuiltIn.IZR x) <= (BuiltIn.IZR y))%R.
Proof.
exact (IZR_le).
Qed.
......@@ -22,71 +22,80 @@ Require real.ExpLog.
Import Rpower.
(* Why3 goal *)
Definition pow: R -> R -> R.
exact Rpower.
Defined.
(* Why3 comment *)
(* pow is replaced with (Reals.Rpower.Rpower x x1) by the coq driver *)
(* Why3 goal *)
Lemma Pow_def : forall (x:R) (y:R), (0%R < x)%R -> ((pow x
y) = (Reals.Rtrigo_def.exp (y * (Reals.Rpower.ln x))%R)).
intros x y h1.
now unfold pow.
Lemma Pow_def : forall (x:R) (y:R), (0%R < x)%R ->
((Reals.Rpower.Rpower x y) = (Reals.Rtrigo_def.exp (y * (Reals.Rpower.ln x))%R)).
Proof.
easy.
Qed.
(* Why3 goal *)
Lemma Pow_pos : forall (x:R) (y:R), (0%R < x)%R -> (0%R < (pow x y))%R.
Lemma Pow_pos : forall (x:R) (y:R), (0%R < x)%R ->
(0%R < (Reals.Rpower.Rpower x y))%R.
Proof.
intros x y h1.
unfold pow, Rpower.
apply Exp_prop.exp_pos.
Qed.
(* Why3 goal *)
Lemma Pow_plus : forall (x:R) (y:R) (z:R), (0%R < z)%R -> ((pow z
(x + y)%R) = ((pow z x) * (pow z y))%R).
Lemma Pow_plus : forall (x:R) (y:R) (z:R), (0%R < z)%R ->
((Reals.Rpower.Rpower z (x + y)%R) = ((Reals.Rpower.Rpower z x) * (Reals.Rpower.Rpower z y))%R).
Proof.
intros x y z h1.
now apply Rpower_plus.
Qed.
(* Why3 goal *)
Lemma Pow_mult : forall (x:R) (y:R) (z:R), (0%R < x)%R -> ((pow (pow x y)
z) = (pow x (y * z)%R)).
Lemma Pow_mult : forall (x:R) (y:R) (z:R), (0%R < x)%R ->
((Reals.Rpower.Rpower (Reals.Rpower.Rpower x y) z) = (Reals.Rpower.Rpower x (y * z)%R)).
Proof.
intros x y z h1.
now apply Rpower_mult.
Qed.
(* Why3 goal *)
Lemma Pow_x_zero : forall (x:R), (0%R < x)%R -> ((pow x 0%R) = 1%R).
Lemma Pow_x_zero : forall (x:R), (0%R < x)%R ->
((Reals.Rpower.Rpower x 0%R) = 1%R).
Proof.
intros x h1.
now apply Rpower_O.
Qed.
(* Why3 goal *)
Lemma Pow_x_one : forall (x:R), (0%R < x)%R -> ((pow x 1%R) = x).
Lemma Pow_x_one : forall (x:R), (0%R < x)%R ->
((Reals.Rpower.Rpower x 1%R) = x).
Proof.
intros x h1.
now apply Rpower_1.
Qed.
(* Why3 goal *)
Lemma Pow_one_y : forall (y:R), ((pow 1%R y) = 1%R).
Lemma Pow_one_y : forall (y:R), ((Reals.Rpower.Rpower 1%R y) = 1%R).
Proof.
intros y.
unfold pow, Rpower.
unfold Rpower.
rewrite ln_1.
rewrite Rmult_0_r.
now apply Rtrigo_def.exp_0.
Qed.
(* Why3 goal *)
Lemma Pow_x_two : forall (x:R), (0%R < x)%R -> ((pow x
2%R) = (Reals.RIneq.Rsqr x)).
Lemma Pow_x_two : forall (x:R), (0%R < x)%R ->
((Reals.Rpower.Rpower x 2%R) = (Reals.RIneq.Rsqr x)).
Proof.
intros x h1.
rewrite Rpower_plus.
rewrite Rpower_1; auto.
rewrite (Rpower_pow 2) by easy.
simpl.
now rewrite Rmult_1_r.
Qed.
(* Why3 goal *)
Lemma Pow_half : forall (x:R), (0%R < x)%R -> ((pow x
(05 / 10)%R) = (Reals.R_sqrt.sqrt x)).
Lemma Pow_half : forall (x:R), (0%R < x)%R ->
((Reals.Rpower.Rpower x (05 / 10)%R) = (Reals.R_sqrt.sqrt x)).
Proof.
intros x h1.
replace (5 / 10)%R with (/ 2)%R by field.
now apply Rpower_sqrt.
......
......@@ -24,7 +24,8 @@ Require Import Fourier.
Notation truncate := Ztrunc.
(* Why3 goal *)
Lemma Truncate_int : forall (i:Z), ((truncate (Reals.Raxioms.IZR i)) = i).
Lemma Truncate_int : forall (i:Z), ((truncate (BuiltIn.IZR i)) = i).
Proof.
intro i.
rewrite <-Z2R_IZR.
apply Ztrunc_Z2R.
......@@ -32,8 +33,9 @@ Qed.
(* Why3 goal *)
Lemma Truncate_down_pos : forall (x:R), (0%R <= x)%R ->
(((Reals.Raxioms.IZR (truncate x)) <= x)%R /\
(x < (Reals.Raxioms.IZR ((truncate x) + 1%Z)%Z))%R).
(((BuiltIn.IZR (truncate x)) <= x)%R /\
(x < (BuiltIn.IZR ((truncate x) + 1%Z)%Z))%R).
Proof.
intros x h.
rewrite (Ztrunc_floor x h), <-Z2R_IZR, <-Z2R_IZR.
split.
......@@ -44,8 +46,9 @@ Qed.
(* Why3 goal *)
Lemma Truncate_up_neg : forall (x:R), (x <= 0%R)%R ->
(((Reals.Raxioms.IZR ((truncate x) - 1%Z)%Z) < x)%R /\
(x <= (Reals.Raxioms.IZR (truncate x)))%R).
(((BuiltIn.IZR ((truncate x) - 1%Z)%Z) < x)%R /\
(x <= (BuiltIn.IZR (truncate x)))%R).
Proof.
intros x h.
rewrite (Ztrunc_ceil x h), <-Z2R_IZR, <-Z2R_IZR.
split;[|apply Zceil_ub].
......@@ -61,10 +64,11 @@ Qed.
(* Why3 goal *)
Lemma Real_of_truncate : forall (x:R),
((x - 1%R)%R <= (Reals.Raxioms.IZR (truncate x)))%R /\
((Reals.Raxioms.IZR (truncate x)) <= (x + 1%R)%R)%R.
((x - 1%R)%R <= (BuiltIn.IZR (truncate x)))%R /\
((BuiltIn.IZR (truncate x)) <= (x + 1%R)%R)%R.
Proof.
intro x.
rewrite <-Z2R_IZR.
rewrite <- (Z2R_IZR (truncate x)).
destruct (Rle_lt_dec x 0).
+ rewrite Ztrunc_ceil; auto.
destruct (Req_dec (Z2R (Zfloor x)) x).
......@@ -82,12 +86,14 @@ Qed.
(* Why3 goal *)
Lemma Truncate_monotonic : forall (x:R) (y:R), (x <= y)%R ->
((truncate x) <= (truncate y))%Z.
Proof.
apply Ztrunc_le.
Qed.
(* Why3 goal *)
Lemma Truncate_monotonic_int1 : forall (x:R) (i:Z),
(x <= (Reals.Raxioms.IZR i))%R -> ((truncate x) <= i)%Z.
(x <= (BuiltIn.IZR i))%R -> ((truncate x) <= i)%Z.
Proof.
intros x i h.
rewrite <-Z2R_IZR in h.
destruct (Rle_lt_dec x 0).
......@@ -100,7 +106,8 @@ Qed.
(* Why3 goal *)
Lemma Truncate_monotonic_int2 : forall (x:R) (i:Z),
((Reals.Raxioms.IZR i) <= x)%R -> (i <= (truncate x))%Z.
((BuiltIn.IZR i) <= x)%R -> (i <= (truncate x))%Z.
Proof.
intros x i h.
rewrite <-Z2R_IZR in h.
destruct (Rle_lt_dec x 0).
......@@ -118,20 +125,23 @@ Notation floor := Zfloor.
Notation ceil := Zceil.
(* Why3 goal *)
Lemma Floor_int : forall (i:Z), ((floor (Reals.Raxioms.IZR i)) = i).
Lemma Floor_int : forall (i:Z), ((floor (BuiltIn.IZR i)) = i).
Proof.
intro i; rewrite <-Z2R_IZR.
apply Zfloor_Z2R.
Qed.
(* Why3 goal *)
Lemma Ceil_int : forall (i:Z), ((ceil (Reals.Raxioms.IZR i)) = i).
Lemma Ceil_int : forall (i:Z), ((ceil (BuiltIn.IZR i)) = i).
Proof.
intro i; rewrite <-Z2R_IZR.
apply Zceil_Z2R.
Qed.
(* Why3 goal *)
Lemma Floor_down : forall (x:R), ((Reals.Raxioms.IZR (floor x)) <= x)%R /\
(x < (Reals.Raxioms.IZR ((floor x) + 1%Z)%Z))%R.
Lemma Floor_down : forall (x:R), ((BuiltIn.IZR (floor x)) <= x)%R /\
(x < (BuiltIn.IZR ((floor x) + 1%Z)%Z))%R.
Proof.
intro x.
rewrite <-Z2R_IZR, <-Z2R_IZR; split.
apply Zfloor_lb.
......@@ -140,6 +150,7 @@ Lemma Floor_down : forall (x:R), ((Reals.Raxioms.IZR (floor x)) <= x)%R /\
Qed.
Lemma ceil_lb: forall x, ((Z2R (ceil x) - 1) < x).
Proof.
intro.
case (Req_dec (Z2R (Zfloor x)) x); intro.
rewrite <-H, Zceil_Z2R, H; simpl; fourier.
......@@ -151,9 +162,9 @@ Lemma ceil_lb: forall x, ((Z2R (ceil x) - 1) < x).
Qed.
(* Why3 goal *)
Lemma Ceil_up : forall (x:R),
((Reals.Raxioms.IZR ((ceil x) - 1%Z)%Z) < x)%R /\
(x <= (Reals.Raxioms.IZR (ceil x)))%R.
Lemma Ceil_up : forall (x:R), ((BuiltIn.IZR ((ceil x) - 1%Z)%Z) < x)%R /\
(x <= (BuiltIn.IZR (ceil x)))%R.
Proof.
intro x.
rewrite <-Z2R_IZR, <-Z2R_IZR; split; [|apply Zceil_ub].
rewrite Z2R_minus.
......@@ -163,12 +174,14 @@ Qed.
(* Why3 goal *)
Lemma Floor_monotonic : forall (x:R) (y:R), (x <= y)%R ->
((floor x) <= (floor y))%Z.
Proof.
apply Zfloor_le.
Qed.
(* Why3 goal *)
Lemma Ceil_monotonic : forall (x:R) (y:R), (x <= y)%R ->
((ceil x) <= (ceil y))%Z.
Proof.
apply Zceil_le.
Qed.
This diff is collapsed.
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