Require Import Prelim.

Section string_rewriting.

  Variable sig: Type.
  Definition rule : Type := list sig * list sig.
  Definition srs := list rule.

  Implicit Types (a b c: sig) (x y z u v: list sig)
                 (r: list sig* list sig) (R S: srs).

  Inductive rew : srs -> list sig -> list sig -> Prop:=
  |rewR R x u y v : (u,v) el R -> rew R (x++u++y) (x++v++y).
  Hint Constructors rew.

  Inductive rewt (S: srs) (x: list sig) : list sig -> Prop :=
  |rewtRefl : rewt S x x
  |rewtRule y z : rew S x y -> rewt S y z -> rewt S x z.
  Hint Constructors rewt.

  Lemma rewtTrans R x y z:
    rewt R x y -> rewt R y z -> rewt R x z.
  Proof.
    induction 1. auto. intros IH. now apply rewtRule with (y:= y), IHrewt.
  Qed.

  Lemma subset_rewriting S R x y:
    S <<= R -> rewt S x y -> rewt R x y.
  Proof.
    intros Sub H. induction H. auto. apply rewtRule with (y:=y).
    inv H. apply rewR with (x:=x0) (u:=u) (v:=v). now apply Sub. exact IHrewt.
  Qed.

  Lemma rewrite_app R x y z:
    rewt R x y -> rewt R (z++x) (z++y).
  Proof.
    induction 1. auto. inv H. revert IHrewt. apply rewtRule.
    rewrite app_assoc. setoid_rewrite app_assoc at 2. now apply rewR.
  Qed.

End string_rewriting.

Definition SR (S: sigT (fun (sig:finType) => (prod (prod (srs sig) (list sig)) (list sig)))) :=
   match (projT2 S) with
    |(rules,x,y) => rewt rules x y
   end.

Definition RSR (S: sigT (fun (sig:finType) =>
                            (prod (prod {R:srs sig |forall r,r el R -> (fst r) <> nil /\ (snd r) <> nil}
                                        (list sig)) (list sig)))) :=
    match (projT2 S) with
    |((exist _ R H),x,y) => rewt R x y
    end.