Library CoLoR.MPO.VMpo

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Solange Coupet-Grimal and William Delobel, 2005-09-19
This file provides a definition of the multiset path ordering and proofs that it preserves various properties


Module Type VMpo_Struct.
  Parameter Sig : Signature.
  Parameter ltF : relation Sig.
  Parameter wf_ltF : well_founded ltF.
  Parameter ltF_trans : transitive ltF.
End VMpo_Struct.

Module Make (Import S : VMpo_Struct).

  Notation term := (term Sig).
  Notation terms := (list term).

eqset module of terms

  Module Term <: Eqset.

    Definition A := term.

    Definition eqA := eq (A := term).
    Notation "X =A= Y" := (eqA X Y) (at level 70).

    Instance eqA_Equivalence : Equivalence eqA.


  End Term.

  Module Term_dec <: Eqset_dec.

    Module Export Eq := Term.

    Definition eqA_dec := @term_eq_dec Sig.

  End Term_dec.

multisets on terms
mpo

  Inductive lt_mpo : relation term :=
  | mpo1 : forall f g ss ts, ltF g f ->
    (forall t, In t ts -> lt_mpo t (Fun f ss)) -> lt_mpo (Fun g ts) (Fun f ss)
  | mpo2 : forall f ss ts,
    mult (transp lt_mpo) ts ss -> lt_mpo (Fun f ts) (Fun f ss)
  | mpo3 : forall t f ss,
    ex (fun s => In s ss /\ (s = t \/ lt_mpo t s)) -> lt_mpo t (Fun f ss).

  Notation "ss << ts" := (mult (transp term lt_mpo) ss ts) (at level 50).


  Definition le_mpo := fun t s => t = s \/ lt_mpo t s.

compatibility with setoid equality

  Lemma tlt_mpo_eqA_compat : forall x x' y y',
    eqA x x' -> eqA y y' -> transp lt_mpo x y -> transp lt_mpo x' y'.

  Lemma IN_eqA_compat : forall ss x x', In x' ss -> x =A= x' -> In x ss.

inductive predicate saying when a variable occurs in a term

  Inductive in_term_vars : variable -> term -> Prop :=
  | is_var : forall x, in_term_vars x (Var x)
  | is_in_list : forall x f ss,
    ex (fun s => In s ss /\ in_term_vars x s) -> in_term_vars x (Fun f ss).

basic properties

  Lemma var_in : forall x t, lt_mpo (Var x) t -> in_term_vars x t.

  Lemma in_var : forall x t, in_term_vars x t -> le_mpo (Var x) t.

  Lemma strict_subterm_less : forall s f ss, In s ss -> lt_mpo s (Fun f ss).

  Lemma var_in_s_in_terms_greater_than_s : forall t s, le_mpo t s ->
    forall x, in_term_vars x t -> in_term_vars x s.

  Lemma var_cant_be_greater_than_another_term : forall x t,
    lt_mpo t (Var x) -> False.

transitivity

  Lemma transitive_lt_mpo : forall u t s : term,
    lt_mpo u t -> lt_mpo t s -> lt_mpo u s.

  Lemma transitive_le_mpo : transitive le_mpo.

preservation of irreflexivity
well-foundedness

  Lemma Acc_lt_mpo_var : forall x, Acc lt_mpo (Var x).

  Lemma wf_lt_mpo : well_founded lt_mpo.

End Make.