Reducing Restricted String Rewriting to PCP


Require Import Prelim Reductions String_rewriting PCP.

Section srs_pcp.
  Variable sig: finType.

  Inductive psig' : Type := hash | sigma (s: sig).
  Inductive psig : Type := dollar | Left (p: psig') | Right (p: psig').

  Definition tagL := map (fun (s: sig) => Left (sigma s)).
  Definition tagR := map (fun (s: sig) => Right (sigma s)).

  Notation "$" := dollar.
  Notation "#" := hash.

  Lemma split_map_fst_LR A:
    concat (map fst (map (fun s => ([Left(sigma s)], [Right(sigma s)])) A)) = tagL A.
  Proof.
    induction A. auto. cbn. rewrite IHA. reflexivity.
  Qed.

  Lemma split_map_fst_RL A:
    concat (map fst (map (fun s => ([Right(sigma s)], [Left(sigma s)])) A)) = tagR A.
  Proof.
    induction A. auto. cbn. rewrite IHA. reflexivity.
  Qed.

  Lemma split_map_snd_LR A:
    concat (map snd (map (fun s => ([Left(sigma s)], [Right(sigma s)])) A)) = tagR A.
  Proof.
    induction A. auto. cbn. rewrite IHA. reflexivity.
  Qed.

  Lemma split_map_snd_RL A:
    concat (map snd (map (fun s => ([Right(sigma s)], [Left(sigma s)])) A)) = tagL A.
  Proof.
    induction A. auto. cbn. rewrite IHA. reflexivity.
  Qed.

