Merge pull request #408 from chdoc/existsPn

add existsPn/forallPn lemmas

10 files changed, 33 insertions, 17 deletions

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 6b3ba93..c4906fc 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -28,7 +28,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 - Added theorems `flatten_map1`, `allpairs_consr`, and `mask_filter` in `seq.v`.
 
 - Fintype theorems: `fintype0`, `card_le1P`, `mem_card1`,
-  `card1P`, `fintype_le1P`, `fintype1`, `fintype1P`.
+  `card1P`, `fintype_le1P`, `fintype1`, `fintype1P`,
+  `existsPn`, `exists_inPn`, `forallPn`, `forall_inPn`.
 
 - Bigop theorems: `big_rmcond`, `bigD1_seq`,
   `big_enum_val_cond`, `big_enum_rank_cond`,
diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v
index 95381ba..122457d 100644
--- a/mathcomp/algebra/intdiv.v
+++ b/mathcomp/algebra/intdiv.v
@@ -948,8 +948,7 @@ move=> {A leA IHa} IHa; wlog Di: i M Da / i = 0; last rewrite {i}Di in Da.
   exists R => //; exists d; rewrite //= xrowE -!mulmxA (mulmxA L) -dM xrowE.
   by rewrite mulmxA -perm_mxM tperm2 perm_mx1 mul1mx.
 without loss /forallP a_dvM0: / [forall j, a %| M 0 j]%Z.
-  have [_|] := altP forallP; first exact; rewrite negb_forall => /existsP/sigW.
-  by move/IHa=> IH _; apply: IH.
+  case: (altP forallP) => [_ IH|/forallPn/sigW/IHa IH _]; exact: IH.
 without loss{Da a_dvM0} Da: M / forall j, M 0 j = a.
   pose Uur := col' 0 (\row_j (1 - (M 0 j %/ a)%Z)).
   pose U : 'M_(1 + n) := block_mx 1 Uur 0 1%:M; pose M1 := M *m U.
@@ -963,8 +962,7 @@ without loss{Da a_dvM0} Da: M / forall j, M 0 j = a.
   exists L => //; exists (R * U^-1); first by rewrite unitmx_mul uR unitmx_inv.
   by exists d; rewrite //= mulmxA -dM mulmxK.
 without loss{IHa} /forallP/(_ (_, _))/= a_dvM: / [forall k, a %| M k.1 k.2]%Z.
