Upgrade to Flocq 4.1.

1 files changed, 39 insertions, 34 deletions

diff --git a/flocq/Core/Raux.v b/flocq/Core/Raux.v
index a418bf19..4b2ce8d7 100644
--- a/flocq/Core/Raux.v
+++ b/flocq/Core/Raux.v
@@ -66,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 ->
@@ -90,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.
@@ -115,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 ->
@@ -245,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.
@@ -1270,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 ->
@@ -1330,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.
 
@@ -2211,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.