Reducing String Rewriting to Restricted String Rewriting

Require Import Prelim String_rewriting Reductions.
Section epsilon_srs.

  Variable esig: Type.
  Inductive sig : Type := hash | sigma (s: esig).
  Definition esig_sig := map (fun (s: esig) => sigma s).
  Notation "#" := hash.

  Definition esig_list_pair_sig :=
    map (fun (p: list esig * list esig) => (esig_sig (fst p), esig_sig (snd p))).

  Definition hash_right A :=
    concat (map (fun (e: esig) => [(sigma e);#]) A).

  Definition hash_left A :=
    concat (map (fun (e: esig) => [#;(sigma e)]) A).

  Lemma move_hash A:
    #:: hash_right A = (hash_left A)++[#].
    induction A.
    - reflexivity.
    - cbn. unfold hash_right in IHA. now rewrite IHA.

  Lemma hash_hash_right A B:
    hash_right (A++B) = hash_right A ++ hash_right B.
    unfold hash_right. now rewrite map_app, concat_app.

  Definition replace_nil : (srs esig) -> list (list sig * list sig) :=
    map (fun (p: list esig * list esig) => (#::(hash_right (fst p)), #::(hash_right (snd p)))).

  Lemma no_nil_in_R (R: srs esig): forall r, r el (replace_nil R) -> (fst r) <> nil /\ (snd r) <> nil.
    induction R. auto. intros r. cbn. intros [<-|HR]. split; inversion 1. now apply IHR.

  Definition srs_no_epsilon_reduction (P: (srs esig) * list esig * list esig):
    ({R: srs sig |forall r,r el R -> (fst r) <> nil /\ (snd r) <> nil} * list sig * list sig) :=
    match P with
    |((R,x),y) => ((exist _ (replace_nil R) (@no_nil_in_R R), #::(hash_right x), #::(hash_right y)))

  Fact hash_right_inj : Injective hash_right.
    intros A. induction A; intros B.
    - destruct B. auto. inversion 1.
    - destruct B. inversion 1. inversion 1. subst.
      specialize (IHA B H2). now subst.

  Lemma shift_hash_right l y o :
    hash_right l ++ y = hash_right o -> exists a, l++a = o /\ y = hash_right a.
    revert y o. induction l; intros y o H.
    - cbn in *. exists o. now split.
    - cbn in *. destruct o. inversion H. cbn in *. inv H.
      destruct (IHl y o H2). exists x. destruct H. split. now rewrite H. assumption.

  Lemma remove_hash x l y o :
    x ++#::hash_right l ++ y = #::hash_right o
    -> exists a b, o = a++l++b /\ x++[#] = #::hash_right a /\ y = hash_right b.
    revert x l y. induction o; intros x l y H; cbn in *.
    - destruct x. rewrite app_nil_l in H. inv H. destruct l. rewrite app_nil_l in H1.
      subst. exists [],[]. repeat split. inversion H1. inversion H. symmetry in H2.
      apply app_cons_not_nil in H2. contradiction.
    - destruct x.
      + rewrite app_nil_l in H. inv H. assert ((hash_right l ++ y) = hash_right (a::o)).
        cbn. assumption. apply shift_hash_right in H as [b [HA HB]]. subst.
        exists [], b. repeat split. auto.
      + inv H. destruct x. rewrite app_nil_l in H2. inversion H2. inv H2.
        specialize (IHo x l y H1). destruct IHo as [b [c [H2 [H3 H4]]]]. subst.
        exists (a::b), c. repeat split. cbn. unfold hash_right in H3. now rewrite <- H3.

  Lemma rewrite_SR_iff_rewrite_RSR S x y:
    rewt S x y <-> rewt (replace_nil S) (hash:: hash_right x) (hash:: hash_right y).
    - cbn. induction 1. constructor.
      inv H. apply (rewtRule) with (y:= (# :: hash_right (x0 ++ v ++ y0))).
      + rewrite !hash_hash_right, !app_comm_cons, !move_hash. rewrite <- !app_assoc.
        setoid_rewrite app_assoc at 4. setoid_rewrite app_assoc at 2. apply rewR.
        apply in_map_iff. exists (u,v). now split.
      + assumption.
    - cbn. intros H. remember (#::hash_right x) as a. remember (#::hash_right y) as b.
      revert Heqa Heqb. revert x y. induction H; intros o p HA HB.
      + rewrite HB in HA. inv HA. apply hash_right_inj in H0 as <-. constructor.
      + inv H. unfold replace_nil in H1. apply in_map_iff in H1 as [k [Hk Hm]].
        inv Hk. destruct k. cbn in *. apply remove_hash in H3 as [a [b [H1 [H2 H4]]]].
        subst. apply rewtRule with (y:= a++l0++b).
        * apply rewR. assumption.
        * apply IHrewt. rewrite app_comm_cons.
          change (# :: concat (map (fun e : esig => [sigma e; #]) l0))
            with ([#]++ concat (map (fun e : esig => [sigma e; #]) l0)).
          rewrite app_assoc, app_assoc. rewrite H2.
          rewrite !hash_hash_right. cbn. now rewrite <- !app_assoc. reflexivity.

End epsilon_srs.

Instance eq_dec_sig (gam: finType) : eq_dec (sig gam).
Proof. intros a b. unfold dec. decide equality.
       assert (H: eq_dec gam). intros u v. apply (eqType_dec u v).
       apply H.

Definition FinType_sig (gam:finType) : finTypeC (EqType (sig gam)).
    exists ((hash gam)::( (fun s => sigma s) (elem gam))).
    intros x. destruct x; cbn. induction (elem gam); auto.
    apply inductive_count. intros x y; now inversion 1. apply (@enum_ok gam (class gam) s).

Definition sig_finType (gam:finType) : finType:= (@FinType (EqType (sig gam)) (FinType_sig gam)).

Theorem reduction_sr_restricted_sr : red SR RSR.
Proof. unfold red.
       exists (fun S => existT (fun (F:finType) => (prod (prod {R : srs F | forall r : rule F, r el R -> fst r <> [] /\ snd r <> []} (list F))) (list F)) (sig_finType (projT1 S)) (srs_no_epsilon_reduction (projT2 S))).
       intros [gam [[S x] y]]. unfold SR, RSR. cbn.
       apply rewrite_SR_iff_rewrite_RSR.