Library Coq.Sorting.CPermutation


Circular Shifts (aka Cyclic Permutations)

The main inductive CPermutation relates lists up to circular shifts of their elements.
For example: CPermutation [a1;a2;a3;a4;a5] [a4;a5;a1;a2;a3]
Note: Terminology does not seem to be strongly fixed in English. For the record, it is "permutations circulaires" in French.

Require Import List Permutation Morphisms PeanoNat.
Import ListNotations. Set Implicit Arguments.

Local Ltac Tauto.intuition_solver ::= auto with datatypes.

Section CPermutation.

Variable A:Type.

Definition
Some facts about CPermutation
Equivalence relation

Theorem CPermutation_refl : forall l, CPermutation l l.

Instance CPermutation_refl' : Proper (Logic.eq ==> CPermutation) id.

Theorem CPermutation_sym : forall l l', CPermutation l l' -> CPermutation l' l.

Theorem CPermutation_trans : forall l l' l'',
 CPermutation l l' -> CPermutation l' l'' -> CPermutation l l''.

End CPermutation.

#[global]
Hint Resolve CPermutation_refl : core.


Local Hint Resolve cperm CPermutation_sym CPermutation_trans : core.

#[global]
Instance CPermutation_Equivalence A : Equivalence (@CPermutation A) | 10 := {
  Equivalence_Reflexive := @CPermutation_refl A ;
  Equivalence_Symmetric := @CPermutation_sym A ;
  Equivalence_Transitive := @CPermutation_trans A }.

Section CPermutation_properties.

Variable A B:Type.

Implicit Types a b : A.
Implicit Types l : list A.

Compatibility with others operations on lists
rev, in, map, Forall, Exists, etc.

Global Instance CPermutation_rev A :
  Proper (@CPermutation A ==> @CPermutation A) (@rev A) | 10.

Global Instance CPermutation_in A a :
  Proper (@CPermutation A ==> Basics.impl) (In a).

Global Instance CPermutation_in' A :
  Proper (Logic.eq ==> @CPermutation A ==> iff) (@In A) | 10.

Global Instance CPermutation_map A B (f : A -> B) :
   Proper (@CPermutation A ==> @CPermutation B) (map f) | 10.

Lemma CPermutation_map_inv A B : forall (f : A -> B) m l,
  CPermutation m (map f l) -> exists l', m = map f l' /\ CPermutation l l'.

Lemma CPermutation_image A B : forall (f : A -> B) a l l',
  CPermutation (a :: l) (map f l') -> exists a', a = f a'.

#[global]
Instance CPermutation_Forall A (P : A -> Prop) :
  Proper (@CPermutation A ==> Basics.impl) (Forall P).

#[global]
Instance CPermutation_Exists A (P : A -> Prop) :
  Proper (@CPermutation A ==> Basics.impl) (Exists P).

Lemma CPermutation_Forall2 A B (P : A -> B -> Prop) :
  forall l1 l1' l2, CPermutation l1 l1' -> Forall2 P l1 l2 -> exists l2',
    CPermutation l2 l2' /\ Forall2 P l1' l2'.

As an equivalence relation compatible with some operations, CPermutation can be used through rewrite.