Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: bug5778.v Sprache: Coq

Original von: Coq^©

(************************************************************************)
(*         *   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.18 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.