The Coq Proof Assistant

# 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
Inductive CPermutation : list A -> list A -> Prop :=
| cperm : forall l1 l2, CPermutation (l1 ++ l2) (l2 ++ l1).
Instance CPermutation_Permutation : Proper (CPermutation ==> (@Permutation A)) id.
Some facts about CPermutation
Theorem CPermutation_nil : forall l, CPermutation [] l -> l = [].
Theorem CPermutation_nil_cons : forall l a, ~ CPermutation [] (a :: l).
Theorem CPermutation_nil_app_cons : forall l1 l2 a,
~ CPermutation [] (l1 ++ a ::l2).
Lemma CPermutation_split : forall l1 l2,
CPermutation l1 l2 <-> exists n, l2 = skipn n l1 ++ firstn n l1.
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
Lemma CPermutation_app : forall l1 l2 l3,
CPermutation (l1 ++ l2) l3 -> CPermutation (l2 ++ l1) l3.
Theorem CPermutation_app_comm : forall l1 l2, CPermutation (l1 ++ l2) (l2 ++ l1).
Lemma CPermutation_app_rot : forall l1 l2 l3,
CPermutation (l1 ++ l2 ++ l3) (l2 ++ l3 ++ l1).
Lemma CPermutation_cons_append : forall l a,
CPermutation (a :: l) (l ++ [a]).
Lemma CPermutation_morph_cons : forall P : list A -> Prop,
(forall a l, P (l ++ [a]) -> P (a :: l)) ->
Proper (@CPermutation A ==> iff) P.
Lemma CPermutation_length_1 : forall a b, CPermutation [a] [b] -> a = b.
Lemma CPermutation_length_1_inv : forall a l, CPermutation [a] l -> l = [a].
Lemma CPermutation_swap : forall a b, CPermutation [a; b] [b; a].
Lemma CPermutation_length_2 : forall a1 a2 b1 b2,
CPermutation [a1; a2] [b1; b2] ->
a1 = b1 /\ a2 = b2 \/ a1 = b2 /\ a2 = b1.
Lemma CPermutation_length_2_inv : forall a b l,
CPermutation [a; b] l -> l = [a; b] \/ l = [b; a].
Lemma CPermutation_vs_elt_inv : forall l l1 l2 a,
CPermutation l (l1 ++ a :: l2) ->
exists l' l'', l2 ++ l1 = l'' ++ l' /\ l = l' ++ a :: l''.
Lemma CPermutation_vs_cons_inv : forall l l0 a,
CPermutation l (a :: l0) -> exists l' l'', l0 = l'' ++ l' /\ l = l' ++ a :: l''.
End CPermutation_properties.
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.
Example CPermutation_rewrite_rev A (l1 l2 l3: list A) :
CPermutation l1 l2 ->
CPermutation (rev l1) l3 -> CPermutation l3 (rev l2).