Library CoLoR.NonTermin.SLoop

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui & Wang Qian & Zhang Lianyi, 2009-05-11
definition and correctness proof of a boolean function checking that there is a loop in an SRS

Set Implicit Arguments.


Section S.

  Variable Sig : Signature.

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

  Ltac case_beq_symb := VSignature.case_beq_symb Sig.

  Variable R : rules Sig.

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

  Fixpoint FS t us :=
    match us with
      | nil => True
      | u :: us' => red R t u /\ FS u us'
    end.

  Definition strings_of_reduc : forall t, {us| FS t us} -> list string.



  Definition proof_of_reduc :
    forall t, forall x : {us| FS t us}, FS t (strings_of_reduc x).



  Lemma FS_rtc : forall us t, FS t us -> red R # t (last us t).

matching

  Fixpoint matches (p t : string) : option string :=
    match p, t with
      | nil, _ => Some t
      | a :: p', b :: t' => if beq_symb a b then matches p' t' else None
      | _, _ => None
    end.

  Lemma matches_correct : forall p t u, matches p t = Some u -> t = p ++ u.


  Lemma matches_complete : forall p t u, t = p ++ u -> matches p t = Some u.

data necessary for a sequence of rewrite steps


  Definition data := (nat * rule Sig)%type.

  Definition rewrite (t : string) (d : data) : option string :=
    let (p,a) := d in let (l,r) := a in
      if mem (@beq_rule Sig) (mkRule l r) R then
        match split t p with
          | None => None
          | Some (u,v) =>
            match matches l v with
              | None => None
              | Some w => Some (u ++ r ++ w)
            end
        end
        else None.

  Lemma rewrite_correct : forall t d s, rewrite t d = Some s -> red R t s.


  Fixpoint rewrites t (ds : list data) : option (list string) :=
    match ds with
      | nil => Some nil
      | d :: ds' =>
        match rewrite t d with
          | None => None
          | Some u =>
            match rewrites u ds' with
              | None => None
              | Some us => Some (u::us)
            end
        end
    end.

  Lemma rewrites_correct : forall ds t us, rewrites t ds = Some us -> FS t us.



  Notation default := (@nil letter).

  Lemma FS_red : forall ts t, FS t ts -> forall i, i < length ts ->
    red R (nth i (t::ts) default) (nth (S i) (t::ts) default).

hyps for non-termination

  Section loop.

    Variables (t : string) (ds : list data)
      (us : list string) (h1 : rewrites t ds = Some us).

    Definition k := length us.

    Definition nth i := nth i us default.

    Definition last_string := nth (k-1).

    Variable h0 : k > 0.

    Lemma FS_red' : forall i, i < k - 1 -> red R (nth i) (nth (S i)).

    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.


    Definition seq : nat -> string.



    Lemma IS_seq : IS (red R) seq.

    Lemma loop : EIS (red R).

  End loop.

boolean function testing non-termination

  Definition is_loop t ds p :=
    match rewrites t ds with
      | None => false
      | Some us =>
        match us with
          | nil => false
          | _ =>
            let u := last us default in
              match split u p with
                | None => false
                | Some (_,w) =>
                  match matches t w with
                    | None => false
                    | Some _ => true
                  end
              end
        end
    end.

  Lemma is_loop_correct : forall t ds p, is_loop t ds p = true -> EIS (red R).

End S.


tactics

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

Ltac loop t' ds' p' :=
  match goal with
    | |- EIS (red_mod ?E _) =>
      remove_relative_rules E; check_loop t' ds' p'
    | |- EIS (red _) => check_loop t' ds' p'
  end.