Skip to content

Commit

Permalink
fix more deprecations
Browse files Browse the repository at this point in the history
  • Loading branch information
@palmskog
palmskog committed Dec 2, 2023
1 parent 0b060c1 commit 949436d
Show file tree
Hide file tree
Showing 21 changed files with 301 additions and 277 deletions.
47 changes: 27 additions & 20 deletions Arith/Nbinomial.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -58,13 +58,13 @@ induction n.
intros.
compute.
destruct m.
apply lt_irrefl in H.
apply Nat.lt_irrefl in H.
contradiction.
reflexivity.
intros.
unfold Nsimple_binomial. fold Nsimple_binomial.
destruct m.
apply lt_n_O in H.
apply Nat.nlt_0_r in H.
contradiction.
assert (n<m).
auto with arith.
Expand Down Expand Up @@ -200,10 +200,10 @@ Proof.
induction n.
intros.
destruct k.
apply le_Sn_O in H.
apply Nat.nle_succ_0 in H.
contradiction.
rewrite Nbinomial_outside.
rewrite mult_0_r.
rewrite Nat.mul_0_r.
assert (Nfinite_prod_0_n (pred (S k)) (fun x : nat => 0 - x) =
Nfinite_prod_0_n (pred (S k)) (fun x : nat => 0)).
apply Nfinite_prod_eq_compat.
Expand All @@ -222,11 +222,11 @@ exact H0.
apply (Nat.le_trans k) in H0.

destruct k.
apply le_Sn_O in H.
apply Nat.nle_succ_0 in H.
contradiction.

rewrite <- Nbinomial_pascal.
rewrite mult_plus_distr_l.
rewrite Nat.mul_add_distr_l.
apply le_le_S_eq in H.
destruct H.
apply le_le_S_eq in H0.
Expand All @@ -238,15 +238,15 @@ rewrite <- Nat.mul_assoc.
rewrite IHn.
assert (exists k', k=S k').
destruct k.
apply le_Sn_n in H. contradiction.
apply Nat.nle_succ_diag_l in H. contradiction.
exists k. reflexivity.
destruct H1.
rewrite H1.

