# Library CoLoR.Util.Multiset.MultisetListOrder

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
• Solange Coupet-Grimal and William Delobel, 2005-09
This file provides an order on lists derived from the order on multisets, along with some properties of this order.

Module MultisetListOrder (ES : Eqset_dec).

Module Export FMultisetList := MultisetList ES.

Module Export MOrder := MultisetOrder FMultisetList.
Export MSet.

Section MultisetListOrderFacts.

Variable r : relation A.

Variable r_eqA_compat :
forall x x' y y', x =A=x' -> y=A=y' -> r x y -> r x' y'.

Lemma r_eqA : Proper (eqA ==> eqA ==> impl) r.

Variable In_eqA_compat : forall ss x x',
In x' ss -> x =A= x' -> In x ss.

Definition mult ss ts :=
MultisetLT r (list2multiset ss) (list2multiset ts).

Lemma mult2element : forall ss ts, mult ss ts ->
forall s, In s ss -> ex (fun t => In t ts /\ (t =A= s \/ r t s)).

Lemma transp_trans_to_mult_trans : forall us,
(forall u, In u us -> forall t s,
transp r u t -> transp r t s -> transp r u s) ->
forall ts ss, mult us ts -> mult ts ss -> mult us ss.

Lemma nonempty_mset_ind : forall (P : Multiset -> Prop),
(forall M N, P M -> M =mul= N -> P N) ->
(forall a, P {{a}}) -> (forall a M, P M -> P (M+{{a}})) ->
forall M : Multiset, M <>mul empty -> P M.

Lemma self_dom : transitive r -> forall X, X <>mul empty ->
(forall x, x in X -> ex (fun x' => x' in X /\ r x' x)) ->
ex (fun x => x in X /\ r x x).

Lemma self_dom2 : forall X, X <>mul empty ->
(forall x, x in X -> forall y z, r y x -> r z y -> r z x) ->
(forall x, x in X -> ex (fun x' => x' in X /\ r x' x)) ->
ex (fun x => x in X /\ r x x).

Lemma irrefl_to_MultisetGT_irrefl : transitive r -> forall M,
(forall m, m in M -> r m m -> False) -> MultisetGT r M M -> False.

Lemma irrefl_to_mult_irrefl : transitive r ->
forall ss, (forall s, In s ss -> r s s -> False) -> mult ss ss -> False.

Lemma transp_SPO_to_mult_SPO : forall us,
(forall u, In u us ->
((forall t s, transp r u t -> transp r t s -> transp r u s)
/\ (transp r u u -> False))) ->
(forall ts ss, mult us ts -> mult ts ss -> mult us ss)
/\ (mult us us -> False).

Lemma Acc_multiset_list : transitive r -> forall ss,
Acc (MultisetLt r) (list2multiset ss) -> Acc mult ss.

Lemma Acc_list_multiset : transitive r -> forall ss,
Acc mult ss -> Acc (MultisetLt r) (list2multiset ss).

Lemma HAccTermsToTermlist : forall ss,
(forall s, In s ss -> Acc (transp r) s) -> Acc mult ss.

Lemma HAccTermlistToTerms : transitive r -> forall ss : list A,
Acc mult ss -> (forall s, In s ss -> Acc (transp r) s).

End MultisetListOrderFacts.

Import AccUtil ListUtil.

Lemma mult_lifting : forall (r : relation A),
(forall x x' y y', x =A= x' -> y =A= y' -> r x y -> r x' y') ->
(forall l x x', In x' l -> x =A= x' -> In x l) ->
forall l, Accs r l -> Restricted_acc (Accs r) (mult (transp r)) l.

Section Mult_and_one_less.

Lemma mult_insert : forall r l l' h,
mult (transp r) l l' -> mult (transp r) (h :: l) (h :: l').

Lemma one_less2mult : forall r : relation A,
(forall x x' y y', x =A=x' -> y=A=y' -> r x y -> r x' y') ->
forall l l', one_less r l l' -> mult (transp r) l l'.

End Mult_and_one_less.

End MultisetListOrder.