Library CoLoR.DP.ADecomp

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.

Frederic Blanqui, 2008-05-19

decomposition of an over DP graph

Set Implicit Arguments.

Section S.

  Variable Sig : Signature.

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

we consider the relation (hd_red_Mod S R)

Variable S : relation term.
Variable D : rules.

a decomposition of a list of rules is a list of list of rules

Notation decomp := (list rules).

we assume given a decidable graph on rules

Variable approx : rule -> rule -> bool.

Definition Graph x y := approx x y = true.

we assume that Graph is an over graph of (hd_rules_graph S D)

Variable approx_correct : hd_rules_graph S D << Graph.

a decomposition cs = c1; ..; cn is valid wrt D if for all i, for all rule b in ci, for all j > i, and for all rule c in cj, there is no edge from b to c

  Fixpoint valid_decomp (cs : decomp) : bool :=
    match cs with
      | nil => true
      | ci :: cs' => valid_decomp cs' &&
        forallb (fun b =>
          forallb (fun cj =>
            forallb (fun c => negb (approx b c)) cj)
          cs')
        ci
    end.

relation corresponding to a decomposition

  Fixpoint Union (cs : decomp) : relation term :=
    match cs with
      | nil => empty_rel
      | ci :: cs' => hd_red_Mod S ci U Union cs'
    end.

  Lemma decomp_incl :
    forall cs (hyp1 : incl D (flat cs)), hd_red_Mod S D << Union cs.

  Lemma In_Union_elim : forall cs x y, Union cs x y ->
    exists ci, In ci cs /\ hd_red_Mod S ci x y.

main theorem

  Lemma WF_hd_red_Mod_decomp :
    forall (hypD : rules_preserve_vars D)
      (cs : decomp)
      (hyp1 : incl (flat cs) D)
      (hyp2 : valid_decomp cs = true)
      (hyp3 : lforall (fun ci => WF (hd_red_Mod S ci)) cs),
      WF (Union cs).

  Lemma WF_decomp :
    forall (hypD : rules_preserve_vars D)
      (cs : decomp)
      (hyp1 : incl D (flat cs))
      (hyp2 : incl (flat cs) D)
      (hyp3 : valid_decomp cs = true)
      (hyp4 : lforall (fun ci => WF (hd_red_Mod S ci)) cs),
      WF (hd_red_Mod S D).

improvement

  Definition co_scc ci :=
    forallb (fun r => forallb (fun s => negb (approx r s)) ci) ci.

  Lemma WF_co_scc : forall (hypD : rules_preserve_vars D) ci,
    incl ci D -> co_scc ci = true -> WF (hd_red_Mod S ci).

  Lemma WF_decomp_co_scc :
    forall (hypD : rules_preserve_vars D)
      (cs : decomp)
      (hyp4 : incl D (flat cs))
      (hyp1 : incl (flat cs) D)
      (hyp2 : valid_decomp cs = true)
      (hyp3 : lforall (fun ci => co_scc ci = true \/ WF (hd_red_Mod S ci)) cs),
      WF (hd_red_Mod S D).

End S.

tactics

Ltac co_scc := check_eq || fail 10 "not a co_scc".

Ltac graph_decomp Sig f d :=
  apply WF_decomp_co_scc with (approx := f) (cs := d);
  [idtac
    | rules_preserve_vars
    | incl_rule Sig || fail 10 "the decomposition does not contain all DPs"
    | incl_rule Sig || fail 10 "the decomposition contains a rule that is not a DP"
    | check_eq || fail 10 "the decomposition is not valid"
    | unfold lforall; repeat split].