-  have [_|] := altP forallP; first exact; rewrite negb_forall => /existsP/sigW.
-  case=> [[i j] /= a'Mij] _.
+  case: (altP forallP) => [_|/forallPn/sigW [[i j] /= a'Mij] _]; first exact.
   have [|||L uL [R uR [d dvD dM]]] := IHa _ _ M^T j; rewrite ?mxE 1?addnC //.
     by exists i; rewrite mxE.
   exists R^T; last exists L^T; rewrite ?unitmx_tr //; exists d => //.
diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v
index 8d6c03b..a39aba1 100644
--- a/mathcomp/algebra/mxalgebra.v
+++ b/mathcomp/algebra/mxalgebra.v
@@ -609,7 +609,7 @@ Arguments rV_subP {m1 m2 n A B}.
 
 Lemma row_subPn m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
   reflect (exists i, ~~ (row i A <= B)%MS) (~~ (A <= B)%MS).
-Proof. by rewrite (sameP row_subP forallP) negb_forall; apply: existsP. Qed.
+Proof. by rewrite (sameP row_subP forallP); apply: forallPn. Qed.
 
 Lemma sub_rVP n (u v : 'rV_n) : reflect (exists a, u = a *: v) (u <= v)%MS.
 Proof.
diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v
index ae12064..0266dea 100644
--- a/mathcomp/algebra/ssralg.v
+++ b/mathcomp/algebra/ssralg.v
@@ -4625,9 +4625,7 @@ Proof. by move=> x0 y0; rewrite mulf_eq0; apply/norP. Qed.
 
 Lemma prodf_neq0 (I : finType) (P : pred I) (F : I -> R) :
   reflect (forall i, P i -> (F i != 0)) (\prod_(i | P i) F i != 0).
-Proof.
-by rewrite (sameP (prodf_eq0 _ _) exists_inP) negb_exists_in; apply: forall_inP.
-Qed.
+Proof. by rewrite (sameP (prodf_eq0 _ _) exists_inP); apply: exists_inPn. Qed.
 
 Lemma prodf_seq_neq0 I r (P : pred I) (F : I -> R) :
   (\prod_(i <- r | P i) F i != 0) = all (fun i => P i ==> (F i != 0)) r.
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v
index dd84f31..f8c5675 100644
--- a/mathcomp/algebra/ssrnum.v
+++ b/mathcomp/algebra/ssrnum.v
@@ -3193,8 +3193,7 @@ apply/lerifP; case: ifPn => [/forall_inP-Econstant | Enonconstant].
 set mu := \sum_(i in A) E i; pose En i := E i *+ n.
 pose cmp_mu s := [pred i | s * mu < s * En i].
 have{Enonconstant} has_cmp_mu e (s := (-1) ^+ e): {i | i \in A & cmp_mu s i}.
-  apply/sig2W/exists_inP; apply: contraR Enonconstant.
-  rewrite negb_exists_in => /forall_inP-mu_s_A.
+  apply/sig2W/exists_inP; apply: contraR Enonconstant => /exists_inPn-mu_s_A.
   have n_gt0 i: i \in A -> (0 < n)%N by rewrite [n](cardD1 i) => ->.
   have{mu_s_A} mu_s_A i: i \in A -> s * En i <= s * mu.
     move=> Ai; rewrite real_lerNgt ?mu_s_A ?rpredMsign ?ger0_real ?Ege0 //.
@@ -4692,7 +4691,7 @@ rewrite horner_poly (eq_bigr _ (fun _ _ => mul1r _)) in pw_0.
 have wn1: w ^+ n = 1 by apply/eqP; rewrite -subr_eq0 subrX1 pw_0 mulr0.
 suffices /existsP[i ltRwi0]: [exists i : 'I_n, 'Re (w ^+ i) < 0].
   by exists (w ^+ i) => //; rewrite exprAC wn1 expr1n.
-apply: contra_eqT (congr1 Re pw_0); rewrite negb_exists => /forallP geRw0.
+apply: contra_eqT (congr1 Re pw_0) => /existsPn geRw0.
 rewrite raddf_sum raddf0 /= (bigD1 (Ordinal (ltnW n_gt1))) //=.
 rewrite (Creal_ReP _ _) ?rpred1 // gtr_eqF ?ltr_paddr ?ltr01 //=.
 by apply: sumr_ge0 => i _; rewrite real_lerNgt ?rpred0.
diff --git a/mathcomp/character/character.v b/mathcomp/character/character.v
index c2a7ef4..c95d03b 100644
--- a/mathcomp/character/character.v
+++ b/mathcomp/character/character.v
@@ -2930,7 +2930,7 @@ have [-> | ntG] := eqsVneq G [1]; first by exists 0; apply: cfker_sub.
 have{pG} [[p_pr _ _] pZ] := (pgroup_pdiv pG ntG, pgroupS (center_sub G) pG).
 have ntZ: 'Z(G) != [1] by rewrite center_nil_eq1.
 have{pZ} oZ: #|Z| = p by apply: Ohm1_cyclic_pgroup_prime.
-apply/existsP; apply: contraR ntZ; rewrite negb_exists => /forallP-not_ffulG.
+apply/existsP; apply: contraR ntZ => /existsPn-not_ffulG.
 rewrite -Ohm1_eq1 -subG1 /= -/Z -(TI_cfker_irr G); apply/bigcapsP=> i _.
 rewrite prime_meetG ?oZ // setIC meet_Ohm1 // meet_center_nil ?cfker_normal //.
 by rewrite -subG1 not_ffulG.
diff --git a/mathcomp/character/integral_char.v b/mathcomp/character/integral_char.v
index 0109b83..c6d40e2 100644
--- a/mathcomp/character/integral_char.v
+++ b/mathcomp/character/integral_char.v
@@ -687,7 +687,7 @@ Theorem nonlinear_irr_vanish gT (G : {group gT}) i :
   'chi[G]_i 1%g > 1 -> exists2 x, x \in G & 'chi_i x = 0.
 Proof.
 move=> chi1gt1; apply/exists_eq_inP; apply: contraFT (ltr_geF chi1gt1).
-rewrite negb_exists_in => /forall_inP-nz_chi.
+move/exists_inPn => -nz_chi.
 rewrite -(norm_Cnat (Cnat_irr1 i)) -(@expr_le1 _ 2) ?normr_ge0 //.
 rewrite -(ler_add2r (#|G|%:R * '['chi_i])) {1}cfnorm_irr mulr1.
 rewrite (cfnormE (cfun_onG _)) mulVKf ?neq0CG // (big_setD1 1%g) //=.
@@ -708,4 +708,4 @@ apply: sum_norm2_char_generators => [|s Ss].
 by rewrite -resS // nz_chi ?(subsetP sgG) ?cycle_generator.
 Qed.
 
-End MoreIntegralChar.
\ No newline at end of file
+End MoreIntegralChar.
diff --git a/mathcomp/field/galois.v b/mathcomp/field/galois.v
index 9a2bdfd..7937a24 100644
--- a/mathcomp/field/galois.v
+++ b/mathcomp/field/galois.v
@@ -1358,7 +1358,7 @@ rewrite ltnS (cardD1x Px) in lePn; move/IHn: lePn => {n IHn}/=IH_P.
 have [/eqfun_inP c_Px'_0 | ] := boolP [forall (y | P y && (y != x)), c_ y == 0].
   exists 1; rewrite ?mem1v // (bigD1 x Px) /= rmorph1 mulr1.
   by rewrite big1 ?addr0 // => y /c_Px'_0->; rewrite mul0r.
-rewrite negb_forall_in => /exists_inP[y Px'y nz_cy].
+case/forall_inPn => y Px'y nz_cy.
 have [Py /gal_eqP/eqlfun_inP/subvPn[a Ea]] := andP Px'y.
 rewrite memv_ker !lfun_simp => nz_yxa; pose d_ y := c_ y * (y a - x a).
 have /IH_P[//|b Eb nz_sumb]: d_ y != 0 by rewrite mulf_neq0.
diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v
index fe85e35..5c2ad4c 100644
--- a/mathcomp/ssreflect/finset.v
+++ b/mathcomp/ssreflect/finset.v
@@ -2251,7 +2251,7 @@ Lemma fixsetK : F fixset = fixset.
 Proof.
 suff /'exists_eqP[x /= e]: [exists k : 'I_n.+1, iterF k == iterF k.+1].
   by rewrite /fixset -(subnK (leq_ord x)) /iterF iter_add iter_fix.
-apply: contraT; rewrite negb_exists => /forallP /(_ (Ordinal _)) /= neq_iter.
+apply: contraT => /existsPn /(_ (Ordinal _)) /= neq_iter.
 suff iter_big k : k <= n.+1 -> k <= #|iter k F set0|.
   by have := iter_big _ (leqnn _); rewrite ltnNge max_card.
 elim: k => [|k IHk] k_lt //=; apply: (leq_ltn_trans (IHk (ltnW k_lt))).
diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v
index 32d2898..ffdf0a5 100644
--- a/mathcomp/ssreflect/fintype.v
+++ b/mathcomp/ssreflect/fintype.v
@@ -973,6 +973,22 @@ Lemma negb_exists_in D P :
   ~~ [exists (x | D x), P x] = [forall (x | D x), ~~ P x].
 Proof. by rewrite negb_exists; apply/eq_forallb => x; rewrite [~~ _]fun_if. Qed.
 
+Lemma existsPn P :
+  reflect (forall x, ~~ P x) (~~ [exists x, P x]).
+Proof. rewrite negb_exists. exact: forallP. Qed.
+
+Lemma forallPn P :
+  reflect (exists x, ~~ P x) (~~ [forall x, P x]).
+Proof. rewrite negb_forall. exact: existsP. Qed.
+
+Lemma exists_inPn D P :
+  reflect (forall x, x \in D -> ~~ P x) (~~ [exists x in D, P x]).
+Proof. rewrite negb_exists_in. exact: forall_inP. Qed.
+
+Lemma forall_inPn D P :
+  reflect (exists2 x, x \in D & ~~ P x) (~~ [forall x in D, P x]).
+Proof. rewrite negb_forall_in. exact: exists_inP. Qed.
+
 End Quantifiers.
 
 Arguments forallP {T P}.
@@ -983,6 +999,10 @@ Arguments existsP {T P}.
 Arguments exists_eqP {T rT f1 f2}.
 Arguments exists_inP {T D P}.
 Arguments exists_eq_inP {T rT D f1 f2}.
+Arguments existsPn {T P}.
+Arguments exists_inPn {T D P}.
+Arguments forallPn {T P}.
+Arguments forall_inPn {T D P}.
 
 Notation "'exists_in_ view" := (exists_inPP _ (fun _ => view))
   (at level 4, right associativity, format "''exists_in_' view").