CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
• Frederic Blanqui, 2007-01-22
dependancy pairs graph
a more general development is given in AGraph.

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).

Variable R : rules.

Variable hyp : rules_preserve_vars R.

Notation DP := (dp R). Notation Chain := (chain R).

Lemma hyp' : rules_preserve_vars DP.

dependancy pairs graph

Definition dp_graph a1 a2 := In a1 DP /\ In a2 DP
/\ exists p, exists s,
int_red R # (sub s (rhs a1)) (sub s (shift p (lhs a2))).

Lemma restricted_dp_graph : is_restricted dp_graph DP.

chain relation for a given dependency pair

Definition chain_dp a t u := In a DP /\
exists s, int_red R # t (sub s (lhs a)) /\ u = sub s (rhs a).

Lemma chain_dp_chain : forall a, chain_dp a << Chain.

Lemma chain_chain_dp : forall t u, Chain t u -> exists a, chain_dp a t u.

iteration of chain steps given a list of dependency pairs

Fixpoint chain_dps (a : rule) (l : rules) : relation term :=
match l with
| nil => chain_dp a
| b :: m => chain_dp a @ chain_dps b m
end.

Lemma chain_dps_app : forall l a b m,
chain_dps a (l ++ b :: m) << chain_dps a l @ chain_dps b m.

Lemma chain_dps_app' : forall a l m b p, a :: l = m ++ b :: p ->
chain_dps a l << chain_dps a (tail m) % @ chain_dps b p.

Lemma chain_dps_iter_chain :
forall l a, chain_dps a l << iter Chain (length l).

Lemma iter_chain_chain_dps : forall n t u, iter Chain n t u ->
exists a, exists l, length l = n /\ chain_dps a l t u.

two consecutive chain steps provide a dp_graph step

Lemma chain_dp2_dp_graph : forall a1 a2 t u v,
chain_dp a1 t u -> chain_dp a2 u v -> dp_graph a1 a2.

Lemma chain_dps_path_dp_graph : forall l a b t u,
chain_dps a (l ++ b :: nil) t u -> path dp_graph a b l.

hypotheses of the criterion based on cycles using the same reduction pair for every cycle

Variables (succ succ_eq : relation term)
(Hredord : weak_rewrite_ordering succ succ_eq)
(Hreword : rewrite_ordering succ_eq)
(Habsorb : absorbs_left succ succ_eq)
(HcompR : compat succ_eq R)
(HcompDP : compat succ_eq (dp R))
(Hwf : WF succ)
(Hcycle : forall a l, length l < length DP -> cycle_min dp_graph a l ->
exists b, In b (a :: l) /\ succ (lhs b) (rhs b)).

Notation eq_dec := (@eq_rule_dec Sig).
Notation occur := (occur eq_dec).

compatibility properties of chains

Lemma chain_dp_hd_red_mod : forall a, chain_dp a << hd_red_mod R (a::nil).

Lemma compat_chain_dp : forall a, chain_dp a << succ_eq#.

Lemma compat_chain_dps : forall l a, chain_dps a l << succ_eq#.

Lemma compat_chain_dp_strict : forall a,
succ (lhs a) (rhs a) -> chain_dp a << succ.

proof of the criterion based on cycles

Lemma WF_cycles : WF (chain R).

End S.