Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Deprecate le_not_lt for Nat.le_ngt #190

Merged
merged 3 commits into from
May 20, 2023
Merged

Deprecate le_not_lt for Nat.le_ngt #190

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
414d996
'Deprecate le_not_lt for Nat.le_ngt'
anandadalton May 20, 2023
e9affa7
'Deprecate lt_n_S for Nat.succ_lt_mono'
anandadalton May 20, 2023
79d5b5f
'Deprecate lt_not_le for Nat.lt_nge'
anandadalton May 20, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 6 additions & 6 deletions algebra/Bernstein.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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.
Expand All @@ -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).
Expand Down Expand Up @@ -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.
Expand All @@ -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.

Expand Down
4 changes: 2 additions & 2 deletions algebra/COrdCauchy.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
4 changes: 2 additions & 2 deletions algebra/COrdFields2.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down
6 changes: 3 additions & 3 deletions algebra/CPoly_Degree.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down Expand Up @@ -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.
Expand Down
8 changes: 4 additions & 4 deletions algebra/CSums.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand All @@ -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)] *)
Expand Down Expand Up @@ -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.

Expand Down
8 changes: 4 additions & 4 deletions algebra/Cauchy_COF.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down
6 changes: 3 additions & 3 deletions ftc/COrdLemmas.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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.
Expand All @@ -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.
4 changes: 2 additions & 2 deletions ftc/FunctSums.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -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),
Expand Down
24 changes: 12 additions & 12 deletions ftc/Integral.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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.

Expand All @@ -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.
Expand All @@ -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).
Expand Down Expand Up @@ -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.
Expand All @@ -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.
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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 ].
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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.
Expand Down
2 changes: 1 addition & 1 deletion ftc/Partitions.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
20 changes: 10 additions & 10 deletions ftc/RefLemma.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 _ _)).
Expand Down Expand Up @@ -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.
Expand Down
Loading