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.


strings

Section definition.

Variable Sig : Signature.

Definition string := list Sig.

Definition beq_string := beq_list (@beq_symb Sig).
Definition beq_string_ok := beq_list_ok (@beq_symb_ok Sig).

rules

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

Fixpoint beq_rule (a1 a2 : rule) : bool :=
  let (l1,r1) := a1 in let (l2,r2) := a2 in
    beq_string l1 l2 && beq_string r1 r2.

Lemma beq_rule_ok : forall a1 a2, beq_rule a1 a2 = true <-> a1 = a2.

Definition rules := list rule.

rewriting

Definition red R : relation string := fun s1 s2 =>
  exists l, exists r, exists 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.


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 w := fresh "ww" in
      unfold red in H; destruct H as [l [r [c [? [? ?]]]]]; try subst

    | H : red_mod _ _ _ _ |- _ =>
      do 2 destruct H; redtac
  end.

basic properties

Section S.

Variable Sig : Signature.

Notation string := (string Sig). Notation rules := (rules Sig).

Section red.

Variable R : rules.

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

Lemma red_rule_top : forall l r, In (mkRule l r) R ->
  red R l r.

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

Lemma rtc_red_fill : forall c t u,
  red R # t u -> red R # (fill c t) (fill c u).

Lemma red_nil : forall x y : string, red nil x y -> x = y.

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

Lemma red_mod_empty_incl_red : red_mod nil R << red R.

Lemma red_incl_red_mod_empty : red R << red_mod nil R.

Lemma red_mod_empty : red_mod nil R == red R.

End red.

Section red_mod.

Variables E R : rules.

Lemma red_mod_fill : forall c t u,
  red_mod E R t u -> red_mod E R (fill c t) (fill c u).

End red_mod.

End S.

tactics


Ltac remove_relative_rules E := norm E; rewrite red_mod_empty
  || fail "this certificate cannot be applied on a relative system".

Ltac no_relative_rules :=
  match goal with
    | |- WF (red_mod ?E _) => remove_relative_rules E
    | |- EIS (red_mod ?E _) => remove_relative_rules E
    | |- _ => idtac
  end.