Library Stdlib.Sorting.CPermutation
Circular Shifts (aka Cyclic Permutations)
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).
CPermutation l1 l2 ->
CPermutation (rev l1) l3 -> CPermutation l3 (rev l2).