Add all_filter, all_pmap, and all_allpairsP in seq.v

2 files changed, 28 insertions, 2 deletions

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 28d1b5c..fa91781 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -25,7 +25,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 - Added theorems `ffact_prod`, `prime_modn_expSn` and `fermat_little`
   in `binomial.v`
 
-- Added theorems `flatten_map1`, `allpairs_consr`, and `mask_filter` in `seq.v`.
+- Added theorems `flatten_map1`, `allpairs_consr`, `mask_filter`,
+  `all_filter`, `all_pmap`, and `all_allpairsP` in `seq.v`.
 
 - Fintype theorems: `fintype0`, `card_le1P`, `mem_card1`,
   `card1P`, `fintype_le1P`, `fintype1`, `fintype1P`,
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index 35d9a69..57c9437 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -555,6 +555,10 @@ Proof. by move=> Ea s; rewrite !has_count (eq_count Ea). Qed.
 Lemma eq_all a1 a2 : a1 =1 a2 -> all a1 =1 all a2.
 Proof. by move=> Ea s; rewrite !all_count (eq_count Ea). Qed.
 
+Lemma all_filter (p q : pred T) xs :
+  all p (filter q xs) = all [pred i | q i ==> p i] xs.
+Proof. by elim: xs => //= x xs <-; case: (q x). Qed.
+
 Section SubPred.
 
 Variable (a1 a2 : pred T).
@@ -2260,6 +2264,10 @@ Proof. by elim: s => //= x s <-; rewrite -{3}(fK x); case: (f _). Qed.
 Lemma pmap_cat s t : pmap (s ++ t) = pmap s ++ pmap t.
 Proof. by elim: s => //= x s ->; case/f: x. Qed.
 
+Lemma all_pmap (p : pred rT) s :
+  all p (pmap s) = all [pred i | oapp p true (f i)] s.
+Proof. by elim: s => //= x s <-; case: f. Qed.
+
 End Pmap.
 
 Section EqPmap.
@@ -2922,6 +2930,8 @@ Qed.
 
 End EqAllPairsDep.
 
+Arguments allpairsPdep {S T R f s t z}.
+
 Section MemAllPairs.
 
 Variables (S : Type) (T : S -> Type) (R : eqType).
@@ -2944,7 +2954,22 @@ Qed.
 
 End MemAllPairs.
 
-Arguments allpairsPdep {S T R f s t z}.
+Lemma all_allpairsP
+      (S : eqType) (T : S -> eqType) (R : Type)
+      (p : pred R) (f : forall x : S, T x -> R)
+      (s : seq S) (t : forall x : S, seq (T x)) :
+  reflect (forall (x : S) (y : T x), x \in s -> y \in t x -> p (f x y))
+          (all p [seq f x y | x <- s, y <- t x]).
+Proof.
+elim: s => [|x s IHs]; first by constructor.
+rewrite /= all_cat all_map /preim.
+apply/(iffP andP)=> [[/allP /= ? ? x' y x'_in_xs]|p_xs_t].
+  by move: x'_in_xs y; rewrite inE => /predU1P [-> //|? ?]; exact: IHs.
+split; first by apply/allP => ?; exact/p_xs_t/mem_head.
+by apply/IHs => x' y x'_in_s; apply: p_xs_t; rewrite inE x'_in_s orbT.
+Qed.
+
+Arguments all_allpairsP {S T R p f s t}.
 
 Section EqAllPairs.