diff options
author | Pierre Letouzey <pierre.letouzey@inria.fr> | 2015-03-04 15:12:46 +0100 |
---|---|---|
committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2015-03-04 15:22:12 +0100 |
commit | d169ecbac96fe2a8a6a44395ad7fa83612e725c4 (patch) | |
tree | 320ae485363f28f62ff56e51ce9a6743e8658498 /theories/Lists/SetoidPermutation.v | |
parent | caf8907992fdfe655af95fa74e9c749be98c430c (diff) |
Introducing MMaps, a modernized FMaps.
NB: this is work-in-progress, there is currently only one
provided implementation (MMapWeakList).
In the same spirit as MSets w.r.t FSets, the main difference between
MMaps and former FMaps is the use of a new version of OrderedType
(see Orders.v instead of obsolete OrderedType.v).
We also try to benefit more from recent notions such as Proper.
For most function specifications, the style has changed : we now use
equations over "find" instead of "MapsTo" predicates, whenever possible
(cf. Maps in Compcert for a source of inspiration). Former specs are
now derived in FMapFacts, so this is mostly a matter of taste.
Two changes inspired by the current Maps of OCaml:
- "elements" is now "bindings"
- "map2" is now "merge" (and its function argument also receives a key).
We now use a maximal implicit argument for "empty".
Diffstat (limited to 'theories/Lists/SetoidPermutation.v')
-rw-r--r-- | theories/Lists/SetoidPermutation.v | 74 |
1 files changed, 73 insertions, 1 deletions
diff --git a/theories/Lists/SetoidPermutation.v b/theories/Lists/SetoidPermutation.v index afc7c25bd..cea3e839f 100644 --- a/theories/Lists/SetoidPermutation.v +++ b/theories/Lists/SetoidPermutation.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -Require Import SetoidList. +Require Import Permutation SetoidList. (* Set Universe Polymorphism. *) Set Implicit Arguments. @@ -123,4 +123,76 @@ Proof. apply equivlistA_NoDupA_split with x y; intuition. Qed. +Lemma Permutation_eqlistA_commute l₁ l₂ l₃ : + eqlistA eqA l₁ l₂ -> Permutation l₂ l₃ -> + exists l₂', Permutation l₁ l₂' /\ eqlistA eqA l₂' l₃. +Proof. + intros E P. revert l₁ E. + induction P; intros. + - inversion_clear E. now exists nil. + - inversion_clear E. + destruct (IHP l0) as (l0',(P',E')); trivial. clear IHP. + exists (x0::l0'). split; auto. + - inversion_clear E. inversion_clear H0. + exists (x1::x0::l1). now repeat constructor. + - clear P1 P2. + destruct (IHP1 _ E) as (l₁',(P₁,E₁)). + destruct (IHP2 _ E₁) as (l₂',(P₂,E₂)). + exists l₂'. split; trivial. econstructor; eauto. +Qed. + +Lemma PermutationA_decompose l₁ l₂ : + PermutationA l₁ l₂ -> + exists l, Permutation l₁ l /\ eqlistA eqA l l₂. +Proof. + induction 1. + - now exists nil. + - destruct IHPermutationA as (l,(P,E)). exists (x₁::l); auto. + - exists (x::y::l). split. constructor. reflexivity. + - destruct IHPermutationA1 as (l₁',(P,E)). + destruct IHPermutationA2 as (l₂',(P',E')). + destruct (@Permutation_eqlistA_commute l₁' l₂ l₂') as (l₁'',(P'',E'')); + trivial. + exists l₁''. split. now transitivity l₁'. now transitivity l₂'. +Qed. + +Lemma Permutation_PermutationA l₁ l₂ : + Permutation l₁ l₂ -> PermutationA l₁ l₂. +Proof. + induction 1. + - constructor. + - now constructor. + - apply permA_swap. + - econstructor; eauto. +Qed. + +Lemma eqlistA_PermutationA l₁ l₂ : + eqlistA eqA l₁ l₂ -> PermutationA l₁ l₂. +Proof. + induction 1; now constructor. +Qed. + +Lemma NoDupA_equivlistA_decompose l1 l2 : + NoDupA eqA l1 -> NoDupA eqA l2 -> equivlistA eqA l1 l2 -> + exists l, Permutation l1 l /\ eqlistA eqA l l2. +Proof. + intros. apply PermutationA_decompose. + now apply NoDupA_equivlistA_PermutationA. +Qed. + +Lemma PermutationA_preserves_NoDupA l₁ l₂ : + PermutationA l₁ l₂ -> NoDupA eqA l₁ -> NoDupA eqA l₂. +Proof. + induction 1; trivial. + - inversion_clear 1; constructor; auto. + apply PermutationA_equivlistA in H0. contradict H2. + now rewrite H, H0. + - inversion_clear 1. inversion_clear H1. constructor. + + contradict H. inversion_clear H; trivial. + elim H0. now constructor. + + constructor; trivial. + contradict H0. now apply InA_cons_tl. + - eauto. +Qed. + End Permutation. |