Library CoLoR.NonTermin.AModLoop

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2009-05-20
definition and correctness proof of a boolean function checking that there is a loop in a relative TRS

Set Implicit Arguments.

Section S.

  Variable Sig : Signature.

  Notation term := (term Sig). Notation data := (data Sig).

  Variable E R : rules Sig.

predicates saying that t::us is in a sequence of rewriting steps

  Fixpoint mod_FS t us :=
    match us with
      | nil => True
      | u :: us' => red_mod E R t u /\ mod_FS u us'

  Definition mod_terms_of_reduc : forall t, {us| mod_FS t us} -> list term.

  Definition mod_proof_of_reduc :
    forall t, forall x : {us| mod_FS t us}, mod_FS t (mod_terms_of_reduc x).

data necessary for a sequence of red_mod steps

  Definition mod_data := (list data * data)%type.

  Definition mod_rewrite (t : term) (dm : mod_data) : option term :=
    let (ds,d) := dm in
      match rewrites E t ds with
        | None => None
        | Some ts => rewrite R (last ts t) d

  Lemma mod_rewrite_correct : forall t dm u,
    mod_rewrite t dm = Some u -> red_mod E R t u.

  Fixpoint mod_rewrites t (mds : list mod_data) : option (list term) :=
    match mds with
      | nil => Some nil
      | md :: mds' =>
        match mod_rewrite t md with
          | None => None
          | Some u =>
            match mod_rewrites u mds' with
              | None => None
              | Some us => Some (u::us)

  Lemma mod_rewrites_correct : forall ds t us,
    mod_rewrites t ds = Some us -> mod_FS t us.

  Notation default := (Var 0).

  Lemma mod_FS_red : forall ts t, mod_FS t ts -> forall i, i < length ts ->
    red_mod E R (nth i (t::ts) default) (nth (S i) (t::ts) default).

hyps for non-termination

  Section loop.

    Variables (t : term) (mds : list mod_data)
      (us : list term) (h1 : mod_rewrites t mds = Some us).

    Definition k := length us.

    Variable h0 : k > 0.

    Definition nth i := nth i us default.

    Definition last_term := nth (k-1).

    Lemma red_mod_nth : forall i, i < k-1 -> red_mod E R (nth i) (nth (S i)).

    Variables (ds : list data) (us' : list term)
      (h1' : rewrites E last_term ds = Some us').

    Definition last_term' := last us' last_term.

    Variables (p : position) (u : term) (h2 : subterm_pos last_term' p = Some u)
      (s : substitution Sig) (h3 : matches t u = Some s).

proof of non-termination

    Definition c : context Sig.

    Definition g t := fill c (sub s t).

    Lemma last_term'_g : last_term' = g t.

    Lemma red_last_term_g : red E # last_term (g t).

    Lemma red_mod_g : forall a b, red_mod E R a b -> red_mod E R (g a) (g b).

    Definition seq : nat -> term.

    Lemma IS_seq : IS (red_mod E R) seq.

    Lemma loop : EIS (red_mod E R).

  End loop.

boolean function testing non-termination

  Definition is_mod_loop t mds ds p :=
    match mod_rewrites t mds with
      | None => false
      | Some us =>
        match us with
          | nil => false
          | _ =>
            let u := last us default in
              match rewrites E u ds with
                | None => false
                | Some us' =>
                  let u' := last us' u in
                    match subterm_pos u' p with
                      | None => false
                      | Some v =>
                        match matches t v with
                          | None => false
                          | Some _ => true

  Lemma is_mod_loop_correct : forall t mds ds p,
    is_mod_loop t mds ds p = true -> EIS (red_mod E R).

End S.


Ltac loop t' mds' ds' p' :=
  apply is_mod_loop_correct with (t:=t') (mds:=mds') (ds:=ds') (p:=p');
    (check_eq || fail 10 "not a loop").