(****************************************************************
   File: multiset.v                                                 
   Authors: Amy Felty
   Version: Coq V8.4pl2
   Date: January 2014
                                                                 
   A version of multisets built on lists (that doesn't require
   decidable equality).

   Adhoc for now.  Need to replace the permutation lemmas with a
   tactic to automate proofs of equality between multisets.
  ***************************************************************)

Require Export Omega.
Require Export List.
Require Export Setoid.
Require Export SetoidPermutation.
Require Export Relation_Definitions.

Set Implicit Arguments.

Section multiset.

Variable A:Type.
Variable eqA:A -> A -> Prop.
Hypothesis eqA_refl: forall t:A, eqA t t.
Hypothesis eqA_symm: forall (t1 t2:A), eqA t1 t2 -> eqA t2 t1.
Hypothesis eqA_trans:
  forall (t1 t2 t3:A), eqA t1 t2 -> eqA t2 t3 -> eqA t1 t3.

Add Parametric Relation : A eqA
  reflexivity proved by eqA_refl
  symmetry proved by eqA_symm
  transitivity proved by eqA_trans as Aeq.

Definition multiset := list A.

Definition mnil : multiset := nil.

Inductive mcount : A -> multiset -> nat -> Prop :=
   | mc_0 : forall (a:A), mcount a mnil 0
   | mc_plus0 : forall (a b:A) (m:multiset) (i:nat),
                  ~(eqA a b) -> mcount a m i -> mcount a (b::m) i
   | mc_plus1 : forall (a b:A) (m:multiset) (i:nat),
                  (eqA a b) -> mcount a m i -> mcount a (b::m) (i+1).

Definition ms_eq (m n:multiset) : Prop :=
  forall (a:A) (i:nat), (mcount a m i <-> mcount a n i).

Hint Resolve mc_0 mc_plus0 mc_plus1.

Lemma ms_eq_refl : forall (m:multiset), ms_eq m m.
Proof.
induction m.
unfold ms_eq; simpl; tauto.
unfold ms_eq in IHm.
unfold ms_eq; simpl; intros b i; subst; split; inversion_clear 1; auto.
Qed.

Lemma ms_eq_symm : forall (m n:multiset), ms_eq m n -> ms_eq n m.
Proof.
unfold ms_eq.
intros m n h a i.
split; intro h1.
generalize h; clear h.
inversion_clear 0; intro h; apply h; auto.
generalize h; clear h.
inversion_clear 0; intro h; apply h; auto.
Qed.

Lemma ms_eq_trans :
  forall (m n p:multiset), ms_eq m n -> ms_eq n p -> ms_eq m p.
Proof.
unfold ms_eq.
intros m n p h1 h2 a i.
split; intro h3.
generalize h1 h2; clear h1 h2.
inversion_clear 0; intros h1 h2; apply h2; apply h1; auto.
generalize h1 h2; clear h1 h2.
inversion_clear 0; intros h1 h2; apply h1; apply h2; auto.
Qed.

Hint Resolve ms_eq_refl ms_eq_symm ms_eq_trans.

Add Parametric Relation : multiset ms_eq
  reflexivity proved by ms_eq_refl
  symmetry proved by ms_eq_symm
  transitivity proved by ms_eq_trans as eq_ms.

Definition madd (a:A) (m:multiset) := (a::m).

Lemma madd_compat:
  forall (a b:A) (m n:multiset), eqA a b -> ms_eq m n ->
  ms_eq (madd a m) (madd b n).
Proof.
unfold madd,ms_eq.
intros a b m n h1 h2 a0 i.
split; intro h3.
inversion_clear 0.
assert (h3:~(eqA a0 b)).
rewrite h1 in H; auto.
apply mc_plus0; auto.
apply h2; auto.
rewrite h1 in H.
apply mc_plus1; auto.
apply h2; auto.
inversion_clear 0.
assert (h3:~(eqA a0 a)).
rewrite <- h1 in H; auto.
apply mc_plus0; auto.
apply h2; auto.
rewrite <- h1 in H.
apply mc_plus1; auto.
apply h2; auto.
Qed.

