Library BioFLL.LL.Multisets

Require Export Permutation.
Require Export Coq.Relations.Relations.
Require Export Coq.Classes.Morphisms.
Require Export Coq.Setoids.Setoid.
Require Export Coq.Sorting.PermutSetoid.
Require Export Coq.Sets.Multiset.
Require Export List.
Require Export Omega.
Require Export LL.Eqset.
Export ListNotations.

Module Type MultisetList (EQ : Eqset_dec).

  Import EQ.

  Fixpoint removeElem (el: A) (l: list A) : list A :=
    match l with
    | nil ⇒ nil
    | hd::tl ⇒
      match eqA_dec el hd with
      | left _ ⇒ tl
      | right _ ⇒ hd::removeElem el tl
      end
    end.

  Fixpoint removeAll (l m: list A) : list A :=
    match m with
    | nil ⇒ l
    | hd::tl ⇒ removeAll (removeElem hd l) tl
    end.

  Lemma removeElem_length_in : ∀ a l, (∃ a', a = a' ∧ In a' l) →
                                           length (removeElem a l) = pred (length l).

  Proof.
    induction l; intros; destruct H as [b [ab bl]]; inversion bl.
    simpl; destruct (eqA_dec a a0); trivial.
    absurd (a = a0); trivial.
    rewrite H; trivial.
    simpl; destruct (eqA_dec a a0); trivial.
    simpl; rewrite IHl; trivial.
    destruct l; auto.
    contradiction.
    ∃ b; split; trivial.
  Qed.

  Definition Multiset := list A.

  Definition empty : Multiset := nil.
  Definition singleton a : Multiset := a :: nil.
  Definition union := app (A:=A).
  Definition mult := count_occ eqA_dec.
  Definition meq X Y := ∀ a, mult X a = mult Y a.

  Definition rem := removeElem.
  Definition diff := removeAll.

  Definition member x M := mult M x > 0.

  Notation "X =mul= Y" := (meq X Y) (at level 70).
  Notation "X <>mul Y" := (¬meq X Y) (at level 50).
  Notation "X / Y" := (diff X Y) .
  Notation "x # M" := (mult M x)(at level 10).
  Notation "x € M" := (member x M) (at level 10).

  Hint Resolve count_occ_In
       count_occ_not_In
       count_occ_nil
       count_occ_inv_nil
       count_occ_cons_eq
       count_occ_cons_neq.


  Lemma in_countIn : ∀ a l, In a l → a # l > 0.
  Proof.
    intros. apply count_occ_In; auto.
  Qed.

  Lemma empty_empty : ∀ M, (∀ x, x # M = 0) → M = [].
  Proof.
    intros.
    eapply (count_occ_inv_nil eqA_dec); eauto.
  Qed.

  Lemma countIn_nil : ∀ (x : A), x # [] = 0%nat.
  Proof. auto. Qed.

  Lemma countIn_not_In: ∀ x l, ¬ In x l ↔ x # l = 0%nat.
  Proof.
    intros.
    apply count_occ_not_In.
  Qed.

  Theorem countIn_inv_nil : ∀ (l : list A), (∀ x:A, x # l = 0%nat) ↔ l = [].
  Proof.
    intros. apply count_occ_inv_nil.
  Qed.

  Lemma countIn_cons_eq : ∀ (l : list A) (x y : A), y = x → y # (x::l) = S (y # l).
  Proof.
    intros. apply count_occ_cons_eq; auto.
  Qed.

  Lemma countIn_cons_neq : ∀ (l : list A) (x y : A), y ≠ x → y # (x::l) = y # l.
  Proof.
    intros. apply count_occ_cons_neq; auto.
  Qed.

  Lemma countIn_In: ∀ x l, In x l ↔ x # l > 0.
  Proof.
    intros. apply count_occ_In.
  Qed.

  Hint Resolve in_eq
       in_cons
       not_in_cons
       in_nil
       in_split
       in_inv.

  Lemma mult_eqA_compat: ∀ x y M, x = y → x # M = y # M.
  Proof.
    induction M; auto.
    intros.
    intuition. simpl.
    destruct (eqA_dec a x); destruct (eqA_dec a y); auto.
    rewrite H in e. contradiction.
    rewrite <- H in e. contradiction.
  Qed.

  Lemma meq_multeq: ∀ M N, M =mul= N → (∀ x, x # M = x # N).
  Proof. auto. Qed.

  Lemma multeq_meq: ∀ M N, (∀ x, x # M = x # N) → M =mul= N.
  Proof. auto. Qed.

  Lemma diff_empty_l : ∀ M, [] / M = [].
  Proof.
    induction M; auto.
  Qed.

  Lemma diff_empty_r : ∀ M, M / [] = M.
  Proof.
    induction M; auto.
  Qed.

  Lemma empty_mult: ∀ x, x # [] = 0%nat.
  Proof. auto. Qed.

  Lemma union_mult: ∀ x M N, x # (M ++ N) = (x # M + x # N).
  Proof.
    induction M; auto.
    intros; simpl. destruct (eqA_dec a x); auto. rewrite IHM. auto.
  Qed.

  Lemma union_mult2: ∀ x a N, x # (a :: N) = (x # [a] + x # N).
  Proof.
    intros.
    change (a::N) with ([a] ++ N).
    apply union_mult.
  Qed.

  Lemma mult_remove_in : ∀ x a M,
      x = a → (x # (rem a M)) = ((x # M) - 1)%nat.
  Proof.
    induction M; auto.
    intro x_a.
    simpl.
    destruct (eqA_dec a a0); destruct (eqA_dec a0 x); subst.
    auto with arith.
    contradiction.
    contradiction.
    simpl.
    destruct (eqA_dec a0 a); auto.
    contradiction.
  Qed.

  Lemma mult_remove_not_in : ∀ M a x,
      x ≠ a → x # (rem a M) = x # M.

  Proof.
    induction M; intros; auto.
    simpl; destruct (eqA_dec a0 a); subst.
    destruct (eqA_dec x a); auto.
    contradiction.
    destruct (eqA_dec a x); subst; auto.
    contradiction.
    simpl.
    destruct (eqA_dec a x); subst; auto.
  Qed.

  Lemma remove_perm_single : ∀ x a b M,
      x # (rem a (rem b M)) = x # (rem b (rem a M)).
  Proof.
    intros x a b M.
    case (eqA_dec x a); case (eqA_dec x b); intros x_b x_a.
    rewrite !mult_remove_in; trivial.
    rewrite mult_remove_in; trivial.
    do 2 (rewrite mult_remove_not_in; trivial).
    rewrite mult_remove_in; trivial.
    rewrite mult_remove_not_in; trivial.
    do 2 (rewrite mult_remove_in; trivial).
    rewrite mult_remove_not_in; trivial.
    rewrite !mult_remove_not_in; trivial.
  Qed.

  Lemma remove_perm_single' : ∀ a b M,
      (rem a (rem b M)) =mul= (rem b (rem a M)).
  Proof.
    intros.
    apply multeq_meq; intros.
    apply remove_perm_single.
  Qed.

  Lemma diff_mult_comp : ∀ x N M M',
      M =mul= M' → x # (M / N) = x # (M' / N).
  Proof.
    induction N.
    intros; apply meq_multeq; trivial.
    intros M M' MM'.
    simpl.
    apply IHN.
    apply multeq_meq.
    intro x'.
    case (eqA_dec x' a).
    intro xa; rewrite !mult_remove_in; trivial.
    erewrite meq_multeq with (N:=M'); trivial.
    intro xna; rewrite !mult_remove_not_in; trivial.
  Qed.

  Lemma diff_perm_single : ∀ x a b M N,
      x # (M / (a::b::N)) = x # (M / (b::a::N)).

  Proof.
    intros x a b M N.
    simpl; apply diff_mult_comp.
    apply multeq_meq.
    intro x'; apply remove_perm_single.
  Qed.

  Lemma diff_perm : ∀ M N a x,
      x # ((rem a M) / N) = x # (rem a (M / N)).

  Proof.
    intros M N; generalize M; clear M.
    induction N.
    auto.
    intros M b x.
    change (rem b M / (a::N)) with (M / (b::a::N)).
    rewrite diff_perm_single.
    simpl; apply IHN.
  Qed.

  Lemma diff_mult_step_eq : ∀ M N a x,
      x = a → x # (rem a M / N) = (x # (M / N)) - 1%nat.

  Proof.
    intros M N a x x_a.
    rewrite diff_perm.
    rewrite mult_remove_in; trivial.
  Qed.

  Lemma diff_mult_step_neq : ∀ M N a x,
      x ≠ a → x # (rem a M / N) = x # (M / N).

  Proof.
    intros M N a x x_a.
    rewrite diff_perm.
    rewrite mult_remove_not_in; trivial.
  Qed.

  Lemma diff_mult : ∀ M N x,
      x # (M / N) = (x # M) - (x # N).

  Proof.
    induction N.
    simpl; intros; omega.
    intro x; simpl.
    destruct (eqA_dec a x); simpl.
    fold rem.
    rewrite diff_mult_step_eq; auto.
    rewrite (IHN x).
    omega.
    fold rem.
    rewrite diff_mult_step_neq; auto.
  Qed.

  Lemma singleton_mult_in: ∀ x y, y = x → x # [y] = 1%nat.
  Proof. intros. simpl. destruct (eqA_dec y x); [trivial | contradiction]. Qed.

  Lemma singleton_mult_notin: ∀ x y, y ≠ x → x # [y] = 0%nat.
  Proof. intros. simpl. destruct (eqA_dec y x); [ contradiction | trivial]. Qed.

  Hint Unfold meq
       empty
       singleton
       mult
       union
       diff.

  Hint Resolve mult_eqA_compat
       meq_multeq
       multeq_meq
       empty_mult
       union_mult
       diff_mult
       singleton_mult_in
       singleton_mult_notin.

  Hint Rewrite empty_mult
       union_mult
       diff_mult using trivial.



  Lemma rem_to_diff : ∀ a M, rem a M =mul= M / [a].
  Proof. auto. Qed.


  Ltac mset_unfold := repeat progress unfold member.

  Ltac try_solve_meq :=
    (intros;
     match goal with
     | |- _ =mul= _ ⇒
       ( apply multeq_meq
         ; intro
         ; try_solve_meq
       )
     | _ ⇒
       ( mset_unfold ; repeat progress (
                                   
                                   try rewrite !union_mult;
                                   try rewrite diff_mult;
                                   try rewrite countIn_nil
                                 
                                 )
            ; try omega
            ; try congruence
            ; try solve [auto]
       )
     end
    ).

  Ltac solve_meq :=
    (solve [try_solve_meq] ||
     fail "Goal is not an equality between multisets or fails to prove").

  Ltac try_solve_meq_ext :=
    (
      let go x := (solve [clear x; try_solve_meq_ext]) in (
        mset_unfold;
        intros;
        try solve_meq;
        (match goal with
         | H : ?A =mul= ?B |- _ ⇒
           ( (try_solve_meq; rewrite (meq_multeq H); go H)
             || (try_solve_meq; rewrite <- (meq_multeq H); go H)
           )
         | H : ?a = ?b |- _ ⇒
           ( (rewrite (singleton_mult_in H); go H)
             || (rewrite H; go H)
             || (rewrite <- H; go H)
             || (rewrite (mult_eqA_compat H); go H)
             || (rewrite <- (mult_eqA_compat H); go H)
           )
         | H : ?a ≠ ?b |- _ ⇒
           (rewrite (singleton_mult_notin H); go H)
         | |- _ =mul= _ ⇒
           ( apply multeq_meq; try_solve_meq_ext )
         end || try_solve_meq))).

  Ltac solve_meq_ext :=
    (solve [try_solve_meq_ext] ||
     fail "Couldn't show multisets equality").

  Hint Unfold member
       remove.

  Section meq_equivalence.

    Lemma meq_refl : ∀ M, M =mul= M.
    Proof. solve_meq. Qed.

    Lemma meq_sym : ∀ M N, M =mul= N → N =mul= M.
    Proof. solve_meq_ext. Qed.

    Lemma meq_trans :
      ∀ M N P, M =mul= N → N =mul= P → M =mul= P.
    Proof. solve_meq_ext. Qed.

  End meq_equivalence.

  Hint Resolve meq_refl meq_sym meq_trans.

  Instance meq_Equivalence : Equivalence meq.
  Proof.
    split; eauto.
  Qed.

  Instance union_morph : Proper (meq ==> meq ==> meq) union.

  Proof. intros a b ab c d cd. solve_meq_ext. Qed.

  Instance insert_morph : Proper (eq ==> meq ==> meq) cons.

  Proof. intros a b ab c d cd. subst.
         change (b::c) with ([b] ++ c).
         change (b::d) with ([b] ++ d).
         rewrite cd. auto. Qed.

  Instance member_morph : Proper (eq ==> meq ==> iff) member.

  Proof. intros a b ab L1 L2 H; subst. unfold member. rewrite H. intuition. Qed.

  Instance union_morph': Proper (meq ==> meq ==> iff) (meq).
  Proof.
    intros a b ab c d cd; split;
      solve_meq_ext.
  Qed.

  Instance mult_morph : Proper (meq ==> eq ==> eq) mult.

  Proof. intros a b ab c d cd. solve_meq_ext. Qed.

  Instance diff_morph : Proper (meq ==> meq ==> meq) diff.

  Proof. intros a b ab c d cd. solve_meq_ext. Qed.

  Instance remove_morph : Proper (eq ==> meq ==> meq) removeAll.

  Proof. intros a b ab c d cd. solve_meq_ext. Qed.

  Instance rem_morph : Proper (eq ==> meq ==> meq) rem.

  Proof. intros a b ab c d cd; subst.
         assert (rem b c =mul= c / [b]) as H1 by auto.
         assert (rem b d =mul= d / [b]) as H2 by auto.
         rewrite H1, H2, cd; auto. Qed.

  Lemma meq_cons_app a M : a :: M =mul= [a] ++ M.
  Proof. auto. Qed.

  Lemma union_comm : ∀ M N, (M ++ N) =mul= (N ++ M).
  Proof. solve_meq. Qed.
  Lemma union_comm_cons : ∀ a M, (a :: M) =mul= (M ++ [a]).
  Proof. intros. rewrite meq_cons_app; solve_meq. Qed.
  Lemma union_assoc : ∀ M N P, M ++ N ++ P =mul= (M ++ N) ++ P.
  Proof. solve_meq. Qed.
  Hint Resolve meq_cons_app union_comm_cons union_comm union_assoc.

  Lemma member_singleton x y : x € [y] → x = y.
  Proof.
    unfold member; intros.
    case (eqA_dec x y); [trivial | intro x_neq_y].
    assert (x # [y] = 0%nat); [auto | idtac].
    rewrite H0 in H; omega.
  Qed.

  Lemma rem_to_union: ∀ L M x, M =mul= [x] ++ L → L =mul= (rem x M).
  Proof.
    intros.
    apply multeq_meq; intros.
    apply meq_multeq with (x:=x0) in H.
    rewrite union_mult in H.
    symmetry in H.
    rewrite Nat.add_comm in H.
    apply Nat.add_sub_eq_r in H.
    rewrite <- H.
    simpl; destruct (eqA_dec x x0); subst.
    symmetry. apply mult_remove_in; auto.
    symmetry. rewrite Nat.sub_0_r. apply mult_remove_not_in; auto.
  Qed.

  Lemma rem_a : ∀ a, rem a ([a]) =mul= [].
  Proof.
    intros; simpl.
    case (eqA_dec a a); auto.
  Qed.

  Lemma rem_ab : ∀ a b, b = a → rem a ([b]) =mul= [ ].
  Proof.
    intros; subst. apply rem_a.
  Qed.

  Lemma rem_not_ab : ∀ a b, b ≠ a → rem a ([b]) =mul= [b].
  Proof.
    intros; simpl.
    case (eqA_dec a b); auto; intros.
    symmetry in e. contradiction.
  Qed.

  Lemma rem_aM : ∀ a M, rem a (a :: M) =mul= M.
  Proof.
    intros.
    simpl.
    case (eqA_dec a a); auto; intros.
    contradiction.
  Qed.

  Lemma rem_aM_app : ∀ a M, rem a ([a] ++ M) =mul= M.
  Proof.
    intros; simpl.
    case (eqA_dec a a); auto; intros.
    contradiction.
  Qed.

  Lemma rem_abM_app : ∀ a b M, b = a → rem a ([b] ++ M) =mul= M.
  Proof.
    intros; simpl.
    case (eqA_dec a b); auto; intros.
    symmetry in H.
    contradiction.
  Qed.

  Lemma rem_not_abM_app : ∀ a b M, b ≠ a → rem a ([b] ++ M) =mul= [b] ++ rem a M.
  Proof.
    intros; simpl.
    case (eqA_dec a b); auto; intros.
    symmetry in e.
    contradiction.
  Qed.

  Lemma rem_aM_cons : ∀ a M, rem a (a :: M) =mul= M.
  Proof.
    intros.
    change (a :: M) with ([a] ++ M).
    apply rem_aM_app.
  Qed.

  Lemma rem_to_union_app: ∀ L M x, M =mul= [x] ++ L → L =mul= (rem x M).
  Proof.
    intros. rewrite H. rewrite rem_aM_app. auto.
  Qed.
  Lemma rem_to_union_cons: ∀ L M x, M =mul= x :: L → L =mul= (rem x M).
  Proof.
    intros. rewrite H. rewrite rem_aM_cons. auto.
  Qed.

  Hint Resolve rem_a rem_ab rem_not_ab rem_aM_app rem_abM_app rem_not_abM_app rem_aM_cons.
  Lemma emp_mult : ∀ M, M =mul= [] ↔ M = [].
  Proof.
    split; intros; subst; auto.
    eapply (count_occ_inv_nil eqA_dec); intros.
    apply meq_multeq with (x:=x) in H; auto.
  Qed.


  Lemma union_perm M N P : M ++ N ++ P =mul= M ++ P ++ N.

  Proof. solve_meq. Qed.
  Hint Resolve union_perm.
  Lemma union_empty M : M ++ [] =mul= M.

  Proof. solve_meq. Qed.

  Lemma notempty_member M : ¬ M =mul= empty → ∃ N a, M =mul= [a] ++ N.

  Proof.
    intros H.
    destruct M.
    absurd ([] =mul= []); auto.
    ∃ M. ∃ a. auto.
  Qed.

  Lemma not_empty M x : x € M → M =mul= [] → False.

  Proof.
    unfold member; intros mult_x_M M_is_empty.
    absurd (x # M = 0%nat).
    omega.
    assert (x # [] = 0%nat); [auto | idtac].
    assert (x # M = x # []); [apply meq_multeq; trivial | idtac].
    omega.
  Qed.

  Lemma member_union_l a M N : a € M → a € (M ++ N).
  Proof. unfold member; intro H. rewrite union_mult. omega. Qed.

  Lemma member_union_r a M N : a € N → a € (M ++ N).
  Proof. unfold member; intro H. rewrite union_mult. omega. Qed.

  Lemma mult_insert : ∀ M a, (a # (M ++ [a])) > 0.
  Proof.
    intros M a.
    replace (a # (M ++ [a])) with ((a # M) + (a # [a]))%nat.
    replace (a # [a]) with 1%nat.
    omega.
    symmetry; auto.
    auto.
  Qed.

  Lemma singleton_member a : a € [a].
  Proof.
    unfold member. assert (a # [a] = 1%nat); [idtac | omega].
    apply singleton_mult_in; auto with sets.
  Qed.

  Lemma member_insert_app a M : a € ([a] ++ M).
  Proof. apply member_union_l. apply singleton_member. Qed.
  Lemma member_insert_cons a M : a € (a :: M).
  Proof. change (a :: M) with ([a] ++ M). apply member_union_l. apply singleton_member. Qed.

  Lemma member_insert a M : a € ([a] ++ M).
  Proof. apply member_union_l. apply singleton_member. Qed.

  Lemma member_diff_member a M N : a € (M / N) → a € M.
  Proof. unfold member. rewrite (diff_mult M N). omega. Qed.

  Lemma diff_member_ly_rn a M N : a € M → ¬a € N → a € (M / N).
  Proof. unfold member; intros H H0. rewrite diff_mult. omega. Qed.

  Lemma diff_remove_both a M N :
    a € M → a € N → M / N =mul= (rem a M) / (rem a N).
  Proof.
    unfold member; intros H H0.
    apply multeq_meq; intro x.
    rewrite !diff_mult.
    destruct (eqA_dec x a); subst.
    rewrite !mult_remove_in; auto.
    rewrite !Nat.sub_1_r.
    rewrite <- (Nat.sub_succ (Nat.pred (a # M)) _).
    rewrite !Nat.succ_pred_pos; auto.
    rewrite !mult_remove_not_in; auto.
  Qed.

  Lemma member_union a M N : a € (M ++ N) → a € M ∨ a € N.
  Proof. unfold member. rewrite (union_mult _ M N). omega. Qed.

  Lemma member_meq_union a M N M' N' :
    M ++ N =mul= M' ++ N' → (a € M ∨ a € N) → ¬a € N' → a € M'.
  Proof.
    unfold member; intros.
    assert (((a#M)+ (a#N))%nat
            = ((a#M') + (a#N'))%nat).
    rewrite <- !union_mult.
    apply meq_multeq; trivial.
    omega.
  Qed.

  Lemma meq_union_meq M N P : M ++ P =mul= N ++ P → M =mul= N.
  Proof.
    intros; try_solve_meq.
    assert (((x#M) + (x#P))%nat
            = ((x#N) + (x#P))%nat).
    rewrite <- !union_mult.
    apply meq_multeq; trivial.
    omega.
  Qed.

  Lemma meq_union_meq2 M N P : P ++ M =mul= P ++ N → M =mul= N.
  Proof.
    intros; try_solve_meq.
    assert (((x#P) + (x#M))%nat
            = ((x#P) + (x#N))%nat).
    rewrite <- !union_mult.
    apply meq_multeq; trivial.
    omega.
  Qed.

  Hint Resolve meq_union_meq meq_union_meq2.

  Lemma meq_meq_union M N P : M =mul= N → M ++ P =mul= N ++ P.
  Proof. solve_meq. Qed.
  Hint Resolve meq_meq_union.
  Lemma meq_ins_ins_eq a a' M M' :
    M ++ [a] =mul= M' ++ [a'] → a = a' → M =mul= M'.
  Proof.
    intros.
    cut (M ++ [a] =mul= M' ++ [a']).
    rewrite H0; intro; apply meq_union_meq with [a']; trivial.
    trivial.
  Qed.

  Lemma member_ins_ins_meq a a' M M' :
    M ++ [a] =mul= M' ++ [a'] → a' ≠ a → a € M'.

  Proof.
    unfold member; intros.
    assert (((a#M) + 1)%nat = ((a#M') + 0)%nat).
    erewrite <- singleton_mult_in with (x:=a) (y:=a); auto.
    erewrite <- (singleton_mult_notin _ _ H0).
    rewrite <- !union_mult.
    apply meq_multeq; trivial.
    omega.
  Qed.

  Lemma meq_ins_rem a M : a € M → M =mul= (rem a M) ++ [a].

  Proof.
    unfold member; intros.
    apply multeq_meq; intro.
    rewrite union_mult.
    case (eqA_dec a x); intro x_a.
    rewrite singleton_mult_in; trivial.
    assert (x#M = a#M).
    apply mult_eqA_compat; auto.
    rewrite mult_remove_in; auto.
    omega.
    rewrite !singleton_mult_notin; auto.
    rewrite mult_remove_not_in; auto.
  Qed.

  Lemma meq_remove_insert a M : rem a (M ++ [a]) =mul= M.
  Proof.
    induction M.
    × simpl;destruct (eqA_dec a a); auto.
    × simpl.
      destruct (eqA_dec a a0); subst; auto.

      rewrite IHM; auto.
  Qed.

  Lemma meq_remove a M N : a :: M =mul= N → M =mul= rem a N.
  Proof. intros. rewrite <- H. rewrite rem_aM. auto. Qed.

  Lemma insert_meq M N a : a :: M =mul= a :: N → M =mul= N.
  Proof.
    intros.
    eapply meq_union_meq with (P:=[a]).
    rewrite union_comm, (union_comm N _).
    auto.
  Qed.
  Hint Resolve insert_meq.
  Lemma insert_remove_eq a b M : a = b → M =mul= rem a (b :: M).

  Proof.
    intros.
    apply multeq_meq.
    intro x.
    rewrite rem_to_diff.
    rewrite diff_mult.
    destruct (eqA_dec a x).
    rewrite union_mult2.
    rewrite !singleton_mult_in; subst; auto.
    omega.
    rewrite union_mult2.
    rewrite !singleton_mult_notin; subst; auto.
    omega.
  Qed.

  Lemma meq_insert_remove a M : a € M → a :: (rem a M) =mul= M.

  Proof.
    intros.
    apply multeq_meq; intro x.
    rewrite rem_to_diff.
    rewrite union_mult2.
    rewrite diff_mult.
    destruct (eqA_dec x a).
    rewrite singleton_mult_in; auto.
    rewrite (mult_eqA_compat _ _ M e).
    unfold member in H.
    omega.
    rewrite singleton_mult_notin; auto.
    omega.
  Qed.

  Lemma insert_remove_noteq a a' M :
    a ≠ a' → rem a (a' :: M) =mul= a' :: (rem a M).
  Proof.
    intros.
    apply multeq_meq.
    intro x.
    rewrite !rem_to_diff.
    change (a' :: M / [a]) with ([a'] ++ M / [a]).
    rewrite diff_mult.
    rewrite union_mult2.
    rewrite union_mult.
    rewrite diff_mult.
    destruct (eqA_dec a' x).
    rewrite singleton_mult_in; auto.
    rewrite e in H.
    rewrite singleton_mult_notin; auto.
    omega.
    rewrite (@singleton_mult_notin x a'); trivial.
  Qed.

  Lemma meq_cons a M N :
    M ++ [a] =mul= N → ∃ N', N =mul= N' ++ [a] ∧ M =mul= N'.
  Proof.
    intros.
    ∃ (rem a N); split.
    assert (aN: a € N).
    rewrite <- H.
    rewrite (union_comm M [a]).
    apply member_insert.
    set (N' := N) in |- × at 1.
    rewrite (meq_ins_rem _ _ aN); unfold N'; clear N'.
    rewrite (meq_remove_insert a (N / [a])).
    apply meq_ins_rem; trivial.
    rewrite <- H.
    symmetry.
    apply meq_remove_insert.
  Qed.

  Lemma meq_diff_meq M N P : M =mul= N → M / P =mul= N / P.

  Proof. solve_meq. Qed.

  Section Decidability.

    Lemma member_dec a M : {a € M}+{¬a € M}.

    Proof.
      intros; case (Compare_dec.zerop (a # M)); intro.
      right; mset_unfold. omega.
      left; auto.
    Qed.

    Lemma empty_dec : ∀ M, {M =mul= empty}+{¬ M =mul= empty}.

    Proof.
      induction M; intros.
      left; solve_meq.
      right; intro emp.
      absurd (a # (a :: M) = a # []); auto.
      rewrite empty_mult; rewrite union_mult2.
      set (w := singleton_member a); unfold member in w.
      omega.
    Qed.

    Lemma empty_decomp_dec : ∀ M,
        {Ma: (Multiset × A) | M =mul= fst Ma ++ [snd Ma]} + {M =mul= empty}.
    Proof.
      intros.
      induction M.
      right; auto.
      left. ∃ (M, a).
      simpl. rewrite union_comm; auto.
    Qed.

  End Decidability.

  Lemma diff_MM_empty M : M / M =mul= [].
  Proof. solve_meq. Qed.

  Lemma ins_meq_union M N P a :
    M ++ [a] =mul= N ++ P → a € N → M =mul= (N / [a]) ++ P.
  Proof.
    mset_unfold; intros.
    apply multeq_meq; intro x.
    assert (((x#M) + (x#[a]))%nat
            = ((x#N) + (x#P))%nat).
    rewrite <- !union_mult.
    apply meq_multeq; trivial.
    case (eqA_dec x a); intro x_a.
    assert (x#N = a#N).
    apply mult_eqA_compat; trivial.
    rewrite union_mult.
    rewrite diff_mult.
    rewrite singleton_mult_in; auto.
    assert (((x#M) + 1)%nat = ((x#N) + (x#P))%nat).
    rewrite <- (singleton_mult_in _ _ (symmetry x_a)); trivial.
    omega.
    rewrite union_mult.
    rewrite diff_mult.
    assert ( a ≠ x) by auto.
    rewrite (singleton_mult_notin _ _ H2).
    assert (((x#M) + 0)%nat = ((x#N) + (x#P))%nat).
    rewrite <- (singleton_mult_notin _ _ H2); trivial.
    omega.
  Qed.

  Lemma mem_memrem M a b : a ≠ b → a € M → a € (M / [b]).
  Proof.
    unfold member; intros.
    rewrite diff_mult.
    rewrite singleton_mult_notin, Nat.sub_0_r;
      auto.
  Qed.

  Lemma member_notempty M x : x € M → ¬ M =mul= [].
  Proof.
    unfold not; intros.
    absurd (x # M = 0%nat).
    unfold member in H; omega.
    erewrite meq_multeq with (N:=[]); auto.
  Qed.

  Lemma singleton_notempty x : ¬ [x] =mul= [].
  Proof. intro. apply emp_mult in H. inversion H. Qed.

  Lemma union_isempty M N : M ++ N =mul= [] → M =mul= [].
  Proof.
    intros.
    eapply emp_mult in H.
    apply app_eq_nil in H.
    destruct H; subst; auto.
  Qed.

  Lemma union_notempty M N : ¬ M =mul= [] → ¬ M ++ N =mul= [].
  Proof.
    compute in *; intros; apply H. apply union_isempty with N; trivial.
  Qed.

  Lemma remove_union a L R :
    a € L → rem a (L ++ R) =mul= (rem a L) ++ R.
  Proof.
    intros.
    apply multeq_meq; intros.
    rewrite !rem_to_diff.
    repeat (rewrite diff_mult || rewrite union_mult).
    destruct (eqA_dec a x).
    rewrite singleton_mult_in; trivial.
    erewrite mult_eqA_compat with (y:=a); auto.
    unfold member in H; omega.
    rewrite singleton_mult_notin; trivial.
    omega.
  Qed.

  Lemma meq_remove_elem_right a M L R :
    M ++ [a] =mul= L ++ R → a € R → M =mul= L ++ (rem a R).
  Proof.
    intros. rewrite union_comm, <- remove_union, union_comm, <- H; auto.
    symmetry.
    apply meq_remove_insert.
  Qed.

  Hint Immediate member_singleton
       
       member_diff_member
       member_union
       member_meq_union
       union_comm
       union_assoc.

  Hint Resolve union_empty
       not_empty
       singleton_member
       meq_union_meq
       meq_meq_union
       meq_ins_ins_eq
       
       member_ins_ins_meq
       meq_ins_rem
       meq_diff_meq
       diff_MM_empty
       ins_meq_union
       mem_memrem
       member_union_r
       member_union_l
       member_notempty
       singleton_notempty
       union_isempty
       union_notempty.

  Section Multiset.

    Lemma multiset_meq_non_empty : ∀ M,
      ¬ M =mul= [] → M ≠ nil.
    Proof.
      intros.
      destruct M; auto.
      intro.
      inversion H0.
    Qed.

    Lemma multiset_meq_empty : ∀ M,
        M =mul= [] → M = [].
    Proof.
      apply emp_mult.
    Qed.

    Lemma member_list_multiset : ∀ l,
        ∀ x, In x l → member x l.
    Proof.
      induction l.
      intros x x_In_nil; absurd (In x nil); auto.
      simpl; intros x x_In_al; case x_In_al.
      intro ax; rewrite ax; apply member_insert.
      intro x_In_l; mset_unfold.
      change (a :: l) with ([a] ++ l).
      rewrite union_mult.
      assert ((x # l) > 0).
      apply (IHl x); trivial.
      omega.
    Qed.

    Lemma member_multiset : ∀ l,
        ∀ x, member x l → ∃ y, In y l ∧ x = y.
    Proof.
      induction l.
      simpl; intros x x_in_empty.
      absurd (¬ empty =mul= empty); eauto.
      change (a::l) with ([a] ++ l).
      intros x x_in_al.
      case (member_union _ _ _ x_in_al).
      intro x_a; ∃ a; simpl; auto.
      intro x_l; destruct (IHl x x_l).
      destruct H.
      ∃ x0; simpl; auto with sets.
    Qed.

  End Multiset.

  Add Parametric Relation : Multiset meq
      reflexivity proved by meq_refl
      symmetry proved by meq_sym
      transitivity proved by meq_trans as eq_ms.

  Lemma eq_step : ∀ a x,
      a = x → x # [a] = 1%nat.
  Proof. intros. simpl. case (eqA_dec a x); [trivial | contradiction]. Qed.

  Lemma not_eq_zero : ∀ a x,
      a ≠ x → x # [a] = 0%nat.
  Proof. intros. simpl. case (eqA_dec a x); [contradiction | trivial]. Qed.

  Lemma union_mult_step_eq : ∀ M N a x,
      a = x → x # ( [a] ++ (M ++ N)) = x # (M ++ N) + 1.
  Proof.
    intros M N a x x_a.
    rewrite union_mult.
    rewrite eq_step; auto. omega.
  Qed.

  Lemma eq_then_meq: ∀ M N,
      M = N → M =mul= N.
  Proof. intros; destruct M; subst; apply multeq_meq; auto. Qed.

  Lemma union_left : ∀ M N1 N2, N1 =mul= N2 → (N1 ++ M) =mul= (N2 ++ M).
  Proof. auto. Qed.

  Lemma union_right : ∀ M N1 N2, N1 =mul= N2 → (M ++ N1) =mul= (M ++ N2).
  Proof. solve_meq. Qed.

  Hint Resolve union_left union_right.

  Lemma union_rotate x y z : x ++ (y ++ z) =mul= z ++ (x ++ y).
  Proof. solve_meq. Qed.

  Lemma union_reverse x y z : x ++ (y ++ z) =mul= z ++ (y ++ x).
  Proof. solve_meq. Qed.

  Lemma meq_congr x y z t : x =mul= y → z =mul= t → x ++ z =mul= y ++ t.
  Proof. solve_meq. Qed.

  Lemma union_perm_left x y z : x ++ (y ++ z) =mul= y ++ (x ++ z).
  Proof. solve_meq. Qed.

  Lemma union_perm_left' x a z : x ++ (a :: z) =mul= a :: (x ++ z).
  Proof. change ( x ++ (a :: z) =mul= a :: (x ++ z)) with
             (x ++ ([a] ++ z) =mul= [a] ++ (x ++ z)).
         apply union_perm_left. Qed.

  Lemma union_perm_left'' x a z : (a :: x) ++ z =mul= a :: (x ++ z).
  Proof. auto. Qed.

  Hint Resolve union_rotate union_reverse meq_congr union_perm_left union_perm_left' union_perm_left''.

  Lemma multiset_twist1 x y z t : x ++ ((y ++ z) ++ t) =mul= (y ++ (x ++ t)) ++ z.
  Proof. solve_meq. Qed.

  Lemma multiset_twist2 x y z t : x ++ ((y ++ z) ++ t) =mul= (y ++ (x ++ z)) ++ t.
  Proof. solve_meq. Qed.

  Hint Resolve multiset_twist1 multiset_twist2.

  Lemma treesort_twist1 x y z t u :
    u =mul= (y ++ z) →
    x ++ (u ++ t) =mul= (y ++ (x ++ t)) ++ z.
  Proof.
    intros.
    apply multeq_meq; intros.
    apply meq_multeq with (x:=x0) in H.
    rewrite !union_mult.
    rewrite !union_mult in H.
    omega.
  Qed.

  Lemma treesort_twist2 x y z t u :
    u =mul= (y ++ z) →
    x ++ (u ++ t) =mul= (y ++ (x ++ z)) ++ t.
  Proof.
    intros.
    apply multeq_meq; intros.
    apply meq_multeq with (x:=x0) in H.
    rewrite !union_mult.
    rewrite !union_mult in H.
    omega.
  Qed.

  Hint Resolve treesort_twist1 treesort_twist2.

  Lemma my_p x y z t : ((x ++ y) ++ z) ++ t =mul= t ++ (z ++ (x ++ y)).
  Proof. solve_meq. Qed.

  Hint Resolve my_p.

  Lemma meq_skip : ∀ a M1 M2, M1 =mul= M2 → a :: M1 =mul= a :: M2.
  Proof. intros. change (a :: M1 =mul= a :: M2) with ([a] ++ M1 =mul= [a] ++ M2).
         apply union_right; auto.
  Qed.

  Lemma meq_swap : ∀ a b M1 M2, M1 =mul= M2 → (a::b:: M1) =mul= (b::a:: M2).
  Proof.
    intros.
    change (a::b:: M1 =mul= b::a:: M2) with ([a]++ [b] ++ M1 =mul= [b]++ [a] ++ M2).
    apply multeq_meq; intros.
    apply meq_multeq with (x:=x) in H.
    rewrite !union_mult.
    omega.
  Qed.

  Lemma meq_swap_cons a b M : (a :: b:: M) =mul= (b :: a :: M).
  Proof.
    change ((a :: b:: M)) with (([a] ++ [b] ++ M)).
    rewrite meq_swap; simpl; auto.
  Qed.

  Lemma union_rotate_cons a b c M : (a :: b :: c :: M) =mul= (c :: a :: b :: M).
  Proof. change ((a :: b :: c :: M) =mul= (c :: a :: b :: M)) with
             (([a] ++ [b] ++ [c] ++ M) =mul= ([c] ++ [a] ++ [b] ++ M)).
         solve_meq. Qed.
  Hint Resolve meq_skip meq_swap meq_swap_cons union_rotate_cons.

  Lemma pair_app (F G: A) : [F; G] = [F]++[G].
  Proof. auto. Qed.
  Ltac app_normalize_aux :=
    try rewrite !pair_app;
    repeat
      match goal with
      | |- _ =mul= ?a::?M ⇒ change (a :: M) with
            ([a] ++ M)
      | |- ?a::?M =mul= _ ⇒ change (a :: M) with
            ([a] ++ M)
      | |- _ =mul= _++?a::?M++?N ⇒ change (a::M++N) with
            ([a]++M++N)
      | |- _++?a::?M++?N =mul= _ ⇒ change (a::M++N) with
            ([a]++M++N)
      end.

  Lemma union_assoc_cons
    : ∀ a (M N P : list A), a :: M ++ N ++ P =mul= (a :: M ++ N) ++ P.
  Proof.
    intros. rewrite app_assoc.
    auto.
  Qed.
  Hint Resolve union_assoc_cons.

  Ltac app_normalize := repeat (
                            rewrite <- !union_assoc_cons ||
                            rewrite <- !app_assoc ||
                            rewrite app_nil_l); auto.

  Lemma perm_cons_single a b: a::[b] =mul= b::[a].
  Proof.
    change (a :: [b] =mul= b :: [a]) with
        ([a] ++ [b] =mul= [b] ++ [a]). auto. Qed.

  Lemma perm_cons a b L: a::b::L =mul= b::a::L.
  Proof.
    change (a :: b :: L =mul= b :: a :: L) with
        ([a] ++ [b] ++ L =mul= [b] ++ [a] ++ L). auto. Qed.

  Hint Resolve perm_cons_single perm_cons.

  Lemma union_middle : ∀ M N1 N2 : list A, N1 =mul= N2 → N1 ++ M =mul= M ++ N2.
  Proof.
    intros.
    rewrite union_comm.
    auto.
  Qed.

  Ltac perm_simplify := app_normalize; repeat (
                                           rewrite app_nil_r || auto ||
                                           match goal with
                                           | [ |- ?L1 =mul= ?L1 ] ⇒ reflexivity
                                           | [ |- (?A1++_) =mul= (?A1++_) ] ⇒ apply union_right
                                           | [ |- (_++?A1) =mul= (?A1++_) ] ⇒ apply union_middle
                                           | [ |- (_++?A1) =mul= (_++?A1) ] ⇒ apply union_left
                                           | [ |- (?A1::_) =mul= (?A1::_) ] ⇒ apply meq_skip
                                           | [ |- _ =mul= (?L1++_) ] ⇒ (
                                               rewrite (union_perm_left L1) at 1 ||
                                               rewrite <- (union_perm_left' L1) at 1 ||
                                               rewrite (union_comm L1) at 1 ||
                                               rewrite (meq_cons_app L1) at 1 )
                                           | [ |- _ =mul= (?A1::_) ] ⇒ rewrite !(perm_cons _ A1)
                                           | [ |- _ =mul= _ ] ⇒ fail
                                           end).

  Ltac solv_P :=
    try rewrite !union_perm_left'; auto;
    repeat
      match goal with
      | |- _ =mul= ?a::?M ⇒ change (a :: M) with
            ([a] ++ M); try rewrite !union_perm_left'
      | |- ?a::?M =mul= _ ⇒ change (a :: M) with
            ([a] ++ M) ; try rewrite !union_perm_left'
      end.

  Ltac solver_permute :=
    match goal with
    | [ |- _ =mul= _ ] ⇒ perm_simplify; fail "perm failed"
    | [ |- _ ] ⇒ fail "perm can't solve this system."
    end.


  Ltac solve_permutation :=
    solve [auto |
           simpl; rewrite !union_perm_left'; timeout 3 perm_simplify |
           solv_P; unfold meq; intro; rewrite !union_mult; omega | timeout 3 solver_permute ].


  Lemma In_union_or : ∀ x N M, (x € (N ++ M)) ↔ x € M ∨ x € N.
  Proof.
    split; intros;
      unfold member in *; unfold mult in ×. apply countIn_In in H.
    apply in_app_or in H. destruct H;[right;apply countIn_In | left;apply countIn_In]; auto.
    apply countIn_In.
    rewrite <- countIn_In in H. apply or_comm in H. rewrite <- countIn_In in H.
    apply in_or_app; auto.
  Qed.

  Lemma In_union_or' : ∀ x M, x € M → ∀ N, x € (N ++ M).
  Proof.
    intros.
    apply In_union_or.
    left; auto.
  Qed.
  Lemma In_to_in : ∀ x M, In x M ↔ x € M.
  Proof.
    split;intros;
      destruct M;
      unfold member in *;
      unfold mult in *;
      apply countIn_In; auto.
  Qed.

  Lemma meq_In_In: ∀ L1 L2, L1 =mul= L2 → (∀ x, x € L1 ↔ x € L2).
  Proof.
    unfold meq in ×.
    unfold member in ×.
    split;
      intros P.
    rewrite <- H; auto.
    rewrite H; auto.
  Qed.

  Lemma meq_cons_In :
    ∀ l1 l2 e, ([e] ++ l1) =mul= l2 → e € l2.
  Proof.
    intros.
    eapply meq_In_In with (L2:=[e] ++ l1).
    rewrite <- H; eauto.
    apply In_union_or.
    right.
    apply In_to_in.
    firstorder.
  Qed.
  Lemma meq_cons_append : ∀ l x,
      (x :: l) =mul= (l ++ x :: nil).
  Proof.
    intros.
    change (x::l) with ([x]++l).
    auto.
  Qed.