Library CoLoR.Util.Multiset.MultisetOrder

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Adam Koprowski, 2004-09-06
  • Solange Coupet-Grimal and William Delobel, 2005-09-19
Theory concerning extension of an relation to multisets is developed in this file.

Set Implicit Arguments.


Module MultisetOrder (MC: MultisetCore).

  Module Import MSet := MultisetTheory.Multiset MC.

Section OrderDefinition.

  Variable gtA : relation A.

  Let ltA := transp gtA.
  Let leA x y := ~gtA x y.
  Let gtA_trans := clos_trans gtA.
  Let geA x y := gtA x y \/ eqA x y.
  Hint Unfold ltA leA gtA_trans : sets.

  Notation "X >A Y" := (gtA X Y) (at level 50).
  Notation "X <A Y" := (ltA X Y) (at level 50).
  Notation "X <=A Y" := (leA X Y) (at level 50).
  Notation "X >=A Y" := (geA X Y) (at level 50).
  Notation "X >*A Y" := (gtA_trans X Y) (at level 50).



  Inductive MultisetRedGt (A B: Multiset) : Prop :=
  | MSetRed: forall X a Y,
       A =mul= X + {{a}} ->
       B =mul= X + Y ->
       (forall y, y in Y -> a >A y) ->
       MultisetRedGt A B.


  Definition MultisetGt := clos_trans MultisetRedGt.


  Definition MultisetRedLt := transp MultisetRedGt.
  Definition MultisetLt := transp MultisetGt.


  Inductive MultisetGT (M N: Multiset) : Prop :=
  | MSetGT: forall X Y Z,
     X <>mul empty ->
     M =mul= Z + X ->
     N =mul= Z + Y ->
     (forall y, y in Y -> (exists2 x, x in X & x >A y)) ->
     MultisetGT M N.

  Definition MultisetLT := transp MultisetGT.

  Let AccA := Acc ltA.
  Let AccM := Acc MultisetLt.
  Let AccM_1 := Acc MultisetRedLt.
  Let ACC_M := Acc MultisetLT.

  Let clos_transM_RedGt := clos_trans MultisetRedGt.
  Let clos_transM_RedLt := clos_trans MultisetRedLt.


  Notation "X >mul Y" := (MultisetGt X Y) (at level 70) : mord_scope.
  Notation "X >MUL Y" := (MultisetGT X Y) (at level 70) : mord_scope.
  Notation "X <mul Y" := (MultisetLt X Y) (at level 70) : mord_scope.
  Notation "X <MUL Y" := (MultisetLT X Y) (at level 70) : mord_scope.
  Notation "X >mul_1 Y" := (MultisetRedGt X Y) (at level 70) : mord_scope.
  Notation "X <mul_1 Y" := (MultisetRedLt X Y) (at level 70) : mord_scope.

  Delimit Scope mord_scope with mord.
  Open Scope mord_scope.


  Instance MultisetRedGt_morph : Proper (meq ==> meq ==> iff) MultisetRedGt.


  Instance AccM_1_morph : Proper (meq ==> iff) AccM_1.


  Instance clos_transM_RedGt_morph :
    Proper (meq ==> meq ==> iff) clos_transM_RedGt.


  Instance clos_transM_RedLt_morph :
    Proper (meq ==> meq ==> iff) clos_transM_RedLt.


  Instance MultisetGt_morph_equiv : Proper (meq ==> meq ==> iff) MultisetGt.


  Instance MultisetGT_morph : Proper (meq ==> meq ==> iff) MultisetGT.


  Lemma MultisetGt_morph : forall x1 x2 : Multiset, x1 =mul= x2 ->
    forall x3 x4 : Multiset, x3 =mul= x4 -> x1 >mul x3 -> x2 >mul x4.

  Instance AccM_morph : Proper (meq ==> iff) AccM.



  Variable gtA_transitive : Transitive gtA.
  Variable gtA_irreflexive : RelUtil.irreflexive gtA.
  Variable gtA_eqA_compat : Proper (eqA ==> eqA ==> impl) gtA.

  Hint Resolve (gtA_transitive) : sets.
  Hint Resolve (gtA_irreflexive) : sets.
  Hint Resolve (so_not_symmetric
    (Build_strict_order gtA_transitive gtA_irreflexive)) : sets.

  Lemma gtA_eqA_compat' :
    forall a b, eqA a b -> forall c d, eqA c d -> gtA a c -> gtA b d.

  Hint Resolve gtA_eqA_compat' : sets.

  Instance gtA_morph : Proper (eqA ==> eqA ==> iff) gtA.


  Instance ltA_morph : Proper (eqA ==> eqA ==> iff) ltA.


  Instance gtA_trans_morph : Proper (eqA ==> eqA ==> iff) gtA_trans.


  Instance geA_morph : Proper (eqA ==> eqA ==> iff) geA.



