Library CoLoR.DP.ADecomp
CoLoR, a Coq library on rewriting and termination.
See the COPYRIGHTS and LICENSE files.
decomposition of an over DP graph
- Frederic Blanqui, 2008-05-19
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)
a decomposition of a list of rules is a list of list of rules
we assume given a decidable graph on rules
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].