Definition of PCP Dominoes


  Definition sigma_psig_lr A :=
    (map (fun s => ([Left(sigma s)], [Right(sigma s)])) A)
      ++ (map (fun s => ([Right(sigma s)], [Left(sigma s)])) A).

  Definition sigma_psig_pair_list_lr (A: list (list sig * list sig)) :=
    (map (fun p => (tagL (fst p), tagR (snd p))) A)
      ++ (map (fun p => (tagR (fst p), tagL (snd p))) A).

  Definition pcp_dominos' (R: srs sig) :=
    sigma_psig_lr (elem sig)
                  ++ sigma_psig_pair_list_lr R
                  ++ [([Left #],[Right #]);([Right #],[Left #])].

  Definition pcp_rules_left (R: srs sig) :=
    (map (fun s => ([Left(sigma s)], [Right(sigma s)])) (elem sig))
      ++ (map (fun p => (tagL (fst p), tagR (snd p))) R).

  Definition pcp_rules_right (R: srs sig) :=
    (map (fun s => ([Right(sigma s)], [Left(sigma s)])) (elem sig))
      ++ (map (fun p => (tagR (fst p), tagL (snd p))) R).

  Definition firstD (x: list sig) := ([$],$::(tagL x)++[Left #]).
  Definition lastD (y: list sig) := ((tagL y)++[Left #;$],[$]).

  Definition pcp_dominos (R: srs sig) :=
    ([Left #],[Right #])::([Right #],[Left #])::(pcp_rules_left R ++ pcp_rules_right R).

  Definition red' R x y := (firstD x)::(lastD y)::(pcp_dominos R).

  Lemma map_RL_in_dominos A R:
    map (fun s : sig => ([Right (sigma s)], [Left (sigma s)])) A <<= pcp_dominos R.
  Proof.
    intros a HA. apply in_map_iff in HA as [x [H1 H2]]. subst. right. right.
    apply in_app_iff. right. apply in_app_iff. left. apply in_map_iff. exists x. now split.
  Qed.

  Lemma map_LR_in_dominos A R:
    map (fun s : sig => ([Left (sigma s)], [Right (sigma s)])) A <<= pcp_dominos R.
  Proof.
    intros a HA. apply in_map_iff in HA as [x [H1 H2]]. subst. right. right.
    apply in_app_iff. left. apply in_app_iff. left. apply in_map_iff. exists x. now split.
  Qed.

  Lemma left_right_in_dominos R s:
    ([Left (sigma s)],[Right (sigma s)]) el pcp_dominos R.
  Proof.
    right. right. apply in_app_iff. left. apply in_app_iff. left. apply in_map_iff.
    exists s. now split.
  Qed.

  Lemma right_left_in_dominos R s:
    ([Right (sigma s)],[Left (sigma s)]) el pcp_dominos R.
  Proof.
    right. right. apply in_app_iff. right. apply in_app_iff. left. apply in_map_iff.
    exists s. now split.
  Qed.

  Lemma rule_LR_in_dominos R u v:
    (u,v) el R -> (tagL u, tagR v) el pcp_dominos R.
  Proof.
    intros H. right. right. apply in_app_iff. left. apply in_app_iff. right.
    apply in_map_iff. exists (u,v). now split.
  Qed.

  Lemma rule_RL_in_dominos R u v:
    (u,v) el R -> (tagR u, tagL v) el pcp_dominos R.
  Proof.
    intros H. right. right. apply in_app_iff. right. apply in_app_iff. right.
    apply in_map_iff. exists (u,v). now split.
  Qed.

String Rewriting to PCP Match


  Definition reduction_srs_pcp (P: srs sig * list sig * list sig) : list (list psig * list psig) :=
    match P with
    |((R,x),y) => red' R x y
    end.

  Lemma rewrite_exists_pcp_list R x y:
    rewt R x y -> (exists A, (concat (map fst A))++(tagL y)++[Left #] =
                       (tagL x++[Left #]++(concat (map snd A))) /\ A <<= (pcp_dominos R)).
  Proof.
    induction 1.
     + exists []. split; auto.
     + destruct IHrewt as [A [HA HB]]. inv H.
       exists ((map (fun s => ([Left (sigma s)],[Right (sigma s)])) x0)
                                     ++[((tagL u),(tagR v))]
                                     ++(map (fun s => ([Left (sigma s)],
                                                    [Right (sigma s)])) y0)
                                     ++ [([Left #],[Right #])]
                                     ++ (map (fun s => ([Right (sigma s)],[Left (sigma s)])) (x0++v++y0))
                                     ++ [([Right #],[Left #])]++A). split.
       * rewrite !map_app, !concat_app, !split_map_fst_LR, !split_map_snd_LR, !split_map_fst_RL,
         !split_map_snd_RL. cbn. rewrite !app_nil_r, <- !app_assoc. cbn.
         rewrite <- !app_assoc, <- app_comm_cons, HA. unfold tagL, tagR.
         rewrite !map_app. cbn. now rewrite <- !app_assoc.
       * intros a [H|[H%in_sing|[H|[H%in_sing|[H|[H|H]]%in_app_iff]%in_app_iff]
                                  %in_app_iff]%in_app_iff]%in_app_iff.
          -- now apply (@map_LR_in_dominos x0 R).
          -- subst. now apply rule_LR_in_dominos.
          -- now apply (@map_LR_in_dominos y0 R).
          -- subst. now left.
          -- now apply (@map_RL_in_dominos (x0++v++y0) R).
          -- subst. right. now left.
          -- now apply HB.
  Qed.

  Theorem reduction_string_rewriting_pcp R x y:
    rewt R x y -> PCP (red' R x y).
  Proof.
    intros HR. apply rewrite_exists_pcp_list in HR as [A [H1 H2]]. unfold PCP.
      exists (([$] , ($::(tagL x)++[Left #]))::A++[lastD y]). repeat split.
    - inversion 1.
    - intros e [<-|[HA|HA%in_sing]%in_app_iff].
      + now left.
      + right. right. auto.
      + right. now left.
    - unfold solution. cbn. rewrite !map_app, !concat_app. cbn. rewrite app_nil_r.
      change [Left #; $] with ([Left #]++[$]). setoid_rewrite app_assoc at 2.
      setoid_rewrite app_assoc at 1. rewrite H1. now rewrite <- !app_assoc.
  Qed.

PCP Match to String Rewriting


  Lemma rule_takes_symbol_left a u (A B: list psig):
   u <> nil ->
    tagL u ++ A = tagL a ++ (Left #)::B
    -> exists a', a = u ++ a'.
  Proof.
    intros NN SL. destruct u. contradiction. clear NN.
    revert SL. revert a e. induction u; intros b e H.
    - cbn. destruct b. inv H. inv H. exists b. reflexivity.
    - destruct b. inv H. inv H. destruct (IHu b a). cbn. assumption.
      rewrite H. exists x. now cbn.
  Qed.

  Lemma rule_takes_symbol_right a u (A B: list psig):
   u <> nil ->
    tagR u ++ A = tagR a ++ (Right #)::B
    -> exists a', a = u ++ a'.
  Proof.
    intros NN SL. destruct u. contradiction. clear NN.
    revert SL. revert a e. induction u; intros b e H.
    - cbn. destruct b. inv H. inv H. exists b. reflexivity.
    - destruct b. inv H. inv H. destruct (IHu b a). cbn. assumption.
      rewrite H. exists x. now cbn.
  Qed.

  Lemma lastD_false y b d D A B:
   (tagL (y) ++ [Left #; $]) ++ A = tagL (b) ++ Left # :: tagR (d::D) ++ B -> False.
  Proof.
    revert b. induction y; intros b HC; cbn in *; destruct b; inv HC.
    apply (IHy b H1).
  Qed.

  Lemma pcp_first_rule R A x y a1 a2:
    (forall p, p el R -> fst p <> [] /\ snd p <> []) ->
    (a1,a2) el (red' R x y) ->
    a1 ++ (concat (map fst A)) = a2 ++ (concat (map snd A))
    -> (a1,a2) = ([$],$::(tagL x)++[Left #]).
  Proof.
    intros HM.
    intros [H1|[H1|[H1|[H1|[[H1|H1]%in_app_iff|[H1|H1]%in_app_iff]%in_app_iff]]]];
      try (apply in_map_iff in H1 as [? [H1 ?]]); inv H1; try now inversion 1.
    - destruct y; inversion 1.
    - destruct (HM x0 H). destruct (fst x0), (snd x0); try contradiction. inversion 1.
    - destruct (HM x0 H). destruct (fst x0), (snd x0); try contradiction. inversion 1.
  Qed.

  Lemma next_rules_left' R x y a c A:
    (forall p, p el R -> fst p <> [] /\ snd p <> [])
    -> A <<= red' R x y -> c <> nil
    -> concat (map fst A) = tagL (a) ++ Left # :: (tagR c)++concat (map snd A)
    -> exists A' B b, B <<= pcp_dominos R /\ concat (map fst B ) = tagL a
                /\ concat (map snd B) = tagR b /\ A = B++[([Left #], [Right #])]++A' /\ rewt R a b.
  Proof.
    intros HR. revert A c. pattern a. apply (@size_induction (list sig) (@length sig)).
    intros b IH. intros B c SB NC SL. destruct b.
    - cbn in SL. destruct B. inv SL. destruct (SB p(or_introl eq_refl))
        as [H1|[H1|[H1|[H1|[[H1|H1]%in_app_iff|[H1|H1]%in_app_iff]%in_app_iff]]]].
      + subst. inv SL.
      + subst. destruct y. inv SL. destruct c. contradiction. inv H0. inv SL.
      + exists B, [], []. repeat split. auto. inv H1. auto. constructor.
      + inv H1. inv SL.
      + apply in_map_iff in H1 as [?[]]. subst. inv SL.
      + apply in_map_iff in H1 as [?[]]. subst. destruct (HR x0 H0).
        destruct (fst x0). contradiction. inv SL.
      + apply in_map_iff in H1 as [?[]]. subst. inv SL.
      + apply in_map_iff in H1 as [?[]]. destruct (HR x0 H0).
        destruct (fst x0). contradiction. subst. inv SL.
    - assert (SB' := SB). destruct B. inv SL. destruct (SB p (or_introl eq_refl))
         as [H1|[H1|[H1|[H1|[[H1|H1]%in_app_iff|[H1|H1]%in_app_iff]%in_app_iff]]]].
      + subst. inv SL.
      + subst. cbn[map concat] in SL. destruct c. contradiction. now apply lastD_false in SL.
      + inv H1. inv SL.
      + inv H1. inv SL.
      + apply in_map_iff in H1 as [?[]]. subst. inv SL.
        assert (|b| < |e::b|).
        { cbn. omega. } specialize (IH b H B (c++[e])). destruct IH as [A' [B' [b' [? [? [? []]]]]]].
        intros m HM. apply SB. now right. intros HM. symmetry in HM.
        now apply app_cons_not_nil in HM. unfold tagR. rewrite map_app.
        unfold tagR in H2. cbn in *. rewrite <- app_assoc. exact H2.
        exists A', (([Left (sigma e)], [Right (sigma e)])::B'), (e::b'). repeat split.
        * intros d [<-|HD]. apply left_right_in_dominos. now apply H1.
        * cbn. now rewrite H3.
        * cbn. now rewrite H4.
        * rewrite H5. now cbn.
        * apply rewtTrans with (y:= e::b). constructor. change (e::b) with ([e]++b).
          change (e::b') with ([e]++b'). now apply rewrite_app.
      + apply in_map_iff in H1 as [?[]]. subst. cbn in SL. inv SL. destruct x0 as (u,v).
        destruct (HR (u,v) H0). cbn[fst snd] in *.
        destruct (@rule_takes_symbol_left (e::b) u (concat (map fst B))
                                     (tagR (c) ++ tagR (snd (u, v)) ++ concat (map snd B)) H H1).
        change (Left (sigma e) :: tagL (b) ++ Left # :: tagR (c) ++ tagR (v) ++ concat (map snd B))
          with ((tagL (e::b)) ++ Left # :: tagR (c) ++ tagR (v) ++ concat (map snd B)) in H1.
        rewrite H3 in H1. unfold tagL in H1. rewrite !map_app in H1. rewrite <- app_assoc in H1.
        apply app_inv_head in H1.
        assert (|x0| < |e::b|).
        { rewrite H3. rewrite app_length. destruct u. contradiction. cbn. omega. }
        specialize (IH x0 H4 B (c++v)). destruct IH as [A' [B' [b' [? [? [? []]]]]]].
        intros m HM. apply SB. now right. destruct c. contradiction. inversion 1.
        rewrite H1. unfold tagR, tagL. rewrite map_app. now rewrite <- app_assoc.
        exists A', ((tagL (u), tagR (v))::B'), (v++b'). repeat split.
        * intros d [<-|HD]. now apply rule_LR_in_dominos. now apply H5.
        * cbn. change (Left (sigma e) :: tagL b) with (tagL (e::b)). rewrite H3, H6.
          unfold tagL. now rewrite map_app.
        * cbn. rewrite H7. unfold tagR. now rewrite map_app.
        * rewrite H8. now rewrite app_comm_cons.
        * rewrite H3. apply rewtRule with (y:= v++x0). rewrite <- app_nil_l.
          setoid_rewrite <- app_nil_l at 2. now apply rewR. now apply rewrite_app.
      + apply in_map_iff in H1 as [?[]]. subst. cbn in SL. inv SL.
      + apply in_map_iff in H1 as [?[]]. subst. cbn in SL. destruct (HR x0 H0).
        destruct x0 as (u,v). cbn in *. destruct u. contradiction. inv SL.
  Qed.


  Lemma lastD_equal_symbols y a A B:
        (tagL (y) ++ [Left #; $]) ++ A =
        tagL (a) ++ Left # :: $ :: B -> y = a.
  Proof.
    revert a. induction y; intros b; cbn; destruct b; try inversion 1. auto.
    f_equal. apply (IHy b). assumption.
  Qed.


  Lemma next_rules_left R x y a A:
    (forall p, p el R -> fst p <> [] /\ snd p <> [])
    -> A <<= red' R x y
    -> concat (map fst A) = tagL (a) ++ Left # :: concat (map snd A)
    -> a = y \/ exists A' B b, B <<= pcp_dominos R /\ concat (map fst B ) = tagL a
                /\ concat (map snd B) = tagR b /\ A = B++[([Left #], [Right #])]++A' /\ rewt R a b.
  Proof.
    intros HR SB SL. destruct a.
    - destruct A. inv SL. cbn in SL. destruct (SB p(or_introl eq_refl))
        as [H1|[H1|[H1|[H1|[[H1|H1]%in_app_iff|[H1|H1]%in_app_iff]%in_app_iff]]]].
      + subst. inv SL.
      + subst. cbn in SL. destruct y. now left. inv SL.
      + right. exists A, [], []. repeat split. auto. inv H1. auto. constructor.
      + inv H1. inv SL.
      + apply in_map_iff in H1 as [?[]]. subst. inv SL.
      + apply in_map_iff in H1 as [?[]]. subst. destruct (HR x0 H0).
        destruct (fst x0). contradiction. inv SL.
      + apply in_map_iff in H1 as [?[]]. subst. inv SL.
      + apply in_map_iff in H1 as [?[]]. destruct (HR x0 H0).
        destruct (fst x0). contradiction. subst. inv SL.
    - assert (SB' := SB). destruct A. inv SL. destruct (SB p (or_introl eq_refl))
        as [H1|[H1|[H1|[H1|[[H1|H1]%in_app_iff|[H1|H1]%in_app_iff]%in_app_iff]]]].
      + subst. inv SL.
      + subst. cbn[map concat] in SL. left. symmetry. apply (lastD_equal_symbols SL).
      + inv H1. inv SL.
      + inv H1. inv SL.
      + apply in_map_iff in H1 as [?[]]. subst. inv SL. right.
        destruct (@next_rules_left' R x y a [e] A) as [? [? [? [? [? [? []]]]]]].
        assumption. intros d HE. apply SB. now right. inversion 1. assumption.
        exists x0, (([Left (sigma e)], [Right (sigma e)])::x1), (e::x2). repeat split.
        * intros d [<-|HD]. apply left_right_in_dominos. now apply H.
        * cbn. now rewrite H1.
        * cbn. now rewrite H3.
        * rewrite H4. now rewrite app_comm_cons.
        * change (e::a) with ([e]++a). change (e::x2) with ([e]++x2). now apply rewrite_app.
      + apply in_map_iff in H1 as [?[]]. subst. cbn [map concat] in SL.
        destruct (HR x0 H0). destruct x0 as (u,v). cbn [fst snd] in *.
        destruct (@rule_takes_symbol_left (e::a) u (concat (map fst A))
                                     (tagR(v) ++ concat (map snd A))); try assumption.
        right. rewrite H2 in SL. unfold tagL in SL. rewrite !map_app in SL.
        rewrite <- app_assoc in SL. apply app_inv_head in SL.
        destruct (@next_rules_left' R x y x0 v A) as [? [? [? [? [? [? []]]]]]].
        assumption. intros d HE. apply SB. now right. assumption. exact SL.
        rewrite H2. exists x1, ((tagL (u), tagR (v))::x2), (v++x3). repeat split.
        * intros d [<-|HD]. now apply rule_LR_in_dominos. now apply H3.
        * unfold tagL. rewrite map_app. cbn. f_equal. now rewrite H4.
        * unfold tagR at 2. rewrite map_app. cbn. f_equal. exact H5.
        * rewrite H6. now rewrite app_comm_cons.
        * rewrite <- app_nil_l. setoid_rewrite <- app_nil_l at 2.
          apply rewtRule with (y:= []++v++x0).
          -- now apply rewR.
          -- apply rewrite_app. now apply rewrite_app.
      + apply in_map_iff in H1 as [?[]]. subst. inv SL.
      + apply in_map_iff in H1 as [? []]. subst. cbn in SL.
        destruct (HR x0 H0). destruct x0 as (u,v).
        destruct u. contradiction. inv SL.
  Qed.

  Lemma hash_y_nil R x y A:
    (forall p : list sig * list sig, p el R -> fst p <> [] /\ snd p <> [])
                               -> A <<= red' R x y
                               -> concat (map fst A) = Left # :: concat (map snd A)
                                 \/ concat (map fst A) = Right # :: concat (map snd A)
                               -> [] = y.
  Proof.
    intros HR SB. induction A; intros [].
    - inversion H.
    - inversion H.
    - destruct (SB a (or_introl eq_refl))
               as [H1|[H1|[H1|[H1|[[H1|H1]%in_app_iff|[H1|H1]%in_app_iff]%in_app_iff]]]].
      + subst. inv H.
      + subst. inv H. destruct y. reflexivity. inv H1.
      + subst. inv H. apply IHA. intros a HA. auto. now right.
      + subst. inv H.
      + apply in_map_iff in H1 as [? []]. subst. inv H.
      + apply in_map_iff in H1 as [? []]. subst. destruct (HR x0 H1).
        destruct x0 as (u,v). destruct u. contradiction. inv H.
      + apply in_map_iff in H1 as [? []]. subst. inv H.
      + apply in_map_iff in H1 as [? []]. subst. destruct (HR x0 H1).
        destruct x0 as (u,v). destruct u. contradiction. inv H.
    - destruct (SB a (or_introl eq_refl))
               as [H1|[H1|[H1|[H1|[[H1|H1]%in_app_iff|[H1|H1]%in_app_iff]%in_app_iff]]]].
      + subst. inv H.
      + subst. inv H. destruct y. reflexivity. inv H1.
      + subst. inv H.
      + subst. inv H. apply IHA. intros a HA. auto. now left.
      + apply in_map_iff in H1 as [? []]. subst. inv H.
      + apply in_map_iff in H1 as [? []]. subst. destruct (HR x0 H1).
        destruct x0 as (u,v). destruct u. contradiction. inv H.
      + apply in_map_iff in H1 as [? []]. subst. inv H.
      + apply in_map_iff in H1 as [? []]. subst. destruct (HR x0 H1).
        destruct x0 as (u,v). destruct u. contradiction. inv H.
  Qed.

  Lemma next_rules_right R x y a c A:
    (forall p, p el R -> fst p <> [] /\ snd p <> [])
    -> A <<= red' R x y
    -> concat (map fst A) = tagR (a) ++ Right # :: tagL c ++ concat (map snd A)
    -> exists A' B b, B <<= pcp_dominos R /\ concat (map fst B ) = tagR a
                /\ concat (map snd B) = tagL b /\ A = B++[([Right #], [Left #])]++A' /\ rewt R a b.
  Proof.
    intros HR. revert A c. pattern a. apply (@size_induction (list sig) (@length sig)).
    intros b IH. intros B c SB SL. destruct b; cbn in *.
    - destruct B. inv SL. destruct (SB p(or_introl eq_refl))
        as [H1|[H1|[H1|[H1|[[H1|H1]%in_app_iff|[H1|H1]%in_app_iff]%in_app_iff]]]].
      + subst. inv SL.
      + subst. destruct y; inv SL.
      + subst. inv SL.
      + subst. exists B, [], []. repeat split. auto. constructor.
      + apply in_map_iff in H1 as [?[]]. subst. inv SL.
      + apply in_map_iff in H1 as [?[]]. subst. destruct (HR x0 H0).
        destruct (fst x0). contradiction. inv SL.
      + apply in_map_iff in H1 as [?[]]. subst. inv SL.
      + apply in_map_iff in H1 as [?[]]. destruct (HR x0 H0).
        destruct (fst x0). contradiction. subst. inv SL.
    - assert (SB' := SB). destruct B. inv SL. destruct (SB p (or_introl eq_refl))
         as [H1|[H1|[H1|[H1|[[H1|H1]%in_app_iff|[H1|H1]%in_app_iff]%in_app_iff]]]].
      + subst. inv SL.
      + subst. destruct y; inv SL.
      + inv H1. inv SL.
      + inv H1. inv SL.
      + apply in_map_iff in H1 as [?[]]. subst. inv SL.
      + apply in_map_iff in H1 as [?[]]. subst. cbn in SL. destruct (HR x0 H0).
        destruct x0 as (u,v). cbn in *. destruct u. contradiction. inv SL.
      + apply in_map_iff in H1 as [?[]]. subst. inv SL.
        assert (|b| < S(|b|)) by omega.
        specialize (IH b H B (c++[e])). destruct IH as [A' [B' [b' [? [? [? []]]]]]].
        intros m HM. apply SB. now right. unfold tagL. rewrite map_app.
        rewrite <- app_assoc. cbn. exact H2.
        exists A', (([Right (sigma e)], [Left (sigma e)])::B'), (e::b'). repeat split.
        * intros d [<-|HD]. apply right_left_in_dominos. now apply H1.
        * cbn. now rewrite H3.
        * cbn. now rewrite H4.
        * rewrite H5. now cbn.
        * apply rewtTrans with (y:= e::b). constructor. change (e::b) with ([e]++b).
          change (e::b') with ([e]++b'). now apply rewrite_app.
      + apply in_map_iff in H1 as [?[]]. subst. cbn in SL. destruct x0 as (u,v).
        destruct (HR (u,v) H0). cbn[fst snd] in *.
        change (Right (sigma e) ::tagR (b) ++ Right # :: tagL (c) ++ tagL (v) ++ concat (map snd B))
          with ((tagR (e::b)) ++ Right # :: tagL (c) ++ tagL (v) ++ concat (map snd B)) in SL.
        destruct (@rule_takes_symbol_right (e::b) u (concat (map fst B))
                                           (tagL (c) ++ tagL v ++ concat (map snd B)) H SL).
        rewrite H2 in SL. unfold tagR in SL. rewrite !map_app, <- app_assoc in SL.
        apply app_inv_head in SL. assert (|x0| < (|e::b|)).
        { rewrite H2. rewrite app_length. destruct u. contradiction. cbn. omega. }
        specialize (IH x0 H3 B (c++v)). destruct IH as [A' [B' [b' [? [? [? []]]]]]].
        intros m HM. apply SB. now right. unfold tagL. now rewrite map_app, <- app_assoc.
        exists A', ((tagR (u), tagL (v))::B'), (v++b'). repeat split.
        * intros d [<-|HD]. now apply rule_RL_in_dominos. now apply H4.
        * cbn. change (Right (sigma e) :: tagR b) with (tagR (e::b)). rewrite H2, H5.
          unfold tagR. now rewrite map_app.
        * cbn. rewrite H6. unfold tagL. now rewrite map_app.
        * rewrite H7. now rewrite app_comm_cons.
        * rewrite H2. apply rewtRule with (y:= v++x0). rewrite <- app_nil_l.
          setoid_rewrite <- app_nil_l at 2. now apply rewR. now apply rewrite_app.
  Qed.

  Lemma pcp_rewriting R x y a A:
    (forall p, p el R -> fst p <> [] /\ snd p <> [])
    -> A <<= red' R x y
    -> (concat (map fst A)) = (tagL a)++(Left #)::(concat (map snd A)) \/
      (concat (map fst A)) = (tagR a)++(Right #)::(concat (map snd A))
    -> rewt R a y.
  Proof.
    intros HR. revert a. pattern A.
    apply (@size_induction (srs psig) (@length (list psig* list psig))).
    intros B IH a SB [H|H].
    - destruct (next_rules_left HR SB H) as [<-|[A' [B' [b [SB' [L1 [L2 [L3 L4]]]]]]]].
      constructor. apply rewtTrans with (y:= b). assumption. apply (IH A').
      + rewrite L3. rewrite app_length. cbn. omega.
      + intros c EC. apply SB. rewrite L3. apply in_app_iff. right. apply in_app_iff. now right.
      + right. rewrite L3 in H. rewrite !map_app, !concat_app in H. rewrite L1, L2 in H.
        cbn in H. apply app_inv_head in H. now inv H.
    - setoid_rewrite <- app_nil_l in H at 8.
      destruct (@next_rules_right R x y a [] B HR SB H) as [A' [B' [b [SB' [L1 [L2 [L3 L4]]]]]]].
      apply rewtTrans with (y:= b). assumption. apply (IH A').
      + rewrite L3. rewrite app_length. cbn. omega.
      + intros c EC. apply SB. rewrite L3. apply in_app_iff. right. apply in_app_iff. now right.
      + left. rewrite L3 in H. rewrite !map_app, !concat_app in H. rewrite L1, L2 in H.
        cbn in H. apply app_inv_head in H. now inv H.
  Qed.

  Theorem reduction_pcp_srs_no_epsilon R x y:
    (forall p, p el R -> fst p <> [] /\ snd p <> [])
      -> PCP (red' R x y) -> rewt R x y.
  Proof.
    intros HR. unfold PCP, pcp_solution. intros [A [HN [Hsub Hsol]]].
    destruct A. contradiction. destruct p as (u,v). assert (H' := Hsol).
    eapply pcp_first_rule in H'. Focus 2. exact HR. Focus 2.
    apply Hsub. now left. inv H'. unfold solution in Hsol. cbn in *.
    inv Hsol. apply (@pcp_rewriting R x y x A HR). intros e HE. auto.
    left. now rewrite <- app_assoc in H0.
  Qed.

  Definition reduction_RSR_PCP (P: {R : srs sig | forall r : list sig * list sig,
                                       r el R -> fst r <> [] /\ snd r <> []} *
                 list sig * list sig): srs psig :=
    match P with
    |((exist _ R H),x,y) => red' R x y
    end.

End srs_pcp.

Theorem reduction_restricted_sr_pcp : red RSR PCPD.
Proof. unfold red. exists (fun S => existT (fun X => pcp X) (psig (projT1 S)) (reduction_RSR_PCP (projT2 S))).
       intros [sig [[[R HR] x] y]]. unfold RSR, PCPD. cbn. split.
       apply reduction_string_rewriting_pcp. now apply reduction_pcp_srs_no_epsilon.
Qed.