Library CoLoR.Term.WithArity.AMonAlg

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Adam Koprowski and Hans Zantema, 2007-03
    This file contains a definition of weakly monotone algebra and extended monotone algebra and some results concerning them, based on:
References: J. Endrullis, J. Waldmann and H. Zantema, "Matrix Interpretations for Proving Termination of Term Rewriting", Proceedings of the 3rd International Joint Conference (IJCAR 2006), 2006.

Module type specifying a weakly monotone algebra.

Module Type MonotoneAlgebraType.

  Parameter Sig : Signature.

A weakly monotone algebra consist of:
  • interpretation I
  • succ and succeq relations
along with the following conditions:
  • IM: I is monotone with respect to succ
  • succ_wf: succ is well-founded
  • succ_succeq_compat: compatibility between succ and succeq
  • succ_dec (succeq_dec): decidability of succ (succeq)
An extended monotone algebra additionaly requires that every operation is monotone with respect to succ but we demand it as an extra hypothesis in respective theorems (dealing with extended monotone algebras).
  Parameter I : interpretation Sig.

  Notation A := (domain I).

  Parameter succ : relation A.
  Parameter succeq : relation A.

  Parameter refl_succeq : reflexive succeq.
  Parameter trans_succ : transitive succ.
  Parameter trans_succeq : transitive succeq.

  Parameter monotone_succeq : monotone I succeq.

  Parameter succ_wf : WF succ.

  Parameter succ_succeq_compat : absorbs_left succ succeq.

For certification of concrete examples we need some subrelations of succ and succeq that are decidable

  Notation IR_succ := (IR I succ).
  Notation IR_succeq := (IR I succeq).

  Notation term := (term Sig).

  Parameters (succ' : relation term) (succeq' : relation term).
  Parameters (succ'_sub : succ' << IR_succ)
    (succeq'_sub : succeq' << IR_succeq).
  Parameters (succ'_dec : rel_dec succ') (succeq'_dec : rel_dec succeq').

End MonotoneAlgebraType.

Functor with a theory of weakly monotone algebras

Module MonotoneAlgebraResults (MA : MonotoneAlgebraType).

  Export MA.

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

  Lemma absorb_succ_succeq : absorbs_left IR_succ IR_succeq.

  Lemma IR_rewrite_ordering : forall succ,
    monotone I succ -> rewrite_ordering (IR I succ).

  Lemma ma_succeq_rewrite_ordering : rewrite_ordering IR_succeq.

  Definition part_succeq := rule_partition succeq'_dec.
  Definition part_succ := rule_partition succ'_dec.

  Lemma partition_succ_compat : forall R,
    compat IR_succ (fst (partition part_succ R)).

relative termination criterion with monotone algebras

  Section RelativeTermination.

    Variable R E : rules.

    Lemma ma_compat_red_mod :
      monotone I succ ->
      compat IR_succ R ->
      compat IR_succeq E ->
      WF (red_mod E R).

  End RelativeTermination.

top termination (for DP setting) criterion with monotone algebras

  Section RelativeTopTermination.

    Variable R E : rules.

    Lemma ma_compat_hd_red_mod :
      compat IR_succ R ->
      compat IR_succeq E ->
      WF (hd_red_mod E R).

  End RelativeTopTermination.

results and tactics for proving relative termination of concrete examples.

  Section RelativeTerminationCriterion.

    Variable R E : rules.

    Lemma partition_succeq_compat : forall R,
      snd (partition part_succeq R) = nil ->
      compat IR_succeq (snd (partition part_succ R)).

    Lemma ma_relative_termination :
      let E_gt := partition part_succ E in
      let E_ge := partition part_succeq E in
      let R_gt := partition part_succ R in
      let R_ge := partition part_succeq R in
        monotone I succ ->
        snd R_ge = nil ->
        snd E_ge = nil ->
        WF (red_mod (snd E_gt) (snd R_gt)) ->
        WF (red_mod E R).

  End RelativeTerminationCriterion.

results and tactics for proving termination (as a special case of relative termination) of concrete examples.

  Section TerminationCriterion.

    Variable R : rules.

    Lemma ma_termination :
      let R_gt := partition part_succ R in
      let R_ge := partition part_succeq R in
        monotone I succ ->
        snd R_ge = nil ->
        WF (red (snd R_gt)) ->
        WF (red R).

  End TerminationCriterion.

results and tactics for proving relative top termination of concrete examples.

  Section RelativeTopTerminationCriterion.

    Variable R E : rules.

    Lemma partition_succeq_compat_fst : forall R,
      compat IR_succeq (fst (partition part_succeq R)).

    Lemma partition_succeq_compat_snd : forall R,
      snd (partition part_succeq R) = nil ->
      compat IR_succeq (snd (partition part_succ R)).

    Lemma ma_relative_top_termination :
      let E_ge := partition part_succeq E in
      let R_gt := partition part_succ R in
      let R_ge := partition part_succeq R in
        snd R_ge = nil ->
        snd E_ge = nil ->
        WF (hd_red_mod E (snd R_gt)) ->
        WF (hd_red_mod E R).

  End RelativeTopTerminationCriterion.


  Ltac partition R := norm (snd (partition part_succ R)).

  Ltac do_prove_termination prove_int_monotonicity lemma R :=
    apply lemma;
      match goal with
      | |- monotone _ _ => prove_int_monotonicity
      | |- WF _ => partition R
      | |- _ = _ => refl
      | _ => first
        [ solve [vm_compute; trivial]
        | idtac
        | fail 10 "Failed to deal with generated goal"

  Ltac prove_termination prove_int_monotone :=
    let prove := do_prove_termination prove_int_monotone in
    match goal with
    | |- WF (red ?R) =>
            prove ma_termination R
    | |- WF (red_mod _ ?R) =>
            prove ma_relative_termination R
    | |- WF (hd_red_mod _ ?R) =>
            prove ma_relative_top_termination R
    | |- WF (hd_red_Mod _ ?R) =>
            eapply WF_incl;[try apply hd_red_mod_of_hd_red_Mod;
                        try apply hd_red_mod_of_hd_red_Mod_int | idtac];
            prove ma_relative_top_termination R
    | _ => fail 10 "Unsupported termination problem type"

End MonotoneAlgebraResults.