RIS.bijection: generate permutations.

Require Import tools atoms PeanoNat Nat.

Set Implicit Arguments.

Applying a permutation commutes with computing the shuffles.

Lemma shuffles_act {X: Set} `{Nominal X} π (l : list X) : shuffles (π ∙l) = π ∙ shuffles l.

Section bijection.
Context {atom : Set} {A : Atom atom}.

Permutation out of two lists

If l and m are duplication-free and have the same length, then there is a permutation (computed by make_perm l m) that send l to m. Furthermore, every atom mentioned by this permutation comes from either l or m.

  Fixpoint make_perm (l m : list atom) : perm :=
    match (l ,m ) with
    | ([],_) | (_,[]) ⇒ []
    | (a::l,b::m) ⇒
      let p := make_perm l m in
      (p ∙a,b)::p
    end.
  Notation " l >> m " := (make_perm l m) (at level 80).

  Lemma make_perm_spec (l m : list atom) :
    NoDup l → NoDup m → ⎢l ⎥ = ⎢m ⎥ →
    let p := (l >> m) in
    p ∙ l = m ∧ elements p ⊆ l ++m.

  Lemma make_bij (l m : list atom) :
    NoDup l → NoDup m → ⎢l ⎥ = ⎢m ⎥ → (l >> m ) ∙ l = m.

Applying make_perm to two copies of the same lists yields a permutation equivalent to the identity.

Lemma make_perm_id l : (l >> l ) ≃ [].

Permutation out of a bijection

Atom bijections with finite support are equivalent to permutations.

Lemma to_perm_correct f l :
injective f → has_support f l → ∀ x, ({{l }} >> map f {{l }}) ∙ x = f x.

Functions that are injective and finitely supported may be represented as permutations.

Theorem bijection_iff_perm (f : atom → atom) :
(injective f ∧ supported f ) ↔ ∃ p, f ≃ (act p ).

Enumerate permutations

permutations l lists every permutation supported by l.

Definition permutations l : list perm :=
map (make_perm {{l }}) (shuffles {{l }}).

Indeed, if every atom a such that q∙a≠a belongs to the list l, then there is a permutation p that is equivalent to q and belongs to the list permutations l.

Lemma permutations_spec q l :
(∃ p, p ≃ q ∧ p ∈ permutations l ) ↔ (∀ a, a ≠ q ∙a → a ∈ l ).

This means that if p is a permutation supported by l, for every name a we know that a∈l if and only if a∈p∙l.

Lemma permutations_image p l :
p ∈ permutations l → p ∙l ≈ l.

The permutations appearing in permutations l have the additional property that they only mention names from l.

Lemma permutations_elements p l :
p ∈ permutations l → elements p ⊆ l.

End bijection.
Notation " l >> m " := (make_perm l m) (at level 80).