Add Parametric Morphism : madd with
  signature eqA ==> ms_eq ==> ms_eq as madd_mor.
Proof.
intros; apply madd_compat; auto.
Qed.

Definition msingl (a:A) := madd a mnil.

Lemma msingl_compat:
  forall (a b:A), eqA a b -> ms_eq (msingl a) (msingl b).
Proof.
unfold msingl.
intros a b h1.
rewrite h1; auto.
Qed.

Add Parametric Morphism : msingl with
  signature eqA ==> ms_eq as msingl_mor.
Proof.
exact msingl_compat.
Qed.

Definition munion (m n:multiset) := m ++ n.

Lemma munion_mcount : forall (a:A) (m n:multiset) (i j:nat),
  mcount a m i -> mcount a n j -> mcount a (munion m n) (i+j).
Proof.
intros a m n i j h.
generalize h n j; clear n j h.
induction 1.
simpl; auto.
simpl; intros n j h1; auto.
simpl; intros n j h1.
replace (i+1+j) with (i+j+1); try omega.
auto.
Qed.

Hint Resolve munion_mcount.

Lemma munion_mnil : forall (m n:multiset),
  mnil = munion m n -> m = mnil /\ n = mnil.
Proof.
unfold munion,mnil.
induction m.
simpl; auto.
intros n h.
simpl in h.
discriminate h.
Qed.

Hint Resolve munion_mnil.

Lemma mcount_munion : forall (m n:multiset) (a:A) (i:nat),
  mcount a (munion m n) i ->
  exists (j k:nat), mcount a m j /\ mcount a n k /\ i = j+k.
Proof.
unfold munion.
induction m; simpl.
intros n a i h; exists 0; exists i; repeat split; auto.
simpl; intros n a0 i h.
inversion_clear 0.
specialize IHm with (1:=H0); destruct IHm as [j [k [h1 [h2 h3]]]]; subst.
exists j; exists k; repeat split; auto.
specialize IHm with (1:=H0); destruct IHm as [j [k [h1 [h2 h3]]]]; subst.
exists (j+1); exists k; repeat split; auto; omega.
Qed.

Lemma munion_compat: forall (m1 n1:multiset), ms_eq m1 n1 ->
  forall (m2 n2:multiset), ms_eq m2 n2 -> ms_eq (munion m1 m2) (munion n1 n2).
Proof.
unfold ms_eq.
intros m1 n1 h.
assert (h1:forall (a:A)(i:nat), mcount a m1 i -> mcount a n1 i).
intros; apply h; auto.
assert (h2:forall (a:A)(i:nat), mcount a n1 i -> mcount a m1 i).
intros; apply h; auto.
clear h.
intros m2 n2 h.
assert (h3:forall (a:A)(i:nat), mcount a m2 i -> mcount a n2 i).
intros; apply h; auto.
assert (h4:forall (a:A)(i:nat), mcount a n2 i -> mcount a m2 i).
intros; apply h; auto.
clear h.
intros a i; split; intro h5.
specialize mcount_munion with (1:=h5); intros [j [k [h6 [h7 h8]]]]; subst; auto.
specialize mcount_munion with (1:=h5); intros [j [k [h6 [h7 h8]]]]; subst; auto.
Qed.

Add Parametric Morphism : munion with
  signature ms_eq ==> ms_eq ==> ms_eq as munion_mor.
Proof.
exact munion_compat.
Qed.

Definition mset_mem (a:A) (m:multiset) : Prop := In a m.

Definition ms_dec (a b:A) := (eqA a b) \/ ~(eqA a b).
Definition ms_dec3 (a b c:A) :=
  (ms_dec a b) /\ (ms_dec a c) /\ (ms_dec b c).
Definition ms_dec4 (a b c d:A) :=
  (ms_dec a b) /\ (ms_dec a c) /\ (ms_dec a d) /\ (ms_dec3 b c d).

