Merge pull request #190 from anandadalton/easy_fixes

Deprecate le_not_lt for Nat.le_ngt
coq-community · May 20, 2023 · ad827d3 · ad827d3
2 parents afa55ac + 79d5b5f
commit ad827d3
Show file tree

Hide file tree

Showing 28 changed files with 142 additions and 141 deletions.
diff --git a/algebra/Bernstein.v b/algebra/Bernstein.v
@@ -59,12 +59,12 @@ end.
 
 (** These lemmas provide an induction principle for polynomials using the Bernstien basis *)
 Lemma Bernstein_inv1 : forall n i (H:i < n) (H0:S i <= S n),
- Bernstein H0[=]([1][-]_X_)[*](Bernstein (proj1 (Nat.lt_succ_r _ _) (lt_n_S _ _ H)))[+]_X_[*](Bernstein (le_S_n _ _ H0)).
+ Bernstein H0[=]([1][-]_X_)[*](Bernstein (proj1 (Nat.lt_succ_r _ _) (proj1 (Nat.succ_lt_mono _ _) H)))[+]_X_[*](Bernstein (le_S_n _ _ H0)).
 Proof.
  intros n i H H0.
  simpl (Bernstein H0).
  destruct (le_lt_eq_dec _ _ H0).
-  replace (proj1 (Nat.lt_succ_r (S i) n) l) with (proj1 (Nat.lt_succ_r _ _) (lt_n_S _ _ H)) by apply le_irrelevent.
+  replace (proj1 (Nat.lt_succ_r (S i) n) l) with (proj1 (Nat.lt_succ_r _ _) (proj1 (Nat.succ_lt_mono _ _) H)) by apply le_irrelevent.
   reflexivity.
  exfalso; lia.
 Qed.
@@ -176,7 +176,7 @@ Proof.
   rstepr (Bernstein (le_n_S 0 (S n) H)).
   set (le_n_S 0 n (Nat.le_0_l n)).
   rewrite (Bernstein_inv1 l).
-  rewrite (le_irrelevent _ _ (proj1 (Nat.lt_succ_r 1 (S n)) (lt_n_S 0 (S n) l)) l).
+  rewrite (le_irrelevent _ _ (proj1 (Nat.lt_succ_r 1 (S n)) (proj1 (Nat.succ_lt_mono 0 (S n)) l)) l).
   rewrite (le_irrelevent _ _ H (le_S_n 0 (S n) (le_n_S 0 (S n) H))).
   reflexivity.
  simpl (Bernstein H) at 1.
@@ -189,7 +189,7 @@ Proof.
   replace (le_n_S i n (le_S_n i n H)) with H by apply le_irrelevent.
   rstepl ((nring (S i)[+][1])[*](([1][-]_X_)[*]Bernstein l0[+]_X_[*]Bernstein H)).
   rewrite (Bernstein_inv1 l).
-  replace (proj1 (Nat.lt_succ_r (S (S i)) (S n)) (lt_n_S (S i) (S n) l)) with l0 by apply le_irrelevent.
+  replace (proj1 (Nat.lt_succ_r (S (S i)) (S n)) (proj1 (Nat.succ_lt_mono (S i) (S n)) l)) with l0 by apply le_irrelevent.
   replace (le_S_n (S i) (S n) (le_n_S (S i) (S n) H)) with H by apply le_irrelevent.
   reflexivity.
  rstepl (_X_[*](nring (S n)[*]_X_[*]Bernstein (proj1 (Nat.lt_succ_r _ _) H))[+] _X_[*]Bernstein H).
@@ -240,7 +240,7 @@ Proof.
   rstepl ((nring (n - i)[+][1])[*](X0[*]Bernstein H[+]_X_[*]Bernstein l0)).
   rewrite -> (Bernstein_inv1 H).
   fold X0.
-  replace (proj1 (Nat.lt_succ_r _ _) (lt_n_S _ _ H)) with H by apply le_irrelevent.
+  replace (proj1 (Nat.lt_succ_r _ _) (proj1 (Nat.succ_lt_mono _ _) H)) with H by apply le_irrelevent.
   replace (le_S_n _ _ (le_S (S i) (S n) H)) with l0 by apply le_irrelevent.
   reflexivity.
  revert H.
@@ -256,7 +256,7 @@ Proof.
  replace (S (S n) - S n) with 1 by auto with *.
  replace (le_S_n n (S n) (le_S (S n) (S n) H))
    with (le_S n n (proj1 (Nat.lt_succ_r n n) H)) by apply le_irrelevent.
