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)++[#].
Proof.
induction A.
- reflexivity.
- cbn. unfold hash_right in IHA. now rewrite IHA.
Qed.
Lemma hash_hash_right A B:
hash_right (A++B) = hash_right A ++ hash_right B.
Proof.
unfold hash_right. now rewrite map_app, concat_app.
Qed.
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.
Proof.
induction R. auto. intros r. cbn. intros [<-|HR]. split; inversion 1. now apply IHR.
Qed.
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)))
end.
Fact hash_right_inj : Injective hash_right.
Proof.
intros A. induction A; intros B.
- destruct B. auto. inversion 1.
- destruct B. inversion 1. inversion 1. subst.
specialize (IHA B H2). now subst.
Qed.
Lemma shift_hash_right l y o :
hash_right l ++ y = hash_right o -> exists a, l++a = o /\ y = hash_right a.
Proof.
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.
Qed.
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.
Proof.
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.
Qed.
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).
Proof.
split.
- 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.
Qed.
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.
Defined.
Definition FinType_sig (gam:finType) : finTypeC (EqType (sig gam)).
Proof.
exists ((hash gam)::(List.map (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).
Qed.
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.
Qed.