Lemma ms_eq_cons: forall (a:A) (m n:multiset),
  ms_eq m n -> ms_eq (a::m) (a::n).
Proof.
intros a m n h.
rewrite h; auto.
Qed.

Hint Resolve ms_eq_cons.

Lemma ms_perm21 : forall (a1 a2:A) (m:multiset), ms_dec a1 a2 ->
  ms_eq (a1::a2::m) (a2::a1::m).
Proof.
intros a1 a2 m h.
change (ms_eq (munion (madd a1 (madd a2 nil)) m)
              (munion (madd a2 (madd a1 nil)) m)).
apply munion_compat; auto.
destruct h as [h1 | h1]; simpl.
rewrite h1; auto.
intros a i; split; intro h2; simpl.
inversion_clear 0; auto; inversion_clear H0; auto.
inversion_clear h2; auto; inversion_clear H0; auto.
Qed.

Hint Resolve ms_perm21.

Definition ms_perm := PermutationA eqA.

Definition ms_all_dec (m n:multiset) := 
  forall (a b:A), (In a m \/ In a n) -> (In b m \/ In b n) -> ms_dec a b.

Lemma ms_perm312 : forall (a1 a2 a3:A) (m:multiset), ms_dec3 a1 a2 a3 ->
  ms_eq (a1::a2::a3::m) (a3::a1::a2::m).
Proof.
intros a1 a2 a3 m [h1 [h2 h3]]; simpl.
change (ms_eq (munion (madd a1 (madd a2 (madd a3 nil))) m)
              (munion (madd a3 (madd a1 (madd a2 nil))) m)).
apply munion_compat; auto.
destruct h1 as [h1 | h1]; destruct h2 as [h2 | h2]; destruct h3 as [h3 | h3];
  simpl;
  intros a i; split; intro h4; simpl;
  inversion_clear h4; auto; inversion_clear H0; auto;
  inversion_clear H2; auto; inversion_clear H2; auto.
Qed.

Hint Resolve ms_perm312.

Lemma ms_perm321 : forall (a1 a2 a3:A) (m:multiset), ms_dec3 a1 a2 a3 ->
  ms_eq (a1::a2::a3::m) (a3::a2::a1::m).
Proof.
intros a1 a2 a3 m [h1 [h2 h3]]; simpl.
change (ms_eq (munion (madd a1 (madd a2 (madd a3 nil))) m)
              (munion (madd a3 (madd a2 (madd a1 nil))) m)).
apply munion_compat; auto.
destruct h1 as [h1 | h1]; destruct h2 as [h2 | h2]; destruct h3 as [h3 | h3];
  simpl;
  intros a i; split; intro h4; simpl;
  inversion_clear h4; auto; inversion_clear H0; auto;
  inversion_clear H2; auto; inversion_clear H2; auto.
Qed.

Hint Resolve ms_perm321.

Lemma ms_perm231 : forall (a1 a2 a3:A) (m:multiset), ms_dec3 a1 a2 a3 ->
  ms_eq (a1::a2::a3::m) (a2::a3::a1::m).
Proof.
intros a1 a2 a3 m [h1 [h2 h3]]; simpl.
change (ms_eq (munion (madd a1 (madd a2 (madd a3 nil))) m)
              (munion (madd a2 (madd a3 (madd a1 nil))) m)).
apply munion_compat; auto.
destruct h1 as [h1 | h1]; destruct h2 as [h2 | h2]; destruct h3 as [h3 | h3];
  simpl;
  intros a i; split; intro h4; simpl;
  inversion_clear h4; auto; inversion_clear H0; auto;
  inversion_clear H2; auto; inversion_clear H2; auto.
Qed.

Hint Resolve ms_perm231.

Lemma ms_perm4231 : forall (a1 a2 a3 a4:A) (m:multiset), ms_dec3 a1 a3 a4 ->
  ms_eq (a1::a2::a3::a4::m) (a4::a2::a3::a1::m).
