Library CoLoR.Term.String.SReverse
CoLoR, a Coq library on rewriting and termination.
See the COPYRIGHTS and LICENSE files.
string reversing
Termination of String Rewriting Proved Automatically, H. Zantema,
Journal of Automated Reasoning, 2005, volume 34, pages 105-139
- Frederic Blanqui, 2008-02-04
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