proposition: Lemma BSM_computable_to_MM_computable {k} (R : Vector.t nat k -> nat -> Prop) : BSM_computable R -> MM_computable R.
proof: Proof. intros (i & n & P & HP1 & HP2) % BSM_computable_iff. eapply MM_computable_iff. unshelve (epose proof (@bsm_mm_compiler_strong (1 + k + i) n P (pos_right _ Fin.F1) (pos_right _ (Fin.FS Fin.F1)) (pos_right _ (pos2)) (pos_left _) (1 + length (PREPALL k i 1)) _ _ _ _ ) as HQ0; edestruct HQ0 as [Q HQ]). - eapply tmp0_tmp1. - intros p. intros H. eapply pos_right_left. now rewrite H. - intros. intros H. eapply pos_right_left. now rewrite H. - now intros ? ? ? % pos_left_inj. - exact cases. - intros ? % pos_right_inj; congruence. - intros ? % pos_right_inj % pos_nxt_inj. congruence. - intros p. intros H. eapply pos_right_left. now rewrite H. - exists (i + 3). assert (E : 1 + k + i + 3 = (1 + k) + (i + 3)) by lia. pose (q' := PREPALL k i 1 ++ Q ++ mm_transfert pos0 (pos_right (1 + k + i) pos2) (pos_right (1 + k + i) pos0) (1 + length (PREPALL k i 1) + length Q) ++ POSTP k i (4 + length (PREPALL k i 1) + length Q)). assert (Eq1 : forall v, cast (append (append (0 ## v) (const 0 i)) (const 0 3)) E = append (0 ## v) (const 0 (i + 3))). { intros v. clear. cbn. f_equal. match goal with [ |- context [@f_equal ?A ?B ?f ?x ?y ?e]] => generalize (@f_equal A B f x y e) end. clear. induction v; cbn; intros E. - induction i in E |- *; cbn. + reflexivity. + now rewrite IHi. - f_equal. now rewrite IHv. } exists (MM_cast q' E). fold plus. split. + intros v m. intros ? % HP1. setoid_rewrite eval_iff. destruct H as (c & v' & H % BSM_sss.eval_iff). fold plus in *. eapply HQ in H. eexists. eexists ?[v']. rewrite <- Eq1. unshelve eassert (Eq2 : forall v' : Vector.t nat (k + (i + 3)), m ## v' = cast (m ## _) E). { fold plus. refine (Vector.cast v' _). abstract lia. } { clear. intros v. cbn. f_equal. match goal with [ |- context [@f_equal ?A ?B ?f ?x ?y ?e]] => generalize (@f_equal A B f x y e) end. fold plus. intros E2. generalize (BSM_computable_to_MM_computable_subproof k i E). clear. intros E1. cbn in *. revert v E1 E2. generalize (k + i + 2). generalize (k + (i + 2)). clear. intros. destruct E1. now rewrite !cast_eq_refl. } rewrite Eq2. instantiate (v' := (cast _ _)). rewrite <- @MM_cast_spec. subst q'. split. 1: { eapply subcode_sss_compute_trans. 2: eapply PREPALL_spec. 1: auto. match goal with [H : sss_output _ _ ?st1 _ |- sss_compute _ _ ?st2 _ ] => enough (st1 = st2) end. 1: rewrite H0 in H. 1: eapply subcode_sss_compute_trans. 2: eapply H. 1: auto. 2:{ f_equal. 1: rewrite PREPALL_length. 1: lia. clear. eapply vec_pos_ext. intros p. unfold vec_enc. rewrite vec_pos_set. destruct (cases p) as [ [[-> | ->] | ->] | [q ->]]. - cbn. rewrite <- !vec_app_spec. now rewrite vec_pos_app_right. - cbn. rewrite <- !vec_app_spec. now rewrite vec_pos_app_right. - cbn. rewrite <- !vec_app_spec. now rewrite vec_pos_app_right. - rewrite <- !vec_app_spec. rewrite vec_pos_app_left. revert q. eapply pos_left_right_rect. + intros p. rewrite !vec_pos_app_left. rewrite <- !vec_map_spec. eapply (Fin.caseS' p). * cbn. reflexivity. * cbn. intros. rewrite !vec_pos_map. reflexivity. + intros p. rewrite !vec_pos_app_right. now rewrite !vec_pos_const. } eapply subcode_sss_compute_trans with (P := (1 + length (PREPALL k i 1) + length Q, mm_transfert pos0 (pos_right (1 + k + i) pos2) (pos_right (1 + k + i) pos0) (1 + length (PREPALL k i 1) + length Q))). { eexists (PREPALL k i 1 ++ Q). eexists (POSTP _ _ _). split. 1: now rewrite <- app_assoc. rewrite !app_length, PREPALL_length. lia. } 1: eapply sss_progress_compute. 1: eapply mm_transfert_progress. 1-5: clear. { cbn. congruence. } { cbn. congruence. } { cbn. intros ? % pos_nxt_inj % pos_right_inj. congruence. } { unfold vec_enc. rewrite vec_pos_set. destruct cases as [ [ [| ] | ] | [q Hq]]; rew vec. exfalso. eapply pos_right_left. now rewrite Hq. } { unfold vec_enc. rewrite vec_pos_set. destruct cases as [ [ [| ] | ] | [q Hq]]; rew vec. exfalso. eapply pos_right_left. now rewrite Hq. } { reflexivity. } eapply subcode_sss_compute_trans with (P := (4 + length (PREPALL k i 1) + length Q, POSTP k i (4 + length (PREPALL k i 1) + length Q))). { eexists _. eexists List.nil. split. 1: rewrite app_nil_r. 1: now rewrite !app_assoc. rewrite !app_length, PREPALL_length. cbn. lia. } 1: eapply POSTP_spec. { unfold vec_enc. rewrite vec_pos_set. destruct cases as [ [ | ] | [q Hq]]; rew vec. } { unfold vec_enc. rewrite !vec_pos_set. destruct cases as [ [ [| ] | ] | [q Hq]]; rew vec. all: try now (cbn in e; congruence). revert Hq. eapply (Fin.caseS' q). all: try now (cbn; congruence). intros _. rewrite vec_change_neq. 2: intros ? % pos_right_inj; congruence. rewrite vec_change_neq. 2: cbn; congruence. rewrite vec_pos_set. destruct cases as [ [ [| ] | ] | [q' Hq']]; rew vec. exfalso. eapply pos_right_left. now rewrite Hq'. } { unfold vec_enc. rewrite !vec_pos_set. destruct cases as [ [ [| ] | ] | [q Hq]]; rew vec. { rewrite vec_pos_set. destruct cases as [ [ [| ] | ] | [q' Hq']]; rew vec. exfalso. eapply pos_right_left. now rewrite Hq'. } { rewrite vec_pos_set. destruct cases as [ [ [| ] | ] | [q' Hq']]; rew vec. exfalso. eapply pos_right_left. now rewrite Hq'. } { rewrite vec_change_neq. 2: intros ? % pos_right_inj % pos_nxt_inj; congruence. rewrite vec_change_neq. 2: cbn; congruence. rewrite vec_pos_set. destruct cases as [ [ [| ] | ] | [q' Hq']]; rew vec. exfalso. eapply pos_right_left. now rewrite Hq'. } } 2:{ fold plus. mm sss stop. cbn. f_equal. rewrite cast_cast. reflexivity. } { unfold vec_enc. rewrite !vec_pos_set. destruct cases as [ [ [| ] | ] | [q' Hq']]; rew vec. all: try now (cbn in e; congruence). revert Hq'. eapply (Fin.caseS' q'). all: try now (cbn; congruence). } Unshelve. lia. } cbn. autorewrite with list. cbn. setoid_rewrite PREPALL_length. right. lia. + intros v H2. eapply HP2. eapply HQ. eapply MM_cast_terminates with (E := E). eapply subcode_sss_terminates. 2:{ eapply subcode_sss_terminates_inv. 1: eapply mm_sss_fun. 1: eapply H2. 2:{ rewrite <- Eq1. rewrite <- MM_cast_spec. rewrite PREPALL_length. cbn [plus]. match goal with [ |- sss_output _ _ _ (_, ?st) ] => evar (t : Vector.t nat (1 + k + i + 3)); enough (Eq : st = t) end; subst t. 1: rewrite Eq. 1: eapply PREPALL_spec. clear. eapply vec_pos_ext. intros p. unfold vec_enc. rewrite vec_pos_set. destruct (cases p) as [ [[-> | ->] | ->] | [q ->]]. - cbn. rewrite <- !vec_app_spec. now rewrite vec_pos_app_right. - cbn. rewrite <- !vec_app_spec. now rewrite vec_pos_app_right. - cbn. rewrite <- !vec_app_spec. now rewrite vec_pos_app_right. - rewrite <- !vec_app_spec. rewrite vec_pos_app_left. revert q. eapply pos_left_right_rect. + intros p. repeat setoid_rewrite vec_pos_app_left. repeat setoid_rewrite <- vec_map_spec. eapply (Fin.caseS' p). * cbn. reflexivity. * intros. repeat setoid_rewrite vec_pos_map. f_equal. rewrite (@vec_pos_app_left (list bool) (1 + k) i). cbn. rewrite vec_pos_map. reflexivity. + intros p. rewrite !vec_pos_app_right. rewrite (@vec_pos_app_right (list bool) (S k) i). now rewrite !vec_pos_const. } clear. subst q'. generalize (PREPALL k i 1). intros l. generalize (mm_transfert pos0 (pos_right (1 + k + i) pos2) (pos_right (1 + k + i) pos0) (1 + length l + length Q) ++ POSTP k i (4 + length l + length Q)). fold plus. revert l. destruct E. cbn. intros. exists nil. cbn. eauto. } clear. subst q'. generalize (PREPALL k i 1). intros l. generalize (mm_transfert pos0 (pos_right (1 + k + i) pos2) (pos_right (1 + k + i) pos0) (1 + length l + length Q) ++ POSTP k i (4 + length l + length Q)). fold plus. revert l. destruct E. cbn. intros. exists l. cbn. eauto. Qed.
imports: Undecidability.MinskyMachines(MM_computable MM_sss mm_utils) Undecidability.StackMachines(BSM_computable) Undecidability.Shared.Libs.DLW(vec pos sss subcode) Lia Vector Nat Arith List Undecidability.MinskyMachines.MM(mm_defs mm_utils mm_comp_strong)