Proof.
intros a1 a2 a3 a4 m [h1 [h2 h3]]; simpl.
change (ms_eq (munion (madd a1 (madd a2 (madd a3 (madd a4 nil)))) m)
              (munion (madd a4 (madd a2 (madd a3 (madd a1 nil)))) m)).
apply munion_compat; auto.
destruct h1 as [h1 | h1]; destruct h2 as [h2 | h2]; destruct h3 as [h3 | h3];
  simpl;
  intros a i; split; intro h4; simpl;
  inversion_clear h4; auto; inversion_clear H0; auto;
  inversion_clear H2; auto; inversion_clear H3; auto.
Qed.

Hint Resolve ms_perm4231.

Lemma ms_perm3412 : forall (a1 a2 a3 a4:A) (m:multiset), ms_dec4 a1 a2 a3 a4 ->
  ms_eq (a1::a2::a3::a4::m) (a3::a4::a1::a2::m).
Proof.
intros a1 a2 a3 a4 m [h1 [h2 [h3 [h4 [h5 h6]]]]]; simpl.
change (ms_eq (munion (madd a1 (madd a2 (madd a3 (madd a4 nil)))) m)
              (munion (madd a3 (madd a4 (madd a1 (madd a2 nil)))) m)).
apply munion_compat; auto.
destruct h5 as [h5 | h5]; try rewrite h5; auto.
apply ms_perm321; auto.
assert (h:ms_dec a4 a3).
unfold ms_dec in *. 
destruct h6 as [h6 | h6].
left; auto.
right; auto.
unfold ms_dec3,ms_dec in *; auto.
destruct h2 as [h2 | h2]; try rewrite h2; auto.
apply ms_eq_cons; auto.
destruct h4 as [h4 | h4]; destruct h6 as [h6 | h6];
 simpl;
 intros a i; split; intro h7; simpl;
 inversion_clear h7; auto; inversion_clear H0; auto;
 inversion_clear H2; auto; inversion_clear H3; auto.
destruct h1 as [h1 | h1]; destruct h3 as [h3 | h3];
 destruct h4 as [h4 | h4]; destruct h6 as [h6 | h6];
 simpl;
 intros a i; split; intro h7; simpl;
 inversion_clear h7; auto; inversion_clear H0; auto;
 inversion_clear H2; auto; inversion_clear H3; auto.
Qed.

Hint Resolve ms_perm4231.

Lemma ms_perm4312 : forall (a1 a2 a3 a4:A) (m:multiset), ms_dec4 a1 a2 a3 a4 ->
  ms_eq (a1::a2::a3::a4::m) (a4::a3::a1::a2::m).
Proof.
intros a1 a2 a3 a4 m [h1 [h2 [h3 [h4 [h5 h6]]]]]; simpl.
change (ms_eq (munion (madd a1 (madd a2 (madd a3 (madd a4 nil)))) m)
              (munion (madd a4 (madd a3 (madd a1 (madd a2 nil)))) m)).
apply munion_compat; auto.
destruct h5 as [h5 | h5]; try rewrite h5; auto.
apply ms_perm231; auto.
assert (h:ms_dec a4 a3).
unfold ms_dec in *. 
destruct h6 as [h6 | h6].
left; auto.
right; auto.
unfold ms_dec3,ms_dec in *; auto.
destruct h3 as [h3 | h3]; try rewrite h3; auto.
apply ms_eq_cons; auto.
destruct h4 as [h4 | h4]; destruct h6 as [h6 | h6];
 simpl;
 intros a i; split; intro h7; simpl;
 inversion_clear h7; auto; inversion_clear H0; auto;
 inversion_clear H2; auto; inversion_clear H3; auto.
destruct h1 as [h1 | h1]; destruct h2 as [h2 | h2];
 destruct h4 as [h4 | h4]; destruct h6 as [h6 | h6];
 simpl;
 intros a i; split; intro h7; simpl;
 inversion_clear h7; auto; inversion_clear H0; auto;
 inversion_clear H2; auto; inversion_clear H3; auto.
Qed.

Hint Resolve ms_perm4312.

End multiset.