- replace (proj1 (Nat.lt_succ_r (S n) (S n)) (lt_n_S n (S n) l)) with H by apply le_irrelevent.
+ replace (proj1 (Nat.lt_succ_r (S n) (S n)) (proj1 (Nat.succ_lt_mono n (S n)) l)) with H by apply le_irrelevent.
  ring.
 Qed.
 

diff --git a/algebra/COrdCauchy.v b/algebra/COrdCauchy.v
@@ -266,9 +266,9 @@ Proof.
   apply less_leEq_trans with e; eauto with arith.
  unfold CS_seq_recip_seq in |- *.
  elim lt_le_dec; intro; simpl in |- *.
-  exfalso; apply le_not_lt with N n; eauto with arith.
+  exfalso; apply Nat.le_ngt with N n; eauto with arith.
  elim lt_le_dec; intro; simpl in |- *.
-  exfalso; apply le_not_lt with N (Nat.max K N); eauto with arith.
+  exfalso; apply Nat.le_ngt with N (Nat.max K N); eauto with arith.
  rstepr (f (Nat.max K N)[-]f n).
  apply AbsSmall_leEq_trans with (d[*]e[*]e).
   apply mult_resp_leEq_both.

diff --git a/algebra/COrdFields2.v b/algebra/COrdFields2.v
@@ -797,9 +797,9 @@ Proof.
   assumption.
  intros.
  elim (le_lt_dec m i); intro;
-   [ simpl in |- * | exfalso; apply (le_not_lt m i); auto with arith ].
+   [ simpl in |- * | exfalso; apply (Nat.le_ngt m i); auto with arith ].
  elim (le_lt_dec i n); intro;
-   [ simpl in |- * | exfalso; apply (le_not_lt i n); auto with arith ].
+   [ simpl in |- * | exfalso; apply (Nat.le_ngt i n); auto with arith ].
  apply H0.
 Qed.
 

diff --git a/algebra/CPoly_Degree.v b/algebra/CPoly_Degree.v
@@ -457,13 +457,13 @@ Proof.
    simpl in |- *. auto with arith.
   induction  p as [| s p Hrecp]; intros.
   simpl in H. elim (ap_irreflexive_unfolded _ _ H).
-  simpl in |- *. simpl in H. apply lt_n_S. auto.
+  simpl in |- *. simpl in H. apply -> Nat.succ_lt_mono. auto.
 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.
 
@@ -495,7 +495,7 @@ Proof.
   cut (i <> i0). intro.
   Step_final (nth_coeff i0 p[*][0]).
  intro; rewrite <- H2 in H1.
- apply (le_not_lt i n); auto.
+ apply (Nat.le_ngt i n); auto.
 Qed.
 
 Hint Resolve poly_as_sum'': algebra.

diff --git a/algebra/CSums.v b/algebra/CSums.v
@@ -87,7 +87,7 @@ Proof.
  intros n f Hf i Hi.
  unfold part_tot_nat_fun in |- *.
  elim le_lt_dec; intro.
-  exfalso; apply (le_not_lt n i); auto.
+  exfalso; apply (Nat.le_ngt n i); auto.
  simpl in |- *; apply Hf; auto.
 Qed.
 
@@ -98,7 +98,7 @@ Proof.
  unfold part_tot_nat_fun in |- *.
  elim le_lt_dec; intro.
   simpl in |- *; algebra.
- exfalso; apply (le_not_lt n i); auto.
+ exfalso; apply (Nat.le_ngt n i); auto.
 Qed.
 
 (** [Sum0] defines the sum for [i=0..(n-1)] *)
@@ -365,8 +365,8 @@ Proof.
  apply Sum_wd'.
   assumption.
  intros i H1 H2.
- elim le_lt_dec; intro H3; [ simpl in |- * | exfalso; apply (le_not_lt i n); auto ].
- elim le_lt_dec; intro H4; [ simpl in |- * | exfalso; apply (le_not_lt m i); auto ].
+ elim le_lt_dec; intro H3; [ simpl in |- * | exfalso; apply (Nat.le_ngt i n); auto ].
+ elim le_lt_dec; intro H4; [ simpl in |- * | exfalso; apply (Nat.le_ngt m i); auto ].
  algebra.
 Qed.
 

diff --git a/algebra/Cauchy_COF.v b/algebra/Cauchy_COF.v
@@ -592,31 +592,31 @@ Proof.
     eapply leEq_wdr.
      apply (HM (Nat.max K N)); auto with arith.
     unfold CS_seq_recip_seq in |- *; elim lt_le_dec; intro.
