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

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

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

s_SCC's properties

  Lemma s_SCC's_spec_cover i : i < dim -> In i s_SCC's.

  Lemma s_SCC's_spec_bound i : In i s_SCC's -> i < dim.

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

  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.


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

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]

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

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)