assert (pred (S(S x))=S(pred (S x))).
rewrite pred_of_minus.
rewrite <- minus_Sn_m.
rewrite pred_of_minus.
rewrite <- Nat.sub_1_r.
rewrite Nat.sub_succ_l.
rewrite <- Nat.sub_1_r.
reflexivity.
auto with arith.
rewrite H2.
Expand All @@ -263,14 +263,14 @@ assert (Nfinite_prod_0_n (pred (S x)) (fun x0 : nat => n - x0) * (n - S (pred (S
auto with arith.
rewrite H3. clear H3.
rewrite <- Nat.mul_add_distr_r.
rewrite <- minus_n_O.
rewrite Nat.sub_0_r.
assert (S (S x) + (n - S (pred (S x))) = S n).
rewrite <- pred_Sn.
assert (n-S x=S n-S(S x)).
auto with arith.
rewrite H3.
symmetry.
apply le_plus_minus.
rewrite Nat.add_comm.
apply Nat.sub_add.
rewrite <- H1.
auto with arith.
auto with arith.
Expand All @@ -285,7 +285,7 @@ auto with arith.
rewrite H1.
rewrite Nbinomial_diag.
rewrite Nbinomial_outside.
rewrite mult_0_r.
rewrite Nat.mul_0_r.
rewrite Nat.add_0_r.
rewrite Nat.mul_1_r.
rewrite Nfinite_prod_index_reversal.
Expand All @@ -302,17 +302,23 @@ rewrite Nat.add_comm in H3.
rewrite H3.
rewrite Nat.add_comm.
assert (x-0=k0+x-(k0+0)).
apply minus_plus_simpl_l_reverse.
rewrite <- minus_n_O in H4.
rewrite Nat.sub_0_r, Nat.add_0_r.
rewrite Nat.add_comm.
symmetry.
rewrite Nat.add_sub; reflexivity.
rewrite Nat.sub_0_r in H4.
rewrite Nat.add_0_r in H4.
rewrite <- H4.
assert (S(k0+x)=S k0+x).
auto with arith.
rewrite H5. clear H4. clear H5.
assert (S k0-0=x+S k0-(x+0)).
apply minus_plus_simpl_l_reverse.
rewrite Nat.sub_0_r, Nat.add_0_r.
rewrite Nat.add_comm.
symmetry.
rewrite Nat.add_sub; reflexivity.
rewrite Nat.add_0_r in H4.
rewrite <- minus_n_O in H4.
rewrite Nat.sub_0_r in H4.
rewrite Nat.add_comm in H4.
exact H4.
auto with arith.
Expand Down Expand Up @@ -357,7 +363,8 @@ rewrite Nfinite_prod_index_reversal.
rewrite Nat.mul_1_r.
apply Nfinite_prod_subtle_eq_compat.
intros.
apply minus_Sn_m.
symmetry.
apply Nat.sub_succ_l.
exact H1.
Qed.

Expand All @@ -372,7 +379,7 @@ destruct H.
destruct k.
inversion H.
simpl. auto with arith.
rewrite <- minus_n_O. apply Ndiv_n_n.
rewrite Nat.sub_0_r. apply Ndiv_n_n.
destruct H.
destruct k.
inversion H.
Expand Down
88 changes: 45 additions & 43 deletions Arith/Ndiv.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1209,34 +1209,35 @@ destruct (le_dec n p).
apply (Nat.add_le_mono_l (p-n) q n) in H3.
rewrite Nat.add_comm in H3.
rewrite Nat.sub_add in H3.
apply (minus_le_compat_r p (n+q) q) in H3.
rewrite Nat.add_comm in H3.
rewrite minus_plus in H3.
apply (Nat.sub_le_mono_r p (n+q) q) in H3.
rewrite Nat.add_sub in H3.
auto.
auto.
apply Nat.le_trans with p.
apply le_minus.
apply Nat.le_sub_l.
auto.
auto.

destruct H1.
rewrite <- minus_Sn_m.
rewrite <- minus_n_n.
simpl. rewrite <- minus_n_O.
rewrite Nat.sub_succ_l.
rewrite Nat.sub_diag.
simpl. rewrite Nat.sub_0_r.
apply Ndiv_algo_correct in H4.
rewrite H4. auto. auto. auto.

rewrite <- minus_Sn_m.
rewrite Nat.sub_succ_l.
simpl.
apply Ndiv_algo_correct in H4.
assert(q<=m).
auto with arith.
apply Nle_plus in H5.
destruct H5.
rewrite H5.
rewrite minus_plus.
rewrite Nat.add_comm at 2.
rewrite Nat.add_sub.
rewrite Nat.add_comm.
rewrite minus_plus.
rewrite Nat.add_comm at 1.
rewrite Nat.add_sub.
rewrite H5 in H4.
rewrite Nat.add_comm.
rewrite H4.
Expand All @@ -1255,9 +1256,9 @@ auto. auto with arith. auto. auto with arith.
apply Nle_plus in H.
destruct H.
rewrite H.
rewrite minus_plus.
rewrite Nat.add_comm.
rewrite minus_plus.
rewrite Nat.add_comm at 2.
rewrite Nat.add_sub.
rewrite Nat.add_sub.
auto.
auto.
Qed.
Expand Down Expand Up @@ -1299,16 +1300,16 @@ simpl.
assert(~(p-S n|p)).
apply H1.
split.
apply (minus_le_compat_r (S(S(S(S n)))) p (S n)) in H.
rewrite <- minus_Sn_m in H.
rewrite <- minus_Sn_m in H.
rewrite <- minus_Sn_m in H.
rewrite <- minus_n_n in H.
apply (Nat.sub_le_mono_r (S(S(S(S n)))) p (S n)) in H.
rewrite Nat.sub_succ_l in H.
rewrite Nat.sub_succ_l in H.
rewrite Nat.sub_succ_l in H.
rewrite Nat.sub_diag in H.
auto with arith.
auto.
auto.
auto with arith.
apply lt_minus.
apply Nat.sub_lt.
apply Nat.le_trans with (S(S(S n))).
auto with arith. auto.
auto with arith.
Expand All @@ -1317,25 +1318,25 @@ assert (~Ndiv_algo (p-S n) p=true).
intro.
apply H1 with (p-S n).
split.
apply (minus_le_compat_r (S(S(S(S n)))) p (S n)) in H.
rewrite <- minus_Sn_m in H.
rewrite <- minus_Sn_m in H.
rewrite <- minus_Sn_m in H.
rewrite <- minus_n_n in H.
apply (Nat.sub_le_mono_r (S(S(S(S n)))) p (S n)) in H.
rewrite Nat.sub_succ_l in H.
rewrite Nat.sub_succ_l in H.
rewrite Nat.sub_succ_l in H.
rewrite Nat.sub_diag in H.
auto with arith.
auto.
auto.
auto.
apply lt_minus.
apply Nat.sub_lt.
apply Nat.le_trans with (S(S(S(S n)))).
auto. auto. auto with arith.
apply Ndiv_algo_complete.
unfold gt.
apply (minus_le_compat_r (S(S(S(S n)))) p (S n)) in H.
rewrite <- minus_Sn_m in H.
rewrite <- minus_Sn_m in H.
rewrite <- minus_Sn_m in H.
rewrite <- minus_n_n in H.
apply (Nat.sub_le_mono_r (S(S(S(S n)))) p (S n)) in H.
rewrite Nat.sub_succ_l in H.
rewrite Nat.sub_succ_l in H.
rewrite Nat.sub_succ_l in H.
rewrite Nat.sub_diag in H.
apply Nat.le_trans with 3. auto. auto. auto. auto. auto. auto. auto with arith.

destruct (Ndiv_algo (p-S n) p).
Expand All @@ -1351,9 +1352,9 @@ destruct p. inversion H.
do 3 apply eq_add_S in H.
rewrite H.
unfold Nleast_div_ge.
rewrite <- minus_Sn_m.
rewrite <- minus_Sn_m.
rewrite <- minus_n_n.
rewrite Nat.sub_succ_l.
rewrite Nat.sub_succ_l.
rewrite Nat.sub_diag.
assert(~(Ndiv_algo 2 (S(S(S p)))=true)).
intro.
apply H1 with 2.
Expand All @@ -1370,7 +1371,7 @@ rewrite H.
auto.
auto.
auto.
Qed.
Qed.

(** Implication of primality on lowest strict divisor *)
Theorem Nprime_least_div_p : forall p, Nprime p -> Nleast_div p = p.
Expand All @@ -1381,9 +1382,9 @@ destruct p.
apply Nnot_prime_0 in H. contradiction.
destruct p.
apply Nnot_prime_1 in H. contradiction.
rewrite minus_Sn_m.
rewrite <- Nat.sub_succ_l.
apply Nat.le_trans with (S (S p)).
apply lt_n_S.
apply Nat.succ_lt_mono.
auto with arith. auto. auto with arith.
auto.
Qed.
Expand Down Expand Up @@ -1449,7 +1450,7 @@ apply Nleast_div_div.
auto with arith.
destruct H2.
destruct q.
rewrite mult_0_l in H2.
rewrite Nat.mul_0_l in H2.
rewrite H2 in H.
inversion H.
destruct q.
Expand Down Expand Up @@ -1523,6 +1524,7 @@ auto.
Qed.

(** * Compatibility of coprimality with multiplication *)

Theorem Nrel_prime_mult_compat : forall p n m,
Nrel_prime p n -> Nrel_prime p m -> Nrel_prime p (n * m).
Proof.
Expand Down Expand Up @@ -1589,7 +1591,7 @@ split.
apply Nleast_div_gt_1. auto with arith.
split.
destruct q.
rewrite mult_0_l in H1.
rewrite Nat.mul_0_l in H1.
rewrite H1 in H.
inversion H.
destruct q.
Expand Down Expand Up @@ -1702,7 +1704,7 @@ apply Nat.mul_le_mono_r.
auto.
auto with arith.
destruct q.
rewrite mult_0_l in H0. rewrite H0 in H. inversion H.
rewrite Nat.mul_0_l in H0. rewrite H0 in H. inversion H.
destruct q.
rewrite Nat.mul_1_l in H0.
assert(Ngreatest_div n<n).
Expand All @@ -1727,7 +1729,7 @@ destruct H3.
replace q with (q*1).
rewrite H0.
rewrite H2.
apply mult_S_lt_compat_l.
apply Nat.mul_lt_mono_pos_l; [apply Nat.lt_0_succ|].
auto. ring.
symmetry in H3.
apply Ngreatest_div_1_prime in H3.
Expand All @@ -1748,7 +1750,7 @@ apply Nat.mul_le_mono_r.
auto.
auto with arith.
destruct q.
rewrite mult_0_l in H1.
rewrite Nat.mul_0_l in H1.
rewrite H1 in H. inversion H.
auto with arith.
apply Ndiv_le in H2.
Expand All @@ -1765,13 +1767,13 @@ rewrite H1.
rewrite H2.
destruct n.
inversion H.
apply mult_S_lt_compat_l.
apply Nat.mul_lt_mono_pos_l; [apply Nat.lt_0_succ|].
auto. ring.
destruct n.
inversion H.
auto with arith.

apply le_antisym; auto.
apply Nat.le_antisymm; auto.
Qed.

Lemma div_mod a b : a <> 0 -> (a | b) <-> b mod a = 0.
Expand Down
6 changes: 3 additions & 3 deletions Arith/Nfinite_prod.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -118,8 +118,8 @@ Proof.
induction n.
intros.
compute.
apply le_n_O_eq in H.
rewrite <- H in H0.
apply Nat.le_0_r in H.
rewrite H in H0.
exact H0.

intros.
Expand Down Expand Up @@ -159,7 +159,7 @@ intros.
rewrite Nfinite_prod_split_upper.
rewrite Nfinite_prod_split_lower.
rewrite IHn.
rewrite <- minus_n_O.
rewrite Nat.sub_0_r.
assert (Nfinite_prod_0_n n (fun k : nat => f (S n - S k)) =
Nfinite_prod_0_n n (fun k : nat => f (n - k))).
apply Nfinite_prod_subtle_eq_compat.
Expand Down
3 changes: 1 addition & 2 deletions Arith/Ninductions.v
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,3 @@

Require Import Arith MyNat.

Lemma nat_strong : forall (P : nat -> Prop), P O ->
Expand All @@ -19,5 +18,5 @@ intros P P0 P1 PSS ; apply nat_strong.
assumption.
intros [] HN.
assumption.
apply PSS, HN, le_n_Sn.
apply PSS, HN, Nat.le_succ_diag_r.
Qed.
Loading

0 comments on commit 949436d

Please sign in to comment.