Library Coq.Sets.Multiset



Require Import Permut Setoid.
Require Plus.
Set Implicit Arguments.

Section multiset_defs.

  Variable A : Type.
  Variable eqA : A -> A -> Prop.
  Hypothesis eqA_equiv : Equivalence eqA.
  Hypothesis Aeq_dec : forall x y:A, {eqA x y} + {~ eqA x y}.

  Inductive multiset : Type :=
    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.

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

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

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).

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

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

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

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

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

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)).

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

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

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

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

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).

  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).

SingletonBag

  Lemma meq_singleton : forall a a',
    eqA a a' -> meq (SingletonBag a) (SingletonBag a').


End multiset_defs.

Unset Implicit Arguments.

#[global]
Hint Unfold meq multiplicity: datatypes.
#[global]
Hint Resolve munion_empty_right munion_comm munion_ass meq_left meq_right
  munion_empty_left: datatypes.
#[global]
Hint Immediate meq_sym: datatypes.