|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \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) *)
(************************************************************************)
Require Import Relations Setoid SetoidList List Multiset PermutSetoid Permutation Omega.
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 [Permutation.Permutation] and
[PermutSetoid.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 :
forall l a, In a l <-> 0 < multiplicity (list_contents l) a.
Proof.
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;
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 :
forall l, NoDup l <-> (forall a, multiplicity (list_contents l) a <= 1).
Proof.
induction l.
simpl.
split; auto with arith.
intros; apply NoDup_nil.
split; simpl.
inversion_clear 1.
rewrite IHl in H1.
intros; destruct (eq_dec a a0) as [H2|H2]; simpl; auto.
subst a0.
rewrite multiplicity_In_O; auto.
intros; constructor.
rewrite multiplicity_In.
generalize (H a).
destruct (eq_dec a a) as [H0|H0].
destruct (multiplicity (list_contents l) a); auto with arith.
simpl; inversion 1.
inversion H3.
destruct H0; auto.
rewrite IHl; intros.
generalize (H a0); auto with arith.
destruct (eq_dec a a0); simpl; auto with arith.
Qed.
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.
generalize (H a) (H0 a) (H1 a); clear H H0 H1.
do 2 rewrite multiplicity_In.
destruct 3; omega.
Qed.
(** Permutation is compatible with In. *)
Lemma permut_In_In :
forall l1 l2 e, permutation l1 l2 -> In e l1 -> In e l2.
Proof.
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).
intros.
generalize (multiplicity_In_S _ _ IN).
rewrite H0.
inversion 1.
Qed.
Lemma permut_cons_In :
forall l1 l2 e, permutation (e :: l1) l2 -> In e l2.
Proof.
intros; eapply permut_In_In; eauto.
red; auto.
Qed.
(** Permutation of an empty list. *)
Lemma permut_nil :
forall l, permutation l nil -> l = nil.
Proof.
intro l; destruct l as [ | e l ]; trivial.
assert (In e (e::l)) by (red; auto).
intro Abs; generalize (permut_In_In _ Abs H).
inversion 1.
Qed.
(** When used with [eq], this permutation notion is equivalent to
the one defined in [List.v]. *)
Lemma permutation_Permutation :
forall l l', Permutation l l' <-> permutation l l'.
Proof.
split.
induction 1.
apply permut_refl.
apply permut_cons; auto.
change (permutation (y::x::l) ((x::nil)++y::l)).
apply permut_add_cons_inside; simpl; apply permut_refl.
apply permut_trans with l'; auto.
revert l'.
induction l.
intros.
rewrite (permut_nil (permut_sym H)).
apply Permutation_refl.
intros.
destruct (In_split _ _ (permut_cons_In H)) as (h2,(t2,H1)).
subst l'.
apply Permutation_cons_app.
apply IHl.
apply permut_remove_hd with a; auto with typeclass_instances.
Qed.
(** Permutation for short lists. *)
Lemma permut_length_1:
forall a b, permutation (a :: nil) (b :: nil) -> a=b.
Proof.
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).
Proof.
intros a1 b1 a2 b2 P.
assert (H:=permut_cons_In P).
inversion_clear H.
left; split; auto.
apply permut_length_1.
red; red; intros.
generalize (P a); clear P; simpl.
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.
right.
inversion_clear H0; [|inversion H].
split; auto.
apply permut_length_1.
red; red; intros.
generalize (P a); clear P; simpl.
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.
destruct H2; transitivity b2; auto.
Qed.
(** Permutation is compatible with length. *)
Lemma permut_length :
forall l1 l2, permutation l1 l2 -> length l1 = length l2.
Proof.
induction l1; intros l2 H.
rewrite (permut_nil (permut_sym H)); auto.
destruct (In_split _ _ (permut_cons_In H)) as (h2,(t2,H1)).
subst l2.
rewrite app_length.
simpl; rewrite <- plus_n_Sm; f_equal.
rewrite <- app_length.
apply IHl1.
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 }.
(** Permutation is compatible with map. *)
Lemma permutation_map :
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.
intros l2 P.
simpl.
destruct (In_split _ _ (permut_cons_In P)) as (h2,(t2,H1)).
subst l2.
rewrite map_app.
simpl.
apply permut_add_cons_inside.
rewrite <- map_app.
apply IHl1; auto.
apply permut_remove_hd with a; auto with typeclass_instances.
Qed.
End Perm.
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
