Library CoLoR.Term.WithArity.AWFMInterpretation

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2006-10-19
  • Sebastien Hinderer, 2004-02-25
well-founded monotone interpretations

Set Implicit Arguments.

Section S.

  Variable Sig : Signature.

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

  Variable I : interpretation Sig.

  Section IR.

    Variable R : relation I.

    Definition IR : relation term :=
      fun t u => forall xint, R (term_int xint t) (term_int xint u).

properties of IR

    Lemma IR_reflexive : reflexive R -> reflexive IR.

    Lemma IR_transitive : transitive R -> transitive IR.

    Lemma IR_substitution_closed : substitution_closed IR.

    Definition monotone := forall f, Vmonotone1 (fint I f) R.

    Lemma IR_context_closed : monotone -> context_closed IR.

    Lemma IR_WF : WF R -> WF IR.

    Lemma IR_reduction_ordering : monotone -> WF R -> reduction_ordering IR.

equivalent definition

    Definition IR' : relation term := fun t u =>
      let n := 1 + max (maxvar t) (maxvar u) in
        forall v : vector I n,
          let xint := val_of_vec I v in
            R (term_int xint t) (term_int xint u).

    Lemma IR_incl_IR' : IR << IR'.

    Lemma IR'_incl_IR : IR' << IR.

    Lemma IR_eq_IR' : IR == IR'.

  End IR.

monotony wrt R

  Section inclusion.

    Variables R R' : relation I.

    Lemma IR_inclusion : R << R' -> IR R << IR R'.

  End inclusion.

End S.