Library CoLoR.MannaNess.AMannaNess

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2006-12-01
termination by using compatible reduction orderings

Set Implicit Arguments.


Section S.

  Variable Sig : Signature.

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

Manna-Ness theorem (1970)

  Lemma manna_ness (R : rules) succ :
    reduction_ordering succ -> compat succ R -> WF (red R).

an extension for proving the well-foundedness of relations of the form: several steps of R1 followed by a step of R2

  Lemma manna_ness_mod (R E : rules) (rp : Reduction_pair Sig) :
    compat (rp_succ_eq rp) E -> compat (rp_succ rp) R -> WF (red_mod E R).

an extension for proving the well-foundedness of relations of the form: several steps of R1 followed by a -head- step of R2
rule elimination

  Section rule_elimination.

    Variables R Rgt Rge : rules.

    Section mod.

      Variables E Egt Ege : rules.

      Lemma rule_elimination_mod : forall rp : Reduction_pair Sig,
        compat (rp_succ rp) Rgt ->
        compat (rp_succ_eq rp) Rge ->
        compat (rp_succ rp) Egt ->
        compat (rp_succ_eq rp) Ege ->
        WF (red_mod Ege Rge) ->
        WF (red_mod (Egt ++ Ege) (Rgt ++ Rge)).

      Lemma rule_elimination_hd_mod : forall wp : Weak_reduction_pair Sig,
        compat (wp_succ_eq wp) E ->
        compat (wp_succ_eq wp) Rge ->
        compat (wp_succ wp ) Rgt ->
        WF (hd_red_mod E Rge) ->
        WF (hd_red_mod E (Rgt ++ Rge)).

    End mod.

    Lemma rule_elimination : forall rp : Reduction_pair Sig,
      compat (rp_succ_eq rp) Rge ->
      compat (rp_succ rp ) Rgt ->
      WF (red Rge) ->
      WF (red (Rgt ++ Rge)).

    Lemma rule_elimination_hd_red : forall wp : Weak_reduction_pair Sig,
      compat (wp_succ_eq wp) Rge ->
      compat (wp_succ wp ) Rgt ->
      WF (hd_red Rge) ->
      WF (hd_red (Rgt ++ Rge)).

  End rule_elimination.

End S.