Library CoLoR.DP.ADPGraph

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

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.