-     exfalso; apply le_not_lt with N (Nat.max K N); auto with arith.
+     exfalso; apply Nat.le_ngt with N (Nat.max K N); auto with arith.
     simpl in |- *; rational.
    apply (less_irreflexive_unfolded _ d).
    apply leEq_less_trans with ([0]:F); auto.
    simpl in HM.
    eapply leEq_wdr.
     apply (HM (Nat.max K N)); auto with arith.
    unfold CS_seq_recip_seq in |- *; elim lt_le_dec; intro.
-    exfalso; apply le_not_lt with N (Nat.max K N); auto with arith.
+    exfalso; apply Nat.le_ngt with N (Nat.max K N); auto with arith.
    simpl in |- *; rational.
   apply (less_irreflexive_unfolded _ d).
   apply leEq_less_trans with ([0]:F); auto.
   simpl in HM.
   eapply leEq_wdr.
    apply (HM (Nat.max K N)); auto with arith.
   unfold CS_seq_recip_seq in |- *; elim lt_le_dec; intro.
-   exfalso; apply le_not_lt with N (Nat.max K N); auto with arith.
+   exfalso; apply Nat.le_ngt with N (Nat.max K N); auto with arith.
   simpl in |- *; rational.
  apply (less_irreflexive_unfolded _ d).
  apply leEq_less_trans with ([0]:F); auto.
  simpl in HM.
  eapply leEq_wdr.
   apply (HM (Nat.max K N)); auto with arith.
  unfold CS_seq_recip_seq in |- *; elim lt_le_dec; intro.
-  exfalso; apply le_not_lt with N (Nat.max K N); auto with arith.
+  exfalso; apply Nat.le_ngt with N (Nat.max K N); auto with arith.
  simpl in |- *; rational.
 Qed.
 

diff --git a/ftc/COrdLemmas.v b/ftc/COrdLemmas.v
@@ -347,7 +347,7 @@ Proof.
       exfalso; lia.
      elim (le_lt_dec (f (S n)) i); intro; simpl in |- *.
       cut (f n < f (S n)); [ intro | apply f_mon; apply Nat.lt_succ_diag_r ].
-      exfalso; apply (le_not_lt (f n) i); auto.
+      exfalso; apply (Nat.le_ngt (f n) i); auto.
       apply Nat.le_trans with (f (S n)); auto with arith.
      intros; unfold part_tot_nat_fun in |- *;
        elim (le_lt_dec (f (S n)) i);elim (le_lt_dec (f n) i);simpl;intros; try reflexivity;try exfalso; try lia.
@@ -443,7 +443,7 @@ Proof.
        intro.
        rewrite <- H6.
        rewrite <- plus_n_Sm; auto with arith.
-      exfalso; apply (le_not_lt i m); auto with arith.
+      exfalso; apply (Nat.le_ngt i m); auto with arith.
      set (x := f m (le_n m)) in *; clearbody x; auto with arith.
     assumption.
    intros.
@@ -458,7 +458,7 @@ Proof.
  unfold f' in |- *.
  elim (le_lt_dec i m); intro; simpl in |- *.
   apply H0; auto.
- elim (le_not_lt i m); auto.
+ lia; auto.
 Qed.
 
 End More_Lemmas.
diff --git a/ftc/FunctSums.v b/ftc/FunctSums.v
@@ -390,7 +390,7 @@ Proof.
  do 6 intro.
  unfold FSumx_to_FSum in |- *.
  elim (le_lt_dec n i); intro; simpl in |- *.
-  exfalso; apply (le_not_lt n i); auto.
+  exfalso; apply (Nat.le_ngt n i); auto.
  intros; apply H; auto.
  algebra.
 Qed.
@@ -402,7 +402,7 @@ Proof.
  unfold FSumx_to_FSum in |- *.
  elim (le_lt_dec n i); intro; simpl in |- *.
   intro; algebra.
- intros; exfalso; apply (le_not_lt n i); auto.
+ intros; exfalso; apply (Nat.le_ngt n i); auto.
 Qed.
 
 Lemma FSum_FSumx_to_FSum : forall n (f : forall i, i < S n -> PartIR),

diff --git a/ftc/Integral.v b/ftc/Integral.v
@@ -750,7 +750,7 @@ Proof.
  intros; unfold partition_join_fun in |- *.
  elim le_lt_dec; intro; simpl in |- *.
   apply prf1; auto.
- exfalso; apply le_not_lt with i n; auto.
+ exfalso; apply Nat.le_ngt with i n; auto.
 Qed.
 
 Lemma pjf_2 : forall (i : nat) Hi, i = n -> partition_join_fun i Hi [=] c.
