Multiset.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   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)         *)
(************************************************************************)

(* G. Huet 1-9-95 *)

Require Import Permut Setoid.
Require Plus. (* comm. and ass. of 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.A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x : multiset, meq x x
  Proof.A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x : multiset, meq x x
    destruct x; unfold meq; reflexivity.
  Qed.

  Lemma meq_trans : forall x y z:multiset, meq x y -> meq y z -> meq x z.A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x y z : multiset, meq x y -> meq y z -> meq x z
  Proof.A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x y z : multiset, meq x y -> meq y z -> meq x z
    unfold meq.A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x y z : multiset,
(forall a : A, multiplicity x a = multiplicity y a) ->
(forall a : A, multiplicity y a = multiplicity z a) ->
forall a : A, multiplicity x a = multiplicity z a
    destruct x; destruct y; destruct z.A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x y : A, {eqA x y} + {~ eqA x y}
n, n0, n1:A -> nat
(forall a : A,
 multiplicity (Bag n) a = multiplicity (Bag n0) a) ->
(forall a : A,
 multiplicity (Bag n0) a = multiplicity (Bag n1) a) ->
forall a : A,
multiplicity (Bag n) a = multiplicity (Bag n1) a
    intros; rewrite H; auto.
  Qed.

  Lemma meq_sym : forall x y:multiset, meq x y -> meq y x.A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x y : multiset, meq x y -> meq y x
  Proof.A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x y : multiset, meq x y -> meq y x
    unfold meq.A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x y : multiset,
(forall a : A, multiplicity x a = multiplicity y a) ->
forall a : A, multiplicity y a = multiplicity x a
    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).A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x : multiset, meq x (munion EmptyBag x)
  Proof.A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x : multiset, meq x (munion EmptyBag x)
    unfold meq; unfold munion; simpl; auto.
  Qed.

  Lemma munion_empty_right : forall x:multiset, meq x (munion x EmptyBag).A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x : multiset, meq x (munion x EmptyBag)
  Proof.A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x : multiset, meq x (munion x EmptyBag)
    unfold meq; unfold munion; simpl; auto.
  Qed.

  Lemma munion_comm : forall x y:multiset, meq (munion x y) (munion y x).A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x y : multiset, meq (munion x y) (munion y x)
  Proof.A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x y : multiset, meq (munion x y) (munion y x)
    unfold meq; unfold multiplicity; unfold munion.A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall (x y : multiset) (a : A),
multiplicity x a + multiplicity y a =
multiplicity y a + multiplicity x a
    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)).A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x y z : multiset,
meq (munion (munion x y) z) (munion x (munion y z))
  Proof.A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x y z : multiset,
meq (munion (munion x y) z) (munion x (munion y z))
    unfold meq; unfold munion; unfold multiplicity.A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall (x y z : multiset) (a : A),
(let (f) := x in f a) + (let (f) := y in f a) +
(let (f) := z in f a) =
(let (f) := x in f a) +
((let (f) := y in f a) + (let (f) := z in f a))
    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).A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x y z : multiset,
meq x y -> meq (munion x z) (munion y z)
  Proof.A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x y z : multiset,
meq x y -> meq (munion x z) (munion y z)
    unfold meq; unfold munion; unfold multiplicity.A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x y z : multiset,
(forall a : A,
 (let (f) := x in f a) = (let (f) := y in f a)) ->
forall a : A,
(let (f) := x in f a) + (let (f) := z in f a) =
(let (f) := y in f a) + (let (f) := z in f a)
    destruct x; destruct y; destruct z.A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x y : A, {eqA x y} + {~ eqA x y}
n, n0, n1:A -> nat
(forall a : A, n a = n0 a) ->
forall a : A, n a + n1 a = n0 a + n1 a
    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).A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x y z : multiset,
meq x y -> meq (munion z x) (munion z y)
  Proof.A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x y z : multiset,
