diff options
author | 2012-07-10 15:38:59 +0000 | |
---|---|---|
committer | 2012-07-10 15:38:59 +0000 | |
commit | a884f7dcebed71608f395fe140722790367089e2 (patch) | |
tree | 942398bdde4d6419e25ca7bfd76aa9b150d7b54d /theories/Lists/SetoidList.v | |
parent | 43582a9c7ac7e5f2311c8ce52d8107553b2c9673 (diff) |
isolate instances about Permutation and PermutationA which may slow rewrite
After discovering a rewrite in Ergo that takes a loooong time due
to a bad interaction with the instances of Permutation and PermutationA :
- PermutationA is now in a separate file SetoidPermutation
- File Permutation.v isn't Require'd by SetoidList anymore
nor MergeSort.v, just the definitions in Sorted.v
- Attempt to put a priority on these instances.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15584 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Lists/SetoidList.v')
-rw-r--r-- | theories/Lists/SetoidList.v | 114 |
1 files changed, 1 insertions, 113 deletions
diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v index f6eab8649..7d3c383c1 100644 --- a/theories/Lists/SetoidList.v +++ b/theories/Lists/SetoidList.v @@ -7,7 +7,7 @@ (***********************************************************************) Require Export List. -Require Export Sorting. +Require Export Sorted. Require Export Setoid Basics Morphisms. Set Implicit Arguments. Unset Strict Implicit. @@ -908,118 +908,6 @@ Qed. End Find. -(** Permutations of list modulo a setoid equality. *) -(** Section contributed by Robbert Krebbers (Nijmegen University). *) - -Section Permutation. -Context {A : Type} (eqA : relation A) (e : Equivalence eqA). - -Inductive PermutationA : list A -> list A -> Prop := - | permA_nil: PermutationA nil nil - | permA_skip x₁ x₂ l₁ l₂ : - eqA x₁ x₂ -> PermutationA l₁ l₂ -> PermutationA (x₁ :: l₁) (x₂ :: l₂) - | permA_swap x y l : PermutationA (y :: x :: l) (x :: y :: l) - | permA_trans l₁ l₂ l₃ : - PermutationA l₁ l₂ -> PermutationA l₂ l₃ -> PermutationA l₁ l₃. -Local Hint Constructors PermutationA. - -Global Instance: Equivalence PermutationA. -Proof. - constructor. - - intro l. induction l; intuition. - - intros l₁ l₂. induction 1; eauto. apply permA_skip; intuition. - - exact permA_trans. -Qed. - -Global Instance PermutationA_cons : - Proper (eqA ==> PermutationA ==> PermutationA) (@cons A). -Proof. - repeat intro. now apply permA_skip. -Qed. - -Lemma PermutationA_app_head l₁ l₂ l : - PermutationA l₁ l₂ -> PermutationA (l ++ l₁) (l ++ l₂). -Proof. - induction l; trivial; intros. apply permA_skip; intuition. -Qed. - -Global Instance PermutationA_app : - Proper (PermutationA ==> PermutationA ==> PermutationA) (@app A). -Proof. - intros l₁ l₂ Pl k₁ k₂ Pk. - induction Pl. - - easy. - - now apply permA_skip. - - etransitivity. - * rewrite <-!app_comm_cons. now apply permA_swap. - * rewrite !app_comm_cons. now apply PermutationA_app_head. - - do 2 (etransitivity; try eassumption). - apply PermutationA_app_head. now symmetry. -Qed. - -Lemma PermutationA_app_tail l₁ l₂ l : - PermutationA l₁ l₂ -> PermutationA (l₁ ++ l) (l₂ ++ l). -Proof. - intros E. now rewrite E. -Qed. - -Lemma PermutationA_cons_append l x : - PermutationA (x :: l) (l ++ x :: nil). -Proof. - induction l. - - easy. - - simpl. rewrite <-IHl. intuition. -Qed. - -Lemma PermutationA_app_comm l₁ l₂ : - PermutationA (l₁ ++ l₂) (l₂ ++ l₁). -Proof. - induction l₁. - - now rewrite app_nil_r. - - rewrite <-app_comm_cons, IHl₁, app_comm_cons. - now rewrite PermutationA_cons_append, <-app_assoc. -Qed. - -Lemma PermutationA_cons_app l l₁ l₂ x : - PermutationA l (l₁ ++ l₂) -> PermutationA (x :: l) (l₁ ++ x :: l₂). -Proof. - intros E. rewrite E. - now rewrite app_comm_cons, PermutationA_cons_append, <-app_assoc. -Qed. - -Lemma PermutationA_middle l₁ l₂ x : - PermutationA (x :: l₁ ++ l₂) (l₁ ++ x :: l₂). -Proof. - now apply PermutationA_cons_app. -Qed. - -Lemma PermutationA_equivlistA l₁ l₂ : - PermutationA l₁ l₂ -> equivlistA eqA l₁ l₂. -Proof. - induction 1. - - reflexivity. - - now apply equivlistA_cons_proper. - - now apply equivlistA_permute_heads. - - etransitivity; eassumption. -Qed. - -Lemma NoDupA_equivlistA_PermutationA l₁ l₂ : - NoDupA eqA l₁ -> NoDupA eqA l₂ -> - equivlistA eqA l₁ l₂ -> PermutationA l₁ l₂. -Proof. - intros Pl₁. revert l₂. induction Pl₁ as [|x l₁ E1]. - - intros l₂ _ H₂. symmetry in H₂. now rewrite (equivlistA_nil_eq eqA). - - intros l₂ Pl₂ E2. - destruct (@InA_split _ eqA l₂ x) as [l₂h [y [l₂t [E3 ?]]]]. - { rewrite <-E2. intuition. } - subst. transitivity (y :: l₁); [intuition |]. - apply PermutationA_cons_app, IHPl₁. - now apply NoDupA_split with y. - apply equivlistA_NoDupA_split with x y; intuition. -Qed. - -End Permutation. - (** Compatibility aliases. [Proper] is rather to be used directly now.*) Definition compat_bool {A} (eqA:A->A->Prop)(f:A->bool) := |