'Deprecate lt_not_le for Nat.lt_nge'

coq-community · May 20, 2023 · 79d5b5f · 79d5b5f
1 parent e9affa7
commit 79d5b5f
Show file tree

Hide file tree

Showing 8 changed files with 29 additions and 29 deletions.
diff --git a/algebra/CPoly_Degree.v b/algebra/CPoly_Degree.v
@@ -463,7 +463,7 @@ Qed.
 Lemma poly_degree_lth : forall p : RX, degree_le (lth_of_poly p) p.
 Proof.
  unfold degree_le in |- *. intros. apply not_ap_imp_eq. intro.
- elim (lt_not_le _ _ H). apply Nat.lt_le_incl.
+ elim (proj1 (Nat.lt_nge _ _) H). apply Nat.lt_le_incl.
  apply lt_i_lth_of_poly. auto.
 Qed.
 

diff --git a/ftc/RefSepRef.v b/ftc/RefSepRef.v
@@ -704,7 +704,7 @@ Proof.
   elim (le_lt_dec m j); intro; simpl in |- *.
    rewrite not_le_minus_0.
     rewrite <- plus_n_O; auto with arith.
-   apply lt_not_le; auto.
+   apply Nat.lt_nge; auto.
   apply plus_pred_pred_plus.
   elim (ProjT2 (RSR_h_g' _ (lt_pred' _ _ b1 b2))); intros.
   assumption.

diff --git a/logic/CLogic.v b/logic/CLogic.v
@@ -454,7 +454,7 @@ Proof.
  elim (gt_eq_gt_dec p q); intro H0.
   elim H0; auto.
  exfalso.
- apply lt_not_le with q p; auto.
+ apply Nat.lt_nge with q p; auto.
 Qed.
 
 Lemma Cnat_total_order : forall m n : nat, m <> n -> {m < n} + {n < m}.

diff --git a/reals/CReals1.v b/reals/CReals1.v
@@ -248,7 +248,7 @@ Proof.
   intro; apply not_ge; auto.
  intro.
  cut (f n <= f m).
-  apply lt_not_le; auto.
+  apply Nat.lt_nge; auto.
  apply monF; assumption.
 Qed.
 (* end hide *)

diff --git a/reals/stdlib/CMTProductIntegral.v b/reals/stdlib/CMTProductIntegral.v
@@ -666,11 +666,11 @@ Proof.
   destruct b. destruct b0. exact (ndiff eq_refl). contradiction.
   destruct b0. contradiction. exact (ndiff eq_refl).
   rewrite nth_error_None, <- H in des0.
-  exact (lt_not_le _ _ nlen des0).
+  exact (proj1 (Nat.lt_nge _ _) nlen des0).
   rewrite nth_error_None in desl.
-  exact (lt_not_le _ _ nlen desl).
+  exact (proj1 (Nat.lt_nge _ _) nlen desl).
   rewrite nth_error_None, <- H0 in des.
-  exact (lt_not_le _ _ nlen des).
+  exact (proj1 (Nat.lt_nge _ _) nlen des).
 Qed.
 
 Definition ProdIntegrableSimplify
@@ -1122,12 +1122,12 @@ Proof.
       rewrite nth_list_prod in des2. unfold fst in des2.
       rewrite (FreeSubsetsLength
                  (length hn) (nth (nl / length (FreeSubsets (length hn))) (FreeSubsets (length hn)) nil)) in des2.
-      exact (lt_not_le _ _ H0 des2).
+      exact (proj1 (Nat.lt_nge _ _) H0 des2).
       apply nth_In.
       apply Nat.div_lt_upper_bound in H1. exact H1.
       intro abs. rewrite abs in flen. inversion flen. exact H1.
       exfalso. apply nth_error_None in des. rewrite map_length in des.
