Library CoLoR.Term.String.Srs

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2005-02-17
string rewriting

Set Implicit Arguments.

Require Import Relations.
Require Import LogicUtil.
Require Export SContext.
Require Import RelUtil.

basic definitions

Section definition.

Variable Sig : Signature.

Notation string := (list Sig).

Record rule : Type := mkRule { lhs : string; rhs : string }.

Definition red R : relation string := fun s1 s2
   l, r, c,
    In (mkRule l r) R s1 = fill c l s2 = fill c r.

Definition red_mod E R := red E # @ red R.

End definition.

Implicit Arguments mkRule [Sig].

tactics

Ltac redtac := repeat
  match goal with
    | H : red _ ?t ?u |- _
      let l := fresh "l" in let r := fresh "r" in let c := fresh "c" in
      let h1 := fresh in
      (unfold red in H; destruct H as [l]; destruct H as [r];
        destruct H as [c]; destruct H as [H h1]; destruct h1)
    | H : red_mod _ _ _ _ |- _do 2 destruct H; redtac
  end.

basic properties

Section S.

Variable Sig : Signature.

Notation string := (list Sig).
Notation rule := (rule Sig).

Variable R : list rule.

Lemma red_rule : l r c, In (mkRule l r) R red R (fill c l) (fill c r).

Proof.
intros. unfold red. l. r. c. auto.
Qed.

Lemma red_fill : c t u, red R t u red R (fill c t) (fill c u).

Proof.
intros. redtac. unfold red.
l. r. (comp c c0). split. assumption.
subst t. subst u. do 2 rewrite fill_comp. auto.
Qed.

Lemma red_nil : x y : string, red nil x y x = y.

Proof.
unfold red. intros. decomp H. destruct H1.
Qed.

Lemma red_nil_rtc : x y : string, red nil # x y x = y.

Proof.
induction 1. apply red_nil. exact H. refl. transitivity y; assumption.
Qed.

Lemma red_mod_empty_incl_red : red_mod nil R << red R.

Proof.
unfold inclusion. intros. redtac. ded (red_nil_rtc H). subst x0.
subst x. subst y. apply red_rule. exact H0.
Qed.

Lemma red_incl_red_mod_empty : red R << red_mod nil R.

Proof.
unfold inclusion. intros. x. split. apply rt_refl. exact H.
Qed.

Lemma red_mod_empty : red_mod nil R == red R.

Proof.
split. apply red_mod_empty_incl_red. apply red_incl_red_mod_empty.
Qed.

End S.

tactics

Require Import SN.

Ltac no_relative_rules :=
  match goal with
    |- WF (@red_mod ?S ?E _) ⇒
      norm E; eapply WF_incl; [apply (@red_mod_empty_incl_red S) | idtac]
    | _idtac
  end.