Section OrderCharacterization.

  Lemma lt_as_red: same_relation MultisetLt clos_transM_RedLt.

  Lemma empty_min_red: forall M, ~(empty >mul_1 M).


  Lemma empty_min: forall M, ~(empty >mul M).

  Lemma mOrd_trans: forall M N P, M >MUL N -> N >MUL P -> M >MUL P.

  Lemma gtA_comp: forall a, comp_eqA (gtA a).

  Lemma leA_comp: forall a, comp_eqA (leA a).


  Lemma acc_mord : forall M, AccM M -> (forall x, x in M -> AccA x).

  Lemma sub_transp_trans_2_mOrd_trans: forall P,
    (forall p, p in P -> forall x y, x >A p -> y >A x -> y >A p) ->
    forall M N, MultisetGT M N -> MultisetGT N P -> MultisetGT M P.

  Lemma partition2 : forall Y X a,
    (forall y, y in Y -> exists2 x : A, x in (X + {{a}}) & x >A y) ->
    exists Ya, (exists2 Yx : Multiset,
      Y =mul= Ya + Yx & (forall y, y in Ya -> a >A y)
      /\ (forall y, y in Yx -> exists2 x, x in X & x >A y)).


  Lemma direct_subset_red : forall M N, M >MUL N -> M >mul N.

  Lemma red_eq_direct : forall M N, M >mul N <-> M >MUL N.

  Lemma red_insert: forall M N a, N <mul_1 (M + {{a}}) -> exists M',
    (N =mul= M' + {{a}} /\ M' <mul_1 M)
    \/ (N =mul= M + M' /\ forall x, x in M' -> x <A a).

  Lemma noext_big: forall a M N, M >mul N ->
    (forall m, m in M -> a >A m) -> (forall n, n in N -> a >A n).

  Lemma maxin_not_lt: forall M N, M >mul N ->
    {x:A | x in N & (forall y, y in M -> x >A y)} -> False.

  Lemma mord_ext1_aux: forall a X Y, a in X -> a in Y ->
    (forall y, y in Y -> (exists2 x, x in X & x >A y)) ->
    (forall y, y in (Y - {{a}}) -> (exists2 x, x in (X - {{a}}) & x >A y)).

  Lemma mord_ext1: forall M N a, M >mul N <-> M + {{a}} >mul N + {{a}}.

  Lemma mord_ext_r: forall M N P, M >mul N <-> M + P >mul N + P.

  Lemma mord_ext_l M N P : M >mul N <-> union P M >mul union P N.

End OrderCharacterization.

Hint Resolve empty_min empty_min_red : multisets.


Section MultisetOrder_StrictOrder.


  Lemma mord_irreflex: forall M, ~ M >mul M.


  Lemma mord_trans: forall X Y Z, X >mul Y -> Y >mul Z -> X >mul Z.


  Lemma mred_irreflex: forall M, ~M >mul_1 M.

  Lemma mord_sorder : strict_order MultisetGt.

End MultisetOrder_StrictOrder.


Section MultisetOrder_Wf.

  Lemma mord_wf_1: forall a M0,
    (forall b M, b <A a -> AccM_1 M -> AccM_1 (M + {{b}})) ->
    AccM_1 M0 -> (forall M, M <mul_1 M0 -> AccM_1 (M + {{a}})) ->
    AccM_1 (M0 + {{a}}).

  Lemma mord_wf_2: forall a,
    (forall b M, b <A a -> AccM_1 M -> AccM_1 (M + {{b}})) ->
    forall M, AccM_1 M -> AccM_1 (M + {{a}}).

  Lemma mord_wf_3:
    forall a, AccA a -> forall M, AccM_1 M -> AccM_1 (M + {{a}}).

  Lemma mred_acc : forall M, (forall x, x in M -> AccA x) -> AccM_1 M.

  Lemma mred_wf : well_founded ltA -> well_founded MultisetRedLt.

  Lemma mord_acc : forall M, (forall x, x in M -> AccA x) -> AccM M.

  Lemma mord_wf : well_founded ltA -> well_founded MultisetLt.

  Lemma mord_acc_mOrd_acc : forall x, AccM x -> ACC_M x.

  Lemma mOrd_acc : forall M, (forall x, x in M -> AccA x) -> ACC_M M.

  Lemma mOrd_wf : well_founded ltA -> well_founded MultisetLT.

End MultisetOrder_Wf.


Section OrderLemmas.

  Variables M N : Multiset.

  Lemma mord_meq_compat mA mA' mB mB' :
     mA =mul= mA' -> mB =mul= mB' -> mA >mul mB -> mA' >mul mB'.

  Lemma mOrd_elts_ge : M >MUL N ->
   (forall n, n in N -> exists2 m, m in M & m >=A n).

  Lemma mord_elts_ge: M >mul N -> forall n, n in N ->
    exists2 m, m in M & m >*A n \/ m =A= n.

End OrderLemmas.

