Merge pull request #194 from anandadalton/easy_fixes

Deprecated notations
coq-community · May 24, 2023 · b446ae7 · b446ae7
2 parents e358180 + 2a7c386
commit b446ae7
Show file tree

Hide file tree

Showing 25 changed files with 89 additions and 85 deletions.
diff --git a/algebra/Bernstein.v b/algebra/Bernstein.v
@@ -280,7 +280,7 @@ match v in Vector.t _ i return i <= n -> cpoly_cring R with
 |Vector.cons a i' v' =>
   match n as n return (S i' <= n) -> cpoly_cring R with
   | O => fun p => False_rect _ (Nat.nle_succ_0 _ p)
-  | S n' => fun p => _C_ a[*]Bernstein (le_S_n _ _ p)[+]evalBernsteinBasisH v' (le_Sn_le _ _ p)
+  | S n' => fun p => _C_ a[*]Bernstein (le_S_n _ _ p)[+]evalBernsteinBasisH v' (Nat.lt_le_incl _ _ p)
   end
 end.
 
@@ -367,7 +367,7 @@ Proof.
   intros H H'.
   replace (proj1 (Nat.lt_succ_r j n) H) with (proj1 (Nat.lt_succ_r j n) H') by apply le_irrelevent.
   reflexivity.
- rstepl (evalBernsteinBasisH (Vector.const c i) (le_Sn_le i (S n) l)[+]
+ rstepl (evalBernsteinBasisH (Vector.const c i) (Nat.lt_le_incl i (S n) l)[+]
    _C_ c[*](Bernstein (le_S_n i n l)[+] Sum (S i) n (part_tot_nat_fun (cpoly_cring R) (S n)
      (fun (i0 : nat) (H : i0 < S n) => Bernstein (proj1 (Nat.lt_succ_r i0 n) H))))).
  replace (Bernstein (le_S_n _ _ l)) with (part_tot_nat_fun (cpoly_cring R) (S n)
@@ -400,7 +400,7 @@ match v in Vector.t _ i return i <= n -> Vector.t R (S i) with
 | Vector.nil => fun _ => Vector.cons [0] _ Vector.nil
 | Vector.cons a i' v' => match n as n return S i' <= n -> Vector.t R (S (S i')) with
   | O => fun p => False_rect _ (Nat.nle_succ_0 _ p)
-  | S n' => fun p => Vector.cons (eta(Qred (i#P_of_succ_nat n'))[*]a) _ (BernsteinBasisTimesXH v' (le_Sn_le _ _ p))
+  | S n' => fun p => Vector.cons (eta(Qred (i#P_of_succ_nat n'))[*]a) _ (BernsteinBasisTimesXH v' (Nat.lt_le_incl _ _ p))
   end
 end.
 

diff --git a/algebra/CPoly_ApZero.v b/algebra/CPoly_ApZero.v
@@ -316,8 +316,8 @@ Lemma poly_01_zero : forall n i j, j <= n -> j <> i -> (poly_01 i n) ! (a_ j) [=
 Proof.
  intros.
  induction  n0 as [| n0 Hrecn0]; intros.
-  rewrite <- (le_n_O_eq j H).
-  rewrite <- (le_n_O_eq j H) in H0.
+  rewrite (proj1 (Nat.le_0_r j) H).
+  rewrite (proj1 (Nat.le_0_r j) H) in H0.
   simpl in |- *.
   elim (eq_nat_dec i 0); intro y.
    rewrite y in H0.

diff --git a/fta/KeyLemma.v b/fta/KeyLemma.v
@@ -479,7 +479,7 @@ Proof.
    split. auto.
    intros j H9 k_j r i H10 H11.
   unfold k_j, r in |- *.
-  rewrite <- (le_n_O_eq _ H9).
+  rewrite (proj1 (Nat.le_0_r _) H9).
   replace (p3m 0) with OneR.
    2: auto.
   astepr (a k_0[*] (t[^]k_0[*][1][^]k_0)).

diff --git a/ftc/FunctSeries.v b/ftc/FunctSeries.v
@@ -764,7 +764,7 @@ Proof.
    simpl in |- *; rational.
   auto with arith.
  rewrite b0; intros.
- rewrite <- minus_n_n.
+ rewrite Nat.sub_diag.
  apply eq_imp_leEq.
  simpl in |- *; eapply eq_transitive_unfolded.
   2: apply eq_symmetric_unfolded; apply mult_one.

diff --git a/ftc/Partitions.v b/ftc/Partitions.v
@@ -182,7 +182,7 @@ Proof.
    apply mult_resp_leEq_rht.
     apply less_leEq; apply less_plusOne.
    apply shift_leEq_div.
-    apply nring_pos; clear Hi; apply neq_O_lt; auto.
+    apply nring_pos; clear Hi; apply Nat.neq_0_lt_0; auto.
    apply shift_leEq_minus.
    astepl ([0][+]a).
    astepl a; assumption.
@@ -660,7 +660,7 @@ Proof.
   eapply eq_transitive_unfolded.
    apply H.
   simpl in |- *; rational.
- apply (lt_O_neq n); auto.
+ apply (Nat.neq_0_lt_0 n); auto.
 Qed.
 
 (**
@@ -707,7 +707,7 @@ Proof.
    intros.
    apply mult_lt_compat_r.
     assumption.
-   apply neq_O_lt; auto.
+   apply Nat.neq_0_lt_0; auto.
   intros.
   cut (i * k <= m).
    intro.
@@ -767,7 +767,7 @@ Proof.
   apply ap_irreflexive_unfolded.
  astepl (nring m[*]nring (R:=IR) n).
  apply mult_resp_ap_zero; apply Greater_imp_ap; astepl (nring (R:=IR) 0);
-   apply nring_less; apply neq_O_lt; auto.
+   apply nring_less; apply Nat.neq_0_lt_0; auto.
 Qed.
 
 End Even_Partitions.
@@ -856,7 +856,7 @@ Lemma _Separated_imp_length_zero : forall n (P : Partition Hab n),
 Proof.
  intros n P H H0.
  cut (~ 0 <> n); [ auto with zarith | intro ].
- cut (0 < n); [ intro | apply neq_O_lt; auto ].
+ cut (0 < n); [ intro | apply Nat.neq_0_lt_0; auto ].
  cut (a [#] b).
   exact (eq_imp_not_ap _ _ _ H0).
  astepl (P _ (Nat.le_0_l _)).
@@ -871,7 +871,7 @@ Lemma partition_less_imp_gt_zero : forall n (P : Partition Hab n), a [<] b -> 0
 Proof.
  intros n P H.
  cut (0 <> n); intro.
-  apply neq_O_lt; auto.
+  apply Nat.neq_0_lt_0; auto.
  exfalso.
  cut (a [=] b).
   intro; apply less_irreflexive_unfolded with (x := a).

diff --git a/ftc/RefSepRef.v b/ftc/RefSepRef.v
@@ -381,7 +381,7 @@ Proof.
   cut (0 = m); [ intro; rewrite <- H0; auto | apply RSR_HR' ].
   apply partition_length_zero with Hab; rewrite <- H; apply P.
  elim (le_lt_dec n n); intro; simpl in |- *.
-  rewrite <- minus_n_n; auto.
+  rewrite Nat.sub_diag; auto.
  exfalso; apply Nat.lt_irrefl with n; auto.
 Qed.
 
@@ -401,7 +401,7 @@ Proof.
    elim (le_lt_dec n j); intro; simpl in |- *.
     apply plus_lt_compat_l.
     apply plus_lt_reg_l with n.
-    repeat rewrite <- le_plus_minus; auto.
+    repeat (rewrite Nat.add_comm; rewrite Nat.sub_add); auto.
    lia; auto; apply Nat.lt_trans with j; auto.
   elim (Nat.lt_irrefl 0); apply Nat.lt_trans with i; auto; apply Nat.lt_le_trans with j; auto.
  elim (le_lt_dec n j); intro; simpl in |- *.
@@ -416,7 +416,7 @@ Proof.
   cut (S (pred (m + n)) = S (pred m + n)); auto.
   rewrite <- plus_Sn_m.
   rewrite <- (Nat.lt_succ_pred 0 m); auto with arith.
-  apply neq_O_lt.
+  apply Nat.neq_0_lt_0.
   intro.
   apply Nat.lt_irrefl with 0.
   apply Nat.lt_trans with i; auto.
@@ -572,7 +572,7 @@ Proof.
   cut (0 = n); [ intro; rewrite <- H0; auto | apply RSR_HP' ].
   apply partition_length_zero with Hab; rewrite <- H; apply R.
  elim (le_lt_dec m m); intro; simpl in |- *.
-  rewrite <- minus_n_n; auto.
+  rewrite Nat.sub_diag; auto.
  elim (Nat.lt_irrefl _ b1).
 Qed.
 
@@ -592,7 +592,7 @@ Proof.
    elim (le_lt_dec m j); intro; simpl in |- *.
     apply plus_lt_compat_l.
     apply plus_lt_reg_l with m.
-    repeat rewrite <- le_plus_minus; auto.
+    repeat (rewrite Nat.add_comm; rewrite Nat.sub_add); auto.
    lia; auto; apply Nat.lt_trans with j; auto.
   elim (Nat.lt_irrefl 0); apply Nat.lt_trans with i; auto; apply Nat.lt_le_trans with j; auto.
  elim (le_lt_dec m j); intro; simpl in |- *.
@@ -610,7 +610,7 @@ Proof.
    apply Nat.lt_succ_pred with 0.
    apply Nat.lt_le_trans with m; auto with arith.
    apply Nat.lt_trans with i; auto.
-  apply neq_O_lt.
+  apply Nat.neq_0_lt_0.
   intro.
   apply Nat.lt_irrefl with 0.
   apply Nat.lt_trans with i; auto.

diff --git a/ftc/RefSeparating.v b/ftc/RefSeparating.v
@@ -70,7 +70,7 @@ Qed.
 Lemma SPap_n : n <> 0.
 Proof.
  intro.
- apply (lt_O_neq n).
+ apply (Nat.neq_0_lt_0 n).
   exact RS'_pos_n.
  auto.
 Qed.
@@ -221,7 +221,7 @@ Proof.
  exists m'.
  cut (m <> 0); intro.
   split.
-   cut (S m' = m); [ intro | unfold m' in |- *; apply Nat.lt_succ_pred with 0; apply neq_O_lt;
+   cut (S m' = m); [ intro | unfold m' in |- *; apply Nat.lt_succ_pred with 0; apply Nat.neq_0_lt_0;
      auto ].
    rewrite H0; clear H0 m'.
    cut (n <= sep__part_h m).
@@ -231,7 +231,7 @@ Proof.
    assumption.
   intros; apply Hm'.
   unfold m' in H0; rewrite <- (Nat.lt_succ_pred 0 m); auto with arith.
-  apply neq_O_lt; auto.
+  apply Nat.neq_0_lt_0; auto.
  apply SPap_n.
  rewrite H in Hm.
  simpl in Hm.
@@ -408,7 +408,8 @@ Proof.
   reflexivity.
  exfalso.
  generalize b0.
- apply lt_O_neq; apply RS'_pos_m.
+ apply Nat.neq_sym.
+ apply Nat.neq_0_lt_0; apply RS'_pos_m.
 Qed.
 
 Lemma sep__part_fun_i :

diff --git a/liouville/CPoly_Euclid.v b/liouville/CPoly_Euclid.v
@@ -107,7 +107,7 @@ Proof.
    apply H; apply -> Nat.succ_lt_mono; apply H3.
   split; [ rewrite -> coeff_Sm_lin; destruct H0; apply H0 | unfold degree_le; intros ].
   destruct m0; [ inversion H3 | simpl; destruct H0 ].
-  apply H4; apply lt_S_n; apply H3.
+  apply H4; apply Nat.succ_lt_mono; apply H3.
  unfold degree_lt_pair.
  split; intros.
   unfold degree_le; intros.

diff --git a/liouville/QX_root_loc.v b/liouville/QX_root_loc.v
@@ -117,7 +117,8 @@ Proof.
  rewrite -> nexp_ring_hom, nexp_ring_hom.
  rewrite <- CRings.mult_assoc, <- CRings.mult_assoc.
  apply mult_wdr.
- rewrite (le_plus_minus _ _ Hn) at 1.
+ rewrite <- (Nat.sub_add _ _ Hn) at 1.
+ rewrite Nat.add_comm.
  clear H0 Hn.
  rewrite <- nexp_plus.
  rewrite -> CRings.mult_assoc.

diff --git a/metric2/Compact.v b/metric2/Compact.v
@@ -607,7 +607,8 @@ Proof.
   - intros s k d1 d2 pt Hpt e1 e2 khalf H.
  set (A:=Z.to_nat (CompactTotallyBoundedIndex e1 d1 d2)) in *.
  set (B:=Z.to_nat (CompactTotallyBoundedIndex e2 d1 d2)) in *.
- rewrite (le_plus_minus _ _ H).
+ rewrite <- (Nat.sub_add _ _ H).
+ rewrite Nat.add_comm.
  assert (proj1_sig k < 1) as Y.
  { apply (Qle_lt_trans _ _ _ khalf). reflexivity. }
   assert (Y0:= (CompactTotallyBoundedStreamCauchyLemma

diff --git a/model/Zmod/ZBasics.v b/model/Zmod/ZBasics.v
@@ -99,7 +99,8 @@ Proof.
  intros k n Hle.
  induction  k as [| k Hreck].
   rewrite <- minus_n_O.
-  apply minus_n_n.
+  symmetry in |- *.
+  apply Nat.sub_diag.
  set (K := k) in |- * at 2.
  rewrite Hreck.
   unfold K in |- *; clear K.

diff --git a/model/Zmod/ZDivides.v b/model/Zmod/ZDivides.v
@@ -503,10 +503,10 @@ Proof.
   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.
+   elim (Coq.ZArith.BinIntDef.Z.pos_div_eucl q (Zpos p)); intros Q R.
    intros Hlt Hp HR; rewrite HR; auto with zarith.
   intros p q.
-  elim (Zdiv_eucl_POS q (Zpos p)); intros Q R.
+  elim (Coq.ZArith.BinIntDef.Z.pos_div_eucl q (Zpos p)); intros Q R.
   case R.
     auto with zarith.
    intro r'; intros H0 H1 H2.
@@ -518,10 +518,10 @@ Proof.
  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.
+  elim (Coq.ZArith.BinIntDef.Z.pos_div_eucl q (Zpos p)); intros Q R.
   case R; intros r' H0; intros; try (cut (Zpos r' = Zpos p); elim H0); auto with zarith.
  intros p q.
- elim (Zdiv_eucl_POS q (Zpos p)); intros Q R.
+ elim (Coq.ZArith.BinIntDef.Z.pos_div_eucl q (Zpos p)); intros Q R.
  case R; intros; try discriminate; try tauto.
 Qed.
 
@@ -536,12 +536,12 @@ Proof.
   case b; unfold Z.opp in |- *.
     auto.
    intro B.
-   elim (Zdiv_eucl_POS A (Zpos B)); intros q r.
+   elim (Coq.ZArith.BinIntDef.Z.pos_div_eucl A (Zpos B)); intros q r.
    intro Hr; rewrite Hr; auto.
   intro B.
   generalize (Z_mod_lt (Zpos A) (Zpos B)).
   unfold Z.modulo, Z.div_eucl in |- *.
-  elim (Zdiv_eucl_POS A (Zpos B)); intros q r.
+  elim (Coq.ZArith.BinIntDef.Z.pos_div_eucl A (Zpos B)); intros q r.
   case r.
     intros _ HR; fold (- q)%Z in |- *; fold (- - q)%Z in |- *; rewrite Z.opp_involutive; auto.
    intros R Hlt HR.
@@ -558,7 +558,7 @@ Proof.
   intro B.
   generalize (Z_mod_lt (Zpos A) (Zpos B)).
   unfold Z.modulo, Z.div_eucl in |- *.
-  elim (Zdiv_eucl_POS A (Zpos B)); intros q r.
+  elim (Coq.ZArith.BinIntDef.Z.pos_div_eucl A (Zpos B)); intros q r.
   case r.
     intros _ HR; fold (- q)%Z in |- *; fold (- - q)%Z in |- *; rewrite Z.opp_involutive; auto.
    intros R Hlt HR.
@@ -572,7 +572,7 @@ Proof.
  intro B.
  generalize (Z_mod_lt (Zpos A) (Zpos B)).
  unfold Z.modulo, Z.div_eucl in |- *.
- elim (Zdiv_eucl_POS A (Zpos B)); intros q r.
+ elim (Coq.ZArith.BinIntDef.Z.pos_div_eucl A (Zpos B)); intros q r.
  case r.
    intros _ HR; fold (- q)%Z in |- *; auto.
   intros; discriminate.

diff --git a/model/structures/Npossec.v b/model/structures/Npossec.v
@@ -82,7 +82,8 @@ Proof.
  cut (0 <> (x*S y0+x) -> (x*S y0+x) <> 0).
   intro H3.
   apply H3.
-  apply lt_O_neq.
+  apply Nat.neq_sym.
+  apply Nat.neq_0_lt_0.
   cut ((x*S y0+x) > 0).
    unfold gt in |- *.
    intuition.
@@ -92,7 +93,7 @@ Proof.
     lia.
    lia.
   unfold gt in |- *.
-  apply neq_O_lt.
+  apply Nat.neq_0_lt_0.
   cut ((x*S y0) <> 0).
    auto.
   apply Hrecy0.

diff --git a/ode/AbstractIntegration.v b/ode/AbstractIntegration.v
@@ -460,7 +460,7 @@ Section integral_approximation.
        rewrite <- Qplus_assoc, <- Qmult_plus_distr_l, <- Zplus_Qplus, <- Nat2Z.inj_add.
        apply Qplus_le_r. change (S n * proj1_sig iw' == proj1_sig w) in A. rewrite <- A.
        apply Qmult_le_compat_r. rewrite <- Zle_Qle. apply inj_le. rewrite Nat.add_comm.
-       now apply lt_le_S.
+       now apply Nat.le_succ_l.
        apply (proj2_sig iw').
        apply Qplus_le_l with (z := x), Qplus_le_l with (z := - proj1_sig w).
        setoid_replace (a - x + x + - proj1_sig w) with (a - proj1_sig w) by ring.