Merge pull request #386 from pi8027/allpairs

Generalize `allpairs_catr` to non-`eqType`s

2 files changed, 12 insertions, 9 deletions

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 43bc379..5e996b9 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -29,3 +29,6 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
   by `true` or `false`, while keeping the ability to use it in the way
   it was used before.
 
+- Generalized the `allpairs_catr` lemma to the case where the types of `s`,
+  `t1`, and `t2` are non-`eqType`s in `[seq E | i <- s, j <- t1 ++ t2]`.
+
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index 9581a95..feba604 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -2911,15 +2911,6 @@ move=> eq_s eq_t z; apply/allpairsPdep/allpairsPdep=> -[x [y [sx ty ->]]];
 by exists x, y; rewrite -eq_s in sx *; rewrite eq_t in ty *.
 Qed.
 
-Lemma allpairs_catr f s t1 t2 :
-  [seq f x y | x <- s, y <- t1 x ++ t2 x] =i
-    [seq f x y | x <- s, y <- t1 x] ++ [seq f x y | x <- s, y <- t2 x].
-Proof.
-move=> z; rewrite mem_cat; apply/allpairsPdep/orP=> [[x [y [s_x]]]|].
-  by rewrite mem_cat => /orP[]; [left|right]; apply/allpairsPdep; exists x, y.
-by case=>/allpairsPdep[x [y [sx ty ->]]]; exists x, y; rewrite mem_cat ty ?orbT.
-Qed.
-
 Lemma allpairs_uniq_dep f s t (st := [seq Tagged T y | x <- s, y <- t x]) :
   let g (p : {x : S & T x}) : R := f (tag p) (tagged p) in
     uniq s -> {in s, forall x, uniq (t x)} -> {in st &, injective g} ->
@@ -2935,6 +2926,15 @@ Qed.
 
 End EqAllPairsDep.
 
+Lemma allpairs_catr
+      (S : Type) (T : S -> Type) (R : eqType) (f : forall x, T x -> R) s t1 t2 :
+  [seq f x y | x <- s, y <- t1 x ++ t2 x] =i
+  [seq f x y | x <- s, y <- t1 x] ++ [seq f x y | x <- s, y <- t2 x].
+Proof.
+move=> z; rewrite mem_cat; elim: s => //= x s ih.
+by rewrite map_cat !mem_cat ih !orbA; congr orb; rewrite orbAC.
+Qed.
+
 Arguments allpairsPdep {S T R f s t z}.
 
 Section EqAllPairs.