Library Combi.Combi.subseq: Subsequence of a sequence as a fintype
Subsequence of a sequence as a fintype
We define a sigma-type subseqs w for subsequence of a given sequence w We show that subseqs w is canonically a finType. We define the three following constructor- Subseqs Pf == construct a subseqs w from a proof subseq x w.
- sub_nil w == the empty sequence [::] as a subseqs w.
- sub_full w == w as as a subseqs w.
From HB Require Import structures.
From mathcomp Require Import all_ssreflect.
Require Import tools combclass sorted.
Set Implicit Arguments.
From mathcomp Require Import all_ssreflect.
Require Import tools combclass sorted.
Set Implicit Arguments.
Section RCons.
Variable (T : eqType).
Implicit Type s w : seq T.
Implicit Type a b l : T.
Lemma subseq_rcons_eq s w l : subseq s w = subseq (rcons s l) (rcons w l).
Lemma subseq_rcons_neq s si w wn :
si != wn -> subseq (rcons s si) (rcons w wn) = subseq (rcons s si) w.
End RCons.
Section SubseqSorted.
Variable (T : eqType) (leT : rel T).
Implicit Type s : seq T.
Lemma sorted_subseqP s1 s2 :
transitive leT -> irreflexive leT -> sorted leT s1 -> sorted leT s2 ->
reflect {subset s1 <= s2} (subseq s1 s2).
End SubseqSorted.
Section SubseqSortedIn.
Variable (T : eqType) (leT : rel T).
Implicit Type s : seq T.
Lemma sorted_subseq_inP s1 s2 :
{in s2 & &, transitive leT} -> {in s2, irreflexive leT} ->
sorted leT s1 -> sorted leT s2 ->
reflect {subset s1 <= s2} (subseq s1 s2).
End SubseqSortedIn.
Variable (T : eqType).
Implicit Type s w : seq T.
Implicit Type a b l : T.
Lemma subseq_rcons_eq s w l : subseq s w = subseq (rcons s l) (rcons w l).
Lemma subseq_rcons_neq s si w wn :
si != wn -> subseq (rcons s si) (rcons w wn) = subseq (rcons s si) w.
End RCons.
Section SubseqSorted.
Variable (T : eqType) (leT : rel T).
Implicit Type s : seq T.
Lemma sorted_subseqP s1 s2 :
transitive leT -> irreflexive leT -> sorted leT s1 -> sorted leT s2 ->
reflect {subset s1 <= s2} (subseq s1 s2).
End SubseqSorted.
Section SubseqSortedIn.
Variable (T : eqType) (leT : rel T).
Implicit Type s : seq T.
Lemma sorted_subseq_inP s1 s2 :
{in s2 & &, transitive leT} -> {in s2, irreflexive leT} ->
sorted leT s1 -> sorted leT s2 ->
reflect {subset s1 <= s2} (subseq s1 s2).
End SubseqSortedIn.
Subsequence of a sequence as a fintype
Section FinType.
Variables (T : choiceType) (w : seq T).
Structure subseqs : predArgType :=
Subseqs {subseqsval :> seq T; _ : subseq subseqsval w}.
Implicit Type (s : subseqs).
Lemma to_mask_spec s : {m : (size w).-tuple bool | mask m w == s}.
Definition to_mask s := let: exist m _ := to_mask_spec s in m.
Lemma to_maskK : cancel to_mask (fun m => Subseqs (mask_subseq (val m) w)).
Lemma subseqsP s : subseq s w.
Definition sub_nil : subseqs := Subseqs (sub0seq w).
Definition sub_full : subseqs := Subseqs (subseq_refl w).
Lemma mask1E x0 i :
i < size w -> mask [tuple val x == i | x < size w] w = [:: nth x0 w i].
Lemma mask_injP :
reflect (injective (fun m : (size w).-tuple bool => mask (val m) w))
(uniq w).
Lemma Subseqs_maskK :
uniq w -> cancel (fun m => Subseqs (mask_subseq (val m) w)) to_mask.
Lemma enum_subseqsE :
perm_eq
(enum {: subseqs})
(undup [seq Subseqs (mask_subseq (val m) w) | m : (size w).-tuple bool]).
Lemma val_enum_subseqs :
perm_eq
(map val (enum {: subseqs}))
(undup [seq mask (val m) w | m : (size w).-tuple bool]).
Lemma seq_masks_uniq :
uniq w -> uniq [seq mask (val m) w | m : (size w).-tuple bool].
Lemma subseqs_masks_uniq :
uniq w ->
uniq [seq Subseqs (mask_subseq (val m) w) | m : (size w).-tuple bool].
End FinType.
Section Bigop.
Context {R : Type} {idx : R} {op : Monoid.com_law idx}.
#[local] Notation "1" := idx.
#[local] Notation "'*%M'" := op (at level 0).
#[local] Notation "x * y" := (op x y).
Context {T : choiceType}.
Lemma big_subseqs (F : seq T -> R) (s : seq T) :
uniq s ->
\big[*%M/1]_(i : subseqs s) F i =
\big[*%M/1]_(m : (size s).-tuple bool) F (mask m s).
Lemma big_subseqs_cond (P : pred (seq T)) (F : seq T -> R) (s : seq T) :
uniq s ->
\big[*%M/1]_(i : subseqs s | P i) F i =
\big[*%M/1]_(m : (size s).-tuple bool | P (mask m s)) F (mask m s).
Lemma big_subseqs0 (F : seq T -> R) :
\big[*%M/1]_(i : subseqs [::]) F i = F [::].
Lemma big_subseqs_cons (F : seq T -> R) (a : T) (s : seq T) :
uniq (a :: s) ->
\big[*%M/1]_(i : subseqs (a :: s)) F i =
\big[*%M/1]_(i : subseqs s) F (a :: i) * \big[*%M/1]_(i : subseqs s) F (i).
Lemma big_subseqs_cons_cond
(F : seq T -> R) (P : pred (seq T)) (a : T) (s : seq T) :
uniq (a :: s) ->
\big[*%M/1]_(i : subseqs (a :: s) | P i) F i =
\big[*%M/1]_(i : subseqs s | P (a :: i)) F (a :: i) *
\big[*%M/1]_(i : subseqs s | P i) F (i).
Lemma big_subseqs_undup (F : seq T -> R) (s : seq T) :
idempotent op ->
\big[*%M/1]_(i : subseqs s) F i =
\big[*%M/1]_(m : (size s).-tuple bool) F (mask m s).
Lemma big_subseqs_undup_cond (F : seq T -> R) (P : pred (seq T)) (s : seq T) :
idempotent op ->
\big[*%M/1]_(i : subseqs s | P i) F i =
\big[*%M/1]_(m : (size s).-tuple bool | P (mask m s)) F (mask m s).
End Bigop.