-      exact (lt_not_le _ _ H0 des).
+      exact (proj1 (Nat.lt_nge _ _) H0 des).
     + assert (Forall (fun h => ~h x) (map prodint_f hn)).
       { apply SubsetIntersectFilterOut. intros.
         destruct (FreeSubsetsFull filter) as [n [H2 H3]].
@@ -1180,11 +1180,11 @@ Proof.
       rewrite nth_list_prod in des2. unfold snd in des2.
       rewrite (FreeSubsetsLength
                  (length hn) (nth (nl mod length (FreeSubsets (length hn))) (FreeSubsets (length hn)) nil)) in des2.
-      exact (lt_not_le _ _ H0 des2).
+      exact (proj1 (Nat.lt_nge _ _) H0 des2).
       apply nth_In. apply Nat.mod_bound_pos. apply Nat.le_0_l.
       exact flen. exact H1.
       exfalso. apply nth_error_None in des. rewrite map_length in des.
-      exact (lt_not_le _ _ H0 des).
+      exact (proj1 (Nat.lt_nge _ _) H0 des).
     + assert (Forall (fun h => ~h y) (map prodint_g hn)).
       { apply SubsetIntersectFilterOut. intros.
         destruct (FreeSubsetsFull filter) as [n [H2 H3]].

diff --git a/reals/stdlib/CMTprofile.v b/reals/stdlib/CMTprofile.v
@@ -985,7 +985,7 @@ Proof.
       apply (CRle_trans _ b). apply BinarySubdivInside.
       apply CRlt_asym, ltab. apply le_S_n, l0. apply CRlt_asym, (snd beta).
       exfalso. pose proof (Nat.lt_le_trans _ _ _ l l0).
-      apply (lt_not_le _ _ H0). apply le_S, Nat.le_refl.
+      apply (proj1 (Nat.lt_nge _ _) H0). apply le_S, Nat.le_refl.
       apply StepApproxIntegralIncr.
       apply CRlt_asym, BinarySubdivIncr. exact (pair aPos ltab).
       apply CRlt_asym, BinarySubdivIncr. exact (pair aPos ltab).
@@ -1626,7 +1626,7 @@ Proof.
                  (CRlt_trans 0 a b aPos ltab, right_ordered ext)
                  (IntExtRightPos ext (CRlt_asym a b ltab), right_ordered ext) ).
       apply CRlt_asym, c1.
-      exfalso; exact (lt_not_le _ _ l0 (Nat.le_refl _)). }
+      exfalso; exact (proj1 (Nat.lt_nge _ _) l0 (Nat.le_refl _)). }
   assert (forall k : nat, sk k <= sk (S k)) as skIncr.
   { unfold sk. intros k. destruct k.
     - destruct (H3 O).
@@ -1714,7 +1714,7 @@ Proof.
       apply (CRlt_trans _ _ _ H4), (CRlt_trans _ _ _ (snd ltxy)).
       apply (CRle_lt_trans _ _ _ H5), (snd ltuv).
       destruct (le_lt_dec (S (2 ^ m)) (S x0)).
-      exfalso. apply le_S_n in l0. exact (lt_not_le _ _ l l0).
+      exfalso. apply le_S_n in l0. exact (proj1 (Nat.lt_nge _ _) l l0).
       assert (v <= BinarySubdiv a b m x0).
       { apply (CRle_trans _ (BinarySubdiv a b m (S x0) +
                              CRpow (CR_of_Q (RealT (ElemFunc IS)) (1 # 2)) m * - (b - a))).
@@ -1806,7 +1806,7 @@ Proof.
         apply CRlt_asym, (snd ltuv).
         destruct (le_lt_dec (S (2 ^ max n m)) (S x0)).
         apply le_S_n in l0.
-        exfalso. exact (lt_not_le _ _ l l0).
+        exfalso. exact (proj1 (Nat.lt_nge _ _) l l0).
         apply CRlt_asym in mcv.
         rewrite <- BinarySubdivNext, CRplus_assoc, CRplus_opp_r, CRplus_0_r in mcv.
         apply StepApproxIntegralIncr.

diff --git a/reals/stdlib/ConstructiveCauchyIntegral.v b/reals/stdlib/ConstructiveCauchyIntegral.v
@@ -1171,7 +1171,7 @@ Proof.
   - apply P.
   - unfold ConcatSequences.
     destruct (lt_dec (S (S (ipt_last P) + ipt_last Q)) (S (ipt_last P))).
-    + exfalso. apply (lt_not_le _ _ l), le_n_S, (Nat.le_trans _ (S (ipt_last P) + 0)).
+    + exfalso. apply (proj1 (Nat.lt_nge _ _) l), le_n_S, (Nat.le_trans _ (S (ipt_last P) + 0)).
       rewrite Nat.add_0_r. apply le_S, Nat.le_refl. apply Nat.add_le_mono_l, Nat.le_0_l.
     + replace (S (S (ipt_last P) + ipt_last Q) - (S (ipt_last P)))%nat
         with (S (ipt_last Q)).
@@ -1226,12 +1226,12 @@ Proof.
     + apply Nat.le_antisymm. apply le_S_n, Nat.nlt_ge, n. exact H.
   - apply CRsum_eq. intros. unfold ConcatSequences.
     destruct (lt_dec (S ipt_last0 + i) (S ipt_last0)).
-    exfalso. apply (lt_not_le _ _ l).
+    exfalso. apply (proj1 (Nat.lt_nge _ _) l).
     apply (Nat.le_trans _ (S ipt_last0 + 0)).
     rewrite Nat.add_0_r. apply Nat.le_refl. apply Nat.add_le_mono_l, Nat.le_0_l.
     clear n.
     destruct (lt_dec (S (S ipt_last0 + i)) (S ipt_last0)).
-    exfalso. apply lt_not_le in l. apply l, le_n_S.
+    exfalso. apply Nat.lt_nge in l. apply l, le_n_S.
     apply (Nat.le_trans _ (S ipt_last0 + 0)).
     rewrite Nat.add_0_r. apply le_S, Nat.le_refl. apply Nat.add_le_mono_l, Nat.le_0_l.
     clear n.
@@ -1280,10 +1280,10 @@ Proof.
       setoid_replace (ConcatSequences xn yn n (S (n + p)) - ConcatSequences xn yn n (n+p))
         with (yn (S p) - yn p).
       apply H0. unfold ConcatSequences.
-      destruct (lt_dec (S (n + p)) n). exfalso. apply (lt_not_le _ _ l).
+      destruct (lt_dec (S (n + p)) n). exfalso. apply (proj1 (Nat.lt_nge _ _) l).
       apply (Nat.le_trans _ (S n + 0)). rewrite Nat.add_0_r. apply le_S, Nat.le_refl.
       simpl. apply le_n_S, Nat.add_le_mono_l, Nat.le_0_l.
-      clear n0. destruct (lt_dec (n + p) n). exfalso. apply (lt_not_le _ _ l).
+      clear n0. destruct (lt_dec (n + p) n). exfalso. apply (proj1 (Nat.lt_nge _ _) l).
       apply (Nat.le_trans _ (n + 0)). rewrite Nat.add_0_r. apply Nat.le_refl.
       apply Nat.add_le_mono_l, Nat.le_0_l. clear n0.
       rewrite (Nat.add_comm n), Nat.add_sub. apply CRplus_morph.
@@ -1384,12 +1384,12 @@ Proof.
       rewrite (Nat.sub_succ_r _ (S ipt_last0)).
       rewrite Nat.succ_pred. reflexivity.
       intro abs. apply Nat.sub_0_le in abs.
-      exact (lt_not_le _ _ H4 abs).
+      exact (proj1 (Nat.lt_nge _ _) H4 abs).
       rewrite (Nat.sub_succ_r _ (S ipt_last0)).
       rewrite Nat.succ_pred.
       rewrite Nat.le_sub_le_add_l, Nat.add_succ_r. exact H3.
       intro abs. apply Nat.sub_0_le in abs.
-      exact (lt_not_le _ _ H4 abs).
+      exact (proj1 (Nat.lt_nge _ _) H4 abs).
 Qed.
 
 Lemma FunLocSorted : forall (xn : list Q),

diff --git a/reals/stdlib/ConstructiveDiagonal.v b/reals/stdlib/ConstructiveDiagonal.v
@@ -57,12 +57,12 @@ Proof.
   intros. generalize dependent n. induction k.
   - simpl. split.
     + intro. destruct (Nat.eq_dec (proj1_sig un O) n).
-      assumption. exfalso. apply (lt_not_le n (S n)).
+      assumption. exfalso. apply (Nat.lt_nge n (S n)).
       apply Nat.le_refl. assumption.
     + intro. destruct (Nat.eq_dec (proj1_sig un O) n). apply Nat.le_0_l.
       exfalso. pose proof (SubSeqAboveId un n).
       destruct un. simpl in H. simpl in n0. simpl in H0.
-      apply (lt_not_le (x n) (x (S n))). apply l. apply Nat.le_refl.
+      apply (Nat.lt_nge (x n) (x (S n))). apply l. apply Nat.le_refl.
       rewrite H. assumption.
   - split.
     + intro. simpl. simpl in H.
@@ -87,7 +87,7 @@ Proof.
     + intros. intro absurd. simpl in H.
       destruct (Nat.eq_dec (proj1_sig un (S k)) n).
       inversion H. subst k. pose proof (SubSeqAboveId un (S n)).
-      rewrite e in H1. apply (lt_not_le n (S n)). apply Nat.le_refl.
+      rewrite e in H1. apply (Nat.lt_nge n (S n)). apply Nat.le_refl.
       assumption. apply Nat.le_succ_r in H0. destruct H0.
       specialize (IHk n) as [IHk _].
       specialize (IHk H p H0). contradiction. subst p. contradiction.
@@ -104,7 +104,7 @@ Proof.
   - simpl. destruct (Nat.eq_dec (proj1_sig un O) (proj1_sig un O)). reflexivity.
     exfalso. exact (n (eq_refl _)).
   - simpl. destruct (Nat.eq_dec (proj1_sig un (S n)) (proj1_sig un O)).
-    exfalso. destruct un. simpl in e. apply (lt_not_le (x O) (x (S n))).
+    exfalso. destruct un. simpl in e. apply (Nat.lt_nge (x O) (x (S n))).
     apply l. apply le_n_S. apply Nat.le_0_l. rewrite e. apply Nat.le_refl.
     apply IHn.
 Qed.
@@ -139,7 +139,7 @@ Proof.
     destruct (Nat.eq_dec (SubSeqInv sub k k) (S k)). reflexivity.
     exfalso. apply n. clear n. apply SubSeqInvNotFound. intros.
     intro absurd. destruct p. rewrite absurd in H. exact (Nat.lt_irrefl k H).
-    destruct sub. simpl in absurd, H. apply (lt_not_le (x O) (x (S p))).
+    destruct sub. simpl in absurd, H. apply (Nat.lt_nge (x O) (x (S p))).
     apply l. apply le_n_S. apply Nat.le_0_l. rewrite absurd. apply le_S in H.
     apply le_S_n in H. apply H.
   - unfold FillSubSeqWithZeros.
@@ -172,10 +172,10 @@ Proof.
     destruct (Nat.lt_trichotomy p (S n)).
     apply Nat.le_succ_r in H2. destruct H2.
     specialize (inc p n H2). rewrite absurd in inc.
-    apply (lt_not_le (S (sub n + k)) (sub n)). assumption.
+    apply (Nat.lt_nge (S (sub n + k)) (sub n)). assumption.
     apply le_S. rewrite <- (Nat.add_0_r (sub n)). rewrite <- Nat.add_assoc.
     apply Nat.add_le_mono_l. apply Nat.le_0_l. inversion H2. subst p.
-    apply (lt_not_le (sub n) (S (sub n + k))). apply le_n_S.
+    apply (Nat.lt_nge (sub n) (S (sub n + k))). apply le_n_S.
     rewrite <- (Nat.add_0_r (sub n)). rewrite <- Nat.add_assoc.
     apply Nat.add_le_mono_l. apply Nat.le_0_l. rewrite <- absurd. apply Nat.le_refl.
     destruct H2. subst p. exact (Nat.lt_irrefl (sub (S n)) H1).