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.