diff options
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 3 | ||||
| -rw-r--r-- | mathcomp/ssreflect/seq.v | 18 |
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. |