nitpicks

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -9,7 +9,7 @@
     `card_big_setU`
 
 - file `pnt.v`
-  + definitions `prime_search`, `prime_seq`
+  + definitions `next_prime`, `prime_seq`
   + lemmas `leq_prime_seq`, `mem_prime_seq`
   + theorem `DivergenceSumInversePrimeNumbers`
 

classical/unstable.v

@@ -35,48 +35,45 @@ Unset Printing Implicit Defensive.
 Import Order.TTheory GRing.Theory Num.Theory.
 Local Open Scope ring_scope.
 
-Lemma coprime_prodr (I : Type) (r : seq I) (P : {pred I}) (F : I -> nat) (a : I) (l : seq I) :
+Lemma coprime_prodr (I : Type) (r : seq I) (P : {pred I}) (F : I -> nat) (a : I)
+    (l : seq I) :
   all (coprime (F a)) [seq F i | i <- [seq i <- l | P i]] ->
   coprime (F a) (\prod_(j <- l | P j) F j).
 Proof.
-elim: l => /= [_|a0 l HI].
-  by rewrite big_nil coprimen1.
-rewrite big_cons. case: (P a0) => //.
-rewrite map_cons => /= /andP [] ? ?.
-rewrite coprimeMr. apply/andP. split=> //.
-exact: HI.
+elim: l => /= [_|h t ih]; first by rewrite big_nil coprimen1.
+rewrite big_cons; case: ifPn => // Ph.
+rewrite map_cons => /= /andP[FaFh FatP].
+by rewrite coprimeMr FaFh/= ih.
 Qed.
 
-Lemma Gauss_dvd_prod (I : eqType) (r : seq I) (P : {pred I}) (F : I -> nat) (n : nat) :
+Lemma Gauss_dvd_prod (I : eqType) (r : seq I) (P : {pred I}) (F : I -> nat)
+    (n : nat) :
   pairwise coprime [seq F i | i <- [seq i <- r | P i]] ->
   reflect (forall i, i \in r -> P i -> F i %| n)
-  (\prod_(i <- r | P i) F i %| n).
+          (\prod_(i <- r | P i) F i %| n).
 Proof.
 elim: r => /= [_|a l HI].
   by rewrite big_nil dvd1n; apply: ReflectT => i; rewrite in_nil.
-rewrite big_cons.
-case: (boolP (P a)) => [Pa|]; last first.
-  rewrite -eqbF_neg => /eqP nPa pairwisecoprime.
-  apply: (equivP (HI pairwisecoprime)).
-  split; last first => [Fidvdn i iinl|Fidvdn i].
-    by apply: Fidvdn; rewrite in_cons; apply/orP; right.
-  rewrite in_cons => /orP [/eqP ->|]; first by rewrite nPa.
-  exact: Fidvdn.
-rewrite map_cons pairwise_cons => /andP [] allcoprimea pairwisecoprime.
+rewrite big_cons; case: ifP => [Pa|nPa]; last first.
+  move/HI/equivP; apply; split=> [Fidvdn i|Fidvdn i il].
+    by rewrite in_cons => /predU1P[->|]; [rewrite nPa|exact: Fidvdn].
+  by apply: Fidvdn; rewrite in_cons il orbT.
+rewrite map_cons pairwise_cons => /andP[allcoprimea pairwisecoprime].
 rewrite Gauss_dvd; last exact: coprime_prodr.
 apply: (equivP (andPP idP (HI pairwisecoprime))).
-split=> [[] Fadvdn Fidvdn i|Fidvdn].
-  by rewrite in_cons => /orP [/eqP ->|]; last exact: Fidvdn.
-split=> [|i iinl].
-  apply: Fidvdn => //; first exact: mem_head.
-by apply: Fidvdn; rewrite in_cons; apply/orP; right.
+split=> [[Fadvdn Fidvdn] i|Fidvdn].
+  by rewrite in_cons => /predU1P[->//|]; exact: Fidvdn.
+split=> [|i il].
+  by apply: Fidvdn => //; exact: mem_head.
+by apply: Fidvdn; rewrite in_cons il orbT.
 Qed.
 
-Lemma expn_prod (I : eqType) (r : seq I) (P : {pred I}) (F : I -> nat) (n : nat) :
+Lemma expn_prod (I : eqType) (r : seq I) (P : {pred I}) (F : I -> nat)
+    (n : nat) :
   ((\prod_(i <- r | P i) F i) ^ n = \prod_(i <- r | P i) (F i) ^ n)%N.
 Proof.
 elim: r => [|a l]; first by rewrite !big_nil exp1n.
-by rewrite !big_cons; case: (P a) => <- //; rewrite expnMn.
+by rewrite !big_cons; case: ifPn => // Pa <-; rewrite expnMn.
 Qed.
 
 Section max_min.
@@ -141,11 +138,10 @@ Qed.
 Definition monotonous d (T : porderType d) (pT : predType T) (A : pT) (f : T -> T) :=
   {in A &, {mono f : x y / (x <= y)%O}} \/ {in A &, {mono f : x y /~ (x <= y)%O}}.
 
-Lemma mono_ext: forall f, {mono f : m n / (m <= n)%N} -> forall n : nat, (n <= f n)%N.
+Lemma mono_ext f : {mono f : m n / (m <= n)%N} -> forall n, (n <= f n)%N.
 Proof.
-move=> f fincr. elim=> [//| n HR]. apply: (leq_ltn_trans HR).
-rewrite ltn_neqAle fincr (inj_eq (incn_inj fincr)) -ltn_neqAle.
-exact: ltnSn.
+move=> fincr; elim=> [//| n HR]; rewrite (leq_ltn_trans HR)//.
+by rewrite ltn_neqAle fincr (inj_eq (incn_inj fincr)) -ltn_neqAle.
 Qed.
 
 (* NB: these lemmas have been introduced to develop the theory of bounded variation *)
@@ -228,13 +224,12 @@ Arguments big_rmcond_in {R idx op I r} P.
 
 Reserved Notation "`1- x" (format "`1- x", at level 2).
 
-Lemma card_big_setU (I : Type) (T : finType) (r : seq I) (P : {pred I}) (F : I -> {set T}) :
+Lemma card_big_setU (I : Type) (T : finType) (r : seq I) (P : {pred I})
+    (F : I -> {set T}) :
   (#|\bigcup_(i <- r | P i)  F i| <= \sum_(i <- r | P i) #|F i|)%N.
 Proof.
-elim: r => [|a l HI]; first by rewrite !big_nil cards0.
-rewrite !big_cons. case: (P a); last exact: HI.
-apply: (leq_trans (leq_card_setU (F a) _)).
-by rewrite leq_add2l.
+elim/big_ind2 : _ => // [|m A n B Am Bn]; first by rewrite cards0.
+by rewrite (leq_trans (leq_card_setU _ _))// leq_add.
 Qed.
 
 Section onem.