Merge pull request #191 from anandadalton/easy_fixes

More deprecations of notation
coq-community · May 22, 2023 · e358180 · e358180
2 parents ad827d3 + 09f7719
commit e358180
Show file tree

Hide file tree

Showing 13 changed files with 35 additions and 35 deletions.
diff --git a/algebra/Bernstein.v b/algebra/Bernstein.v
@@ -231,8 +231,8 @@ Proof.
   rstepl (X0[*](nring (S n)[*]X0[*]Bernstein (proj1 (Nat.lt_succ_r (S i) n) l))[+]
     _X_[*](nring (S n)[*]X0[*]Bernstein (le_S_n i n H))[+] X0[*]Bernstein H).
   do 2 rewrite -> IHn.
-  rewrite <- (minus_Sn_m n i) by auto with *.
-  rewrite <-(minus_Sn_m (S n) (S i)) by auto with *.
+  rewrite (Nat.sub_succ_l i n) by auto with *.
+  rewrite (Nat.sub_succ_l (S i) (S n)) by auto with *.
   replace (S n - S i) with (n - i) by auto with *.
   change (nring (S (n - i)):cpoly_cring R) with (nring (n - i)[+][1]:cpoly_cring R).
   replace (le_S (S i) n (proj1 (Nat.lt_succ_r (S i) n) l)) with H by apply le_irrelevent.

diff --git a/fta/KeyLemma.v b/fta/KeyLemma.v
@@ -165,7 +165,7 @@ Proof.
       apply a_nonneg.
      apply H12.
       replace (n - j) with (S (n - S j)); [auto with arith|].
