Added results about `mask` and `subseq`

3 files changed, 59 insertions, 5 deletions

diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v
index 6b26968..4cf0cef 100644
--- a/mathcomp/ssreflect/bigop.v
+++ b/mathcomp/ssreflect/bigop.v
@@ -1013,13 +1013,25 @@ Qed.
 Lemma big_ord0 P F : \big[op/idx]_(i < 0 | P i) F i = idx.
 Proof. by rewrite big_pred0 => [|[]]. Qed.
 
-Lemma big_tnth I r (P : pred I) F :
-  let r_ := tnth (in_tuple r) in
+Lemma big_mask_tuple I n m (t : n.-tuple I) (P : pred I) F :
+  \big[op/idx]_(i <- mask m t | P i) F i
+    = \big[op/idx]_(i < n | nth false m i && P (tnth t i)) F (tnth t i).
+Proof.
+rewrite [t in LHS]tuple_map_ord/= -map_mask big_map.
+by rewrite mask_enum_ord big_filter_cond/= enumT.
+Qed.
+
+Lemma big_mask I r m (P : pred I) (F : I -> R) (r_ := tnth (in_tuple r)) :
+  \big[op/idx]_(i <- mask m r | P i) F i
+    = \big[op/idx]_(i < size r | nth false m i && P (r_ i)) F (r_ i).
+Proof. exact: (big_mask_tuple _ (in_tuple r)). Qed.
+
+Lemma big_tnth I r (P : pred I) F (r_ := tnth (in_tuple r)) :
   \big[op/idx]_(i <- r | P i) F i
-     = \big[op/idx]_(i < size r | P (r_ i)) (F (r_ i)).
+    = \big[op/idx]_(i < size r | P (r_ i)) (F (r_ i)).
 Proof.
-case: r => /= [|x0 r]; first by rewrite big_nil big_ord0.
-by rewrite (big_nth x0) big_mkord; apply: eq_big => i; rewrite (tnth_nth x0).
+rewrite /= -[r in LHS](mask_true (leqnn (size r))) big_mask//.
+by apply: eq_bigl => i /=; rewrite nth_nseq ltn_ord.
 Qed.
 
 Lemma big_index_uniq (I : eqType) (r : seq I) (E : 'I_(size r) -> R) :
diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v
index 870b797..726b8c2 100644
--- a/mathcomp/ssreflect/fintype.v
+++ b/mathcomp/ssreflect/fintype.v
@@ -1832,6 +1832,13 @@ Proof.
 by rewrite -[in LHS](nth_ord_enum i i) index_uniq ?(enum_uniq, size_enum_ord).
 Qed.
 
+Lemma mask_enum_ord m :
+  mask m (enum 'I_n) = [seq i <- enum 'I_n | nth false m (val i)].
+Proof.
+rewrite mask_filter ?enum_uniq//; apply: eq_filter => i.
+by rewrite in_mask ?enum_uniq ?mem_enum// index_enum_ord.
+Qed.
+
 End OrdinalEnum.
 
 Lemma widen_ord_proof n m (i : 'I_n) : n <= m -> i < m.
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index ac9a225..de512ef 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -1943,6 +1943,14 @@ Proof. by case: b. Qed.
 Lemma mem_mask x m s : x \in mask m s -> x \in s.
 Proof. by rewrite -!has_pred1 => /has_mask. Qed.
 
+Lemma in_mask x m s : uniq s -> x \in s ->
+  (x \in mask m s) = nth false m (index x s).
+Proof.
+elim: s m => [|y s IHs] [|[] m]//= /andP[yNs s_uniq]; rewrite ?in_cons eq_sym;
+have [<-|neq_xy]//= := altP eqP => x_s; do ?by rewrite IHs.
+by apply: contraNF yNs => /mem_mask.
+Qed.
+
 Lemma mask_uniq s : uniq s -> forall m, uniq (mask m s).
 Proof.
 elim: s => [|x s IHs] Uxs [|b m] //=.
@@ -2059,6 +2067,13 @@ Qed.
 Lemma subseq_cons s x : subseq s (x :: s).
 Proof. exact: suffix_subseq [:: x] s. Qed.
 
+Lemma cons_subseq s1 s2 x : subseq (x :: s1) s2 -> subseq s1 s2.
+Proof.
+elim: s2 s1 => [|y s2 IHs2] [|z s1]//= in x *.
+by have [<-|neq_xy] := altP eqP => [|/IHs2] zs1_s2;
+   case: ifP => // _; apply: IHs2 zs1_s2.
+Qed.
+
 Lemma subseq_rcons s x : subseq s (rcons s x).
 Proof. by rewrite -cats1 prefix_subseq. Qed.
 
@@ -2071,6 +2086,14 @@ Proof. exact/subseq_uniq/take_subseq. Qed.
 Lemma drop_uniq s n : uniq s -> uniq (drop n s).
 Proof. exact/subseq_uniq/drop_subseq. Qed.
 
+Lemma undup_subseq s : subseq (undup s) s.
+Proof.
+elim: s => //= x s IHs; have [xs|xNs] := boolP (x \in s); last by rewrite eqxx.
+have: x \in undup s by rewrite mem_undup.
+case: (undup s) => [|y u]//= in IHs * => _; case: eqP => // _.
+exact: cons_subseq IHs.
+Qed.
+
 End Subseq.
 
 Prenex Implicits subseq.
@@ -2272,6 +2295,18 @@ case: eqP => [-> | _] /IHs[s3 perm_s2] {IHs}.
 by exists (rcons s3 y); rewrite -cat_cons -perm_rcons -!cats1 catA perm_cat2r.
 Qed.
 
+Lemma subset_maskP s1 s2 : uniq s1 -> {subset s1 <= s2} ->
+  exists2 m : seq bool, size m = size s2 & perm_eq s1 (mask m s2).
+Proof.
+move=> s1_uniq sub_s1_s2; pose s1' := [seq x <- undup s2 | x \in s1].
+have /subseqP[m sm s1'_eq] : subseq s1' s2.
+  by apply: subseq_trans (undup_subseq _); apply: filter_subseq.
+exists m => //; rewrite -s1'_eq; apply: uniq_perm => //.
+  by rewrite filter_uniq ?undup_uniq.
+move=> x; rewrite mem_filter mem_undup.
+by have [x_s1|//] := boolP (x \in s1); rewrite sub_s1_s2.
+Qed.
+
 End FilterSubseq.
 
 Arguments subseq_uniqP [T s1 s2].