Require Import List Arith Lia.
Import ListNotations.
Require Import Undecidability.Synthetic.Undecidability.
From Undecidability.Shared.Libs.DLW
Require Import utils list_bool pos vec subcode sss.
From Undecidability.StackMachines.BSM
Require Import tiles_solvable bsm_defs bsm_utils bsm_pcp.
From Undecidability.PCP
Require Import PCP PCP_facts.
Set Default Proof Using "Type".
Fact tile_concat_itau ln lt : tile_concat ln lt = (itau1 lt (rev ln), itau2 lt (rev ln)).
Proof.
induction ln as [ | i ln IH ]; simpl; auto.
rewrite itau1_app, itau2_app; simpl.
unfold card, string; generalize (nth i lt ([], [])); intros (a,b); rewrite IH.
repeat rewrite <- app_nil_end; auto.
Qed.
Theorem tiles_solvable_iBPCP lt : tiles_solvable lt <-> iPCPb lt.
Proof.
split.
+ intros (ln & H1 & H2 & H3).
rewrite tile_concat_itau in H3.
exists (rev ln).
rewrite <- Forall_forall.
repeat split; auto.
* apply Forall_rev; auto.
* contradict H1; rewrite <- (rev_involutive ln), H1; auto.
+ intros (ln & H1 & H2 & H3).
exists (rev ln).
rewrite tile_concat_itau, rev_involutive.
repeat split; auto.
* contradict H2; rewrite <- (rev_involutive ln), H2; auto.
* apply Forall_rev, Forall_forall; auto.
Qed.
Local Notation "P // s ->> t" := (sss_compute (@bsm_sss _) P s t).
Local Notation "P // s ~~> t" := (sss_output (@bsm_sss _) P s t).
Local Notation "P // s ↓" := (sss_terminates (@bsm_sss _) P s).
Section iPCPb_to_BSM_HALTING.
Let f (lt : list (card bool)) : BSM_PROBLEM.
Proof.
exists 4, 1, (pcp_bsm lt).
exact (vec_set_pos (fun _ => nil)).
Defined.
Goal forall x, length(pcp_bsm x) >= 80.
Proof.
intros; rewrite pcp_bsm_size; lia.
Qed.
Theorem iPCPb_to_BSM_HALTING : iPCPb ⪯ BSM_HALTING.
Proof.
exists f.
intros lt.
rewrite <- tiles_solvable_iBPCP.
unfold BSM_HALTING; split.
* intros H.
apply pcp_bsm_sound with (v := vec_set_pos (fun _ => nil)) in H.
match type of H with _ // _ ->> (?q,?w) => exists (q, w) end.
split; auto.
simpl; lia.
* intros ((q & w) & H).
apply pcp_bsm_complete in H; tauto.
Qed.
End iPCPb_to_BSM_HALTING.