Library CoLoR.DP.AGraph

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Leo Ducas, 2007-08-06
head rules graph: generalisation of ADPGraph to S @ (hd_red R) instead of (int_red R #) @ (dp R)

Set Implicit Arguments.

Section S.

  Variable Sig : Signature.

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

  Notation rule := (rule Sig). Notation rules := (list rule).
  Notation lhs := (@lhs Sig). Notation rhs := (@rhs Sig).

  Section hd_red_Mod.

    Variable S : relation term.
    Variable D : rules.

head rules graph

    Definition hd_rules_graph a1 a2 := In a1 D /\ In a2 D
      /\ exists p, exists s, S (sub s (rhs a1)) (sub s (shift p (lhs a2))).

    Lemma restricted_dp_graph : is_restricted hd_rules_graph D.

corresponding chain relation

    Definition hd_red_Mod_rule a t u := In a D /\
      exists s, S t (sub s (lhs a)) /\ u = sub s (rhs a).

    Lemma chain_hd_rules_hd_red_Mod : forall a,
      hd_red_Mod_rule a << hd_red_Mod S D.

    Lemma hd_red_Mod_chain_hd_rules : forall t u,
      hd_red_Mod S D t u -> exists a, hd_red_Mod_rule a t u.

    Variable hyp : rules_preserve_vars D.

    Lemma hd_red_Mod_rule2_hd_rules_graph : forall a1 a2 t u v,
      hd_red_Mod_rule a1 t u -> hd_red_Mod_rule a2 u v -> hd_rules_graph a1 a2.

    Lemma hd_red_Mod2_hd_rules_graph : forall t u v,
      hd_red_Mod S D t u -> hd_red_Mod S D u v ->
      exists a1, exists a2, hd_rules_graph a1 a2.

  End hd_red_Mod.

  Lemma hd_rules_graph_incl : forall S D D', incl D D' ->
    hd_rules_graph S D << hd_rules_graph S D'.

relation between hd_red_Mod and chain

  Lemma hd_red_Mod_of_chain : forall R : rules,
    chain R << hd_red_Mod (int_red R #) (dp R).

End S.


Ltac dp_trans := chain; eapply WF_incl; [apply hd_red_Mod_of_chain | idtac].