Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

Commit 99c29d8d authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Changed Ztrunc and Zaway to boolean conditional.

parent 5b5c74d4
...@@ -283,14 +283,12 @@ rewrite Zceil_floor_neq. ...@@ -283,14 +283,12 @@ rewrite Zceil_floor_neq.
rewrite Hm. rewrite Hm.
unfold cond_incr. unfold cond_incr.
simpl. simpl.
generalize (Zlt_cases m 0). case Rlt_bool_spec ; intros Hx' ;
destruct (Rlt_le_dec x 0) as [Hx'|Hx'] ; case Zlt_bool_spec ; intros Hm' ; try apply refl_equal.
case (Zlt_bool m 0) ; try easy ; intros Hm'.
elim Rlt_not_le with (1 := Hx'). elim Rlt_not_le with (1 := Hx').
apply Rlt_le. apply Rlt_le.
apply Rle_lt_trans with (2 := proj1 Hx). apply Rle_lt_trans with (2 := proj1 Hx).
apply (Z2R_le 0). now apply (Z2R_le 0).
now apply Zge_le.
elim Rle_not_lt with (1 := Hx'). elim Rle_not_lt with (1 := Hx').
apply Rlt_le_trans with (1 := proj2 Hx). apply Rlt_le_trans with (1 := proj2 Hx).
apply (Z2R_le _ 0). apply (Z2R_le _ 0).
......
...@@ -1296,7 +1296,7 @@ rewrite Z2R_plus. ...@@ -1296,7 +1296,7 @@ rewrite Z2R_plus.
apply Zfloor_ub. apply Zfloor_ub.
Qed. Qed.
Definition Ztrunc x := if Rlt_le_dec x 0 then Zceil x else Zfloor x. Definition Ztrunc x := if Rlt_bool x 0 then Zceil x else Zfloor x.
Theorem Ztrunc_Z2R : Theorem Ztrunc_Z2R :
forall n, forall n,
...@@ -1304,7 +1304,7 @@ Theorem Ztrunc_Z2R : ...@@ -1304,7 +1304,7 @@ Theorem Ztrunc_Z2R :
Proof. Proof.
intros n. intros n.
unfold Ztrunc. unfold Ztrunc.
destruct Rlt_le_dec as [H|H]. case Rlt_bool_spec ; intro H.
apply Zceil_Z2R. apply Zceil_Z2R.
apply Zfloor_Z2R. apply Zfloor_Z2R.
Qed. Qed.
...@@ -1316,9 +1316,10 @@ Theorem Ztrunc_floor : ...@@ -1316,9 +1316,10 @@ Theorem Ztrunc_floor :
Proof. Proof.
intros x Hx. intros x Hx.
unfold Ztrunc. unfold Ztrunc.
destruct Rlt_le_dec as [H|_]. case Rlt_bool_spec ; intro H.
elim Rlt_irrefl with (1 := Rle_lt_trans _ _ _ Hx H). elim Rlt_irrefl with x.
easy. now apply Rlt_le_trans with R0.
apply refl_equal.
Qed. Qed.
Theorem Ztrunc_ceil : Theorem Ztrunc_ceil :
...@@ -1328,8 +1329,8 @@ Theorem Ztrunc_ceil : ...@@ -1328,8 +1329,8 @@ Theorem Ztrunc_ceil :
Proof. Proof.
intros x Hx. intros x Hx.
unfold Ztrunc. unfold Ztrunc.
destruct Rlt_le_dec as [_|H]. case Rlt_bool_spec ; intro H.
easy. apply refl_equal.
rewrite (Rle_antisym _ _ Hx H). rewrite (Rle_antisym _ _ Hx H).
fold (Z2R 0). fold (Z2R 0).
rewrite Zceil_Z2R. rewrite Zceil_Z2R.
...@@ -1342,9 +1343,9 @@ Theorem Ztrunc_le : ...@@ -1342,9 +1343,9 @@ Theorem Ztrunc_le :
Proof. Proof.
intros x y Hxy. intros x y Hxy.
unfold Ztrunc at 1. unfold Ztrunc at 1.
destruct Rlt_le_dec as [Hx|Hx]. case Rlt_bool_spec ; intro Hx.
unfold Ztrunc. unfold Ztrunc.
destruct Rlt_le_dec as [Hy|Hy]. case Rlt_bool_spec ; intro Hy.
now apply Zceil_le. now apply Zceil_le.
apply Zle_trans with 0%Z. apply Zle_trans with 0%Z.
apply Zceil_glb. apply Zceil_glb.
...@@ -1360,19 +1361,17 @@ Theorem Ztrunc_opp : ...@@ -1360,19 +1361,17 @@ Theorem Ztrunc_opp :
Ztrunc (- x) = Zopp (Ztrunc x). Ztrunc (- x) = Zopp (Ztrunc x).
Proof. Proof.
intros x. intros x.
destruct (Rlt_le_dec x 0) as [H|H]. unfold Ztrunc at 2.
case Rlt_bool_spec ; intros Hx.
rewrite Ztrunc_floor. rewrite Ztrunc_floor.
rewrite Ztrunc_ceil.
apply sym_eq. apply sym_eq.
apply Zopp_involutive. apply Zopp_involutive.
now apply Rlt_le.
rewrite <- Ropp_0. rewrite <- Ropp_0.
apply Ropp_le_contravar. apply Ropp_le_contravar.
now apply Rlt_le. now apply Rlt_le.
rewrite Ztrunc_ceil. rewrite Ztrunc_ceil.
unfold Zceil. unfold Zceil.
rewrite Ropp_involutive. now rewrite Ropp_involutive.
now rewrite Ztrunc_floor.
rewrite <- Ropp_0. rewrite <- Ropp_0.
now apply Ropp_le_contravar. now apply Ropp_le_contravar.
Qed. Qed.
...@@ -1384,7 +1383,7 @@ Proof. ...@@ -1384,7 +1383,7 @@ Proof.
intros x. intros x.
rewrite Ztrunc_floor. 2: apply Rabs_pos. rewrite Ztrunc_floor. 2: apply Rabs_pos.
unfold Ztrunc. unfold Ztrunc.
destruct Rlt_le_dec as [H|H]. case Rlt_bool_spec ; intro H.
rewrite Rabs_left with (1 := H). rewrite Rabs_left with (1 := H).
rewrite Zabs_non_eq. rewrite Zabs_non_eq.
apply sym_eq. apply sym_eq.
...@@ -1408,7 +1407,7 @@ rewrite Ztrunc_floor. 2: apply Rabs_pos. ...@@ -1408,7 +1407,7 @@ rewrite Ztrunc_floor. 2: apply Rabs_pos.
now apply Zfloor_lub. now apply Zfloor_lub.
Qed. Qed.
Definition Zaway x := if Rlt_le_dec x 0 then Zfloor x else Zceil x. Definition Zaway x := if Rlt_bool x 0 then Zfloor x else Zceil x.
Theorem Zaway_Z2R : Theorem Zaway_Z2R :
forall n, forall n,
...@@ -1416,7 +1415,7 @@ Theorem Zaway_Z2R : ...@@ -1416,7 +1415,7 @@ Theorem Zaway_Z2R :
Proof. Proof.
intros n. intros n.
unfold Zaway. unfold Zaway.
destruct Rlt_le_dec as [H|H]. case Rlt_bool_spec ; intro H.
apply Zfloor_Z2R. apply Zfloor_Z2R.
apply Zceil_Z2R. apply Zceil_Z2R.
Qed. Qed.
...@@ -1428,9 +1427,10 @@ Theorem Zaway_ceil : ...@@ -1428,9 +1427,10 @@ Theorem Zaway_ceil :
Proof. Proof.
intros x Hx. intros x Hx.
unfold Zaway. unfold Zaway.
destruct Rlt_le_dec as [H|_]. case Rlt_bool_spec ; intro H.
elim Rlt_irrefl with (1 := Rle_lt_trans _ _ _ Hx H). elim Rlt_irrefl with x.
easy. now apply Rlt_le_trans with R0.
apply refl_equal.
Qed. Qed.
Theorem Zaway_floor : Theorem Zaway_floor :
...@@ -1440,8 +1440,8 @@ Theorem Zaway_floor : ...@@ -1440,8 +1440,8 @@ Theorem Zaway_floor :
Proof. Proof.
intros x Hx. intros x Hx.
unfold Zaway. unfold Zaway.
destruct Rlt_le_dec as [_|H]. case Rlt_bool_spec ; intro H.
easy. apply refl_equal.
rewrite (Rle_antisym _ _ Hx H). rewrite (Rle_antisym _ _ Hx H).
fold (Z2R 0). fold (Z2R 0).
rewrite Zfloor_Z2R. rewrite Zfloor_Z2R.
...@@ -1454,9 +1454,9 @@ Theorem Zaway_le : ...@@ -1454,9 +1454,9 @@ Theorem Zaway_le :
Proof. Proof.
intros x y Hxy. intros x y Hxy.
unfold Zaway at 1. unfold Zaway at 1.
destruct Rlt_le_dec as [Hx|Hx]. case Rlt_bool_spec ; intro Hx.
unfold Zaway. unfold Zaway.
destruct Rlt_le_dec as [Hy|Hy]. case Rlt_bool_spec ; intro Hy.
now apply Zfloor_le. now apply Zfloor_le.
apply le_Z2R. apply le_Z2R.
apply Rle_trans with 0%R. apply Rle_trans with 0%R.
...@@ -1476,15 +1476,15 @@ Theorem Zaway_opp : ...@@ -1476,15 +1476,15 @@ Theorem Zaway_opp :
Proof. Proof.
intros x. intros x.
unfold Zaway at 2. unfold Zaway at 2.
destruct Rlt_le_dec as [H|H]. case Rlt_bool_spec ; intro H.
rewrite Zaway_ceil. rewrite Zaway_ceil.
unfold Zceil. unfold Zceil.
now rewrite Ropp_involutive. now rewrite Ropp_involutive.
apply Rlt_le. apply Rlt_le.
now apply Ropp_0_gt_lt_contravar. now apply Ropp_0_gt_lt_contravar.
rewrite Zaway_floor. rewrite Zaway_floor.
unfold Zceil. apply sym_eq.
now rewrite Zopp_involutive. apply Zopp_involutive.
rewrite <- Ropp_0. rewrite <- Ropp_0.
now apply Ropp_le_contravar. now apply Ropp_le_contravar.
Qed. Qed.
...@@ -1496,7 +1496,7 @@ Proof. ...@@ -1496,7 +1496,7 @@ Proof.
intros x. intros x.
rewrite Zaway_ceil. 2: apply Rabs_pos. rewrite Zaway_ceil. 2: apply Rabs_pos.
unfold Zaway. unfold Zaway.
destruct Rlt_le_dec as [H|H]. case Rlt_bool_spec ; intro H.
rewrite Rabs_left with (1 := H). rewrite Rabs_left with (1 := H).
rewrite Zabs_non_eq. rewrite Zabs_non_eq.
apply (f_equal (fun v => - Zfloor v)%Z). apply (f_equal (fun v => - Zfloor v)%Z).
......
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