Library CoLoR.Util.Multiset.MultisetList

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Adam Koprowski, 2004-09-06
This file provides an implementation of finite multisets using list representation.

Set Implicit Arguments.


Module MultisetList (ES : Eqset_dec) <: MultisetCore with Module Sid := ES.

  Module Export Sid := ES.

Section Operations.

  Definition Multiset := list A.

  Definition empty : Multiset := nil.
  Definition singleton a : Multiset := a :: nil.
  Definition union := app (A:=A).
  Definition meq := permutation eqA eqA_dec.

  Definition mult := countIn eqA eqA_dec.
  Definition rem := removeElem eqA eqA_dec.
  Definition diff := removeAll eqA eqA_dec.

  Definition intersection := inter_as_diff diff.

  Definition fold_left := fun T : Type => List.fold_left (A := T) (B := A).

End Operations.

  Infix "=mul=" := meq (at level 70) : msets_scope.
  Notation "X <>mul Y" := (~meq X Y) (at level 50) : msets_scope.
  Notation "{{ x }}" := (singleton x) (at level 5) : msets_scope.
  Infix "+" := union : msets_scope.
  Infix "-" := diff : msets_scope.
  Infix "#" := intersection (at level 50, left associativity) : msets_scope.
  Infix "/" := mult : msets_scope.

  Delimit Scope msets_scope with msets.
  Open Scope msets_scope.

Section ImplLemmas.

  Lemma empty_empty : forall M, (forall x, x / M = 0) -> M = empty.

End ImplLemmas.

Section SpecConformation.

  Lemma mult_eqA_compat : forall M x y, x =A= y -> x / M = y / M.

  Lemma mult_comp : forall l a,
    a / l = multiplicity (list_contents eqA eqA_dec l) a.

  Lemma multeq_meq : forall M N, (forall x, x / M = x / N) -> M =mul= N.

  Lemma meq_multeq : forall M N, M =mul= N -> forall x, x / M = x / N.

  Lemma empty_mult : forall x, mult x empty = 0.

  Lemma union_mult : forall M N x,
                       (x/(M + N))%msets = ((x/M)%msets + (x/N)%msets)%nat.

  Lemma diff_empty_l : forall M, empty - M = empty.

  Lemma diff_empty_r : forall M, M - empty = M.

  Lemma mult_remove_in : forall x a M,
    x =A= a -> (x / (rem a M))%msets = ((x / M)%msets - 1)%nat.

  Lemma mult_remove_not_in : forall M a x,
    ~ x =A= a -> x / (rem a M) = x / M.

  Lemma remove_perm_single : forall x a b M,
   x / (rem a (rem b M)) = x / (rem b (rem a M)).

  Lemma diff_mult_comp : forall x N M M',
    M =mul= M' -> x / (M - N) = x / (M' - N).

  Lemma diff_perm_single : forall x a b M N,
    x / (M - (a::b::N)) = x / (M - (b::a::N)).

  Lemma diff_perm : forall M N a x,
    x / ((rem a M) - N) = x / (rem a (M - N)).

  Lemma diff_mult_step_eq : forall M N a x,
    x =A= a -> x / (rem a M - N) = ((x / (M - N))%msets - 1)%nat.

  Lemma diff_mult_step_neq : forall M N a x,
    ~ x =A= a -> x / (rem a M - N) = x / (M - N).

  Lemma diff_mult : forall M N x,
                      x / (M - N) = ((x / M)%msets - (x / N)%msets)%nat.

  Definition intersection_mult := inter_as_diff_ok mult diff diff_mult.

  Lemma singleton_mult_in : forall x y, x =A= y -> x / {{y}} = 1.

  Lemma singleton_mult_notin : forall x y, ~x =A= y -> x / {{y}} = 0.

  Lemma rev_list_ind_type : forall P : Multiset -> Type,
    P nil -> (forall a l, P (rev l) -> P (rev (a :: l))) -> forall l, P (rev l).

  Lemma rev_ind_type : forall P : Multiset -> Type,
    P nil -> (forall x l, P l -> P (l ++ x :: nil)) -> forall l, P l.

  Lemma mset_ind_type : forall P : Multiset -> Type,
    P empty -> (forall M a, P M -> P (union M {{a}})) -> forall M, P M.

End SpecConformation.

  Hint Unfold meq
              empty
              singleton
              mult
              union
              diff : multisets.

  Hint Resolve mult_eqA_compat
               meq_multeq
               multeq_meq
               empty_mult
               union_mult
               diff_mult
               intersection_mult
               singleton_mult_in
               singleton_mult_notin : multisets.

  Hint Rewrite empty_mult
               union_mult
               diff_mult
               intersection_mult using trivial : multisets.

End MultisetList.