summaryrefslogtreecommitdiff
path: root/theories/Sorting/PermutEq.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Sorting/PermutEq.v')
-rw-r--r--theories/Sorting/PermutEq.v74
1 files changed, 32 insertions, 42 deletions
diff --git a/theories/Sorting/PermutEq.v b/theories/Sorting/PermutEq.v
index 084aae92..8e6aa6dc 100644
--- a/theories/Sorting/PermutEq.v
+++ b/theories/Sorting/PermutEq.v
@@ -6,61 +6,51 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: PermutEq.v 10739 2008-04-01 14:45:20Z herbelin $ i*)
+(*i $Id$ i*)
-Require Import Omega Relations Setoid List Multiset Permutation.
+Require Import Relations Setoid SetoidList List Multiset PermutSetoid Permutation.
Set Implicit Arguments.
(** This file is similar to [PermutSetoid], except that the equality used here
- is Coq usual one instead of a setoid equality. In particular, we can then
- prove the equivalence between [List.Permutation] and
+ is Coq usual one instead of a setoid equality. In particular, we can then
+ prove the equivalence between [List.Permutation] and
[Permutation.permutation].
*)
Section Perm.
-
+
Variable A : Type.
Hypothesis eq_dec : forall x y:A, {x=y} + {~ x=y}.
-
+
Notation permutation := (permutation _ eq_dec).
Notation list_contents := (list_contents _ eq_dec).
(** we can use [multiplicity] to define [In] and [NoDup]. *)
- Lemma multiplicity_In :
+ Lemma multiplicity_In :
forall l a, In a l <-> 0 < multiplicity (list_contents l) a.
Proof.
- induction l.
- simpl.
- split; inversion 1.
- simpl.
- split; intros.
- inversion_clear H.
- subst a0.
- destruct (eq_dec a a) as [_|H]; auto with arith; destruct H; auto.
- destruct (eq_dec a a0) as [H1|H1]; auto with arith; simpl.
- rewrite <- IHl; auto.
- destruct (eq_dec a a0); auto.
- simpl in H.
- right; rewrite IHl; auto.
+ intros; split; intro H.
+ eapply In_InA, multiplicity_InA in H; eauto with typeclass_instances.
+ eapply multiplicity_InA, InA_alt in H as (y & -> & H); eauto with typeclass_instances.
Qed.
Lemma multiplicity_In_O :
forall l a, ~ In a l -> multiplicity (list_contents l) a = 0.
Proof.
- intros l a; rewrite multiplicity_In;
+ intros l a; rewrite multiplicity_In;
destruct (multiplicity (list_contents l) a); auto.
destruct 1; auto with arith.
Qed.
-
+
Lemma multiplicity_In_S :
forall l a, In a l -> multiplicity (list_contents l) a >= 1.
Proof.
intros l a; rewrite multiplicity_In; auto.
Qed.
- Lemma multiplicity_NoDup :
+ Lemma multiplicity_NoDup :
forall l, NoDup l <-> (forall a, multiplicity (list_contents l) a <= 1).
Proof.
induction l.
@@ -78,7 +68,7 @@ Section Perm.
generalize (H a).
destruct (eq_dec a a) as [H0|H0].
destruct (multiplicity (list_contents l) a); auto with arith.
- simpl; inversion 1.
+ simpl; inversion 1.
inversion H3.
destruct H0; auto.
rewrite IHl; intros.
@@ -86,13 +76,13 @@ Section Perm.
destruct (eq_dec a a0); simpl; auto with arith.
Qed.
- Lemma NoDup_permut :
- forall l l', NoDup l -> NoDup l' ->
+ Lemma NoDup_permut :
+ forall l l', NoDup l -> NoDup l' ->
(forall x, In x l <-> In x l') -> permutation l l'.
Proof.
intros.
red; unfold meq; intros.
- rewrite multiplicity_NoDup in H, H0.
+ rewrite multiplicity_NoDup in H, H0.
generalize (H a) (H0 a) (H1 a); clear H H0 H1.
do 2 rewrite multiplicity_In.
destruct 3; omega.
@@ -102,7 +92,7 @@ Section Perm.
Lemma permut_In_In :
forall l1 l2 e, permutation l1 l2 -> In e l1 -> In e l2.
Proof.
- unfold Permutation.permutation, meq; intros l1 l2 e P IN.
+ unfold PermutSetoid.permutation, meq; intros l1 l2 e P IN.
generalize (P e); clear P.
destruct (In_dec eq_dec e l2) as [H|H]; auto.
rewrite (multiplicity_In_O _ _ H).
@@ -128,11 +118,11 @@ Section Perm.
intro Abs; generalize (permut_In_In _ Abs H).
inversion 1.
Qed.
-
- (** When used with [eq], this permutation notion is equivalent to
+
+ (** When used with [eq], this permutation notion is equivalent to
the one defined in [List.v]. *)
- Lemma permutation_Permutation :
+ Lemma permutation_Permutation :
forall l l', Permutation l l' <-> permutation l l'.
Proof.
split.
@@ -141,7 +131,7 @@ Section Perm.
apply permut_cons; auto.
change (permutation (y::x::l) ((x::nil)++y::l)).
apply permut_add_cons_inside; simpl; apply permut_refl.
- apply permut_tran with l'; auto.
+ apply permut_trans with l'; auto.
revert l'.
induction l.
intros.
@@ -152,7 +142,7 @@ Section Perm.
subst l'.
apply Permutation_cons_app.
apply IHl.
- apply permut_remove_hd with a; auto.
+ apply permut_remove_hd with a; auto with typeclass_instances.
Qed.
(** Permutation for short lists. *)
@@ -160,12 +150,12 @@ Section Perm.
Lemma permut_length_1:
forall a b, permutation (a :: nil) (b :: nil) -> a=b.
Proof.
- intros a b; unfold Permutation.permutation, meq; intro P;
+ intros a b; unfold PermutSetoid.permutation, meq; intro P;
generalize (P b); clear P; simpl.
destruct (eq_dec b b) as [H|H]; [ | destruct H; auto].
destruct (eq_dec a b); simpl; auto; intros; discriminate.
Qed.
-
+
Lemma permut_length_2 :
forall a1 b1 a2 b2, permutation (a1 :: b1 :: nil) (a2 :: b2 :: nil) ->
(a1=a2) /\ (b1=b2) \/ (a1=b2) /\ (a2=b1).
@@ -177,7 +167,7 @@ Section Perm.
apply permut_length_1.
red; red; intros.
generalize (P a); clear P; simpl.
- destruct (eq_dec a1 a) as [H2|H2];
+ destruct (eq_dec a1 a) as [H2|H2];
destruct (eq_dec a2 a) as [H3|H3]; auto.
destruct H3; transitivity a1; auto.
destruct H2; transitivity a2; auto.
@@ -187,7 +177,7 @@ Section Perm.
apply permut_length_1.
red; red; intros.
generalize (P a); clear P; simpl.
- destruct (eq_dec a1 a) as [H2|H2];
+ destruct (eq_dec a1 a) as [H2|H2];
destruct (eq_dec b2 a) as [H3|H3]; auto.
simpl; rewrite <- plus_n_Sm; inversion 1; auto.
destruct H3; transitivity a1; auto.
@@ -206,17 +196,17 @@ Section Perm.
simpl; rewrite <- plus_n_Sm; f_equal.
rewrite <- app_length.
apply IHl1.
- apply permut_remove_hd with a; auto.
+ apply permut_remove_hd with a; auto with typeclass_instances.
Qed.
Variable B : Type.
- Variable eqB_dec : forall x y:B, { x=y }+{ ~x=y }.
+ Variable eqB_dec : forall x y:B, { x=y }+{ ~x=y }.
(** Permutation is compatible with map. *)
Lemma permutation_map :
- forall f l1 l2, permutation l1 l2 ->
- Permutation.permutation _ eqB_dec (map f l1) (map f l2).
+ forall f l1 l2, permutation l1 l2 ->
+ PermutSetoid.permutation _ eqB_dec (map f l1) (map f l2).
Proof.
intros f; induction l1.
intros l2 P; rewrite (permut_nil (permut_sym P)); apply permut_refl.
@@ -229,7 +219,7 @@ Section Perm.
apply permut_add_cons_inside.
rewrite <- map_app.
apply IHl1; auto.
- apply permut_remove_hd with a; auto.
+ apply permut_remove_hd with a; auto with typeclass_instances.
Qed.
End Perm.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 06:47:58 +0000