meq x y -> meq (munion z x) (munion z y)
    unfold meq; unfold munion; unfold multiplicity.A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x y z : multiset,
(forall a : A,
 (let (f) := x in f a) = (let (f) := y in f a)) ->
forall a : A,
(let (f) := z in f a) + (let (f) := x in f a) =
(let (f) := z in f a) + (let (f) := y in f a)
    destruct x; destruct y; destruct z.A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x y : A, {eqA x y} + {~ eqA x y}
n, n0, n1:A -> nat
(forall a : A, n a = n0 a) ->
forall a : A, n1 a + n a = n1 a + n0 a
    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)).A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x y z : multiset,
meq (munion x (munion y z)) (munion z (munion x y))
  Proof.A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x y z : multiset,
meq (munion x (munion y z)) (munion z (munion x y))
    intros; apply (op_rotate multiset munion meq).A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
x, y, z:multiset
forall x0 y0 : multiset,
meq (munion x0 y0) (munion y0 x0)
A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
x, y, z:multiset
forall x0 y0 z0 : multiset,
meq (munion (munion x0 y0) z0)
  (munion x0 (munion y0 z0))
A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
x, y, z:multiset
forall x0 y0 z0 : multiset,
meq x0 y0 -> meq y0 z0 -> meq x0 z0
A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
x, y, z:multiset
forall x0 y0 : multiset, meq x0 y0 -> meq y0 x0
A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
x, y, z:multiset
multiset
      apply munion_comm.A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
x, y, z:multiset
forall x0 y0 z0 : multiset,
meq (munion (munion x0 y0) z0)
  (munion x0 (munion y0 z0))
A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
x, y, z:multiset
forall x0 y0 z0 : multiset,
meq x0 y0 -> meq y0 z0 -> meq x0 z0
A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
x, y, z:multiset
forall x0 y0 : multiset, meq x0 y0 -> meq y0 x0
A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
x, y, z:multiset
multiset
      apply munion_ass.A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
x, y, z:multiset
forall x0 y0 z0 : multiset,
meq x0 y0 -> meq y0 z0 -> meq x0 z0
A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
x, y, z:multiset
forall x0 y0 : multiset, meq x0 y0 -> meq y0 x0
A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
x, y, z:multiset
multiset
      exact meq_trans.A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
x, y, z:multiset
forall x0 y0 : multiset, meq x0 y0 -> meq y0 x0
A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
x, y, z:multiset
multiset
      exact meq_sym.A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
x, y, z:multiset
multiset
      trivial.
  Qed.

  Lemma meq_congr :
    forall x y z t:multiset, meq x y -> meq z t -> meq (munion x z) (munion y t).A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x y z t : multiset,
meq x y -> meq z t -> meq (munion x z) (munion y t)
  Proof.A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x y z t : multiset,
meq x y -> meq z t -> meq (munion x z) (munion y t)
    intros; apply (cong_congr multiset munion meq); auto using meq_left, meq_right.A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
x, y, z, t:multiset
H:meq x y
H0:meq z t
forall x0 y0 z0 : multiset,
meq x0 y0 -> meq y0 z0 -> meq x0 z0
      exact meq_trans.
  Qed.

  Lemma munion_perm_left :
    forall x y z:multiset, meq (munion x (munion y z)) (munion y (munion x z)).A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x y z : multiset,
meq (munion x (munion y z)) (munion y (munion x z))
  Proof.A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x y z : multiset,
meq (munion x (munion y z)) (munion y (munion x z))
    intros; apply (perm_left multiset munion meq); auto using munion_comm, munion_ass, meq_left, meq_right, meq_sym.A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
x, y, z:multiset
forall x0 y0 z0 : multiset,
meq x0 y0 -> meq y0 z0 -> meq x0 z0
      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).A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x y z t : multiset,
meq (munion x (munion (munion y z) t))
  (munion (munion y (munion x t)) z)
  Proof.A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x y z t : multiset,
