Library CoLoR.Term.String.SReverse

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2008-02-04
string reversing
Termination of String Rewriting Proved Automatically, H. Zantema, Journal of Automated Reasoning, 2005, volume 34, pages 105-139

Set Implicit Arguments.


Section S.

Variable Sig : Signature.

Definition reverse (e : rule Sig) := let (l,r) := e in mkRule (rev' l) (rev' r).

Notation reverses := (List.map reverse).

Lemma red_rev : forall R t u, red R t u -> red (reverses R) (rev' t) (rev' u).

Lemma red_rev_rtc : forall E t u,
  red E # t u -> red (reverses E) # (rev' t) (rev' u).

Lemma red_mod_rev : forall E R t u,
  red_mod E R t u -> red_mod (reverses E) (reverses R) (rev' t) (rev' u).


Lemma WF_red_mod_rev : forall E R,
  WF (red_mod (reverses E) (reverses R)) -> WF (red_mod E R).

Lemma reverse_reverse : forall a, reverse (reverse a) = a.

Lemma reverses_reverses : forall R, reverses (reverses R) = R.

Lemma WF_red_mod_rev_eq : forall E R,
  WF (red_mod (reverses E) (reverses R)) <-> WF (red_mod E R).

Lemma WF_red_rev_eq : forall R, WF (red (reverses R)) <-> WF (red R).

End S.

tactics for Rainbow

Ltac rev_tac := rewrite <- WF_red_rev_eq || rewrite <- WF_red_mod_rev_eq.