# Library CoLoR.Util.Multiset.MultisetOrder

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
• 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.