poly_size_eq1 phrased with reflect + combinators

2 files changed, 28 insertions, 2 deletions

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.