Section MOrdPair.

  Variables aL aR bL bR : A.

  Lemma pair_mord_left :
    aL >A aR -> bL >=A bR -> {{ aL, bL }} >mul {{ aR, bR }}.

  Lemma pair_mord_right :
    aL >=A aR -> bL >A bR -> {{ aL, bL }} >mul {{ aR, bR }}.

  Lemma pair_mOrd : {{ aL, bL }} >MUL {{ aR, bR }} ->
    (aL >=A aR /\ aL >=A bR /\ (aL >A aR \/ aL >A bR)) \/
    (bL >=A aR /\ bL >=A bR /\ (bL >A aR \/ bL >A bR)) \/
    (aL >=A aR /\ bL >=A bR /\ (aL >A aR \/ bL >A bR)) \/
    (bL >=A aR /\ aL >=A bR /\ (bL >A aR \/ aL >A bR)).

  Lemma pair_mOrd_left :
    aL >A aR -> bL >=A bR -> {{ aL, bL }} >MUL {{ aR, bR }}.

  Lemma pair_mOrd_right :
    aL >=A aR -> bL >A bR -> {{ aL, bL }} >MUL {{ aR, bR }}.

  Lemma pair_mOrd_fromList :
    aL >=A aR -> bL >=A bR -> aL >A aR \/ bL >A bR ->
    list2multiset (aL :: bL :: nil) >MUL list2multiset (aR :: bR :: nil).

End MOrdPair.

Section OrderSim.

  Variables (P : relation A) (eqA_eq : eqA = eq (A:=A)).
  Lemma eqA_refl : forall x, x =A= x.

  Instance P_eqA_comp : Proper (eqA ==> eqA ==> impl) P.


  Instance eqA_Equivalence : Equivalence eqA.


  Lemma list_sim_insert : forall M M' a b,
    P a b -> list_sim P (multiset2list M) M' ->
    exists M'', list2multiset M'' =mul= insert b (list2multiset M') /\
      list_sim P (multiset2list (insert a M)) M''.

  Lemma list_sim_remove : forall M M' a b,
    P a b -> a in M -> list_sim P (multiset2list (remove a M)) M' ->
    exists M'', list2multiset M'' =mul= insert b (list2multiset M') /\
      list_sim P (multiset2list M) M''.

  Lemma multiset_split : forall xs xs' A B,
    list_sim P xs xs' -> list2multiset xs =mul= A + B ->
    exists A', exists B',
      list2multiset xs' =mul= list2multiset A' + list2multiset B'
      /\ list_sim P (multiset2list A) A' /\ list_sim P (multiset2list B) B'.

  Lemma in_mul_sum : forall xs X Y x, list2multiset xs =mul= X + Y ->
    x in X -> exists x', x =A= x' /\ In x' xs.

  Definition order_compatible xs ys xs' ys' :=
    forall x x' y y',
      In x xs ->
      In x' xs' ->
      P x x' ->
      In y ys ->
      In y' ys' ->
      P y y' ->
      (x >A y -> x' >A y') /\ (x =A= y -> x' =A= y').

  Definition eq_compat xs xs' ys':=
    forall x y y',
      In x xs ->
      In y xs' ->
      In y' ys' ->
      P x y ->
      P x y' ->
      y = y'.

  Lemma mord_list_sim : forall xs ys xs' ys',
    order_compatible xs ys xs' ys' ->
    eq_compat xs xs' ys' ->
    list_sim P xs xs' ->
    list_sim P ys ys' ->
    list2multiset xs >MUL list2multiset ys ->
    list2multiset xs' >MUL list2multiset ys'.

  Lemma mulOrd_oneElemDiff : forall l m a b, a >A b ->
    list2multiset (l ++ a::m) >MUL list2multiset (l ++ b::m).

End OrderSim.

Section OrderDec.

  Lemma mult_split: forall M N,
    {MNS: list (Multiset * Multiset * Multiset) |
      forall L R S,
      (In (L, R, S) MNS -> M =mul= S + L /\ N =mul= S + R) /\
      (M =mul= S + L ->
       N =mul= S + R ->
       exists L', exists R', exists S',
         L =mul= L' /\ R =mul= R' /\ S =mul= S' /\ In (L', R', S') MNS
      )
    }.

  Lemma dom_dec : forall M n,
    (forall m, m in M -> {m >A n} + {~m >A n}) ->
    {m: A | m in M /\ m >A n} + {forall m, m in M -> ~m >A n}.

  Definition Ord L R :=
    L <>mul empty /\
    (forall r, r in R -> (exists2 l, l in L & l >A r)).

  Lemma Ord_dec : forall M N,
    (forall m n, m in M -> n in N -> {m >A n} + {~m >A n}) ->
    {Ord M N} + {~Ord M N}.

  Lemma mOrd_dec_aux : forall M N,
    (forall m n, m in M -> n in N -> {m >A n} + {~m >A n}) ->
    {M >MUL N} + {~M >MUL N}.

  Variable gtA_dec : forall (a b: A), {a >A b}+{a <=A b}.

  Lemma mOrd_dec : forall M N, {M >MUL N} + {~M >MUL N}.

End OrderDec.

End OrderDefinition.

Section MultisetOrder_on_subrelation.

  Variables R R' : relation A.
  Variable R'sub : inclusion R' R.

  Lemma mord_inclusion : forall M N, MultisetGt R' M N -> MultisetGt R M N.

  Lemma mOrd_inclusion: forall M N, MultisetGT R' M N -> MultisetGT R M N.

End MultisetOrder_on_subrelation.

End MultisetOrder.