@@ -781,7 +781,7 @@ Proof.
  intros; unfold partition_join_fun in |- *.
  generalize Hj; rewrite H0; clear Hj; intros.
  elim le_lt_dec; intro; simpl in |- *.
-  exfalso; apply le_not_lt with i n; auto.
+  exfalso; apply Nat.le_ngt with i n; auto.
  apply prf1; auto.
 Qed.
 
@@ -792,10 +792,10 @@ Proof.
  unfold partition_join_fun in |- *.
  elim (le_lt_dec i n); elim (le_lt_dec j n); intros; simpl in |- *.
     apply prf1; auto.
-   exfalso; apply le_not_lt with i n.
+   exfalso; apply Nat.le_ngt with i n.
     assumption.
    rewrite H; assumption.
-  exfalso; apply le_not_lt with j n.
+  exfalso; apply Nat.le_ngt with j n.
    assumption.
   rewrite <- H; assumption.
  apply prf1; auto.
@@ -818,7 +818,7 @@ Proof.
    apply eq_transitive_unfolded with (Q 0 (Nat.le_0_l _)).
     apply eq_symmetric_unfolded; apply start.
    apply prf1; auto with arith.
-  exfalso; apply le_not_lt with n i; auto with arith.
+  exfalso; apply Nat.le_ngt with n i; auto with arith.
  cut (i - n = S (i - S n)); [ intro | lia ].
  cut (S (i - S n) <= m); [ intro | lia ].
  apply leEq_wdr with (Q _ H1).
@@ -896,7 +896,7 @@ Proof.
   elim le_lt_eq_dec; intro; simpl in |- *.
    algebra.
   exfalso; rewrite b0 in Hi'; apply (Nat.lt_irrefl _ Hi').
- exfalso; apply le_not_lt with i n; auto with arith.
+ exfalso; apply Nat.le_ngt with i n; auto with arith.
 Qed.
 
 Lemma pjp_2 : forall (i : nat) Hi, i = n -> partition_join_pts i Hi [=] c.
@@ -914,7 +914,7 @@ Lemma pjp_3 : forall (i : nat) Hi Hi',
 Proof.
  intros; unfold partition_join_pts in |- *.
  elim le_lt_dec; intro; simpl in |- *.
