Library CoLoR.NonTermin.SModLoop

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

Set Implicit Arguments.


Section S.

  Variable Sig : Signature.

  Notation letter := (symbol Sig). Notation string := (string Sig).
  Notation data := (data Sig).

  Variables 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'
    end.

  Definition mod_strings_of_reduc : forall t, {us| mod_FS t us} -> list string.



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


data necessary for a sequence of red_mod steps

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

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

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


  Fixpoint mod_rewrites t (mds : list mod_data) : option (list string) :=
    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)
            end
        end
    end.

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


  Notation default := (@nil letter).


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

hyps for non-termination

  Section loop.

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

    Definition k := length us.

    Definition nth i := List.nth i us default.

    Definition last_string := nth (k-1).

    Variable h0 : k > 0.

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

    Variables (ds : list data) (us' : list string)
      (h1' : rewrites E last_string ds = Some us').

    Definition last_string' := last us' last_string.

    Variables (p : nat) (u v : string) (h2 : split last_string' p = Some (u,v))
      (s : string) (h3 : matches t v = Some s).

proof of non-termination

    Definition c := mkContext u s.

    Definition g t := fill c t.

    Lemma last_string'_g : last_string' = g t.


    Lemma red_last_string_g : red E # last_string (g t).


    Definition seq : nat -> string.



    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 split u' p with
                      | None => false
                      | Some (_,w) =>
                        match matches t w with
                          | None => false
                          | Some _ => true
                        end
                    end
              end
        end
    end.

  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.

tactics

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