Library CoLoR.RPO.VRPO_Prover

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Adam Koprowski, 2007-05-17
RPO employed for proving termination of concrete examples (after converting terms with arities to varyadic terms).

Set Implicit Arguments.

Module Type TRPO.

  Parameter Sig : ASignature.Signature.
  Parameter stat : Sig -> status_name.
  Parameter prec : Sig -> nat.


Module RPO_Prover (Export R : TRPO).

  Notation term := (@ATerm.term Sig). Notation terms := (list term).
  Notation rule := (@ATrs.rule Sig). Notation rules := (@list rule).

  Module VPrecedence <: VPrecedenceType.

    Definition Sig := VSig_of_ASig Sig.

    Definition leF f g := prec f <= prec g.

    Definition ltF := ltA Sig leF.
    Definition eqF := eqA Sig leF.

    Lemma ltF_wf : well_founded ltF.

    Lemma leF_dec : rel_dec leF.

    Lemma leF_preorder : preorder Sig leF.

    Infix "=F=" := eqF (at level 50).
    Infix "<F" := ltF (at level 50).
    Infix "<=F" := leF (at level 50).

  End VPrecedence.

  Module VRPO := RPO_Model VPrecedence.
  Module VRPO_Results := RPO_Results VRPO.

  Definition arpo := Rof (transp (@vterm_of_aterm Sig).

  Lemma arpo_dec : rel_dec arpo.

  Lemma arpo_wf : WF arpo.

End RPO_Prover.