diff options
Diffstat (limited to 'flocq/Core')
| -rw-r--r-- | flocq/Core/Core.v | 3 | ||||
| -rw-r--r-- | flocq/Core/Defs.v | 5 | ||||
| -rw-r--r-- | flocq/Core/Digits.v | 37 | ||||
| -rw-r--r-- | flocq/Core/FIX.v | 13 | ||||
| -rw-r--r-- | flocq/Core/FLT.v | 9 | ||||
| -rw-r--r-- | flocq/Core/FLX.v | 7 | ||||
| -rw-r--r-- | flocq/Core/FTZ.v | 6 | ||||
| -rw-r--r-- | flocq/Core/Float_prop.v | 12 | ||||
| -rw-r--r-- | flocq/Core/Generic_fmt.v | 34 | ||||
| -rw-r--r-- | flocq/Core/Raux.v | 116 | ||||
| -rw-r--r-- | flocq/Core/Round_NE.v | 5 | ||||
| -rw-r--r-- | flocq/Core/Round_pred.v | 3 | ||||
| -rw-r--r-- | flocq/Core/Ulp.v | 12 | ||||
| -rw-r--r-- | flocq/Core/Zaux.v | 108 |
14 files changed, 285 insertions, 85 deletions
diff --git a/flocq/Core/Core.v b/flocq/Core/Core.v index 78a140e1..6ec5728e 100644 --- a/flocq/Core/Core.v +++ b/flocq/Core/Core.v @@ -18,5 +18,4 @@ COPYING file for more details. *) (** To ease the import *) -Require Export Raux Defs Float_prop Round_pred Generic_fmt Round_NE. -Require Export FIX FLX FLT Ulp. +Require Export Zaux Raux Defs Digits Float_prop Round_pred Generic_fmt Round_NE FIX FLX FLT Ulp. diff --git a/flocq/Core/Defs.v b/flocq/Core/Defs.v index 27342df9..4a199e01 100644 --- a/flocq/Core/Defs.v +++ b/flocq/Core/Defs.v @@ -18,7 +18,10 @@ COPYING file for more details. *) (** * Basic definitions: float and rounding property *) -Require Import Raux. + +From Coq Require Import ZArith Reals. + +Require Import Raux Zaux. Section Def. diff --git a/flocq/Core/Digits.v b/flocq/Core/Digits.v index a18ff8d6..7fe51cca 100644 --- a/flocq/Core/Digits.v +++ b/flocq/Core/Digits.v @@ -18,12 +18,12 @@ COPYING file for more details. *) From Coq Require Import Lia ZArith Zquot. +From Coq Require SpecFloat. Require Import Zaux. -Require Import SpecFloatCompat. -Notation digits2_pos := digits2_pos (only parsing). -Notation Zdigits2 := Zdigits2 (only parsing). +Notation digits2_pos := SpecFloat.digits2_pos (only parsing). +Notation Zdigits2 := SpecFloat.Zdigits2 (only parsing). (** Number of bits (radix 2) of a positive integer. @@ -594,12 +594,12 @@ destruct (Zle_or_lt k2' k) as [Hk''|Hk'']. now apply Zdigit_slice_out. rewrite Zdigit_slice by now split. apply Zdigit_slice_out. -zify ; lia. -rewrite Zdigit_slice by (zify ; lia). +lia. +rewrite Zdigit_slice by lia. rewrite (Zdigit_slice n (k1 + k1')) by now split. rewrite Zdigit_slice. now rewrite Zplus_assoc. -zify ; lia. +lia. unfold Zslice. rewrite Z.min_r. now rewrite Zle_bool_false. @@ -821,6 +821,18 @@ Proof. now intros [|n|n]. Qed. +Theorem Zdigits_opp : + forall n, Zdigits (Z.opp n) = Zdigits n. +Proof. +now intros [|n|n]. +Qed. + +Theorem Zdigits_cond_Zopp : + forall s n, Zdigits (cond_Zopp s n) = Zdigits n. +Proof. +now intros [|] [|n|n]. +Qed. + Theorem Zdigits_gt_0 : forall n, n <> Z0 -> (0 < Zdigits n)%Z. Proof. @@ -933,7 +945,7 @@ intros x y Zx Hxy. assert (Hx := Zdigits_correct x). assert (Hy := Zdigits_correct y). apply (Zpower_lt_Zpower beta). -zify ; lia. +lia. Qed. Theorem lt_Zdigits : @@ -1103,6 +1115,17 @@ exact Hm. now rewrite <- (Z.abs_eq m) at 1. Qed. +Theorem Zdigits_succ_le : + forall x, (0 <= x)%Z -> + (Zdigits (x + 1) <= Zdigits x + 1)%Z. +Proof. + destruct x as [| p | p]; [intros _; now simpl | intros _ | lia]. + transitivity (Zdigits (Z.pos p * beta ^ 1)); + [apply Zdigits_le; [lia |] | rewrite Zdigits_mult_Zpower; lia]. + apply Ztac.Zlt_le_add_1. rewrite <-Z.mul_1_r at 1. apply Zmult_lt_compat_l; [lia |]. + rewrite Z.pow_1_r. apply radix_gt_1. +Qed. + End Fcore_digits. (** Specialized version for computing the number of bits of an integer *) diff --git a/flocq/Core/FIX.v b/flocq/Core/FIX.v index 779d94cb..1f4a5676 100644 --- a/flocq/Core/FIX.v +++ b/flocq/Core/FIX.v @@ -19,8 +19,9 @@ COPYING file for more details. (** * Fixed-point format *) -From Coq Require Import Lia. -Require Import Raux Defs Round_pred Generic_fmt Ulp Round_NE. +From Coq Require Import ZArith Reals Lia. + +Require Import Zaux Raux Defs Round_pred Generic_fmt Ulp Round_NE. Section RND_FIX. @@ -101,3 +102,11 @@ right; split; auto. Qed. End RND_FIX. + +Theorem round_FIX_IZR : + forall f x, + round radix2 (FIX_exp 0) f x = IZR (f x). +Proof. + intros f x. unfold round, F2R. simpl. rewrite Rmult_1_r. apply f_equal. + apply f_equal. unfold scaled_mantissa. simpl. apply Rmult_1_r. +Qed. diff --git a/flocq/Core/FLT.v b/flocq/Core/FLT.v index 7301328d..ee0b5d90 100644 --- a/flocq/Core/FLT.v +++ b/flocq/Core/FLT.v @@ -18,9 +18,10 @@ COPYING file for more details. *) (** * Floating-point format with gradual underflow *) -Require Import Raux Defs Round_pred Generic_fmt Float_prop. -Require Import FLX FIX Ulp Round_NE. -Require Import Psatz. + +From Coq Require Import ZArith Reals Psatz. + +Require Import Zaux Raux Defs Round_pred Generic_fmt Float_prop FLX FIX Ulp Round_NE. Section RND_FLT. @@ -336,7 +337,7 @@ rewrite <- bpow_plus. right; apply f_equal. replace (e - 1 + (1 - prec))%Z with (e - prec)%Z by ring. apply Z.max_l; simpl. -assert (emin+prec-1 < e)%Z; try lia. +cut (emin+prec-1 < e)%Z. lia. apply lt_bpow with beta. apply Rle_lt_trans with (1:=Hx). now apply He. diff --git a/flocq/Core/FLX.v b/flocq/Core/FLX.v index 78bffba5..c1abf639 100644 --- a/flocq/Core/FLX.v +++ b/flocq/Core/FLX.v @@ -18,9 +18,10 @@ COPYING file for more details. *) (** * Floating-point format without underflow *) -Require Import Raux Defs Round_pred Generic_fmt Float_prop. -Require Import FIX Ulp Round_NE. -Require Import Psatz. + +From Coq Require Import ZArith Reals Psatz. + +Require Import Zaux Raux Defs Round_pred Generic_fmt Float_prop FIX Ulp Round_NE. Section RND_FLX. diff --git a/flocq/Core/FTZ.v b/flocq/Core/FTZ.v index d6bae6ea..e2c7ebad 100644 --- a/flocq/Core/FTZ.v +++ b/flocq/Core/FTZ.v @@ -19,9 +19,9 @@ COPYING file for more details. (** * Floating-point format with abrupt underflow *) -From Coq Require Import Lia. -Require Import Raux Defs Round_pred Generic_fmt. -Require Import Float_prop Ulp FLX. +From Coq Require Import ZArith Reals Lia. + +Require Import Zaux Raux Defs Round_pred Generic_fmt Float_prop Ulp FLX. Section RND_FTZ. diff --git a/flocq/Core/Float_prop.v b/flocq/Core/Float_prop.v index a1f48d04..36a2a315 100644 --- a/flocq/Core/Float_prop.v +++ b/flocq/Core/Float_prop.v @@ -19,8 +19,9 @@ COPYING file for more details. (** * Basic properties of floating-point formats: lemmas about mantissa, exponent... *) -From Coq Require Import Lia. -Require Import Raux Defs Digits. +From Coq Require Import ZArith Reals Lia. + +Require Import Zaux Raux Defs Digits. Section Float_prop. @@ -381,10 +382,9 @@ rewrite <-IZR_Zpower. 2: now apply Zle_left. now apply IZR_lt. elim Zlt_not_le with (1 := Hm). simpl. -cut (e' - e < 0)%Z. 2: lia. -clear. -case (e' - e)%Z ; try easy. -intros p _. +assert (H: (e' - e < 0)%Z) by lia. +clear -H. +destruct (e' - e)%Z ; try easy. apply Zabs_pos. Qed. diff --git a/flocq/Core/Generic_fmt.v b/flocq/Core/Generic_fmt.v index af1bf3c1..a74c81b9 100644 --- a/flocq/Core/Generic_fmt.v +++ b/flocq/Core/Generic_fmt.v @@ -19,8 +19,9 @@ COPYING file for more details. (** * What is a real number belonging to a format, and many properties. *) -From Coq Require Import Lia. -Require Import Raux Defs Round_pred Float_prop. +From Coq Require Import ZArith Reals Lia. + +Require Import Zaux Raux Defs Round_pred Float_prop. Section Generic. @@ -427,7 +428,7 @@ rewrite Gx. replace (Ztrunc (scaled_mantissa x)) with Z0. apply F2R_0. cut (Z.abs (Ztrunc (scaled_mantissa x)) < 1)%Z. -clear ; zify ; lia. +clear ; lia. apply lt_IZR. rewrite abs_IZR. now rewrite <- scaled_mantissa_generic. @@ -1579,6 +1580,31 @@ apply Zlt_le_succ. now apply mag_gt_bpow. Qed. +Lemma lt_cexp_pos : + forall x y, + (0 < y)%R -> + (cexp x < cexp y)%Z -> + (x < y)%R. +Proof. +intros x y Zy He. +unfold cexp in He. +apply (lt_mag beta) with (1 := Zy). +generalize (monotone_exp (mag beta y) (mag beta x)). +lia. +Qed. + +Theorem lt_cexp : + forall x y, + (y <> 0)%R -> + (cexp x < cexp y)%Z -> + (Rabs x < Rabs y)%R. +Proof. +intros x y Zy He. +apply lt_cexp_pos. +now apply Rabs_pos_lt. +now rewrite 2!cexp_abs. +Qed. + Variable rnd : R -> Z. Context { valid_rnd : Valid_rnd rnd }. @@ -1804,7 +1830,7 @@ Theorem Znearest_imp : Proof. intros x n Hd. cut (Z.abs (Znearest x - n) < 1)%Z. -clear ; zify ; lia. +clear ; lia. apply lt_IZR. rewrite abs_IZR, minus_IZR. replace (IZR (Znearest x) - IZR n)%R with (- (x - IZR (Znearest x)) + (x - IZR n))%R by ring. diff --git a/flocq/Core/Raux.v b/flocq/Core/Raux.v index 221d84d6..4b2ce8d7 100644 --- a/flocq/Core/Raux.v +++ b/flocq/Core/Raux.v @@ -18,9 +18,10 @@ COPYING file for more details. *) (** * Missing definitions/lemmas *) -Require Import Psatz. -Require Export Reals ZArith. -Require Export Zaux. + +From Coq Require Import Psatz Reals ZArith. + +Require Import Zaux. Section Rmissing. @@ -65,15 +66,6 @@ Qed. Theorem Rabs_eq_R0 x : (Rabs x = 0 -> x = 0)%R. Proof. split_Rabs; lra. Qed. -Theorem Rplus_eq_reg_r : - forall r r1 r2 : R, - (r1 + r = r2 + r)%R -> (r1 = r2)%R. -Proof. -intros r r1 r2 H. -apply Rplus_eq_reg_l with r. -now rewrite 2!(Rplus_comm r). -Qed. - Theorem Rmult_lt_compat : forall r1 r2 r3 r4, (0 <= r1)%R -> (0 <= r3)%R -> (r1 < r2)%R -> (r3 < r4)%R -> @@ -89,15 +81,6 @@ apply Rle_lt_trans with (r1 * r4)%R. + exact H12. Qed. -Theorem Rmult_minus_distr_r : - forall r r1 r2 : R, - ((r1 - r2) * r = r1 * r - r2 * r)%R. -Proof. -intros r r1 r2. -rewrite <- 3!(Rmult_comm r). -apply Rmult_minus_distr_l. -Qed. - Lemma Rmult_neq_reg_r : forall r1 r2 r3 : R, (r2 * r1 <> r3 * r1)%R -> r2 <> r3. Proof. @@ -114,7 +97,6 @@ intros r1 r2 r3 H H1 H2. now apply H1, Rmult_eq_reg_r with r1. Qed. - Theorem Rmult_min_distr_r : forall r r1 r2 : R, (0 <= r)%R -> @@ -244,18 +226,6 @@ intros x y H. apply (Rle_trans _ (Rabs x)); [apply Rle_abs|apply (Rsqr_le_abs_0 _ _ H)]. Qed. -Theorem Rabs_le : - forall x y, - (-y <= x <= y)%R -> (Rabs x <= y)%R. -Proof. -intros x y (Hyx,Hxy). -unfold Rabs. -case Rcase_abs ; intros Hx. -apply Ropp_le_cancel. -now rewrite Ropp_involutive. -exact Hxy. -Qed. - Theorem Rabs_le_inv : forall x y, (Rabs x <= y)%R -> (-y <= x <= y)%R. @@ -1269,8 +1239,6 @@ apply Rmult_lt_compat_r with (2 := H1). now apply IZR_lt. Qed. -Section Zdiv_Rdiv. - Theorem Zfloor_div : forall x y, y <> Z0 -> @@ -1317,9 +1285,9 @@ rewrite Ropp_inv_permute with (1 := Zy'). rewrite <- 2!opp_IZR. rewrite <- Zmod_opp_opp. apply H. -clear -Hy. lia. +clear -Hy ; lia. apply H. -clear -Zy Hy. lia. +clear -Zy Hy ; lia. (* *) split. pattern (IZR (x / y)) at 1 ; rewrite <- Rplus_0_r. @@ -1329,7 +1297,36 @@ apply Rplus_lt_compat_l. apply H. Qed. -End Zdiv_Rdiv. +Theorem Ztrunc_div : + forall x y, y <> 0%Z -> + Ztrunc (IZR x / IZR y) = Z.quot x y. +Proof. + destruct y; [easy | |]; destruct x; intros _. + - rewrite Z.quot_0_l; [| easy]. unfold Rdiv. rewrite Rmult_0_l. + rewrite Ztrunc_floor; [| apply Rle_refl]. now rewrite Zfloor_IZR. + - rewrite Z.quot_div_nonneg; [| easy | easy]. rewrite <-Zfloor_div; [| easy]. + unfold Ztrunc. rewrite Rlt_bool_false; [reflexivity |]. + apply Rle_mult_inv_pos; [now apply IZR_le | now apply IZR_lt]. + - rewrite <-Pos2Z.opp_pos. rewrite Z.quot_opp_l; [| easy]. + rewrite Z.quot_div_nonneg; [| easy | easy]. rewrite <-Zfloor_div; [| easy]. + rewrite Ropp_Ropp_IZR. rewrite Ropp_div. unfold Ztrunc. rewrite Rlt_bool_true. + + unfold Zceil. now rewrite Ropp_involutive. + + apply Ropp_lt_gt_0_contravar. apply Rdiv_lt_0_compat; now apply IZR_lt. + - rewrite Z.quot_0_l; [| easy]. unfold Rdiv. rewrite Rmult_0_l. + rewrite Ztrunc_floor; [| apply Rle_refl]. now rewrite Zfloor_IZR. + - rewrite <-Pos2Z.opp_pos. rewrite Z.quot_opp_r; [| easy]. + rewrite Z.quot_div_nonneg; [| easy | easy]. rewrite <-Zfloor_div; [| easy]. + rewrite Ropp_Ropp_IZR. rewrite Ropp_div_den; [| easy]. unfold Ztrunc. + rewrite Rlt_bool_true. + + unfold Zceil. now rewrite Ropp_involutive. + + apply Ropp_lt_gt_0_contravar. apply Rdiv_lt_0_compat; now apply IZR_lt. + - rewrite <-2Pos2Z.opp_pos. rewrite Z.quot_opp_l; [| easy]. rewrite Z.quot_opp_r; [| easy]. + rewrite Z.quot_div_nonneg; [| easy | easy]. rewrite <-Zfloor_div; [| easy]. + rewrite 2Ropp_Ropp_IZR. rewrite Ropp_div. rewrite Ropp_div_den; [| easy]. + rewrite Z.opp_involutive. rewrite Ropp_involutive. + unfold Ztrunc. rewrite Rlt_bool_false; [reflexivity |]. + apply Rle_mult_inv_pos; [now apply IZR_le | now apply IZR_lt]. +Qed. Section pow. @@ -1912,7 +1909,7 @@ apply bpow_le. now apply Zlt_le_weak. apply IZR_le. clear -Zm. -zify ; lia. +lia. Qed. Lemma mag_mult : @@ -2040,6 +2037,33 @@ replace (ex - 1 - 1)%Z with (ex - 2)%Z by ring. now apply Rabs_ge; right. Qed. +Theorem mag_plus_ge : + forall x y, + (x <> 0)%R -> + (mag y <= mag x - 2)%Z -> + (mag x - 1 <= mag (x + y))%Z. +Proof. +intros x y Zx. +destruct (Req_dec y 0) as [Zy|Zy]. +{ intros _. + rewrite Zy, Rplus_0_r. + lia. } +rewrite <- (mag_abs x), <- (mag_abs y). +intros Hm. +assert (H: Rabs x <> Rabs y). +{ intros H. + apply Zlt_not_le with (2 := Hm). + rewrite H. + lia. } +apply mag_minus_lb in Hm ; try now apply Rabs_pos_lt. +apply Z.le_trans with (1 := Hm). +apply mag_le_abs. +now apply Rminus_eq_contra. +rewrite <- (Ropp_involutive y). +rewrite Rabs_Ropp. +apply Rabs_triang_inv2. +Qed. + Lemma mag_div : forall x y : R, x <> 0%R -> y <> 0%R -> @@ -2183,6 +2207,15 @@ now apply Rabs_left. now apply Rabs_pos_eq. Qed. +Theorem Rlt_bool_cond_Ropp : + forall x sx, (0 < x)%R -> + Rlt_bool (cond_Ropp sx x) 0 = sx. +Proof. + intros x sx Hx. destruct sx; simpl. + - apply Rlt_bool_true. now apply Ropp_lt_gt_0_contravar. + - apply Rlt_bool_false. now left. +Qed. + Theorem cond_Ropp_involutive : forall b x, cond_Ropp b (cond_Ropp b x) = x. @@ -2335,8 +2368,7 @@ refine (Rle_not_lt _ _ (lub (/ (INR (S N) + 1))%R _) _). intros Hy. refine (H _ _ Py). apply INR_lt in Hy. - clear -Hy HyN. - lia. + clear -Hy HyN ; lia. now apply Rlt_le, Rinv_0_lt_compat. rewrite S_INR, HN. ring_simplify (IZR (up (/ l)) - 1 + 1)%R. diff --git a/flocq/Core/Round_NE.v b/flocq/Core/Round_NE.v index b7387a62..6a6fb0fb 100644 --- a/flocq/Core/Round_NE.v +++ b/flocq/Core/Round_NE.v @@ -19,8 +19,9 @@ COPYING file for more details. (** * Rounding to nearest, ties to even: existence, unicity... *) -From Coq Require Import Lia. -Require Import Raux Defs Round_pred Generic_fmt Float_prop Ulp. +From Coq Require Import ZArith Reals Lia. + +Require Import Zaux Raux Defs Round_pred Generic_fmt Float_prop Ulp. Notation ZnearestE := (Znearest (fun x => negb (Z.even x))). diff --git a/flocq/Core/Round_pred.v b/flocq/Core/Round_pred.v index b7b6778f..c811aec8 100644 --- a/flocq/Core/Round_pred.v +++ b/flocq/Core/Round_pred.v @@ -18,6 +18,9 @@ COPYING file for more details. *) (** * Roundings: properties and/or functions *) + +From Coq Require Import Reals. + Require Import Raux Defs. Section RND_prop. diff --git a/flocq/Core/Ulp.v b/flocq/Core/Ulp.v index c42b3e65..2459e35b 100644 --- a/flocq/Core/Ulp.v +++ b/flocq/Core/Ulp.v @@ -18,8 +18,10 @@ COPYING file for more details. *) (** * Unit in the Last Place: our definition using fexp and its properties, successor and predecessor *) -Require Import Reals Psatz. -Require Import Raux Defs Round_pred Generic_fmt Float_prop. + +From Coq Require Import ZArith Reals Psatz. + +Require Import Zaux Raux Defs Round_pred Generic_fmt Float_prop. Section Fcore_ulp. @@ -1100,7 +1102,7 @@ exfalso ; lra. intros n Hn H. assert (fexp (mag beta eps) = fexp n). apply valid_exp; try assumption. -assert(mag beta eps-1 < fexp n)%Z;[idtac|lia]. +cut (mag beta eps-1 < fexp n)%Z. lia. apply lt_bpow with beta. apply Rle_lt_trans with (2:=proj2 H). destruct (mag beta eps) as (e,He). @@ -1165,7 +1167,7 @@ lra. intros n Hn H. assert (fexp (mag beta eps) = fexp n). apply valid_exp; try assumption. -assert(mag beta eps-1 < fexp n)%Z;[idtac|lia]. +cut (mag beta eps-1 < fexp n)%Z. lia. apply lt_bpow with beta. apply Rle_lt_trans with (2:=H). destruct (mag beta eps) as (e,He). @@ -1919,7 +1921,7 @@ rewrite ulp_neq_0; trivial. apply f_equal. unfold cexp. apply valid_exp; trivial. -assert (mag beta x -1 < fexp n)%Z;[idtac|lia]. +cut (mag beta x -1 < fexp n)%Z. lia. apply lt_bpow with beta. destruct (mag beta x) as (e,He). simpl. diff --git a/flocq/Core/Zaux.v b/flocq/Core/Zaux.v index 5ca3971f..57e351dd 100644 --- a/flocq/Core/Zaux.v +++ b/flocq/Core/Zaux.v @@ -18,11 +18,10 @@ COPYING file for more details. *) From Coq Require Import ZArith Lia Zquot. +From Coq Require SpecFloat. -Require Import SpecFloatCompat. - -Notation cond_Zopp := cond_Zopp (only parsing). -Notation iter_pos := iter_pos (only parsing). +Notation cond_Zopp := SpecFloat.cond_Zopp (only parsing). +Notation iter_pos := SpecFloat.iter_pos (only parsing). Section Zmissing. @@ -535,6 +534,39 @@ now apply He. now intros _ _. Qed. +Theorem Zeq_bool_diag : + forall x, Zeq_bool x x = true. +Proof. +intros x. +now apply Zeq_bool_true. +Qed. + +Theorem Zeq_bool_opp : + forall x y, + Zeq_bool (Z.opp x) y = Zeq_bool x (Z.opp y). +Proof. +intros x y. +case Zeq_bool_spec. +- intros <-. + apply eq_sym, Zeq_bool_true. + apply eq_sym, Z.opp_involutive. +- intros H. + case Zeq_bool_spec. + 2: easy. + intros ->. + contradict H. + apply Z.opp_involutive. +Qed. + +Theorem Zeq_bool_opp' : + forall x y, + Zeq_bool (Z.opp x) (Z.opp y) = Zeq_bool x y. +Proof. +intros x y. +rewrite Zeq_bool_opp. +apply f_equal, Z.opp_involutive. +Qed. + End Zeq_bool. Section Zle_bool. @@ -575,6 +607,32 @@ now apply Z.le_lt_trans with y. apply refl_equal. Qed. +Theorem Zle_bool_opp_l : + forall x y, + Zle_bool (Z.opp x) y = Zle_bool (Z.opp y) x. +Proof. +intros x y. +case Zle_bool_spec ; intros Hxy ; + case Zle_bool_spec ; intros Hyx ; try easy ; lia. +Qed. + +Theorem Zle_bool_opp : + forall x y, + Zle_bool (Z.opp x) (Z.opp y) = Zle_bool y x. +Proof. +intros x y. +now rewrite Zle_bool_opp_l, Z.opp_involutive. +Qed. + +Theorem Zle_bool_opp_r : + forall x y, + Zle_bool x (Z.opp y) = Zle_bool y (Z.opp x). +Proof. +intros x y. +rewrite <- (Z.opp_involutive x) at 1. +apply Zle_bool_opp. +Qed. + End Zle_bool. Section Zlt_bool. @@ -635,6 +693,33 @@ now rewrite Zle_bool_false. now rewrite Zle_bool_true. Qed. +Theorem Zlt_bool_opp_l : + forall x y, + Zlt_bool (Z.opp x) y = Zlt_bool (Z.opp y) x. +Proof. +intros x y. +rewrite <- 2! negb_Zle_bool. +apply f_equal, Zle_bool_opp_r. +Qed. + +Theorem Zlt_bool_opp_r : + forall x y, + Zlt_bool x (Z.opp y) = Zlt_bool y (Z.opp x). +Proof. +intros x y. +rewrite <- 2! negb_Zle_bool. +apply f_equal, Zle_bool_opp_l. +Qed. + +Theorem Zlt_bool_opp : + forall x y, + Zlt_bool (Z.opp x) (Z.opp y) = Zlt_bool y x. +Proof. +intros x y. +rewrite <- 2! negb_Zle_bool. +apply f_equal, Zle_bool_opp. +Qed. + End Zlt_bool. Section Zcompare. @@ -688,6 +773,12 @@ End Zcompare. Section cond_Zopp. +Theorem cond_Zopp_0 : + forall sx, cond_Zopp sx 0 = 0%Z. +Proof. +now intros [|]. +Qed. + Theorem cond_Zopp_negb : forall x y, cond_Zopp (negb x) y = Z.opp (cond_Zopp x y). Proof. @@ -717,6 +808,15 @@ now apply Zlt_le_weak. now apply Z.abs_eq. Qed. +Theorem Zeq_bool_cond_Zopp : + forall s m n, + Zeq_bool (cond_Zopp s m) n = Zeq_bool m (cond_Zopp s n). +Proof. +intros [|] m n ; simpl. +apply Zeq_bool_opp. +easy. +Qed. + End cond_Zopp. Section fast_pow_pos. |