Library CoLoR.Util.Multiset.MultisetTheory

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Adam Koprowski, 2004-09-06
  • William Delobel, 2005-10-07
This file provides a development of (part of) the theory of finite multisets.

Set Implicit Arguments.


Module Multiset (MC : MultisetCore).

  Export MC.

  Section NewOperations.

    Definition member x M := (x/M)%msets > 0.

    Definition insert x M : Multiset := {{x}}+M.

    Definition pair a b : Multiset := insert a {{b}}.

    Definition remove a A : Multiset := A - {{a}}.

    Fixpoint list2multiset (l : list A) : Multiset :=
      match l with
      | List.nil => empty
      | List.cons x xs => insert x (list2multiset xs)
      end.

  End NewOperations.

  Notation "{{ x , y }}" := (pair x y) (at level 5) : msets_scope.
  Notation "x 'in' M" := (member x M) (at level 10) : msets_scope.

  Ltac mset_unfold := repeat progress unfold insert,remove,pair,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 empty_mult;
              try rewrite intersection_mult
           )
         ; try omega
         ; try congruence
         ; try solve [auto with multisets]
         )
     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 =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 =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
              insert
              pair
              remove : multisets.

  Section meq_equivalence.

    Lemma meq_refl M : M =mul= M.

    Lemma meq_trans M N P : M =mul= N -> N =mul= P -> M =mul= P.

    Lemma meq_sym M N : M =mul= N -> N =mul= M.

  End meq_equivalence.

  Hint Resolve meq_refl meq_trans meq_sym : multisets.

  Instance meq_Equivalence : Equivalence meq.


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


  Instance singleton_morph : Proper (eqA ==> meq) singleton.


  Instance pair_morph : Proper (eqA ==> eqA ==> meq) pair.


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


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


  Instance insert_morph : Proper (eqA ==> meq ==> meq) insert.


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


  Instance remove_morph : Proper (eqA ==> meq ==> meq) remove.


  Instance intersection_morph : Proper (meq ==> meq ==> meq) intersection.


  Section MultisetLemmas.

    Lemma mset_ind : forall P : Multiset -> Prop,
      P empty -> (forall M a, P M -> P (M + {{a}})) -> forall M, P M.

    Lemma mset_ind_set : forall P : Multiset -> Set,
        P empty -> (forall M a, P M -> P (M + {{a}})) -> forall M, P M.

    Lemma union_comm M N : M + N =mul= N + M.

    Lemma intersection_comm M N : M # N =mul= N # M.

    Lemma union_assoc M N P : M + (N + P) =mul= (M + N) + P.

    Lemma member_singleton x y : x in {{y}} -> x =A= y.

    Lemma singleton_member_eqA a b : a in {{b}} -> a =A= b.

    Lemma singleton_mult_union_empty a a' M :
        {{a}} =mul= {{a'}} + M -> M =mul= empty.

    Lemma member_pair x y z : x in {{y,z}} -> x =A= y \/ x =A= z.

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

    Lemma union_empty M : M + empty =mul= M.

    Lemma notempty_member M : M <>mul empty -> exists N a, M =mul= {{a}} + N.

    Lemma not_empty M x : x in M -> M =mul= empty -> False.

    Lemma member_union_l a M N : a in M -> a in (M + N).

    Lemma member_union_r a M N : a in N -> a in (M + N).

    Lemma mult_insert : forall M a, (a/(M + {{a}}))%msets > 0.

    Lemma singleton_member a : a in {{a}}.

    Lemma member_insert a M : a in (insert a M).

    Lemma member_member_union a M N : a in M -> a in (M+N).

    Lemma member_diff_member a M N : a in (M-N) -> a in M.

    Lemma diff_member_ly_rn a M N : a in M -> ~a in N -> a in (M - N).

    Lemma diff_remove_both a M N :
      a in M -> a in N -> M - N =mul= (remove a M) - (remove a N).

    Lemma member_union a M N : a in (M+N) -> a in M \/ a in N.

    Lemma member_meq_union a M N M' N' :
      M + N =mul= M' + N' -> (a in M \/ a in N) -> ~a in N' -> a in M'.

    Lemma meq_union_meq M N P : M + P =mul= N + P -> M =mul= N.

    Lemma meq_meq_union M N P : M =mul= N -> M + P =mul= N + P.

    Lemma meq_ins_ins_eq a a' M M' :
      M + {{a}} =mul= M' + {{a'}} -> a =A= a' -> M =mul= M'.

    Lemma meq_ins_ins a a' M M' :
      M + {{a}} =mul= M' + {{a'}} -> M =mul= M' + {{a'}} - {{a}}.

    Lemma member_ins_ins_meq a a' M M' :
      M + {{a}} =mul= M' + {{a'}} -> ~a =A= a' -> a in M'.

    Lemma meq_ins_rem a M : a in M -> M =mul= M - {{a}} + {{a}}.

    Lemma meq_remove_insert a M : remove a (M + {{a}}) =mul= M.

    Lemma meq_remove a M N : insert a M =mul= N -> M =mul= remove a N.

    Lemma insert_meq M N a : insert a M =mul= insert a N -> M =mul= N.

    Lemma insert_remove_eq a a' M : a =A= a' -> M =mul= remove a (insert a' M).

    Lemma meq_insert_remove a M : a in M -> insert a (remove a M) =mul= M.

    Lemma insert_remove_noteq a a' M :
      ~a =A= a' -> remove a (insert a' M) =mul= insert a' (remove a M).

    Lemma meq_cons a M N :
      M + {{a}} =mul= N -> exists N', N =mul= N' + {{a}} /\ M =mul= N'.

    Lemma meq_diff_meq M N P : M =mul= N -> M - P =mul= N - P.

    Section Decidability.

      Lemma member_dec a M : {a in M}+{~a in M}.

      Lemma empty_dec : forall M, {M =mul= empty}+{M <>mul empty}.

      Lemma empty_decomp_dec : forall M,
          {Ma: (Multiset * A) | M =mul= fst Ma + {{snd Ma}}} + {M =mul= empty}.

    End Decidability.

    Lemma insert_diff a M N :
      insert a M - N =mul= empty -> a in N /\ M - remove a N =mul= empty.

    Lemma diff_MM_empty M : M - M =mul= empty.

    Lemma ins_meq_union M N P a :
      M + {{a}} =mul= N + P -> a in N -> M =mul= N - {{a}} + P.

    Lemma mem_memrem M a b : ~ a =A= b -> a in M -> a in (M - {{b}}).

    Lemma member_notempty M x : x in M -> M <>mul empty.

    Lemma singleton_notempty x : {{x}} <>mul empty.

    Lemma union_isempty M N : M + N =mul= empty -> M =mul= empty.

    Lemma union_notempty M N : M <>mul empty -> M + N <>mul empty.

    Lemma remove_union a L R :
      a in L -> remove a (L + R) =mul= (remove a L) + R.

    Lemma meq_remove_elem_right a M L R :
      M + {{a}} =mul= L + R -> a in R -> M =mul= L + (remove a R).

  End MultisetLemmas.

  Hint Immediate member_singleton
       member_member_union
       member_diff_member
       member_union
       member_meq_union
       union_comm
       intersection_comm
       union_assoc : multisets.

  Hint Resolve union_empty
       not_empty
       singleton_member
       meq_union_meq
       meq_meq_union
       meq_ins_ins_eq
       meq_ins_ins
       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 : multisets.

  Section MultisetLemmas2.

    Lemma double_split L R U D :
      L + R =mul= U + D -> R =mul= (R # D) + (U - L).

    Variables (P Q : A -> Prop) (PQ_dec : forall a, {P a}+{Q a}).

    Definition comp_eqA P := forall a b, a =A= b -> P a -> P b.

    Variables (P_comp : comp_eqA P) (Q_comp : comp_eqA Q).

    Lemma partition : forall M, exists Mp, exists2 Mq, M =mul= Mp + Mq
      & (forall p, p in Mp -> P p) /\ (forall q, q in Mq -> Q q).

  End MultisetLemmas2.

  Section List2Multiset.

    Lemma member_list_multiset : forall l,
      forall x, In x l -> member x (list2multiset l).

    Lemma member_multiset_list : forall l,
        forall x, member x (list2multiset l) -> exists2 y, In y l & x =A= y.

    Lemma list2multiset_app : forall M1 M2,
        list2multiset (M1 ++ M2) =mul= list2multiset M1 + list2multiset M2.

    Lemma list2multiset_mult : forall l a,
        a / (list2multiset l) = multiplicity (list_contents eqA_dec l) a.

    Lemma meq_permutation l l' :
        list2multiset l =mul= list2multiset l' -> permutation eqA_dec l l'.

    Lemma permutation_meq l l' :
      permutation eqA_dec l l' -> list2multiset l =mul= list2multiset l'.

    Lemma list2multiset_eq_length l l' :
      list2multiset l =mul= list2multiset l' -> length l = length l'.

    Lemma list2multiset_cons_length l l' : forall a,
      list2multiset l + {{a}} =mul= list2multiset l' ->
      length l' = S (length l).

    Lemma list2multiset_remove_in a : forall m,
        remove a (list2multiset m)
        =mul= list2multiset (removeElem eqA eqA_dec a m).

    Lemma diff_empty : forall l m,
        list2multiset l - list2multiset m =mul= empty ->
        (length l - length m = 0)%nat.

    Lemma list2multiset_union_length : forall l m n,
        list2multiset l =mul= list2multiset m + list2multiset n ->
        length l = (length m + length n)%nat.

    Lemma list2multiset_diff_length : forall l m n,
        list2multiset l =mul= list2multiset m - list2multiset n ->
        length l >= length m - length n.

    Lemma list2multiset_insert_nth a l p :
      list2multiset (insert_nth l p a) =mul= insert a (list2multiset l).

  End List2Multiset.

  Section Multiset2List.
    Definition mult_to_list : forall M, {l : list A | M =mul= list2multiset l}.


    Definition multiset2list M :=
      match mult_to_list M with @exist _ _ l _ => l end.

    Lemma multiset2list_empty : multiset2list empty = nil.

    Lemma double_convertion : forall M, list2multiset (multiset2list M) =mul= M.

  End Multiset2List.

  Section Multiset2List_Results.

    Lemma multiset2list_meq_non_empty : forall M,
      M <>mul empty -> multiset2list M <> nil.

    Lemma multiset2list_meq_empty : forall M,
        M =mul= empty -> multiset2list M = nil.

    Lemma in_multiset_in_multiset2list : forall M x,
        x in M -> exists y, x =A= y /\ In y (multiset2list M).

    Lemma in_multiset2list_in_multiset : forall M x,
        In x (multiset2list M) -> x in M.

    Lemma multiset2list_insert a M :
    exists a' p, a =A= a' /\
                 permutation eqA_dec (multiset2list M)
                             (drop_nth (multiset2list (insert a M)) p)
                 /\ nth_error (multiset2list (insert a M)) p = Some a'.

    Lemma multiset2list_cons_length M a :
        length (multiset2list (M + {{a}})) = S (length (multiset2list M)).

    Lemma multiset2list_union_length M N :
      length (multiset2list (M + N))
      = (length (multiset2list M) + length (multiset2list N))%nat.

    Lemma multiset2list_diff_length M N :
      length (multiset2list (M - N))
      >= length (multiset2list M) - length (multiset2list N).

    Lemma multiset2list_meq_length M M' :
      M =mul= M' -> length (multiset2list M) = length (multiset2list M').

    Lemma cons_eq_cons_cons_absurd a a' a'' M :
      {{a}} =mul= {{a'}} + {{a''}} + M -> False.

    Lemma multiset2list_singleton a :
      exists a', a =A= a' /\ multiset2list {{a}} = a' :: nil.

  End Multiset2List_Results.

  Section MultisetCardinality.

    Definition card_def (M : Multiset) : { n | length (multiset2list M) = n}.


    Definition card (M : Multiset) := proj1_sig (card_def M).

    Lemma empty_card : card empty = 0.

    Instance card_morph : Proper (meq ==> eq) card.


    Lemma multiset2list_card M : length (multiset2list M) = card M.

    Lemma card_non_empty M : M <>mul empty -> card M > 0.

    Lemma singleton_card x : card {{x}} = 1.

    Lemma pair_card x y : card {{x, y}} = 2.

    Lemma union_card M N : card (M + N) = (card M + card N)%nat.

    Lemma diff_card M N : card (M - N) >= card M - card N.

  End MultisetCardinality.

  Section Pair.

    Lemma pair_eq a b c d :
      {{a, b}} =mul= {{c, d}} -> (a =A= c /\ b =A= d) \/ (a =A= d /\ b =A= c).

    Lemma pair_decomp a b X Y : {{a, b}} =mul= X + Y ->
      (X =mul= {{a, b}} /\ Y =mul= empty) \/
      (X =mul= empty /\ Y =mul= {{a, b}}) \/
      (X =mul= {{a}} /\ Y =mul= {{b}}) \/
      (X =mul= {{b}} /\ Y =mul= {{a}}).

  End Pair.

  Hint Immediate double_split : multisets.


End Multiset.