# Library CoLoR.NonTermin.ALoop

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 a TRS

Set Implicit Arguments.

Section S.

Variable Sig : Signature.

Notation term := (term Sig). Notation beq_rule := (@beq_rule 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 terms_of_reduc : forall t, {us| FS t us} -> list term.

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

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

data necessary for a sequence of rewrite steps

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

Definition rewrite (t : term) (d : data) : option term :=
let (p,a) := d in let (l,r) := a in
if mem beq_rule (mkRule l r) R then
match subterm_pos t p with
| None => None
| Some u =>
match matches l u with
| None => None
| Some s => replace_pos t p (sub s r)
end
end
else None.

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

Fixpoint rewrites t (ds : list data) : option (list term) :=
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 := (Var 0).

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 : term) (ds : list data)
(us : list term) (h1 : rewrites t ds = Some us).

Definition k := length us.

Definition nth i := nth i us default.

Definition last_term := nth (k-1).

Variable h0 : k > 0.

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

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_g : forall a b, red R a b -> red R (g a) (g b).

Definition seq : nat -> term.

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 subterm_pos u p with
| None => false
| Some v =>
match matches t v 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.