poly_size_eq1 phrased with reflect + combinators

3 files changed, 50 insertions, 20 deletions

diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v
index 2eba50d..0f97bb0 100644
--- a/mathcomp/algebra/poly.v
+++ b/mathcomp/algebra/poly.v
@@ -2237,31 +2237,35 @@ move=> nzF; rewrite big_tnth size_prod; last by move=> i; rewrite nzF ?mem_tnth.
 by rewrite cardT /= size_enum_ord [in RHS]big_tnth.
 Qed.
 
-Lemma size_prod_eq1 (I : finType) (P : pred I) (F : I -> {poly R}) :
-  (size (\prod_(i | P i) F i) == 1%N) = [forall (i | P i), size (F i) == 1%N].
+Lemma size_mul_eq1 p q :
+  (size (p * q) == 1%N) = ((size p == 1%N) && (size q == 1%N)).
 Proof.
-have [/forall_inP F_neq0|] := boolP [forall (i | P i), F i != 0]; last first.
-  rewrite negb_forall_in => /exists_inP [i Pi]; rewrite negbK => /eqP Fi_eq0.
-  rewrite (bigD1 i) //= Fi_eq0 mul0r size_poly0; symmetry.
-  by apply/existsP; exists i; rewrite Pi Fi_eq0 size_poly0.
-rewrite size_prod // -sum1_card subSn; last first.
-  by rewrite leq_sum // => i Pi; rewrite size_poly_gt0 F_neq0.
-rewrite (eq_bigr (fun i => (size (F i)).-1 + 1))%N; last first.
-  by move=> i Pi; rewrite addn1 -polySpred ?F_neq0.
-rewrite big_split /= addnK -big_andE /=.
-by elim/big_ind2: _ => // [[] [|n] [] [|m]|i Pi]; rewrite -?polySpred ?F_neq0.
+have [->|pNZ] := eqVneq p 0; first by rewrite mul0r size_poly0.
+have [->|qNZ] := eqVneq q 0; first by rewrite mulr0 size_poly0 andbF.
+rewrite size_mul //.
+by move: pNZ qNZ; rewrite -!size_poly_gt0; (do 2 case: size) => //= n [|[|]].
 Qed.
 
-Lemma size_prod_seq_eq1 (I : eqType) (s : seq I) (F : I -> {poly R}) :
-  (size (\prod_(i <- s) F i) == 1%N) = (all [pred i | size (F i) == 1%N] s).
+Lemma size_prod_seq_eq1 (I : eqType) (s : seq I) (P : pred I) (F : I -> {poly R}) :
+  reflect (forall i, P i && (i \in s) -> size (F i) = 1%N)
+          (size (\prod_(i <- s | P i) F i) == 1%N).
 Proof.
-by rewrite big_tnth size_prod_eq1 -big_all [in RHS]big_tnth big_andE.
+have -> : (size (\prod_(i <- s | P i) F i) == 1%N) =
+  (all [pred i | P i ==> (size (F i) == 1%N)] s).
+  elim: s => [|a s IHs /=]; first by rewrite big_nil size_poly1.
+  by rewrite big_cons; case: (P a) => //=; rewrite size_mul_eq1 IHs.
+apply: (iffP allP) => /= [/(_ _ _)/implyP /(_ _)/eqP|] sF_eq1 i.
+  by move=> /andP[Pi si]; rewrite sF_eq1.
+by move=> si; apply/implyP => Pi; rewrite sF_eq1 ?Pi.
 Qed.
 
-Lemma size_mul_eq1 p q :
-  (size (p * q) == 1%N) = ((size p == 1%N) && (size q == 1%N)).
+Lemma size_prod_eq1 (I : finType) (P : pred I) (F : I -> {poly R}) :
+  reflect (forall i, P i -> size (F i) = 1%N)
+          (size (\prod_(i | P i) F i) == 1%N).
 Proof.
-by have := size_prod_seq_eq1 [:: p; q] id; rewrite unlock /= mulr1 andbT.
+apply: (iffP (size_prod_seq_eq1 _ _ _)) => Hi i.
+  by move=> Pi; apply: Hi; rewrite Pi /= mem_index_enum.
+by rewrite mem_index_enum andbT; apply: Hi.
 Qed.
 
 Lemma size_exp p n : (size (p ^+ n)).-1 = ((size p).-1 * n)%N.
diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v
index 1446fbd..cb2f0a6 100644
--- a/mathcomp/ssreflect/fintype.v
+++ b/mathcomp/ssreflect/fintype.v
@@ -867,9 +867,13 @@ Proof. exact: 'forall_eqP. Qed.
 Lemma forall_inP D P : reflect (forall x, D x -> P x) [forall (x | D x), P x].
 Proof. exact: 'forall_implyP. Qed.
 
