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

Deprecated notations #194

Merged
merged 12 commits into from
May 24, 2023
Merged

Deprecated notations #194

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
12 commits
Select commit Hold shift + click to select a range
7763ce1
'Deprecate le_plus_minus for Nat.sub_add'
anandadalton May 22, 2023
024db94
'Deprecate neq_O_lt for Nat.neq_0_lt_0'
anandadalton May 22, 2023
5b31252
'Deprecate le_n_O_eq for Nat.le_0_r'
anandadalton May 22, 2023
6521bf9
'Deprecate le_Sn_le for Nat.lt_le_incl'
anandadalton May 23, 2023
aa3859d
'Deprecate Zdiv_eucl_POS for Coq.ZArith.BinIntDef.Z.pos_div_eucl'
anandadalton May 23, 2023
7a5dc70
'Deprecate lt_S_n for Nat.succ_lt_mono'
anandadalton May 23, 2023
f41ab4f
'Deprecate minus_n_n for Nat.sub_diag'
anandadalton May 23, 2023
5735f42
'Deprecate le_lt_n_Sm for Nat.lt_succ_r'
anandadalton May 23, 2023
7e39c78
'Deprecate Nat.mod_add for Nat.Div0.mod_add'
anandadalton May 23, 2023
e28ce44
'Deprecate lt_O_neq for Nat.neq_0_lt_0'
anandadalton May 24, 2023
e275fc7
'Deprecate lt_le_S for Nat.le_succ_l'
anandadalton May 24, 2023
2a7c386
Merge branch 'coq-community:master' into easy_fixes
anandadalton May 24, 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
6 changes: 3 additions & 3 deletions algebra/Bernstein.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.

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

Expand Down
4 changes: 2 additions & 2 deletions algebra/CPoly_ApZero.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
2 changes: 1 addition & 1 deletion fta/KeyLemma.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)).
Expand Down
2 changes: 1 addition & 1 deletion ftc/FunctSeries.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
12 changes: 6 additions & 6 deletions ftc/Partitions.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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.

(**
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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 _)).
Expand All @@ -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).
Expand Down
12 changes: 6 additions & 6 deletions ftc/RefSepRef.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.

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

Expand All @@ -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 |- *.
Expand All @@ -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.
Expand Down
9 changes: 5 additions & 4 deletions ftc/RefSeparating.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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).
Expand All @@ -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.
Expand Down Expand Up @@ -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 :
Expand Down
2 changes: 1 addition & 1 deletion liouville/CPoly_Euclid.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
3 changes: 2 additions & 1 deletion liouville/QX_root_loc.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
3 changes: 2 additions & 1 deletion metric2/Compact.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
3 changes: 2 additions & 1 deletion model/Zmod/ZBasics.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
16 changes: 8 additions & 8 deletions model/Zmod/ZDivides.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -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.

Expand All @@ -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.
Expand All @@ -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.
Expand All @@ -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.
Expand Down
5 changes: 3 additions & 2 deletions model/structures/Npossec.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -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.
Expand Down
2 changes: 1 addition & 1 deletion ode/AbstractIntegration.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
Loading