Commit 35769833 authored by BOLDO Sylvie's avatar BOLDO Sylvie

Des admits de moins

parent 00e1c682
......@@ -855,6 +855,25 @@ rewrite Zceil_Z2R.
apply Zfloor_Z2R.
Qed.
Theorem Ztrunc_le :
forall x y, (x <= y)%R ->
(Ztrunc x <= Ztrunc y)%Z.
Proof.
intros x y Hxy; unfold Ztrunc at 1.
destruct Rlt_le_dec as [Hx|Hx].
unfold Ztrunc; destruct Rlt_le_dec as [Hy|Hy].
now apply Zceil_le.
apply Zle_trans with 0%Z.
apply Zceil_glb.
simpl; auto with real.
apply Zfloor_lub.
now simpl.
rewrite Ztrunc_floor.
now apply Zfloor_le.
now apply Rle_trans with (1:=Hx).
Qed.
Theorem Ztrunc_opp :
forall x,
Ztrunc (- x) = Zopp (Ztrunc x).
......
......@@ -619,7 +619,7 @@ Definition mkZrounding2 rnd (mono : forall x y, (x <= y)%R -> (rnd x <= rnd y)%Z
Definition ZrndDN := mkZrounding2 Zfloor Zfloor_le Zfloor_Z2R.
Definition ZrndUP := mkZrounding2 Zceil Zceil_le Zceil_Z2R.
(* Definition ZrndTZ := .. SB *)
Definition ZrndTZ := mkZrounding2 Ztrunc Ztrunc_le Ztrunc_Z2R.
Theorem rounding_DN_or_UP :
......@@ -684,24 +684,18 @@ Qed.
Theorem rounding_monotone_l :
forall rnd x y, generic_format x -> (x <= y)%R -> (x <= rounding rnd y)%R.
Proof.
Admitted. (* SB *)
intros rnd x y Hx Hxy.
rewrite <- (rounding_generic rnd x Hx).
now apply rounding_monotone.
Qed.
Theorem rounding_monotone_r :
forall rnd x y, generic_format y -> (x <= y)%R -> (rounding rnd x <= y)%R.
Proof.
Admitted. (* SB *)
Theorem rounding_monotone_abs_l :
forall rnd x y, generic_format x -> (x <= Rabs y)%R -> (x <= Rabs (rounding rnd y))%R.
Proof.
Admitted. (* SB *)
Theorem rounding_monotone_abs_r :
forall rnd x y, generic_format y -> (Rabs x <= y)%R -> (Rabs (rounding rnd x) <= y)%R.
Proof.
Admitted. (* SB *)
intros rnd x y Hy Hxy.
rewrite <- (rounding_generic rnd y Hy).
now apply rounding_monotone.
Qed.
Theorem rounding_abs_abs :
......@@ -729,6 +723,26 @@ apply rounding_monotone.
now apply Rlt_le.
Qed.
Theorem rounding_monotone_abs_l :
forall rnd x y, generic_format x -> (x <= Rabs y)%R -> (x <= Rabs (rounding rnd y))%R.
Proof.
intros rnd x y.
apply rounding_abs_abs.
clear rnd y; intros rnd y Hy.
now apply rounding_monotone_l.
Qed.
Theorem rounding_monotone_abs_r :
forall rnd x y, generic_format y -> (Rabs x <= y)%R -> (Rabs (rounding rnd x) <= y)%R.
Proof.
intros rnd x y.
apply rounding_abs_abs.
clear rnd x; intros rnd x Hx.
now apply rounding_monotone_r.
Qed.
Theorem rounding_DN_opp :
forall x,
rounding ZrndDN (-x) = (- rounding ZrndUP x)%R.
......
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