+Lemma forall_inPP D P PP : (forall x, reflect (PP x) (P x)) ->
+  reflect (forall x, D x -> PP x) [forall (x | D x), P x].
+Proof. by move=> vP; apply: (iffP (forall_inP _ _)) => /(_ _ _) /vP. Qed.
+
 Lemma eqfun_inP D f1 f2 :
   reflect {in D, forall x, f1 x = f2 x} [forall (x | x \in D), f1 x == f2 x].
-Proof. by apply: (iffP 'forall_implyP) => eq_f12 x Dx; apply/eqP/eq_f12. Qed.
+Proof. exact: (forall_inPP _ (fun=> eqP)). Qed.
 
 Lemma existsP P : reflect (exists x, P x) [exists x, P x].
 Proof. exact: 'exists_idP. Qed.
@@ -881,9 +885,13 @@ Proof. exact: 'exists_eqP. Qed.
 Lemma exists_inP D P : reflect (exists2 x, D x & P x) [exists (x | D x), P x].
 Proof. by apply: (iffP 'exists_andP) => [[x []] | [x]]; exists x. Qed.
 
+Lemma exists_inPP D P PP : (forall x, reflect (PP x) (P x)) ->
+  reflect (exists2 x, D x & PP x) [exists (x | D x), P x].
+Proof. by move=> vP; apply: (iffP (exists_inP _ _)) => -[x?/vP]; exists x. Qed.
+
 Lemma exists_eq_inP D f1 f2 :
   reflect (exists2 x, D x & f1 x = f2 x) [exists (x | D x), f1 x == f2 x].
-Proof. by apply: (iffP (exists_inP _ _)) => [] [x Dx /eqP]; exists x. Qed.
+Proof. exact: (exists_inPP _ (fun=> eqP)). Qed.
 
 Lemma eq_existsb P1 P2 : P1 =1 P2 -> [exists x, P1 x] = [exists x, P2 x].
 Proof. by move=> eqP12; congr (_ != 0); apply: eq_card. Qed.
@@ -928,6 +936,11 @@ Arguments exists_eqP [T rT f1 f2].
 Arguments exists_inP [T D P].
 Arguments exists_eq_inP [T rT D f1 f2].
 
+Notation "'exists_in_ view" := (exists_inPP _ (fun _ => view))
+  (at level 4, right associativity, format "''exists_in_' view").
+Notation "'forall_in_ view" := (forall_inPP _ (fun _ => view))
+  (at level 4, right associativity, format "''forall_in_' view").
+
 Section Extrema.
 
 Variables (I : finType) (i0 : I) (P : pred I) (F : I -> nat).
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index 4347983..4bc704a 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -1004,6 +1004,10 @@ apply: (iffP IHs) => [] [x ysx ax]; exists x => //; first exact: mem_behead.
 by case: (predU1P ysx) ax => [->|//]; rewrite ay.
 Qed.
 
+Lemma hasPP s aP : (forall x, reflect (aP x) (a x)) ->
+  reflect (exists2 x, x \in s & aP x) (has a s).
+Proof. by move=> vP; apply: (iffP (hasP _)) => -[x?/vP]; exists x. Qed.
+
 Lemma hasPn s : reflect (forall x, x \in s -> ~~ a x) (~~ has a s).
 Proof.
 apply: (iffP idP) => not_a_s => [x s_x|].
@@ -1020,6 +1024,10 @@ rewrite /= andbC; case: IHs => IHs /=.
 by right=> H; case IHs => y Hy; apply H; apply: mem_behead.
 Qed.
 
+Lemma allPP s aP : (forall x, reflect (aP x) (a x)) ->
+  reflect (forall x, x \in s -> aP x) (all a s).
+Proof. by move=> vP; apply: (iffP (allP _)) => /(_ _ _) /vP. Qed.
+
 Lemma allPn s : reflect (exists2 x, x \in s & ~~ a x) (~~ all a s).
 Proof.
 elim: s => [|x s IHs]; first by right=> [[x Hx _]].
@@ -1038,6 +1046,11 @@ Qed.
 
 End Filters.
 
+Notation "'has_ view" := (hasPP _ (fun _ => view))
+  (at level 4, right associativity, format "''has_' view").
+Notation "'all_ view" := (allPP _ (fun _ => view))
+  (at level 4, right associativity, format "''all_' view").
+
 Section EqIn.
 
 Variables a1 a2 : pred T.