Library Combi.Combi.permuted: Listing the Permutations of a tuple or seq

The list of the permuted tuple of a given tuple

The main goal is to show that, given a sequence s over an eqType there are only finitely many sequences s' which are a permutation of s (that is perm_eq s s') and to show that the number is a multinomial coefficient.

permuted_tuple t == a sequence of tuples containing (with duplicates) all tuple t' such that perm_eq t t'
permuted_seq s == a sequence of seqs containing (with duplicates) all seqs s' such that perm_eq s s'
permuted t == sigma typle for tuple t' such that perm_eq t t'. this is canonically a fintype, provided the type of the elements of t is a countType.
permutedact t s == the n tuple t permuted by the permutation s
permuted_action == the corresponding action of the symmetric group 'S_n

The main result is the cardinality of the set of permuted of a tuple expressed as a multinomial card_permuted_multinomial.

From HB Require Import structures.
From mathcomp Require Import all_ssreflect.
From mathcomp Require Import perm fingroup action gproduct.

Require Import tools combclass sorted partition composition multinomial.
Require Import permcomp cycles.

Set Implicit Arguments.

Enumeration of the permutation of a tuple

Section Permuted.

Variable T : eqType.

Section SizeN.

Variable n : nat.

Definition permuted_tuple (t : n.-tuple T) :=
  [seq [tuple tnth t (aperm i p) | i < n] | p : 'S_n ].

Lemma size_permuted_tuple (t : n.-tuple T) : size (permuted_tuple t) = n`!.

Lemma perm_eq_permuted_tuple (s : seq T) (H : size s == n) :
  forall s1, perm_eq s s1 ->
             s1 \in [seq tval t | t <- permuted_tuple (Tuple H)].

Lemma mem_enum_permuted (s t : n.-tuple T) :
  perm_eq s t -> t \in permuted_tuple s.

Lemma all_permuted (s : n.-tuple T) :
  all (fun x : n.-tuple T => perm_eq s x) (permuted_tuple s).

End SizeN.

Definition permuted_seq s :=
  [seq tval t | t <- permuted_tuple (Tuple (eq_refl (size s)))].

Lemma size_permuted_seq s : size (permuted_seq s) = (size s)`!.

Lemma eq_seqE s s1 : perm_eq s s1 -> s1 \in permuted_seq s.

End Permuted.

Permutation of a tuple as a fintype

Section FinType.

Variable T : countType.
Variable n : nat.
Variable w : n.-tuple T.

Structure permuted : predArgType :=
Permuted { tpval :> n.-tuple T; _ : perm_eq w tpval }.

Lemma permutedP (p : permuted) : perm_eq w p.

End FinType.

#[export] Hint Resolve permutedP : core.

Import GroupScope.

Action of 'S_n on permuted for and n.-tuple T.

There is no use defining an action on general tuple because most of the lemmas on actions assume that the type acted upon is a finType. We could require moreover that the underlying type is a fintype so that the set of tuple is a fintype too, but the use we have in mind is T = nat allowing to deal with the action on monomials. Instead of that, we decide to act only on the sigma type permuted.

Section ActOnTuple.

Variables (T : countType) (n : nat) (w : n.-tuple T).
Implicit Type (t : permuted w).

#[local] Notation wp := (Permuted (perm_refl w)).

Lemma permutedact_subproof t (s : 'S_n) :
  perm_eq w [tuple tnth t (s^-1 i) | i < n].
Definition permutedact t s := Permuted (permutedact_subproof t s).

#[local] Notation "t # s" := (permutedact t s)
  (at level 40, left associativity, format "t # s").

Lemma permutedact_is_action : is_action [set: 'S_n] permutedact.
Canonical permuted_action := Action permutedact_is_action.
#[local] Notation pact := permuted_action.

Lemma permuted_action_trans :
  [transitive [set: 'S_n], on [set: permuted w] | pact].

The stabilizer of a tuple under permutation

Lemma stab_tuple_prod :
  'C[wp | pact] =
  (\prod_(x : seq_sub w) Sym_group [set i | tnth w i == val x])%G.

Lemma stab_tuple_dprod :
  'C[wp | pact] =
  \big[dprod/1]_(x : seq_sub w) Sym [set i | tnth w i == val x].

Close Scope group_scope.

Lemma card_stab_tuple :
  #|('C[wp | pact])%G| = \prod_(x : seq_sub w) (count_mem (val x) w)`!.

Lemma card_permuted_prod :
  #|[set: permuted w]| * \prod_(x : seq_sub w) (count_mem (val x) w)`! = n`!.

Lemma dvdn_card_permuted :
  \prod_(x : seq_sub w) (count_mem (val x) w)`! %| n`!.

Lemma card_permuted_seq_sub :
  #|[set: permuted w]| = n`! %/ \prod_(x : seq_sub w) (count_mem (val x) w)`!.

Lemma card_permuted :
  #|[set: permuted w]| = n`! %/ \prod_(x <- undup w) (count_mem x w)`!.

Lemma size_count_mem_undup (s : seq T) :
  size s = \sum_(j <- undup s) count_mem j s.

Theorem card_permuted_multinomial :
  #|[set: permuted w]| = 'C [[seq count_mem x w | x <- undup w]].

Corollary card_permuted_multinomial_subset (s : seq T) :
  {subset w <= s } -> uniq s ->
  #|[set: permuted w]| = 'C [[seq count_mem x w | x <- s]].

End ActOnTuple.

Require Import sorted.
Import LeqGeqOrder.

Lemma card_preim_part_of_compn n (sh : 'P_n) :
  #|[set c | partn_of_compn c == sh]| =
  (size sh)`! %/ \prod_(i <- iota 1 n) (count_mem i sh)`!.