-      rewrite minus_Sn_m; auto with arith.
+      rewrite <- Nat.sub_succ_l; auto with arith.
      auto.
     rewrite <- H22.
     astepl (a (n - S j) [*] (a_0[-]eps[/] a (n - S j) [//]H16)).
@@ -193,7 +193,7 @@ Proof.
  elim (le_lt_eq_dec _ _ H15); intro H18.
   apply H12.
    replace (n - j) with (S (n - S j)); [auto with arith|].
-   rewrite minus_Sn_m; auto with arith.
+   rewrite <- Nat.sub_succ_l; auto with arith.
   auto.
  rewrite <- H18.
  apply less_leEq; auto.

diff --git a/ftc/FunctSeries.v b/ftc/FunctSeries.v
@@ -760,7 +760,7 @@ Proof.
    apply mult_resp_leEq_lft.
     apply Hrecn; auto with arith.
    assumption.
-  rewrite <- minus_Sn_m.
+  rewrite Nat.sub_succ_l.
    simpl in |- *; rational.
   auto with arith.
  rewrite b0; intros.

diff --git a/ftc/Integral.v b/ftc/Integral.v
@@ -962,7 +962,7 @@ Proof.
   apply prf1; auto.
  eapply leEq_wdr.
   apply b2.
- apply prf1; rewrite minus_Sn_m; auto with arith.
+ apply prf1; rewrite <- Nat.sub_succ_l; auto with arith.
 Qed.
 
 Lemma partition_join_Pts_wd : forall i j,

diff --git a/liouville/QX_root_loc.v b/liouville/QX_root_loc.v
@@ -182,7 +182,7 @@ Proof.
  rewrite <- CRings.mult_assoc.
  apply mult_wd.
   reflexivity.
- rewrite <- minus_Sn_m; [|assumption].
+ rewrite Nat.sub_succ_l; [|assumption].
  reflexivity.
 Qed.
 

diff --git a/model/Zmod/ZBasics.v b/model/Zmod/ZBasics.v
@@ -66,7 +66,7 @@ Proof.
  intros n k Hlt.
  induction  n as [| n Hrecn].
   inversion Hlt.
- rewrite <- minus_Sn_m.
+ rewrite <- Nat.sub_succ_l.
   simpl in |- *.
   reflexivity.
  unfold lt in Hlt.

diff --git a/model/Zmod/ZDivides.v b/model/Zmod/ZDivides.v
@@ -499,8 +499,8 @@ Proof.
  intros a b.
  generalize (Z_mod_lt (Z.abs a) (Z.abs b)).
  case a.
-   case b; unfold Z.abs, Z.opp, Zmod, Z.div_eucl in |- *; auto with zarith.
-  case b; unfold Z.abs, Z.opp, Zmod, Z.div_eucl in |- *.
+   case b; unfold Z.abs, Z.opp, Z.modulo, Z.div_eucl in |- *; auto with zarith.
+  case b; unfold Z.abs, Z.opp, Z.modulo, Z.div_eucl in |- *.
     auto with zarith.
    intros p q.
    elim (Zdiv_eucl_POS q (Zpos p)); intros Q R.
@@ -515,7 +515,7 @@ Proof.
    auto with zarith.
   intro r'; intros H0 H1 H2.
   elim H0; auto with zarith.
- case b; unfold Z.abs, Z.opp, Zmod, Z.div_eucl in |- *.
+ case b; unfold Z.abs, Z.opp, Z.modulo, Z.div_eucl in |- *.
    auto with zarith.
   intros p q.
   elim (Zdiv_eucl_POS q (Zpos p)); intros Q R.
@@ -529,7 +529,7 @@ Lemma Zdiv_Zopp :
  forall a b : Z, (a mod b)%Z = 0%Z -> (a / - b)%Z = (- (a / b))%Z.
 Proof.
  intros a b.
- unfold Zmod, Z.div, Z.div_eucl in |- *.
+ unfold Z.modulo, Z.div, Z.div_eucl in |- *.
  case a.
    auto.
   intro A.
@@ -540,7 +540,7 @@ Proof.
    intro Hr; rewrite Hr; auto.
   intro B.
   generalize (Z_mod_lt (Zpos A) (Zpos B)).
-  unfold Zmod, Z.div_eucl in |- *.
+  unfold Z.modulo, Z.div_eucl in |- *.
   elim (Zdiv_eucl_POS A (Zpos B)); intros q r.
   case r.
     intros _ HR; fold (- q)%Z in |- *; fold (- - q)%Z in |- *; rewrite Z.opp_involutive; auto.
@@ -557,7 +557,7 @@ Proof.
    auto.
   intro B.
   generalize (Z_mod_lt (Zpos A) (Zpos B)).
-  unfold Zmod, Z.div_eucl in |- *.
+  unfold Z.modulo, Z.div_eucl in |- *.
   elim (Zdiv_eucl_POS A (Zpos B)); intros q r.
   case r.
     intros _ HR; fold (- q)%Z in |- *; fold (- - q)%Z in |- *; rewrite Z.opp_involutive; auto.
@@ -571,7 +571,7 @@ Proof.
   elim Hlt; auto with zarith; intro Hfalse; elim Hfalse; auto with zarith.
  intro B.
  generalize (Z_mod_lt (Zpos A) (Zpos B)).
- unfold Zmod, Z.div_eucl in |- *.
+ unfold Z.modulo, Z.div_eucl in |- *.
  elim (Zdiv_eucl_POS A (Zpos B)); intros q r.
  case r.
    intros _ HR; fold (- q)%Z in |- *; auto.

diff --git a/model/Zmod/Zm.v b/model/Zmod/Zm.v
@@ -571,11 +571,11 @@ Section zp_nonzero.
 Variable x: Zp.
 Hypothesis Hx: x[#][0].
 
-Lemma Zp_nonz_mod: 0<(Zmod x m)<m.
+Lemma Zp_nonz_mod: 0<(Z.modulo x m)<m.
 Proof.
  generalize (Z_mod_lt x m); intro H; elim H; clear H; intros.
   split.
-   elim (Zlt_asymmetric (Zmod x m) 0).
+   elim (Zlt_asymmetric (Z.modulo x m) 0).
     intro Hfalse; elim Hx; elim Hfalse; clear Hfalse; intro Hfalse.
      elim H; apply Z.lt_gt; auto.
     simpl; rewrite <-Hfalse; auto with zarith.
@@ -592,8 +592,8 @@ Proof.
  unfold Zrelprime.
  rewrite <-Zgcd_mod_lft; auto.
   generalize Hxmod0.
-  set (d:=(Zmod x m)).
-  cut (d=(Zmod x m)).
+  set (d:=(Z.modulo x m)).
+  cut (d=(Z.modulo x m)).
    case d.
      intros _ Hfalse; elim (Zlt_irref _ Hfalse).
     intros D HD _.
@@ -662,8 +662,8 @@ Proof.
    unfold Zrelprime.
    rewrite <-Zgcd_mod_rht; auto.
     generalize Hxmod0.
-    set (d:=(Zmod x m)).
-    cut (d=(Zmod x m)); auto.
+    set (d:=(Z.modulo x m)).
+    cut (d=(Z.modulo x m)); auto.
     case d.
       intros _ Hfalse; elim (Zlt_irref _ Hfalse).
      intros D HD _.
@@ -687,8 +687,8 @@ Proof.
   unfold Zrelprime.
   rewrite <-Zgcd_mod_rht; auto.
    generalize Hxmod0.
-   set (d:=(Zmod x m)).
-   cut (d=(Zmod x m)); auto.
+   set (d:=(Z.modulo x m)).
+   cut (d=(Z.modulo x m)); auto.
    case d.
      intros _ Hfalse; elim (Zlt_irref _ Hfalse).
     intros D HD _.

diff --git a/reals/Series.v b/reals/Series.v
@@ -886,7 +886,7 @@ Proof.
  intro; inversion_clear H2.
   apply leEq_transitive with (c[*]AbsIR (x n)).
    apply H; auto with arith.
-  rewrite <- minus_Sn_m.
+  rewrite Nat.sub_succ_l.
    astepr (AbsIR (x N) [*] (c[*]c[^] (n - N))).
    rstepr (c[*] (AbsIR (x N) [*]c[^] (n - N))).
    apply mult_resp_leEq_lft.

diff --git a/reals/fast/Compress.v b/reals/fast/Compress.v
@@ -83,15 +83,15 @@ Proof.
  apply Zmult_gt_0_lt_reg_r with (Zpos d).
  reflexivity.
  replace ((n * Zpos p / Zpos d * 1 + 1) * Zpos d)%Z
-   with (Zpos d* (n*Zpos p/ Zpos d) + (Zmod (n*Zpos p) (Zpos d)) - (Zmod (n*Zpos p) (Zpos d)) + Zpos d)%Z
+   with (Zpos d* (n*Zpos p/ Zpos d) + (Z.modulo (n*Zpos p) (Zpos d)) - (Z.modulo (n*Zpos p) (Zpos d)) + Zpos d)%Z
    by ring.
  rewrite <- (Z_div_mod_eq_full (n*Zpos p) (Zpos d)).
  apply Z.le_lt_trans with (n*1*Zpos p)%Z.
   replace (z*Zpos p*Zpos d)%Z with (z*Zpos d*Zpos p)%Z by ring.
   apply Zmult_lt_0_le_compat_r; auto with *.
  apply Zlt_0_minus_lt.
  replace (n * Zpos p - (n * Zpos p) mod (Zpos d) + Zpos d - n * 1 * Zpos p)%Z
-   with (Zpos d - (Zmod (n*Zpos p) (Zpos d)))%Z by ring.
+   with (Zpos d - (Z.modulo (n*Zpos p) (Zpos d)))%Z by ring.
  rewrite <- Zlt_plus_swap.
  ring_simplify.
  assert (X:(Zpos d >0)%Z) by auto with *.

diff --git a/reals/stdlib/CMTFullSets.v b/reals/stdlib/CMTFullSets.v
@@ -166,7 +166,7 @@ Proof.
   destruct xdf as [xnDiag cvDiag].
   assert (forall a b:nat, lt a b -> lt (diagPlane n a) (diagPlane n b)).
   { intros. unfold diagPlane. apply Nat.add_lt_le_mono. assumption.
-    apply Nat.div_le_mono. auto. apply Nat.mul_le_mono.
+    apply Nat.Div0.div_le_mono. auto. apply Nat.mul_le_mono.
     apply Nat.add_le_mono. apply Nat.le_refl. unfold lt in H0.
     apply (Nat.le_trans _ (S a)). apply le_S. apply Nat.le_refl. assumption.
     apply le_n_S. apply Nat.add_le_mono. apply Nat.le_refl. unfold lt in H0.

diff --git a/reals/stdlib/CMTIntegrableFunctions.v b/reals/stdlib/CMTIntegrableFunctions.v
@@ -434,13 +434,13 @@ Proof.
     apply (CRle_trans _ _ _ (CRabs_triang _ _)).
     setoid_replace (1 # n)%Q with ((1 # (2*n)) + (1 # (2*n)))%Q.
     apply le_S_n in H1. rewrite CR_of_Q_plus. apply CRplus_le_compat.
-    apply H. rewrite <- (Nat.div_mul N 2). apply Nat.div_le_mono.
+    apply H. rewrite <- (Nat.div_mul N 2). apply Nat.Div0.div_le_mono.
     auto. apply (Nat.le_trans (N*2) (N*2 + (S N0)*2)). apply Nat.le_add_r.
     apply (Nat.le_trans _ i). assumption.
     apply le_S. apply Nat.le_refl. auto.
     apply H0. assert (N0 = pred (S N0)). reflexivity.
     rewrite H2. apply Nat.pred_le_mono. rewrite <- (Nat.div_mul (S N0) 2).
-    apply Nat.div_le_mono. auto.
+    apply Nat.Div0.div_le_mono. auto.
     apply (Nat.le_trans _ (N*2 + (S N0)*2)).
     rewrite Nat.add_comm. apply Nat.le_add_r.
     apply (Nat.le_trans (N*2 + (S N0)*2) i). assumption. apply le_S. apply Nat.le_refl. auto.
@@ -453,11 +453,11 @@ Proof.
     apply (CRle_trans _ _ _ (CRabs_triang _ _)).
     setoid_replace (1 # n)%Q with ((1 # (2*n)) + (1 # (2*n)))%Q.
     apply le_S_n in H1. rewrite CR_of_Q_plus. apply CRplus_le_compat.
-    apply H. rewrite <- (Nat.div_mul N 2). apply Nat.div_le_mono.
+    apply H. rewrite <- (Nat.div_mul N 2). apply Nat.Div0.div_le_mono.
     auto. apply (Nat.le_trans (N*2) (N*2 + (S N0)*2)). apply Nat.le_add_r.
     apply (Nat.le_trans _ i). assumption. apply le_S. apply Nat.le_refl. auto.
     apply H0. rewrite <- (Nat.div_mul N0 2).
-    apply Nat.div_le_mono. auto.
+    apply Nat.Div0.div_le_mono. auto.
     apply (Nat.le_trans (N0*2) (N*2 + (S N0)*2)). rewrite Nat.add_comm.
     apply (Nat.le_trans (N0 * 2) (S N0 * 2)).
     apply Nat.mul_le_mono_r. apply le_S. apply Nat.le_refl.

diff --git a/reals/stdlib/ConstructiveDiagonal.v b/reals/stdlib/ConstructiveDiagonal.v
@@ -285,7 +285,7 @@ Proof.
   assert (I = K).
   - destruct (Nat.lt_trichotomy I K).
     + exfalso. unfold lt in H0. assert ((S I) * S (S I) / 2 <= K * S K / 2)%nat.
-      apply Nat.div_le_mono. intro absurd. inversion absurd.
+      apply Nat.Div0.div_le_mono.
       apply Nat.mul_le_mono_nonneg. apply Nat.le_0_l. assumption. apply Nat.le_0_l.
       apply le_n_S. assumption. rewrite diagPlaneAbsNext in H1.
       apply (Nat.add_le_mono_l (I * S I / 2 + S I) (K * S K / 2) l) in H1.
@@ -298,7 +298,7 @@ Proof.
       assumption. apply Nat.le_refl.
     + destruct H0. assumption. exfalso.
       unfold lt in H0. assert ((S K) * S (S K) / 2 <= I * S I / 2)%nat.
-      apply Nat.div_le_mono. intro absurd. inversion absurd.
+      apply Nat.Div0.div_le_mono.
       apply Nat.mul_le_mono_nonneg. apply Nat.le_0_l. assumption. apply Nat.le_0_l.
       apply le_n_S. assumption. rewrite diagPlaneAbsNext in H1.
       apply (Nat.add_le_mono_l (K * S K / 2 + S K) (I * S I / 2) j) in H1.
@@ -433,7 +433,7 @@ Proof.
   rewrite des in H0. unfold diagPlane in H0. unfold diagPlane.
   subst p. rewrite Nat.add_0_l. ring. unfold diagPlane. rewrite Nat.add_0_l.
   rewrite Nat.add_0_l. remember (i + j)%nat. apply Nat.add_le_mono. assumption.
-  apply Nat.div_le_mono. auto. apply Nat.mul_le_mono_nonneg.
+  apply Nat.Div0.div_le_mono. auto. apply Nat.mul_le_mono_nonneg.
   apply Nat.le_0_l. assumption. apply Nat.le_0_l. apply le_n_S. assumption.
 Qed.
 
@@ -558,7 +558,7 @@ Proof.
   remember (S n + p)%nat as n0. assert (n <= n0)%nat.
   subst n0. simpl. apply le_S. rewrite <- (Nat.add_0_r n). rewrite <- Nat.add_assoc.
   apply Nat.add_le_mono_l. apply Nat.le_0_l.
-  apply Nat.add_le_mono. assumption. apply Nat.div_le_mono. auto.
+  apply Nat.add_le_mono. assumption. apply Nat.Div0.div_le_mono. auto.
   apply Nat.mul_le_mono. assumption. apply le_n_S. assumption.
   rewrite CRabs_minus_sym. apply H. apply Nat.le_refl.
   unfold CRminus. rewrite CRplus_assoc. apply CRplus_morph. reflexivity.