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