diff options
| -rw-r--r-- | doc/changelog/10-standard-library/12031-ollibs-cpermutation.rst | 4 | ||||
| -rw-r--r-- | doc/stdlib/index-list.html.template | 1 | ||||
| -rw-r--r-- | theories/Sorting/CPermutation.v | 283 |
3 files changed, 288 insertions, 0 deletions
diff --git a/doc/changelog/10-standard-library/12031-ollibs-cpermutation.rst b/doc/changelog/10-standard-library/12031-ollibs-cpermutation.rst new file mode 100644 index 0000000000..95b4cce2f7 --- /dev/null +++ b/doc/changelog/10-standard-library/12031-ollibs-cpermutation.rst @@ -0,0 +1,4 @@ +- **Added:** + Definition and properties of cyclic permutations / circular shifts: ``CPermutation`` + (`#12031 <https://github.com/coq/coq/pull/12031>`_, + by Olivier Laurent). diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 7fa621c11c..73f1df010d 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -444,6 +444,7 @@ through the <tt>Require Import</tt> command.</p> theories/Sorting/PermutSetoid.v theories/Sorting/Mergesort.v theories/Sorting/Sorted.v + theories/Sorting/CPermutation.v </dd> <dt> <b>Wellfounded</b>: diff --git a/theories/Sorting/CPermutation.v b/theories/Sorting/CPermutation.v new file mode 100644 index 0000000000..fac9cd1d6d --- /dev/null +++ b/theories/Sorting/CPermutation.v @@ -0,0 +1,283 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** * 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. (* For notations [] and [a;b;c] *) +Set Implicit Arguments. + +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. +Proof. intros ? ? [? ?]; apply Permutation_app_comm. Qed. + +(** Some facts about [CPermutation] *) + +Theorem CPermutation_nil : forall l, CPermutation [] l -> l = []. +Proof. +intros l HC; inversion HC as [l1 l2 Heq]; subst. +now apply app_eq_nil in Heq; destruct Heq; subst. +Qed. + +Theorem CPermutation_nil_cons : forall l a, ~ CPermutation [] (a :: l). +Proof. intros l a HC; apply CPermutation_nil in HC; inversion HC. Qed. + +Theorem CPermutation_nil_app_cons : forall l1 l2 a, + ~ CPermutation [] (l1 ++ a ::l2). +Proof. +intros l1 l2 a HC; apply CPermutation_nil in HC; destruct l1; inversion HC. +Qed. + +Lemma CPermutation_split : forall l1 l2, + CPermutation l1 l2 <-> exists n, l2 = skipn n l1 ++ firstn n l1. +Proof. +intros l1 l2; split. +- intros [l1' l2']. + exists (length l1'). + rewrite skipn_app, skipn_all, Nat.sub_diag; simpl; f_equal. + now rewrite firstn_app, firstn_all, Nat.sub_diag; simpl; rewrite app_nil_r. +- now intros [n ->]; rewrite <- (firstn_skipn n) at 1. +Qed. + + +(** Equivalence relation *) + +Theorem CPermutation_refl : forall l, CPermutation l l. +Proof. +intros l; now rewrite <- (app_nil_l l) at 1; rewrite <- (app_nil_r l) at 2. +Qed. + +Instance CPermutation_refl' : Proper (Logic.eq ==> CPermutation) id. +Proof. intros ? ? ->; apply CPermutation_refl. Qed. + +Theorem CPermutation_sym : forall l l', CPermutation l l' -> CPermutation l' l. +Proof. now intros ? ? [? ?]. Qed. + +Theorem CPermutation_trans : forall l l' l'', + CPermutation l l' -> CPermutation l' l'' -> CPermutation l l''. +Proof. +intros l l' l'' HC1 HC2. +inversion HC1 as [l1 l2]; inversion HC2 as [l3 l4 Heq Heq']; subst. +clear - Heq; revert l1 l2 l4 Heq; clear; induction l3; simpl; intros. +- now subst; rewrite app_nil_r. +- destruct l2 as [| b]. + + simpl in Heq; subst. + now rewrite app_nil_r, app_comm_cons. + + inversion Heq as [[Heqb Heq']]; subst. + replace (l1 ++ b :: l2) with ((l1 ++ b :: nil) ++ l2) + by now rewrite <- app_assoc, <- app_comm_cons. + replace (l4 ++ b :: l3) with ((l4 ++ b :: nil) ++ l3) + by now rewrite <- app_assoc, <- app_comm_cons. + apply IHl3. + now rewrite 2 app_assoc, Heq'. +Qed. + +End CPermutation. + +Hint Resolve CPermutation_refl : core. + +(* These hints do not reduce the size of the problem to solve and they + must be used with care to avoid combinatoric explosions *) + +Local Hint Resolve cperm CPermutation_sym CPermutation_trans : core. + +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. +Proof. intros l1 l2 l3 HC; now transitivity (l1 ++ l2). Qed. + +Theorem CPermutation_app_comm : forall l1 l2, CPermutation (l1 ++ l2) (l2 ++ l1). +Proof. apply cperm. Qed. + +Lemma CPermutation_app_rot : forall l1 l2 l3, + CPermutation (l1 ++ l2 ++ l3) (l2 ++ l3 ++ l1). +Proof. intros l1 l2 l3; now rewrite (app_assoc l2). Qed. + +Lemma CPermutation_cons_append : forall l a, + CPermutation (a :: l) (l ++ [a]). +Proof. intros l a; now rewrite <- (app_nil_l l), app_comm_cons. Qed. + +Lemma CPermutation_morph_cons : forall P : list A -> Prop, + (forall a l, P (l ++ [a]) -> P (a :: l)) -> + Proper (@CPermutation A ==> iff) P. +Proof. +enough (forall P : list A -> Prop, + (forall a l, P (l ++ [a]) -> P (a :: l)) -> + forall l1 l2, CPermutation l1 l2 -> P l1 -> P l2) + as Himp + by now intros P HP l1 l2 HC; split; [ | symmetry in HC ]; apply Himp. +intros P HP l1 l2 [l1' l2']. +revert l1'; induction l2' using rev_ind; intros l1' HPl. +- now rewrite app_nil_r in HPl. +- rewrite app_assoc in HPl. + apply HP in HPl. + rewrite <- app_assoc, <- app_comm_cons, app_nil_l. + now apply IHl2'. +Qed. + +Lemma CPermutation_length_1 : forall a b, CPermutation [a] [b] -> a = b. +Proof. intros; now apply Permutation_length_1, CPermutation_Permutation. Qed. + +Lemma CPermutation_length_1_inv : forall l a, CPermutation [a] l -> l = [a]. +Proof. intros; now apply Permutation_length_1_inv, CPermutation_Permutation. Qed. + +Lemma CPermutation_swap : forall a b, CPermutation [a; b] [b; a]. +Proof. +intros; now change [a; b] with ([a] ++ [b]); change [b; a] with ([b] ++ [a]). +Qed. + +Lemma CPermutation_length_2 : forall a1 a2 b1 b2, + CPermutation [a1; a2] [b1; b2] -> + a1 = b1 /\ a2 = b2 \/ a1 = b2 /\ a2 = b1. +Proof. intros; now apply Permutation_length_2, CPermutation_Permutation. Qed. + +Lemma CPermutation_length_2_inv : forall a b l, + CPermutation [a; b] l -> l = [a; b] \/ l = [b; a]. +Proof. intros; now apply Permutation_length_2_inv, CPermutation_Permutation. Qed. + +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''. +Proof. +intros l l1 l2 a HC. +inversion HC as [l1' l2' Heq' Heq]; clear HC; subst. +enough (exists l3, (l2' ++ l3 = l1 /\ l1' = l3 ++ a :: l2) + \/ (l2' = l1 ++ a :: l3 /\ l3 ++ l1' = l2)) + as [l3 [[<- ->]|[-> <-]]]. +- exists l3, (l2 ++ l2'); rewrite app_comm_cons; intuition. +- exists (l1' ++ l1), l3; intuition. +- revert l1' l2' l2 Heq; induction l1; simpl; intros l1' l2' l2 Heq. + + destruct l2'; inversion Heq; subst. + * exists nil; intuition. + * exists l2'; intuition. + + destruct l2'; inversion Heq; subst. + * exists (a0 :: l1); intuition. + * apply IHl1 in H1 as [l3 [[<- ->]|[-> <-]]]; exists l3; intuition. +Qed. + +Lemma CPermutation_vs_cons_inv : forall l l0 a, + CPermutation l (a :: l0) -> exists l' l'', l0 = l'' ++ l' /\ l = l' ++ a :: l''. +Proof. intros; rewrite <- (app_nil_r l0); now apply CPermutation_vs_elt_inv. Qed. + +End CPermutation_properties. + + +(** [rev], [in], [map], [Forall], [Exists], etc. *) + +Global Instance CPermutation_rev A : + Proper (@CPermutation A ==> @CPermutation A) (@rev A) | 10. +Proof. +intro l; induction l; intros l' HC. +- now apply CPermutation_nil in HC; subst. +- symmetry in HC. + destruct (CPermutation_vs_cons_inv HC) as [l1 [l2 [-> ->]]]. + simpl; rewrite ? rev_app_distr; simpl. + now rewrite <- app_assoc. +Qed. + +Global Instance CPermutation_in A a : + Proper (@CPermutation A ==> Basics.impl) (In a). +Proof. +intros l l' HC Hin. +now apply Permutation_in with l; [ apply CPermutation_Permutation | ]. +Qed. + +Global Instance CPermutation_in' A : + Proper (Logic.eq ==> @CPermutation A ==> iff) (@In A) | 10. +Proof. intros a a' <- l l' HC; split; now apply CPermutation_in. Qed. + +Global Instance CPermutation_map A B (f : A -> B) : + Proper (@CPermutation A ==> @CPermutation B) (map f) | 10. +Proof. now intros ? ? [l1 l2]; rewrite 2 map_app. Qed. + +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'. +Proof. +induction m as [| b m]; intros l HC. +- exists nil; split; auto. + destruct l; auto. + apply CPermutation_nil in HC; inversion HC. +- symmetry in HC. + destruct (CPermutation_vs_cons_inv HC) as [m1 [m2 [-> Heq]]]. + apply map_eq_app in Heq as [l1 [l1' [-> [-> Heq]]]]. + symmetry in Heq. + apply map_eq_cons in Heq as [a [l1'' [-> [-> ->]]]]. + exists (a :: l1'' ++ l1); split. + + now simpl; rewrite map_app. + + now rewrite app_comm_cons. +Qed. + +Lemma CPermutation_image A B : forall (f : A -> B) a l l', + CPermutation (a :: l) (map f l') -> exists a', a = f a'. +Proof. +intros f a l l' HP. +now apply CPermutation_Permutation, Permutation_image in HP. +Qed. + +Instance CPermutation_Forall A (P : A -> Prop) : + Proper (@CPermutation A ==> Basics.impl) (Forall P). +Proof. +intros ? ? [? ?] HF. +now apply Forall_app in HF; apply Forall_app. +Qed. + +Instance CPermutation_Exists A (P : A -> Prop) : + Proper (@CPermutation A ==> Basics.impl) (Exists P). +Proof. +intros ? ? [? ?] HE. +apply Exists_app in HE; apply Exists_app; intuition. +Qed. + +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'. +Proof. +intros ? ? ? [? ?] HF. +apply Forall2_app_inv_l in HF as (l2' & l2'' & HF' & HF'' & ->). +exists (l2'' ++ l2'); intuition. +now apply Forall2_app. +Qed. + + +(** 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). +Proof. intros HP1 HP2; rewrite <- HP1, HP2; reflexivity. Qed. |