meq (munion x (munion (munion y z) t))
  (munion (munion y (munion x t)) z)
    intros; apply (twist multiset munion meq); auto using munion_comm, munion_ass, meq_sym, meq_left, meq_right.A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
x, y, z, t:multiset
forall x0 y0 z0 : multiset,
meq x0 y0 -> meq y0 z0 -> meq x0 z0
    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).A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x y z t : multiset,
meq (munion x (munion (munion y z) t))
  (munion (munion y (munion x z)) t)
  Proof.A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall x y z t : multiset,
meq (munion x (munion (munion y z) t))
  (munion (munion y (munion x z)) t)
    intros; apply meq_trans with (munion (munion x (munion y z)) t).A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
x, y, z, t:multiset
meq (munion x (munion (munion y z) t))
  (munion (munion x (munion y z)) t)
A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
x, y, z, t:multiset
meq (munion (munion x (munion y z)) t)
  (munion (munion y (munion x z)) t)
    apply meq_sym; apply munion_ass.A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
x, y, z, t:multiset
meq (munion (munion x (munion y z)) t)
  (munion (munion y (munion x z)) t)
    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).A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x y : A, {eqA x y} + {~ eqA x y}
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.A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x y : A, {eqA x y} + {~ eqA x y}
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)
    intros; apply meq_trans with (munion x (munion (munion y z) t)).A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
x, y, z, t, u:multiset
H:meq u (munion y z)
meq (munion x (munion u t))
  (munion x (munion (munion y z) t))
A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
x, y, z, t, u:multiset
H:meq u (munion y z)
meq (munion x (munion (munion y z) t))
  (munion (munion y (munion x t)) z)
    apply meq_right; apply meq_left; trivial.A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
x, y, z, t, u:multiset
H:meq u (munion y z)
meq (munion x (munion (munion y z) t))
  (munion (munion y (munion x t)) z)
    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).A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x y : A, {eqA x y} + {~ eqA x y}
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.A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x y : A, {eqA x y} + {~ eqA x y}
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)
    intros; apply meq_trans with (munion x (munion (munion y z) t)).A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
x, y, z, t, u:multiset
H:meq u (munion y z)
meq (munion x (munion u t))
  (munion x (munion (munion y z) t))
A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
x, y, z, t, u:multiset
H:meq u (munion y z)
meq (munion x (munion (munion y z) t))
  (munion (munion y (munion x z)) t)
    apply meq_right; apply meq_left; trivial.A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x0 y0 : A,
{eqA x0 y0} + {~ eqA x0 y0}
x, y, z, t, u:multiset
H:meq u (munion y z)
meq (munion x (munion (munion y z) t))
  (munion (munion y (munion x z)) t)
    apply multiset_twist2.
  Qed.

SingletonBag

  Lemma meq_singleton : forall a a',
    eqA a a' -> meq (SingletonBag a) (SingletonBag a').A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall a a' : A,
eqA a a' -> meq (SingletonBag a) (SingletonBag a')
  Proof.A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x y : A, {eqA x y} + {~ eqA x y}
forall a a' : A,
eqA a a' -> meq (SingletonBag a) (SingletonBag a')
    intros; red; simpl; intro a0.A:Type
eqA:A -> A -> Prop
eqA_equiv:Equivalence eqA
Aeq_dec:forall x y : A, {eqA x y} + {~ eqA x y}
a, a':A
H:eqA a a'
a0:A
(if Aeq_dec a a0 then 1 else 0) =
(if Aeq_dec a' a0 then 1 else 0)
    destruct (Aeq_dec a a0) as [Ha|Ha]; rewrite H in Ha;
      decide (Aeq_dec a' a0) with Ha; reflexivity.
  Qed.

(*i theory of minter to do similarly
Require Min.
(* multiset intersection *)
Definition minter := [m1,m2:multiset]
    (Bag [a:A](min (multiplicity m1 a)(multiplicity m2 a))).
i*)

End multiset_defs.

Unset Implicit Arguments.

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