Library CoLoR.DP.ADP

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2004-12-22, 2009-11-04 (Dershowitz' improvement)
  • Joerg Endrullis, 2008-06-19 (extension to minimal chains)
dependancy pairs

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

Variable R : rules.

definition of dependancy pairs

Definition negb_subterm (t u : term) := negb (bsubterm u t).

Fixpoint mkdp (S : rules) : rules :=
  match S with
    | nil => nil
    | a :: S' => let (l, r) := a in
      map (mkRule l) (filter (negb_subterm l) (calls R r)) ++ mkdp S'
  end.

Definition dp := mkdp R.

Lemma mkdp_app : forall l1 l2, mkdp (l1 ++ l2) = mkdp l1 ++ mkdp l2.

Lemma mkdp_elim : forall l t S, In (mkRule l t) (mkdp S) -> exists r,
  In (mkRule l r) S /\ In t (calls R r) /\ negb_subterm l t = true.


basic properties

Lemma dp_intro : forall l r t, In (mkRule l r) R -> In t (calls R r) ->
  negb_subterm l t = true -> In (mkRule l t) dp.

Lemma dp_elim : forall l t, In (mkRule l t) dp -> exists r,
  In (mkRule l r) R /\ In t (calls R r) /\ negb_subterm l t = true.


Lemma in_calls_hd_red_dp : forall l r t s, In (mkRule l r) R ->
  In t (calls R r) -> negb_subterm l t = true -> hd_red dp (sub s l) (sub s t).

Lemma lhs_dp : incl (map lhs dp) (map lhs R).


dependency chains

Definition chain := int_red R # @ hd_red dp.

Lemma in_calls_chain : forall l r t s, In (mkRule l r) R ->
  In t (calls R r) -> negb_subterm l t = true -> chain (sub s l) (sub s t).

Lemma gt_chain : forall f ts us v,
  Vrel1 (red R) ts us -> chain (Fun f us) v -> chain (Fun f ts) v.

minimal dependency chain (subterms are terminating)

Definition chain_min s t := chain s t
  /\ lforall (SN (red R)) (direct_subterms s)
  /\ lforall (SN (red R)) (direct_subterms t).

Lemma chain_min_incl_chain : chain_min << chain.

Lemma gt_chain_min : forall f ts us v, Vrel1 (red R) ts us ->
  Vforall (SN (red R)) ts -> chain_min (Fun f us) v -> chain_min (Fun f ts) v.

hyps on rules

Variable hyp1 : forallb (@is_notvar_lhs Sig) R = true.

Variable hyp2 : rules_preserve_vars R.


dp preserves variables
fundamental dp theorem


Notation capa := (capa R).
Notation cap := (cap R).
Notation alien_sub := (alien_sub R).

Notation SNR := (SN (red R)).

Lemma chain_min_fun : forall f, defined f R = true
  -> forall ts, SN chain_min (Fun f ts) -> Vforall SNR ts -> SNR (Fun f ts).

Lemma chain_fun : forall f, defined f R = true
  -> forall ts, SN chain (Fun f ts) -> Vforall SNR ts -> SNR (Fun f ts).

Lemma WF_chain : WF chain -> WF (red R).

Lemma chain_hd_red_mod : chain << hd_red_mod R dp.

End S.

declaration of implicit arguments


tactics


Ltac chain := no_relative_rules; apply WF_chain;
  [ check_eq || fail 10 "a LHS is a variable"
  | rules_preserve_vars
  | idtac].