Require Import Prelim PCP String_rewriting Reductions.
Section sr_mpcp_reduction.
Variable sig: finType.
Inductive psig: Type := dollar | hash | sigma (s: sig).
Notation "#" := hash.
Notation "$" := dollar.
Definition sig_psig := map (fun (s: sig) =>(sigma s)).
Lemma inj_sigma : Injective (fun s : sig => sigma s).
Proof.
intros a b. now inversion 1.
Qed.
Definition fcard (x: list sig) := ([$],$::(sig_psig x)++[#]).
Definition lcard (y: list sig) : rule psig := ((sig_psig y)++[#;$],[$]).
Definition pcp_dominos : srs sig -> srs psig :=
fun S => map (fun r => (sig_psig (fst r), sig_psig (snd r))) S ++ [([#],[#])]
++ (map (fun s => ([sigma s],[sigma s])) (elem sig)).
Definition reduction_f (T: (srs sig) * list sig * list sig) : (rule psig * srs psig) :=
match T with
|((R,x),y) => ((fcard x),(lcard y)::(pcp_dominos R))
end.
Definition lcard (y: list sig) : rule psig := ((sig_psig y)++[#;$],[$]).
Definition pcp_dominos : srs sig -> srs psig :=
fun S => map (fun r => (sig_psig (fst r), sig_psig (snd r))) S ++ [([#],[#])]
++ (map (fun s => ([sigma s],[sigma s])) (elem sig)).
Definition reduction_f (T: (srs sig) * list sig * list sig) : (rule psig * srs psig) :=
match T with
|((R,x),y) => ((fcard x),(lcard y)::(pcp_dominos R))
end.
Definition copy_string (x: list sig) := map (fun s => ([sigma s],[sigma s])) x.
Lemma copy_string_el x a S:
a el copy_string x -> a el pcp_dominos S.
Proof.
destruct x; cbn. auto. destruct a. intros [HA|HA].
inv HA. apply in_app_iff. right. apply in_app_iff. right.
apply in_map_iff. exists e. now split. apply in_map_iff in HA as [s [H1 H2]].
inv H1. apply in_app_iff. right. apply in_app_iff. right.
apply in_map_iff. exists s. now split.
Qed.
Lemma concat_map_fst_copy x :
concat (map fst (copy_string x)) = sig_psig x.
Proof. induction x; simpl. auto. now rewrite IHx. Qed.
Lemma concat_map_snd_copy x:
concat (map snd (copy_string x)) = sig_psig x.
Proof. induction x; simpl. auto. now rewrite IHx. Qed.
Lemma split_sig_psig x y:
sig_psig (x++y) = sig_psig x ++ sig_psig y.
Proof. unfold sig_psig. now rewrite map_app. Qed.
Lemma copy_string_el x a S:
a el copy_string x -> a el pcp_dominos S.
Proof.
destruct x; cbn. auto. destruct a. intros [HA|HA].
inv HA. apply in_app_iff. right. apply in_app_iff. right.
apply in_map_iff. exists e. now split. apply in_map_iff in HA as [s [H1 H2]].
inv H1. apply in_app_iff. right. apply in_app_iff. right.
apply in_map_iff. exists s. now split.
Qed.
Lemma concat_map_fst_copy x :
concat (map fst (copy_string x)) = sig_psig x.
Proof. induction x; simpl. auto. now rewrite IHx. Qed.
Lemma concat_map_snd_copy x:
concat (map snd (copy_string x)) = sig_psig x.
Proof. induction x; simpl. auto. now rewrite IHx. Qed.
Lemma split_sig_psig x y:
sig_psig (x++y) = sig_psig x ++ sig_psig y.
Proof. unfold sig_psig. now rewrite map_app. Qed.
Lemma rewrite_exists_pcp_list R x y:
rewt R x y -> (exists A, (concat (map fst A))++(sig_psig y)++[#] =
(sig_psig x)++[#]++(concat (map snd A)) /\ A <<= (pcp_dominos R)).
Proof.
induction 1 as [|x z y].
- exists []. split; auto.
- destruct IHrewt as [A [HA HB]]. inv H.
exists ((copy_string x0)++(sig_psig u,sig_psig v)::(copy_string y0)++[([#],[#])]++A). split.
+ cbn. rewrite !map_app, !concat_app. cbn. rewrite !map_app, !concat_app. cbn.
rewrite !concat_map_fst_copy, !concat_map_snd_copy, !split_sig_psig.
rewrite <- !app_assoc. rewrite <- app_comm_cons. rewrite HA.
now rewrite !split_sig_psig, <- !app_assoc.
+ intros a [HC|[<-|[HC|[HC%in_sing|HC]%in_app_iff]%in_app_iff]]%in_app_iff.
* apply (@copy_string_el x0 a R HC).
* apply in_app_iff. left. apply in_map_iff. exists (u,v). split. auto. assumption.
* apply (@copy_string_el y0 a R HC).
* apply in_app_iff. right. apply in_app_iff. left. now left.
* now apply HB.
Qed.
Lemma sr_then_pcp_solution (S: srs sig) (x y : list sig):
rewt S x y -> MPCP (reduction_f (S,x,y)).
Proof.
cbn. intros H. apply rewrite_exists_pcp_list in H as [A [HA HB]].
exists (A++[lcard y]). repeat split. inversion 1. intros e [<-|[HH|HH%in_sing]%in_app_iff].
- now left.
- right. right. now apply HB.
- right. now left.
- unfold solution. cbn. unfold lcard. rewrite !map_app, !concat_app. cbn.
rewrite !app_nil_r. change [#;$] with ([#]++[$]). setoid_rewrite app_assoc at 2.
setoid_rewrite app_assoc at 1. rewrite HA. now rewrite !app_assoc.
Qed.
rewt R x y -> (exists A, (concat (map fst A))++(sig_psig y)++[#] =
(sig_psig x)++[#]++(concat (map snd A)) /\ A <<= (pcp_dominos R)).
Proof.
induction 1 as [|x z y].
- exists []. split; auto.
- destruct IHrewt as [A [HA HB]]. inv H.
exists ((copy_string x0)++(sig_psig u,sig_psig v)::(copy_string y0)++[([#],[#])]++A). split.
+ cbn. rewrite !map_app, !concat_app. cbn. rewrite !map_app, !concat_app. cbn.
rewrite !concat_map_fst_copy, !concat_map_snd_copy, !split_sig_psig.
rewrite <- !app_assoc. rewrite <- app_comm_cons. rewrite HA.
now rewrite !split_sig_psig, <- !app_assoc.
+ intros a [HC|[<-|[HC|[HC%in_sing|HC]%in_app_iff]%in_app_iff]]%in_app_iff.
* apply (@copy_string_el x0 a R HC).
* apply in_app_iff. left. apply in_map_iff. exists (u,v). split. auto. assumption.
* apply (@copy_string_el y0 a R HC).
* apply in_app_iff. right. apply in_app_iff. left. now left.
* now apply HB.
Qed.
Lemma sr_then_pcp_solution (S: srs sig) (x y : list sig):
rewt S x y -> MPCP (reduction_f (S,x,y)).
Proof.
cbn. intros H. apply rewrite_exists_pcp_list in H as [A [HA HB]].
exists (A++[lcard y]). repeat split. inversion 1. intros e [<-|[HH|HH%in_sing]%in_app_iff].
- now left.
- right. right. now apply HB.
- right. now left.
- unfold solution. cbn. unfold lcard. rewrite !map_app, !concat_app. cbn.
rewrite !app_nil_r. change [#;$] with ([#]++[$]). setoid_rewrite app_assoc at 2.
setoid_rewrite app_assoc at 1. rewrite HA. now rewrite !app_assoc.
Qed.
Lemma sigma_hash_equal a b A B:
sig_psig a ++ #::A = sig_psig b ++ #::B -> a = b.
Proof.
revert b. induction a; intros b H; destruct b; inv H. auto.
now rewrite (IHa b H2).
Qed.
Lemma split_sigma a u (A B: list psig):
sig_psig u ++ A = sig_psig a ++ #::B
-> exists a', sig_psig a = sig_psig u ++ sig_psig a'.
Proof.
revert a. induction u; intros b; cbn; intros SL.
- exists b. reflexivity.
- destruct b; inv SL. destruct (IHu b H1). exists x. cbn. f_equal. assumption.
Qed.
Lemma rewrite_solution (R: srs sig) (A: srs psig) (a x y b: list sig):
A <<= (fcard x) :: snd (reduction_f (R,x,y))
-> (concat (map fst A) = sig_psig a++[#]++(sig_psig b)++(concat (map snd A)))
-> (rewt R a y /\ (b = [])) \/ (exists A' B d, (concat (map fst B) = sig_psig a)
/\ (concat (map snd B) = sig_psig d) /\
A = B++[([#],[#])]++A' /\ rewt R a d).
Proof.
revert a x y b. pattern A.
apply (@size_induction (srs psig) (@length (list psig * list psig))).
intros D IH. intros a x y b sub H1. destruct D. now apply app_cons_not_nil in H1.
destruct a; cbn in *.
+ assert (|D|<S(|D|)) as DH by omega.
destruct (sub r (or_introl eq_refl)) as [<-|[<-|[H|[H|H]%in_app_iff]%in_app_iff]].
* inv H1.
* cbn in H1. destruct y, b; cbn in *. left. split. constructor. auto. inv H1. inv H1. inv H1.
* apply in_map_iff in H as [?[]]. subst. destruct x0 as (u,v). destruct u; cbn in *.
-- specialize (IH D DH [] x y (b++v)). destruct IH. intros e HE. apply sub.
now right. rewrite split_sig_psig. now rewrite <- app_assoc.
left. destruct H. split. assumption. destruct b. auto. inv H2.
destruct H as [? [? [? [? [? []]]]]]. right.
exists x0, (([],sig_psig v)::x1), (v++x2). repeat split. cbn. assumption.
cbn. rewrite H2. now rewrite split_sig_psig. cbn. now rewrite H3.
apply rewtTrans with (y:= x2). assumption. setoid_rewrite <- app_nil_l at 2.
apply rewtRule with (y:=(v++x2)). now apply rewR with (x:=[]) (u:=[]) (v:=v).
constructor.
-- inv H1.
* apply in_sing in H. subst. inv H1. right. exists D, [], []. repeat split. constructor.
* apply in_map_iff in H as [?[]]. subst. inv H1.
+ assert (|D|<S(|D|)) as DH by omega.
destruct (sub r (or_introl eq_refl)) as [<-|[<-|[H|[H|H]%in_app_iff]%in_app_iff]].
* inv H1.
* cbn in *. rewrite <- app_assoc in H1. cbn in H1.
rewrite app_comm_cons in H1. change (sigma e::sig_psig a) with (sig_psig (e::a)) in H1.
apply sigma_hash_equal in H1 as H2. subst. inv H1. apply app_inv_head in H0.
inv H0. destruct b. left. split. constructor. auto. inv H1.
* apply in_map_iff in H as [?[]]. subst. destruct x0 as (u,v). cbn in *.
rewrite app_comm_cons in H1. change (sigma e:: sig_psig a) with (sig_psig (e::a)) in H1.
destruct (split_sigma H1) as [a' HA']. rewrite HA' in H1. rewrite <- app_assoc in H1.
apply app_inv_head in H1.
assert (sig_psig (e::a) = sig_psig (u++a')) as H by (now rewrite split_sig_psig).
unfold sig_psig in H. apply (map_inj _ _ inj_sigma) in H.
destruct (IH D DH a' x y (b++v)) as [[]|]. intros d EH. apply sub. now right.
rewrite split_sig_psig, <- app_assoc. assumption.
-- left. rewrite H. apply app_eq_nil in H3 as []. subst. split.
rewrite <- app_nil_l. apply rewtTrans with (y:= []++a').
apply rewtRule with (y:=([]++a')). apply rewR with (x:=[]) (u:=u) (v:=[]).
assumption. constructor. now rewrite !app_nil_l. reflexivity.
-- destruct H2 as [?[?[?[?[?[]]]]]]. right.
exists x0, ((sig_psig u, sig_psig v)::x1),(v++x2). cbn. repeat split.
++ rewrite H2. now rewrite <- HA'.
++ rewrite H3. now rewrite split_sig_psig.
++ now rewrite H4.
++ rewrite H. apply rewtTrans with (y:=v++a'). apply rewtRule with (y:=(v++a')).
now apply rewR with (x:=[]) (u:=u). constructor. now apply rewrite_app.
* apply in_sing in H. subst. inv H1.
* apply in_map_iff in H as [?[]]. subst. inv H1.
destruct (IH D DH a x y (b++[e])). intros d EH. apply sub. now right.
rewrite split_sig_psig. now rewrite <- app_assoc. destruct H. symmetry in H1.
now apply app_cons_not_nil in H1. destruct H as [?[?[?[?[?[]]]]]].
right. exists x0, (([sigma e],[sigma e])::x1), (e::x2). cbn. repeat split.
now rewrite H. now rewrite H1. now rewrite H2. now apply rewrite_app with (z:=[e]).
Qed.
Lemma mpcp_rewriting R x y a A:
A <<= (fcard x) :: snd (reduction_f (R,x,y))
-> (concat (map fst A) = sig_psig a++[#]++(concat (map snd A)))
-> rewt R a y.
Proof.
revert a. pattern A.
apply (@size_induction (srs psig) (@length (list psig* list psig))).
intros B IH a sub H. destruct (@rewrite_solution R B a x y [] sub) as [[]|].
cbn. assumption.
- assumption.
- destruct H0 as [?[?[?[?[?[]]]]]]. rewrite H2 in H. cbn in *.
rewrite !map_app, !concat_app in H. cbn in *.
rewrite H0 in H. rewrite H1 in H. apply app_inv_head in H. inv H.
apply rewtTrans with (y:=x2). assumption. apply (IH x0).
destruct x1. cbn. omega. cbn. rewrite app_length. cbn. omega.
intros e HE. apply sub. apply in_app_iff. right. now right. assumption.
Qed.
Lemma mpcp_solution_then_sr (S: srs sig) (x y: list sig):
MPCP (reduction_f (S,x,y)) -> rewt S x y.
Proof.
cbn. unfold MPCP. intros [A [_ [H2 H3]]]. unfold solution in H3.
cbn in *. inv H3. rewrite <- app_assoc in H0. apply (@mpcp_rewriting S x y x A).
intros e HE. apply H2. now right. assumption.
Qed.
End sr_mpcp_reduction.
Theorem reduction_sr_mpcp : red SR MPCPD.
Proof.
unfold red. exists (fun S => existT (fun X => mpcp X) (psig (projT1 S)) (reduction_f (projT2 S))).
intros [sig [[R x] y]]. unfold SR, MPCPD. cbn. split.
apply sr_then_pcp_solution. apply mpcp_solution_then_sr.
Qed.
sig_psig a ++ #::A = sig_psig b ++ #::B -> a = b.
Proof.
revert b. induction a; intros b H; destruct b; inv H. auto.
now rewrite (IHa b H2).
Qed.
Lemma split_sigma a u (A B: list psig):
sig_psig u ++ A = sig_psig a ++ #::B
-> exists a', sig_psig a = sig_psig u ++ sig_psig a'.
Proof.
revert a. induction u; intros b; cbn; intros SL.
- exists b. reflexivity.
- destruct b; inv SL. destruct (IHu b H1). exists x. cbn. f_equal. assumption.
Qed.
Lemma rewrite_solution (R: srs sig) (A: srs psig) (a x y b: list sig):
A <<= (fcard x) :: snd (reduction_f (R,x,y))
-> (concat (map fst A) = sig_psig a++[#]++(sig_psig b)++(concat (map snd A)))
-> (rewt R a y /\ (b = [])) \/ (exists A' B d, (concat (map fst B) = sig_psig a)
/\ (concat (map snd B) = sig_psig d) /\
A = B++[([#],[#])]++A' /\ rewt R a d).
Proof.
revert a x y b. pattern A.
apply (@size_induction (srs psig) (@length (list psig * list psig))).
intros D IH. intros a x y b sub H1. destruct D. now apply app_cons_not_nil in H1.
destruct a; cbn in *.
+ assert (|D|<S(|D|)) as DH by omega.
destruct (sub r (or_introl eq_refl)) as [<-|[<-|[H|[H|H]%in_app_iff]%in_app_iff]].
* inv H1.
* cbn in H1. destruct y, b; cbn in *. left. split. constructor. auto. inv H1. inv H1. inv H1.
* apply in_map_iff in H as [?[]]. subst. destruct x0 as (u,v). destruct u; cbn in *.
-- specialize (IH D DH [] x y (b++v)). destruct IH. intros e HE. apply sub.
now right. rewrite split_sig_psig. now rewrite <- app_assoc.
left. destruct H. split. assumption. destruct b. auto. inv H2.
destruct H as [? [? [? [? [? []]]]]]. right.
exists x0, (([],sig_psig v)::x1), (v++x2). repeat split. cbn. assumption.
cbn. rewrite H2. now rewrite split_sig_psig. cbn. now rewrite H3.
apply rewtTrans with (y:= x2). assumption. setoid_rewrite <- app_nil_l at 2.
apply rewtRule with (y:=(v++x2)). now apply rewR with (x:=[]) (u:=[]) (v:=v).
constructor.
-- inv H1.
* apply in_sing in H. subst. inv H1. right. exists D, [], []. repeat split. constructor.
* apply in_map_iff in H as [?[]]. subst. inv H1.
+ assert (|D|<S(|D|)) as DH by omega.
destruct (sub r (or_introl eq_refl)) as [<-|[<-|[H|[H|H]%in_app_iff]%in_app_iff]].
* inv H1.
* cbn in *. rewrite <- app_assoc in H1. cbn in H1.
rewrite app_comm_cons in H1. change (sigma e::sig_psig a) with (sig_psig (e::a)) in H1.
apply sigma_hash_equal in H1 as H2. subst. inv H1. apply app_inv_head in H0.
inv H0. destruct b. left. split. constructor. auto. inv H1.
* apply in_map_iff in H as [?[]]. subst. destruct x0 as (u,v). cbn in *.
rewrite app_comm_cons in H1. change (sigma e:: sig_psig a) with (sig_psig (e::a)) in H1.
destruct (split_sigma H1) as [a' HA']. rewrite HA' in H1. rewrite <- app_assoc in H1.
apply app_inv_head in H1.
assert (sig_psig (e::a) = sig_psig (u++a')) as H by (now rewrite split_sig_psig).
unfold sig_psig in H. apply (map_inj _ _ inj_sigma) in H.
destruct (IH D DH a' x y (b++v)) as [[]|]. intros d EH. apply sub. now right.
rewrite split_sig_psig, <- app_assoc. assumption.
-- left. rewrite H. apply app_eq_nil in H3 as []. subst. split.
rewrite <- app_nil_l. apply rewtTrans with (y:= []++a').
apply rewtRule with (y:=([]++a')). apply rewR with (x:=[]) (u:=u) (v:=[]).
assumption. constructor. now rewrite !app_nil_l. reflexivity.
-- destruct H2 as [?[?[?[?[?[]]]]]]. right.
exists x0, ((sig_psig u, sig_psig v)::x1),(v++x2). cbn. repeat split.
++ rewrite H2. now rewrite <- HA'.
++ rewrite H3. now rewrite split_sig_psig.
++ now rewrite H4.
++ rewrite H. apply rewtTrans with (y:=v++a'). apply rewtRule with (y:=(v++a')).
now apply rewR with (x:=[]) (u:=u). constructor. now apply rewrite_app.
* apply in_sing in H. subst. inv H1.
* apply in_map_iff in H as [?[]]. subst. inv H1.
destruct (IH D DH a x y (b++[e])). intros d EH. apply sub. now right.
rewrite split_sig_psig. now rewrite <- app_assoc. destruct H. symmetry in H1.
now apply app_cons_not_nil in H1. destruct H as [?[?[?[?[?[]]]]]].
right. exists x0, (([sigma e],[sigma e])::x1), (e::x2). cbn. repeat split.
now rewrite H. now rewrite H1. now rewrite H2. now apply rewrite_app with (z:=[e]).
Qed.
Lemma mpcp_rewriting R x y a A:
A <<= (fcard x) :: snd (reduction_f (R,x,y))
-> (concat (map fst A) = sig_psig a++[#]++(concat (map snd A)))
-> rewt R a y.
Proof.
revert a. pattern A.
apply (@size_induction (srs psig) (@length (list psig* list psig))).
intros B IH a sub H. destruct (@rewrite_solution R B a x y [] sub) as [[]|].
cbn. assumption.
- assumption.
- destruct H0 as [?[?[?[?[?[]]]]]]. rewrite H2 in H. cbn in *.
rewrite !map_app, !concat_app in H. cbn in *.
rewrite H0 in H. rewrite H1 in H. apply app_inv_head in H. inv H.
apply rewtTrans with (y:=x2). assumption. apply (IH x0).
destruct x1. cbn. omega. cbn. rewrite app_length. cbn. omega.
intros e HE. apply sub. apply in_app_iff. right. now right. assumption.
Qed.
Lemma mpcp_solution_then_sr (S: srs sig) (x y: list sig):
MPCP (reduction_f (S,x,y)) -> rewt S x y.
Proof.
cbn. unfold MPCP. intros [A [_ [H2 H3]]]. unfold solution in H3.
cbn in *. inv H3. rewrite <- app_assoc in H0. apply (@mpcp_rewriting S x y x A).
intros e HE. apply H2. now right. assumption.
Qed.
End sr_mpcp_reduction.
Theorem reduction_sr_mpcp : red SR MPCPD.
Proof.
unfold red. exists (fun S => existT (fun X => mpcp X) (psig (projT1 S)) (reduction_f (projT2 S))).
intros [sig [[R x] y]]. unfold SR, MPCPD. cbn. split.
apply sr_then_pcp_solution. apply mpcp_solution_then_sr.
Qed.