Library CoLoR.DP.ASCCUnion

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
• Leo Ducas, 2007-08-06
Modular termination proof through SCC of an over DPGraph

Set Implicit Arguments.

Section S.

Variable Sig : Signature.

Notation rule := (rule Sig). Notation rules := (list rule).

Variables (S : relation (term Sig)) (R : rules) (hyp : rules_preserve_vars R).

Notation DPG := (hd_rules_graph S R).
Notation rule_eq_dec := (@ATrs.eq_rule_dec Sig).
Notation dim := (length R).

Variables (ODPG : relation rule) (over_DPG : DPG << ODPG)
(restriction : is_restricted ODPG R) (R_nodup : nodup R)
(ODPG_dec : forall x y, {ODPG x y} + {~ODPG x y}).

Definition hyps := mkSCC_dec_hyps rule_eq_dec restriction R_nodup ODPG_dec.

Variables (M : matrix dim dim) (HM : M = SCC_mat_effective hyps) .

Notation empty := (fun _ _ => False).

Definition proj1_sig2 T P Q (e : @sig2 T P Q) :=
match e with
| exist2 _ _ a b c => a
end.

Definition s_SCC's := proj1_sig2 (sorted_SCC' hyps HM).

Notation ODPGquo' := (Rquo' hyps HM).

s_SCC's properties
chain restricted to an SCC

Notation SCC' := (SCC' hyps).
Notation SCC'_tag := (SCC'_tag hyps).
Notation SCC'_dec := (SCC'_dec hyps).

Definition hd_red_SCC' i t1 t2 := exists l, exists r, exists s,
SCC'_tag HM (mkRule l r) = Some i /\ t1 = sub s l /\ t2 = sub s r.

Lemma hd_red_SCC'_cover t1 t2 : hd_red R t1 t2 ->
exists i, hd_red_SCC' i t1 t2 /\ i<dim.

Definition hd_red_Mod_SCC' i := S @ hd_red_SCC' i.

union of chain_SCC'

Notation union := Relation_Operators.union.

Definition sorted_hd_red_Mod_SCC' := map hd_red_Mod_SCC' s_SCC's.

Definition hd_red_Mod_SCC'_union :=
fold_right (@union (term Sig)) empty sorted_hd_red_Mod_SCC'.

Lemma union_list_spec : forall (A : Type) L (x y : A) (r : relation A),
In r L -> r x y -> fold_right (@union A) empty L x y.

Lemma union_list_spec2 : forall (A : Type) L (x y : A),
fold_right (@union A) empty L x y -> exists r, In r L /\ r x y.

Lemma hd_red_Mod_SCC'_cover : hd_red_Mod S R << hd_red_Mod_SCC'_union.

properties of the total order RT relatively to restricted chain

Notation RT_ODPG := (RT hyps HM).

Lemma compose_empty :
forall i j, RT_ODPG i j -> hd_red_Mod_SCC' j @ hd_red_Mod_SCC' i << empty.

Proof of the modular termination criterion

Lemma WF_SCC'_union_aux : forall L,
(forall i, In i L -> WF (hd_red_Mod_SCC' i)) -> sort RT_ODPG L ->
WF (fold_right (@union _) empty (map hd_red_Mod_SCC' L)).

Lemma WF_SCC'_union :
(forall i, i < dim -> WF (hd_red_Mod_SCC' i)) -> WF (hd_red_Mod S R).

Fixpoint SCC'_list_aux i L :=
match L with
| nil => nil
| x :: q =>
match eq_opt_dec eq_nat_dec (SCC'_tag HM x) (Some i) with
| left _ => x :: @SCC'_list_aux i q
| right _ => @SCC'_list_aux i q
end
end.

Lemma SCC'_list_aux_exact : forall i L r,
In r (SCC'_list_aux i L) <-> In r L /\ SCC'_tag HM r = Some i.

Lemma nodup_SCC'_list_aux : forall i L, nodup L -> nodup (SCC'_list_aux i L).

Definition SCC'_list i := SCC'_list_aux i R.

Lemma SCC'_list_exact : forall i r,
In r (SCC'_list i) <-> SCC'_tag HM r = Some i.

Lemma nodup_SCC'_list : forall i, nodup (SCC'_list i).

Lemma chain_SCC'_red_Mod : forall i,
hd_red_Mod_SCC' i << hd_red_Mod S (SCC'_list i).

A faster way to compute SCC'_list but only half-certified

Definition SCC_list_fast i (Hi : i < dim) :=
listfilter R (list_of_vec (Vnth M Hi)).

Lemma incl_SCC_list_fast i (Hi : i < dim) :
Vnth (Vnth M Hi) Hi = true -> incl (SCC'_list i) (SCC_list_fast Hi).

Lemma hd_red_Mod_SCC'_hd_red_Mod_fast : forall i (Hi : i < dim),
Vnth (Vnth M Hi) Hi = true ->
hd_red_Mod_SCC' i << hd_red_Mod S (SCC_list_fast Hi).

Some lemma to prove trivial case of sub-problem termination

Lemma red_Mod_SCC_trivial_empty : WF (hd_red_Mod S nil).

Lemma WF_chain_SCC_trivial : forall i,
SCC'_list i = nil -> WF (hd_red_Mod_SCC' i).

Lemma red_Mod_SCC_trivial_singl : forall i r,
SCC'_list i = r :: nil -> ~ODPG r r -> WF (hd_red_Mod_SCC' i).

Lemma WF_hd_red_Mod_SCC_fast_trivial : forall i (Hi : i < dim),
SCC_list_fast Hi = nil -> WF (hd_red_Mod_SCC' i).

End S.

tactics

Ltac use_SCC_tag h M S R t :=
let x := fresh in
(set (x := SCC_tag_fast h M t); norm_in x (SCC_tag_fast h M t);
match eval compute in x with
| Some ?X1 =>
let Hi := fresh in
(assert (Hi : X1 < length R);
[ norm (length R); omega
| let L := fresh in
(set (L := SCC_list_fast R M Hi);
norm_in L (SCC_list_fast R M Hi);
assert (WF (hd_red_Mod S L)); subst L; clear Hi; clear x)])
end).

Ltac use_SCC_hyp M l :=
let b := fresh "b" in
(set (b := Vnth (Vnth M l) l);
norm_in b (Vnth (Vnth M l) l);
match eval compute in b with
| false => apply WF_hd_red_Mod_SCC_fast_trivial with (Hi:=l); eauto
| true => eapply WF_incl;
[eapply hd_red_Mod_SCC'_hd_red_Mod_fast with (Hi:=l); auto | auto]
end).

Ltac use_SCC_all_hyps M i Hi Hj :=
let rec aux x :=
match x with
| 0 => omega
| S ?y => destruct i; [use_SCC_hyp M Hi | aux y]
end in
match type of Hj with
| le _ ?Y => aux Y
end.

Ltac SCC_name n1 n2 :=
match goal with
| |- WF (chain ?R) => set (n1 := dp R); set (n2 := int_red R #)
| |- WF (hd_red_mod ?E ?R) => set (n1 := R); set (n2 := red E #)
| |- WF (?X @ hd_red ?R) => set (n1 := R); set (n2 := X)
| |- WF (hd_red_Mod ?E ?R) => set (n1 := R); set (n2 := E)
end.