-  exfalso; apply le_not_lt with i n; auto.
+  exfalso; apply Nat.le_ngt with i n; auto.
  cut (fQ _ (partition_join_aux' _ _ _ b0 Hi) [=] fQ _ Hi').
   2: apply HfQ'; auto.
  algebra.
@@ -952,7 +952,7 @@ Proof.
    cut (forall H, Q (n - n) H [=] c); auto.
    cut (n - n = 0); [ intro | auto with arith ].
    rewrite H1; intros; apply start.
-  exfalso; apply le_not_lt with n i; auto with arith.
+  exfalso; apply Nat.le_ngt with n i; auto with arith.
  elim (HfQ _ (partition_join_aux' _ _ _ b1 H)); intros.
  apply compact_wd with (fQ _ (partition_join_aux' _ _ _ b1 H)).
   2: apply eq_symmetric_unfolded; apply pjp_3; assumption.
@@ -1011,9 +1011,9 @@ Proof.
     apply pfwdef; apply eq_symmetric_unfolded; apply pjp_1.
    apply cg_minus_wd; simpl in |- *.
     unfold partition_join_fun in |- *; elim le_lt_dec; simpl in |- *; intro; [ apply prf1; auto
-      | exfalso; apply le_not_lt with n i; auto with arith ].
+      | exfalso; apply Nat.le_ngt with n i; auto with arith ].
    unfold partition_join_fun in |- *; elim le_lt_dec; simpl in |- *; intro; [ apply prf1; auto
-     | exfalso; apply le_not_lt with i n; auto with arith ].
+     | exfalso; apply Nat.le_ngt with i n; auto with arith ].
   intros; apply mult_wd.
    apply pfwdef.
    cut (i = S (n + i) - S n); [ intro | lia ].
@@ -1071,7 +1071,7 @@ Proof.
    eapply leEq_transitive.
     apply Mesh_lemma.
    apply lft_leEq_Max.
-  exfalso; apply le_not_lt with i n; auto with arith.
+  exfalso; apply Nat.le_ngt with i n; auto with arith.
  elim le_lt_dec; intro; simpl in |- *.
   cut (i = n); [ intro | apply Nat.le_antisymm; auto with arith ].
   generalize a0 b0 Hi'; clear Hx Hi Hi' a0 b0.
@@ -1182,7 +1182,7 @@ Proof.
         elim le_lt_eq_dec; intro; simpl in |- *.
          apply Partition_imp_points_2; auto.
         exfalso; rewrite b0 in Hi; apply (Nat.lt_irrefl _ Hi).
-       exfalso; apply le_not_lt with i0 (S i); auto with arith.
+       exfalso; apply Nat.le_ngt with i0 (S i); auto with arith.
       apply cg_minus_wd; simpl in |- *.
        apply eq_symmetric_unfolded; apply pjf_1.
       apply eq_symmetric_unfolded; apply pjf_1.

diff --git a/ftc/Partitions.v b/ftc/Partitions.v
@@ -243,7 +243,7 @@ Proof.
    cut (f j < f n); [ intro | apply Nat.le_lt_trans with i; auto ].
    apply not_ge.
    intro; red in H1.
-   apply (le_not_lt (f j) (f n)); auto with arith.
+   apply (Nat.le_ngt (f j) (f n)); auto with arith.
    apply Hfmon.
    elim (le_lt_eq_dec _ _ H1); intro; auto.
    rewrite b0 in H0; elim (Nat.lt_irrefl (f j)); auto.

diff --git a/ftc/RefLemma.v b/ftc/RefLemma.v
@@ -264,23 +264,23 @@ Proof.
      elim (le_lt_dec (S j) m); intro; simpl in |- *.
       apply prf1; auto.
      cut (S j <= m); [ intro | apply H' with i; assumption ].
-     exfalso; apply (le_not_lt _ _ H2 b0).
+     exfalso; apply (proj1 (Nat.le_ngt _ _) H2 b0).
     elim (le_lt_dec j m); intro; simpl in |- *.
      apply prf1; auto.
     cut (j < m); [ intro | apply H with i; assumption ].
-    exfalso; apply le_not_lt with m j; auto with arith.
-   exfalso; apply le_not_lt with (sub i) j; auto with arith.
-  exfalso; apply (le_not_lt _ _ Hj' b0).
+    exfalso; apply Nat.le_ngt with m j; auto with arith.
+   exfalso; apply Nat.le_ngt with (sub i) j; auto with arith.
+  exfalso; apply (proj1 (Nat.le_ngt _ _) Hj' b0).
  unfold h in |- *.
  apply cg_minus_wd.
   elim (le_lt_dec (S (pred (sub (S i)))) m); intro; simpl in |- *.
    apply prf1; auto.
   exfalso.
-  apply (le_not_lt _ _ P1 b0).
+  apply (proj1 (Nat.le_ngt _ _) P1 b0).
  elim (le_lt_dec (sub i) m); intro; simpl in |- *.
   apply prf1; auto.
  exfalso.
- apply (le_not_lt _ _ P2 b0).
+ apply (proj1 (Nat.le_ngt _ _) P2 b0).
 Qed.
 
 Notation just1 := (incF _ (Pts_part_lemma _ _ _ _ _ _ HfP _ _)).
@@ -329,21 +329,21 @@ Proof.
       exfalso.
       cut (0 < sub (S i)); [ intro | apply RL_sub_S ].
       cut (sub (S i) <= m); intros.
-       apply (le_not_lt _ _ H4); apply Nat.le_lt_trans with j; auto.
+       apply (proj1 (Nat.le_ngt _ _) H4); apply Nat.le_lt_trans with j; auto.
       rewrite <- RL_sub_n.
       apply RL_sub_mon'; apply Hi.
      apply mult_wd.
       apply pfwdef.
       apply HfQ'; auto.
      apply cg_minus_wd; apply prf1; auto.
-    exfalso; apply (le_not_lt _ _ b0).
+    exfalso; apply (proj1 (Nat.le_ngt _ _) b0).
     rewrite (Nat.lt_succ_pred _ _ (RL_sub_S i)); auto.
-   exfalso; apply (le_not_lt _ _ H1 b0).
+   exfalso; apply (proj1 (Nat.le_ngt _ _) H1 b0).
   symmetry  in |- *; apply RL_sub_n.
  apply Sumx_wd; intros.
  unfold part_tot_nat_fun in |- *.
  elim (le_lt_dec m i); intro; simpl in |- *.
-  exfalso; apply le_not_lt with m i; auto.
+  exfalso; apply Nat.le_ngt with m i; auto.
  apply mult_wd.
   apply pfwdef; apply HfQ'; auto.
  apply cg_minus_wd; apply prf1; auto.