From a884f7dcebed71608f395fe140722790367089e2 Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 10 Jul 2012 15:38:59 +0000 Subject: 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 --- doc/stdlib/index-list.html.template | 1 + theories/Lists/SetoidList.v | 114 +------------------------------- theories/Lists/SetoidPermutation.v | 125 ++++++++++++++++++++++++++++++++++++ theories/Lists/vo.itarget | 1 + theories/Sorting/Permutation.v | 14 ++-- 5 files changed, 135 insertions(+), 120 deletions(-) create mode 100644 theories/Lists/SetoidPermutation.v diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 6ad232b5f2..0f21c082b8 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -411,6 +411,7 @@ through the Require Import command.

theories/Lists/List.v theories/Lists/ListSet.v theories/Lists/SetoidList.v + theories/Lists/SetoidPermutation.v theories/Lists/Streams.v theories/Lists/StreamMemo.v theories/Lists/ListTactics.v diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v index f6eab86496..7d3c383c1b 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) := diff --git a/theories/Lists/SetoidPermutation.v b/theories/Lists/SetoidPermutation.v new file mode 100644 index 0000000000..b0657b63aa --- /dev/null +++ b/theories/Lists/SetoidPermutation.v @@ -0,0 +1,125 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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. diff --git a/theories/Lists/vo.itarget b/theories/Lists/vo.itarget index adcfba4954..04994f5932 100644 --- a/theories/Lists/vo.itarget +++ b/theories/Lists/vo.itarget @@ -2,5 +2,6 @@ ListSet.vo ListTactics.vo List.vo SetoidList.vo +SetoidPermutation.vo StreamMemo.vo Streams.vo diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v index fdfcd394a6..eb769b77d3 100644 --- a/theories/Sorting/Permutation.v +++ b/theories/Sorting/Permutation.v @@ -85,7 +85,7 @@ Instance Permutation_Equivalence A : Equivalence (@Permutation A) | 10 := { Equivalence_Transitive := @Permutation_trans A }. Instance Permutation_cons A : - Proper (Logic.eq ==> @Permutation A ==> @Permutation A) (@cons A). + Proper (Logic.eq ==> @Permutation A ==> @Permutation A) (@cons A) | 10. Proof. repeat intro; subst; auto using perm_skip. Qed. @@ -106,7 +106,7 @@ Proof. Qed. Global Instance Permutation_in' : - Proper (Logic.eq ==> @Permutation A ==> iff) (@In A). + Proper (Logic.eq ==> @Permutation A ==> iff) (@In A) | 10. Proof. repeat red; intros; subst; eauto using Permutation_in. Qed. @@ -138,7 +138,7 @@ Proof. Qed. Global Instance Permutation_app' : - Proper (@Permutation A ==> @Permutation A ==> @Permutation A) (@app A). + Proper (@Permutation A ==> @Permutation A ==> @Permutation A) (@app A) | 10. Proof. repeat intro; now apply Permutation_app. Qed. @@ -187,7 +187,7 @@ Proof. Qed. Global Instance Permutation_rev' : - Proper (@Permutation A ==> @Permutation A) (@rev A). + Proper (@Permutation A ==> @Permutation A) (@rev A) | 10. Proof. repeat intro; now rewrite <- 2 Permutation_rev. Qed. @@ -199,7 +199,7 @@ Proof. Qed. Global Instance Permutation_length' : - Proper (@Permutation A ==> Logic.eq) (@length A). + Proper (@Permutation A ==> Logic.eq) (@length A) | 10. Proof. exact Permutation_length. Qed. @@ -407,7 +407,7 @@ Proof. Qed. Global Instance Permutation_NoDup' : - Proper (@Permutation A ==> iff) (@NoDup A). + Proper (@Permutation A ==> iff) (@NoDup A) | 10. Proof. repeat red; eauto using Permutation_NoDup. Qed. @@ -426,7 +426,7 @@ Proof. Qed. Global Instance Permutation_map' : - Proper (@Permutation A ==> @Permutation B) (map f). + Proper (@Permutation A ==> @Permutation B) (map f) | 10. Proof. exact Permutation_map. Qed. -- cgit v1.2.3