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.