Library Coq.Sets.Multiset


Require Import Permut.




Set Implicit Arguments.




Section multiset_defs.




  Variable A : Set.

  Variable eqA : A -> A -> Prop.

  Hypothesis Aeq_dec : forall x y:A, {eqA x y} + {~ eqA x y}.




  Inductive multiset : Set :=

    Bag : (A -> nat) -> multiset.




  Definition EmptyBag := Bag (fun a:A => 0).

  Definition SingletonBag (a:A) :=

    Bag (fun a':A => match Aeq_dec a a' with

                       | left _ => 1

                       | right _ => 0

                     end).




  Definition multiplicity (m:multiset) (a:A) : nat := let (f) := m in f a.

multiset equality


  Definition meq (m1 m2:multiset) :=

    forall a:A, multiplicity m1 a = multiplicity m2 a.




  Lemma meq_refl : forall x:multiset, meq x x.

  Proof.

    destruct x; unfold meq; reflexivity.

  Qed.




  Lemma meq_trans : forall x y z:multiset, meq x y -> meq y z -> meq x z.

  Proof.

    unfold meq in |- *.

    destruct x; destruct y; destruct z.

    intros; rewrite H; auto.

  Qed.




  Lemma meq_sym : forall x y:multiset, meq x y -> meq y x.

  Proof.

    unfold meq in |- *.

    destruct x; destruct y; auto.

  Qed.

multiset union


  Definition munion (m1 m2:multiset) :=

    Bag (fun a:A => multiplicity m1 a + multiplicity m2 a).




  Lemma munion_empty_left : forall x:multiset, meq x (munion EmptyBag x).

  Proof.

    unfold meq in |- *; unfold munion in |- *; simpl in |- *; auto.

  Qed.




  Lemma munion_empty_right : forall x:multiset, meq x (munion x EmptyBag).

  Proof.

    unfold meq in |- *; unfold munion in |- *; simpl in |- *; auto.

  Qed.




  Require Plus. 




  Lemma munion_comm : forall x y:multiset, meq (munion x y) (munion y x).

  Proof.

    unfold meq in |- *; unfold multiplicity in |- *; unfold munion in |- *.

    destruct x; destruct y; auto with arith.

  Qed.




  Lemma munion_ass :

    forall x y z:multiset, meq (munion (munion x y) z) (munion x (munion y z)).

  Proof.

    unfold meq in |- *; unfold munion in |- *; unfold multiplicity in |- *.

    destruct x; destruct y; destruct z; auto with arith.

  Qed.




  Lemma meq_left :

    forall x y z:multiset, meq x y -> meq (munion x z) (munion y z).

  Proof.

    unfold meq in |- *; unfold munion in |- *; unfold multiplicity in |- *.

    destruct x; destruct y; destruct z.

    intros; elim H; auto with arith.

  Qed.




  Lemma meq_right :

    forall x y z:multiset, meq x y -> meq (munion z x) (munion z y).

  Proof.

    unfold meq in |- *; unfold munion in |- *; unfold multiplicity in |- *.

    destruct x; destruct y; destruct z.

    intros; elim H; auto.

  Qed.

Here we should make multiset an abstract datatype, by hiding Bag, munion, multiplicity; all further properties are proved abstractly





  Lemma munion_rotate :

    forall x y z:multiset, meq (munion x (munion y z)) (munion z (munion x y)).

  Proof.

    intros; apply (op_rotate multiset munion meq).

      apply munion_comm.

      apply munion_ass.

      exact meq_trans.

      exact meq_sym.

      trivial.

  Qed.




  Lemma meq_congr :

    forall x y z t:multiset, meq x y -> meq z t -> meq (munion x z) (munion y t).

  Proof.

    intros; apply (cong_congr multiset munion meq); auto using meq_left, meq_right.

      exact meq_trans.

  Qed.




  Lemma munion_perm_left :

    forall x y z:multiset, meq (munion x (munion y z)) (munion y (munion x z)).

  Proof.

    intros; apply (perm_left multiset munion meq); auto using munion_comm, munion_ass, meq_left, meq_right, meq_sym.

      exact meq_trans.

  Qed.




  Lemma multiset_twist1 :

    forall x y z t:multiset,

      meq (munion x (munion (munion y z) t)) (munion (munion y (munion x t)) z).

  Proof.

    intros; apply (twist multiset munion meq); auto using munion_comm, munion_ass, meq_sym, meq_left, meq_right.

    exact meq_trans.

  Qed.




  Lemma multiset_twist2 :

    forall x y z t:multiset,

      meq (munion x (munion (munion y z) t)) (munion (munion y (munion x z)) t).

  Proof.

    intros; apply meq_trans with (munion (munion x (munion y z)) t).

    apply meq_sym; apply munion_ass.

    apply meq_left; apply munion_perm_left.

  Qed.

specific for treesort





  Lemma treesort_twist1 :

    forall x y z t u:multiset,

      meq u (munion y z) ->

      meq (munion x (munion u t)) (munion (munion y (munion x t)) z).

  Proof.

    intros; apply meq_trans with (munion x (munion (munion y z) t)).

    apply meq_right; apply meq_left; trivial.

    apply multiset_twist1.

  Qed.




  Lemma treesort_twist2 :

    forall x y z t u:multiset,

      meq u (munion y z) ->

      meq (munion x (munion u t)) (munion (munion y (munion x z)) t).

  Proof.

    intros; apply meq_trans with (munion x (munion (munion y z) t)).

    apply meq_right; apply meq_left; trivial.

    apply multiset_twist2.

  Qed.




End multiset_defs.




Unset Implicit Arguments.




Hint Unfold meq multiplicity: v62 datatypes.

Hint Resolve munion_empty_right munion_comm munion_ass meq_left meq_right

  munion_empty_left: v62 datatypes.

Hint Immediate meq_sym: v62 datatypes.