# 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.