Reducing the Halting Problem to MPCP


Require Import Prelim Single_TM PCP Reductions.

Section Fix_TM.
  Notation "x 'nel' A" := (~ x el A) (at level 70).
  Variable sig : finType.

  Instance eq_dec_sig: eq_dec sig.
  Proof. exact _. Qed.

  Variable T : (sTM sig).
  Definition conf :Type := mconfig sig (states T).
  Global Instance eq_dec_states : eq_dec (states T).
  Proof. exact _. Defined.

  (* Definition of type "psig" on top of "sigC". The constructor "dollar" is only used for the
     first symbol of the starting domino, whereas the hash delimits configurations of an MPCP match*)
  Inductive psig :Type := hash | dollar | state (s: states T) | sym (a: sig) | blank.
  Notation "#" := hash.
  Notation "$" := dollar.

  Global Instance eq_dec_psig : eq_dec psig.
  Proof.
    intros. hnf. decide equality. apply eq_dec_states. apply eq_dec_sig.
  Defined.

  (* niltape and leftof translate with blank after the state *)
  Definition mconfig_pconfig (c: conf): list psig :=
    match (ctape c) with
    | niltape _ => [#;(state(cstate c));(blank)]++[#]
    | leftof s r => [#; (state(cstate c)); (blank)]++(map sym (s::r))++[#]
    | rightof s l => #::map sym(List.rev (s :: l))++[ (state(cstate c))]++[#]
    | midtape l s r => #::map sym(List.rev l) ++ [(state(cstate c))]
                                ++ map sym(s::r)++[#]
    end.

Definition of MPCP dominoes

  (* see Hopcroft p. 407f *)
  Definition domino : Type := list psig * list psig.

  Definition halting_states : list (states T) :=
    List.filter (fun s => halt s) (elem (states T)).

  Definition not_halting_states : list (states T) :=
    List.filter (fun s => negb (halt s)) (elem (states T)).

Type 1 Card - begin match with initial configuration
  (* First card with two hash symbols cf. Sisper p. 242 *)
  Definition type_1_first_card (con: conf): domino := ([$],$::(mconfig_pconfig con)).

Type 2 Cards - copy symbols to each list
  (* Tape symbols for each symbol in 'sig': (X,X) also for blank???? *)
  Definition type_2_copy : pcp psig :=
    List.map (fun (s: sig) => ([(sym s)], [(sym s)])) (elem sig).

  (* Hash symbol (#,#) *)
  Definition type_2_hash : pcp psig := [([#],[#])].


Type 3 Cards - simulate a transition of TM
  (* Type 3 Transitions read: None *)
  Definition left_none_none (q1 q2: states T) : pcp psig :=
    ([#;(state q1); blank], [#;(state q2); blank])
      :: (List.map (fun (a: sig) => ([(sym a); (state q1); hash],
                                  [(state q2); (sym a); hash])) (elem sig)).

  Definition stay_none_none (q1 q2: states T) : list (list psig*list psig) :=
    [([#;(state q1);blank], [#;(state q2);blank]); ([state q1; hash], [state q2; hash])].

  Definition right_none_none (q1 q2: states T): list (list psig*list psig) :=
    [([#;state q1; blank;#], [#;state q2; blank;#]); ([state q1; hash], [state q2; hash])]
      ++ (List.map (fun (z: sig) =>
                      ([hash; (state q1); blank; sym z],
                       [hash; (state q2); sym z])) (elem sig)).

  Definition left_none_some (q1 q2: states T) (a: sig) : pcp psig :=
    ([hash;state q1; blank],[hash;state q2; blank;sym a])
      :: (List.map (fun (z: sig) => ([sym z; state q1; hash],[state q2;sym z; sym a; hash]))
                   (elem sig)).

  Definition stay_none_some (q1 q2: states T) (a: sig) : pcp psig :=
    [([hash; state q1; blank],[hash;state q2; sym a]);([state q1; hash], [state q2;sym a; hash])].

  Definition right_none_some (q1 q2: states T) (a: sig): pcp psig :=
    [([hash;state q1; blank], [hash;sym a;state q2]);([state q1; hash], [sym a;state q2; hash])].

  Definition type_3_transitions_none : pcp psig :=
    List.concat (List.map (fun (q1: (states T)) => match trans(q1,None) with
                             |(q2, (None, L)) => left_none_none q1 q2
                             |(q2, (None, N)) => stay_none_none q1 q2
                             |(q2, (None, R)) => right_none_none q1 q2
                             |(q2, (Some a, L)) => left_none_some q1 q2 a
                             |(q2, (Some a, N)) => stay_none_some q1 q2 a
                             |(q2, (Some a, R)) => right_none_some q1 q2 a
                                                end) not_halting_states).


  (* Type 3 Transitions read Some *)
  Definition left_some (q1 q2: states T) (old new: sig): pcp psig :=
    ([hash; (state q1); (sym old)],
     [hash; (state q2); blank; (sym new)])
      ::(List.map (fun (z: sig) => ([ (sym z); (state q1); (sym old)],
                                 [ (state q2); (sym z); (sym new)])) (elem sig)).

  Definition stay_some (q1 q2: states T) (old new: sig): pcp psig :=
    [([state q1; sym old], [state q2; sym new])].

  Definition right_some (q1 q2: states T) (old new: sig): pcp psig :=
    [([state q1;sym old], [sym new; state q2])].

  Definition type_3_transitions_some : pcp psig :=
    List.concat (List.map (fun (A: ((states T)*sig)) =>
                              let (q1, old) := A in
                              match trans(q1, Some old) with
                                 |(q2, (None, L)) => left_some q1 q2 old old
                                 |(q2, (None, N)) => stay_some q1 q2 old old
                                 |(q2, (None, R)) => right_some q1 q2 old old
                                 |(q2, (Some new, L)) => left_some q1 q2 old new
                                 |(q2, (Some new, N)) => stay_some q1 q2 old new
                                 |(q2, (Some new, R)) => right_some q1 q2 old new
                                                end) (list_prod not_halting_states (elem sig))).

  Definition type_3_transitions : pcp psig :=
    type_3_transitions_none ++ type_3_transitions_some.

Type 4 Cards - eat up all symbols when a final state is reached

  Definition get_type_4_sig_l (q: states T) (s: sig) :=
    ([sym s; state q],[state q]).
  Definition get_type_4_sig_r (q: states T) (s:sig) :=
    ([state q; sym s],[state q]).
  Definition get_type_4_blank_l (q: states T) :=
    ([blank; state q],[state q]).
  Definition get_type_4_blank_r (q: states T) :=
    ([state q; blank],[state q]).


  Definition type_4_del_left: (pcp psig) :=
  List.map (fun (A: ((states T)* sig)) =>
                let (q, s) := A in get_type_4_sig_l q s) (list_prod halting_states (elem sig))++
           List.map get_type_4_blank_l halting_states.

  Definition type_4_del_right: (pcp psig) :=
  List.map (fun (A: ((states T)* sig)) =>
                let (q, s) := A in get_type_4_sig_r q s) (list_prod halting_states (elem sig))++
  List.map get_type_4_blank_r halting_states.

Type 5 Cards - finish the solution

  Definition get_type_5_final (q: states T): domino :=
    (([#; (state q);#;$],[$])).

  Definition type_5_final_pair: pcp psig :=
    List.map get_type_5_final halting_states.

  Definition TMdominoes: pcp psig :=
    type_2_hash ++ type_2_copy ++ type_3_transitions ++ type_4_del_left
                ++ type_4_del_right ++ type_5_final_pair.

MPCP instance
  Definition MPCP_instance (start: conf): (mpcp psig) :=
    (type_1_first_card start, TMdominoes).


Simulating one Machine Step with Dominoes


  (* Functions to obtain the MPCP solution *)
  Definition get_type_2_sig (A: list sig): (pcp psig) :=
    List.map (fun (s: sig) => ([sym s],[sym s])) A.


  (* definitions to obtain successor configurations *)
  Definition make_leftof_domino_config (q1: states T) (s: sig) (r: list sig) :=
    match (trans (q1, None)) with
    |(q2, (None, R)) => ([hash; (state q1); blank; sym s],
                        [hash; (state q2); sym s])::(get_type_2_sig r)
    |(q2, (None, _)) => ([hash; (state q1); blank],
                          [hash; (state q2); blank])::(get_type_2_sig (s::r))
    |(q2, (Some a, L)) => ([hash; (state q1); blank],
                          [hash; (state q2); blank; sym a])
                           ::(get_type_2_sig (s::r))
    |(q2, (Some a, N)) => ([hash; (state q1); blank],
                          [hash; (state q2); sym a])::(get_type_2_sig (s::r))
    |(q2, (Some a, R)) => ([hash; (state q1); blank],
                          [hash; sym a; (state q2)])::(get_type_2_sig (s::r))
    end.

  Definition make_niltape_domino_config (q1: states T) :=
    match (trans (q1, None)) with
    |(q2, (None, R)) => [([#; (state q1); blank;#],
                         [#; (state q2); blank;#])]
    |(q2, (None, _ )) => [([hash; (state q1); blank],
                         [hash; (state q2); blank])]++[([#],[#])]
    |(q2, (Some a, L)) => [([hash; (state q1); blank],
                          [hash; (state q2); blank; sym a])]++[([#],[#])]
    |(q2, (Some a, N)) => [([hash; (state q1); blank],
                          [hash; (state q2); sym a])]++[([#],[#])]
    |(q2, (Some a, R)) => [([hash; (state q1); blank],
                          [hash; sym a; (state q2)])]++[([#],[#])]
    end.

  Definition make_rightof_domino_config (q1: states T) (s: sig) (l: list sig) :=
    match (trans (q1, None)) with
    |(q2, (None, L)) => (get_type_2_sig (List.rev l))
                         ++[([sym s; (state q1); hash],
                             [ (state q2); sym s; hash])]
    |(q2, (None, _ )) => (get_type_2_sig (List.rev (s::l)))
                          ++[([ (state q1); hash], [ (state q2); hash])]
    |(q2, (Some a, N)) => (get_type_2_sig (List.rev (s::l)))
                           ++[([ (state q1); hash],[ (state q2); sym a; hash])]
    |(q2, (Some a, R)) => (get_type_2_sig (List.rev (s::l)))
                           ++[([ (state q1); hash],[sym a; (state q2); hash])]
    |(q2, (Some a, L)) => (get_type_2_sig (List.rev l))
                           ++[([sym s; (state q1); hash],
                              [ (state q2); sym s; sym a; hash])]
    end.

  Definition make_midtape_domino_config (q1: states T) (s: sig) (l r: list sig) :=
    match (trans (q1, Some s)) with
    |(q2, (None, R )) => [([#],[#])]++(get_type_2_sig (List.rev l))
                         ++[([ (state q1); sym s], [sym s; (state q2)])]
    |(q2, (None, N)) => [([#],[#])]++(get_type_2_sig (List.rev l))
                                ++[([ (state q1); sym s], [ (state q2); sym s])]
    |(q2, (Some a, R)) => [([#],[#])]++(get_type_2_sig (List.rev l))
                               ++[([ (state q1); sym s], [sym a; (state q2)])]
    |(q2, (Some a, N)) => [([#],[#])]++(get_type_2_sig (List.rev l))
                                ++[([ (state q1); sym s], [ (state q2); sym a])]
    |(q2, (None, L)) => match l with
                       |[] => [([hash; (state q1); sym s],
                               [hash; (state q2); blank; sym s])]
                       |z::l' => [([#],[#])]++(get_type_2_sig (List.rev l'))
                                           ++[([sym z; (state q1); sym s],
                                               [ (state q2); sym z; sym s])]
                       end
    |(q2, (Some a, L)) => match l with
                         |[] => [([hash; (state q1); sym s],
                                 [hash; (state q2); blank; sym a])]
                         |z::l'=> [([#],[#])]++(get_type_2_sig (List.rev l'))
                                            ++[([sym z; (state q1); sym s],
                                                [ (state q2); sym z; sym a])]
                         end
    end.

  Definition make_domino_config (con: conf) : (pcp psig) :=
    match (ctape con) with
    | (niltape _) => (make_niltape_domino_config (cstate con))
    | (leftof s r) => (make_leftof_domino_config (cstate con) s r)++[([#],[#])]
    | (rightof s l) => [([#],[#])]++(make_rightof_domino_config (cstate con) s l)
    | (midtape l s r) => (make_midtape_domino_config (cstate con) s l r)
                          ++(get_type_2_sig r)++[([#],[#])]
    end.


Correctness Proof

Halting Computations to MPCP Matches


  Lemma type_2_hash_element :
    forall a, a el [([#],[#])] -> a el TMdominoes.
  Proof.
    intros a ->%in_sing. apply in_or_app. left. now left.
  Qed.

  Lemma type_2_sig_element (L: list sig) :
    forall a, a el (get_type_2_sig L) -> a el TMdominoes.
  Proof.
    induction L as [ |l L]; intros a; simpl. auto. intros [<-|HA].
      + right. apply in_or_app. left. unfold type_2_copy.
        apply in_map_iff. exists l. now split.
      + now apply IHL.
  Qed.

  Lemma type_4_right_sig_element (q: states T) (s: sig):
      halt q = true -> get_type_4_sig_r q s el TMdominoes.
  Proof.
      intros H. unfold TMdominoes. apply in_or_app. right.
      apply in_or_app. right. apply in_or_app. right. apply in_or_app. right.
      apply in_or_app. left. apply in_app_iff. left. apply in_map_iff.
      exists (q,s). split. reflexivity. apply in_prod_iff. split.
      unfold halting_states. apply filter_In. split; auto. auto.
  Qed.

  Lemma type_4_left_sig_element (q: states T) (s: sig):
      halt q = true -> get_type_4_sig_l q s el TMdominoes.
  Proof.
      intros H. unfold TMdominoes. apply in_or_app. right.
      apply in_or_app. right. apply in_or_app. right. apply in_or_app. left.
      apply in_app_iff. left. apply in_map_iff. exists (q,s). split. reflexivity.
      apply in_prod_iff. split. unfold halting_states. apply filter_In. split; auto.
      auto.
  Qed.

  Lemma type_4_blank_r_element (q: states T):
    halt q = true -> (get_type_4_blank_r q) el TMdominoes.
  Proof.
      intros H. unfold TMdominoes. apply in_or_app. right.
      apply in_or_app. right. apply in_or_app. right. apply in_or_app. right.
      apply in_app_iff. left. apply in_app_iff. right. apply in_map_iff. exists q.
      split. auto. unfold halting_states. apply filter_In. split; auto.
  Qed.

  Lemma type_4_blank_l_element (q: states T):
    halt q = true -> (get_type_4_blank_l q) el TMdominoes.
  Proof.
      intros H. unfold TMdominoes. apply in_or_app. right.
      apply in_or_app. right. apply in_or_app. right. apply in_or_app. left.
      apply in_app_iff. right. apply in_map_iff. exists q.
      split. auto. unfold halting_states. apply filter_In. split; auto.
  Qed.

  Lemma get_type_5_element (q: states T):
      halt q = true -> get_type_5_final q el TMdominoes.
  Proof.
      intros H. unfold TMdominoes. apply in_or_app. right.
      apply in_or_app. right. apply in_or_app. right. apply in_or_app. right.
      apply in_or_app. right. apply in_map_iff. exists q. split; auto.
      unfold halting_states. apply filter_In. split; auto.
  Qed.

  Lemma remove_map_fst (E: list sig):
    concat (List.map fst (get_type_2_sig E)) = map sym E.
  Proof.
    induction E; simpl. auto. now rewrite IHE.
  Qed.

  Lemma remove_map_snd (E: list sig):
    concat (List.map snd (get_type_2_sig E)) = map sym E.
  Proof.
    induction E; simpl. auto. now rewrite IHE.
  Qed.

  Lemma deletion_dominoes_right (q: states T) (H: halt q = true) (A B: list sig):
    exists (D: pcp psig), D <<= TMdominoes
                  /\ concat (map fst D) ++ #::(map sym B)++[ (state q);#]
                    = #::(map sym B)++[ (state q)]++(map sym A)
                         ++[#]++concat (map snd D).
  Proof.
    induction A; simpl.
    - exists []. now split.
    - destruct IHA as [D [sub sol]].
      exists (([#],[#])::(get_type_2_sig B)++get_type_4_sig_r q a
                  ::(get_type_2_sig A)++[([#],[#])]++D).
      split.
      + intros e [<-|[HA|[HA|[HA|[HA|HA]%in_app_iff]%in_app_iff]]%in_app_iff].
        * now apply type_2_hash_element.
        * apply (type_2_sig_element HA).
        * subst. now apply type_4_right_sig_element.
        * apply (type_2_sig_element HA).
        * now apply type_2_hash_element.
        * now apply sub.
      + cbn. rewrite !map_app, !concat_app. cbn. rewrite !map_app, !concat_app. cbn.
        rewrite !remove_map_fst, !remove_map_snd. rewrite <- !app_assoc. rewrite <- !app_comm_cons.
        rewrite <- !app_assoc. rewrite <- app_comm_cons. rewrite sol. now cbn.
  Qed.

  Lemma deletion_dominoes_left (q: states T) (H: halt q = true) (A: list sig):
    exists (D: pcp psig), D <<= TMdominoes
                  /\ concat (map fst D) ++ [#; (state q);#;$]
                    = #::(map sym (rev A))++ (state q)::#::concat (map snd D)++[$].
  Proof.
    induction A; simpl.
    - exists []. now split.
    - destruct IHA as [D [sub sol]].
      exists (([#],[#])::get_type_2_sig (rev A)++get_type_4_sig_l q a::([#],[#])::D). split.
      + intros e [<-|[HA|[HA|[HA|HA]]]%in_app_iff].
        * now apply type_2_hash_element.
        * apply (type_2_sig_element HA).
        * subst. now apply type_4_left_sig_element.
        * subst. now apply type_2_hash_element.
        * now apply sub.
      + cbn. rewrite !map_app, !concat_app. rewrite remove_map_fst, remove_map_snd. cbn.
        rewrite <- !app_assoc. rewrite <- !app_comm_cons. now rewrite sol.
  Qed.

  Lemma deletion_dominoes (con:conf) (H: halt (cstate con) = true) :
    exists (D:pcp psig), D <<= TMdominoes
                 /\ concat (map fst D) ++ [#; (state (cstate con));#;$]
                   = (mconfig_pconfig con)++(concat (map snd D))++[$].
  Proof.
    destruct con as (q,t). destruct t eqn: HT; simpl in *.
    - exists [([#],[#]);get_type_4_blank_r q; ([#],[#])]. split.
      + intros e [<-|[H1|H1%in_sing]]. now apply type_2_hash_element. subst.
        now apply type_4_blank_r_element. subst. now apply type_2_hash_element.
      + now cbn.
    - destruct (deletion_dominoes_right H (e::l) []) as [A [H1 H2]].
      exists (([#],[#])::get_type_4_blank_r q ::
                  (get_type_2_sig (e::l))++[([#],[#])]++A). split.
      + intros b [<-|[<-|[HA|[HA%in_sing|HA]%in_app_iff]%in_app_iff]].
        * now apply type_2_hash_element.
        * now apply type_4_blank_r_element.
        * apply (type_2_sig_element HA).
        * subst. now apply type_2_hash_element.
        * now apply H1.
      + cbn. rewrite !map_app, !concat_app. rewrite remove_map_fst, remove_map_snd. cbn.
        rewrite <- !app_assoc. rewrite <- app_comm_cons. cbn in H2.
        change [#; (state q); #; $] with ([#; (state q);#]++[$]).
        setoid_rewrite app_assoc at 1. rewrite H2. cbn. now rewrite <- !app_assoc.
    - destruct (deletion_dominoes_left H (e::l)) as [A [H1 H2]].
      exists A. split. assumption. cbn in H2. now rewrite <- app_assoc.
    - destruct (deletion_dominoes_right H (e::l0) (rev l)) as [A [H1 H2]].
      destruct (deletion_dominoes_left H l) as [B [H3 H4]].
      exists (A++B). split.
      + auto.
      + rewrite !map_app, !concat_app. rewrite <- app_assoc. rewrite H4.
        change ( (state q) :: # :: concat (map snd B)++[$]) with
            ([ (state q);#]++concat (map snd B)++[$]).
        rewrite app_comm_cons, app_assoc, app_assoc. setoid_rewrite <- app_assoc at 2.
        cbn. rewrite H2. cbn. now rewrite <- !app_assoc, !app_comm_cons, <- !app_assoc.
  Qed.

  Lemma not_halting (q: states T) :
    halt q = false -> q el not_halting_states.
  Proof.
    unfold not_halting_states. rewrite filter_In.
    intros H. split. auto. now rewrite H.
  Qed.

  Lemma leftof_domino_config_element q1 s r:
    halt q1 = false -> (make_leftof_domino_config q1 s r) <<= TMdominoes.
  Proof.
    intros HF. intros a. unfold make_leftof_domino_config.
    assert (q1 el not_halting_states) as QH by apply (not_halting HF).
    destruct (trans (q1, None)) as (q2, (o, m)) eqn: DT.
    destruct o,m; intros [<-|HS]; try (apply (type_2_sig_element HS));
      right; apply in_or_app; right; apply in_or_app; right; apply in_or_app;
    left; apply in_or_app; left; unfold type_3_transitions_none; apply in_concat_iff.
    - exists (left_none_some q1 q2 e). split. now left.
      apply in_map_iff. exists q1. now rewrite DT.
    - exists (right_none_some q1 q2 e). split. now left.
      apply in_map_iff. exists q1. now rewrite DT.
    - exists (stay_none_some q1 q2 e). split. now left.
      apply in_map_iff. exists q1. now rewrite DT.
    - exists (left_none_none q1 q2). split. now left.
      apply in_map_iff. exists q1. now rewrite DT.
    - exists (right_none_none q1 q2). split. unfold right_none_none. right.
      apply in_or_app. right. apply in_map_iff. exists s. now split.
      apply in_map_iff. exists q1. now rewrite DT.
    - exists (stay_none_none q1 q2). split. now left.
      apply in_map_iff. exists q1. now rewrite DT.
  Qed.

  Lemma rightof_domino_config_element q1 s l:
    halt q1 = false -> (make_rightof_domino_config q1 s l) <<= TMdominoes.
  Proof.
    intros HF. intros a. unfold make_rightof_domino_config.
    assert (q1 el not_halting_states) as QH by apply (not_halting HF).
    destruct (trans (q1, None)) as (q2, (o,m)) eqn: DT.
    destruct o,m; intros [HS|HS]%in_app_iff; try apply (type_2_sig_element HS);
      right; apply in_or_app; right; apply in_or_app; right; apply in_or_app;
        left; apply in_or_app; left; unfold type_3_transitions_none; apply in_concat_iff;
          apply in_sing in HS; subst.
    - exists (left_none_some q1 q2 e). split.
       unfold left_none_some. right. apply in_map_iff. exists s. now split.
       apply in_map_iff. exists q1. now rewrite DT.
    - exists (right_none_some q1 q2 e). split. right. now left.
      apply in_map_iff. exists q1. now rewrite DT.
    - exists (stay_none_some q1 q2 e). split. right. now left.
      apply in_map_iff. exists q1. now rewrite DT.
    - exists (left_none_none q1 q2). split. right. apply in_map_iff.
      exists s. now split. apply in_map_iff. exists q1. rewrite DT. now split.
    - exists (right_none_none q1 q2). split. right. apply in_app_iff. now left.
      apply in_map_iff. exists q1. now rewrite DT.
    - exists (stay_none_none q1 q2). split. right. now left.
      apply in_map_iff. exists q1. now rewrite DT.
  Qed.

  Lemma midtape_domino_config_element q1 s l r:
    halt q1 = false -> (make_midtape_domino_config q1 s l r) <<= TMdominoes.
  Proof.
    intros HF. intros a. unfold make_midtape_domino_config.
    assert (q1 el not_halting_states) as QH by apply (not_halting HF).
    destruct (trans (q1, Some s)) as (q2, (o,m)) eqn: DT.
    destruct o,m; destruct l; try intros [HS|[HS|HS%in_sing]%in_app_iff]%in_app_iff;
      try apply (type_2_hash_element HS); try apply (type_2_sig_element HS);
           try (intros H%in_sing); subst;
      right; apply in_or_app; right; apply in_or_app; right; apply in_or_app;
        left; apply in_or_app; right; unfold type_3_transitions_some; apply in_concat_iff.
    - exists (left_some q1 q2 s e). split. now left.
      apply in_map_iff. exists (q1,s). rewrite DT. split. auto. now apply in_prod_iff.
    - exists (left_some q1 q2 s e). split. right. apply in_map_iff. exists e0. split; auto.
      apply in_map_iff. exists (q1, s). rewrite DT. split. auto. now apply in_prod_iff.
    - exists (right_some q1 q2 s e). split. now left. apply in_map_iff. exists (q1,s).
      rewrite DT. split. auto. now apply in_prod_iff.
    - exists (right_some q1 q2 s e). split. now left. apply in_map_iff. exists (q1,s).
      rewrite DT. split. auto. now apply in_prod_iff.
    - exists (stay_some q1 q2 s e). split. now left. apply in_map_iff. exists (q1,s).
      rewrite DT. split. auto. now apply in_prod_iff.
    - exists (stay_some q1 q2 s e). split. now left. apply in_map_iff. exists (q1,s).
      rewrite DT. split. auto. now apply in_prod_iff.
    - exists (left_some q1 q2 s s). split. now left. apply in_map_iff. exists (q1,s).
      rewrite DT. split. auto. now apply in_prod_iff.
    - exists (left_some q1 q2 s s). split. right. apply in_map_iff. exists e.
      split; auto. apply in_map_iff. exists (q1, s). rewrite DT. split. auto. now apply in_prod_iff.
    - exists (right_some q1 q2 s s). split. now left. apply in_map_iff. exists (q1,s).
      rewrite DT. split. auto. now apply in_prod_iff.
    - exists (right_some q1 q2 s s). split. now left. apply in_map_iff. exists (q1,s).
      rewrite DT. split. auto. now apply in_prod_iff.
    - exists (stay_some q1 q2 s s). split. now left. apply in_map_iff. exists (q1,s).
      rewrite DT. split. auto. now apply in_prod_iff.
    - exists (stay_some q1 q2 s s). split. now left. apply in_map_iff. exists (q1,s).
      rewrite DT. split. auto. now apply in_prod_iff.
  Qed.

  Lemma niltape_domino_config_element q1:
    halt q1 = false -> (make_niltape_domino_config q1) <<= TMdominoes.
  Proof.
   intros HF. intros a. unfold make_niltape_domino_config.
    assert (q1 el not_halting_states) as QH by apply (not_halting HF).
    destruct (trans (q1, None)) as (q2, (o,m)) eqn: DT.
    destruct o,m; try intros [HS%in_sing|HS]%in_app_iff; try (apply (type_2_hash_element HS));
    try intros HS%in_sing; subst;
      right; apply in_or_app; right; apply in_or_app; right; apply in_or_app;
        left; apply in_or_app; left; unfold type_3_transitions_none; apply in_concat_iff.
   - exists (left_none_some q1 q2 e). split. now left.
      apply in_map_iff. exists q1. now rewrite DT.
    - exists (right_none_some q1 q2 e). split. now left.
      apply in_map_iff. exists q1. now rewrite DT.
    - exists (stay_none_some q1 q2 e). split. now left.
      apply in_map_iff. exists q1. now rewrite DT.
    - exists (left_none_none q1 q2). split. now left.
      apply in_map_iff. exists q1. rewrite DT. now split.
    - exists (right_none_none q1 q2). split. now left.
      apply in_map_iff. exists q1. now rewrite DT.
    - exists (stay_none_none q1 q2). split. now left.
      apply in_map_iff. exists q1. now rewrite DT.
  Qed.

  Lemma make_domino_config_element (con: conf):
    halt (cstate con) = false -> (make_domino_config con) <<= TMdominoes.
  Proof.
    intros HF. unfold make_domino_config.
    destruct (ctape con); try intros a [HA|HA]%in_app_iff; try (now apply type_2_hash_element).
    - apply (niltape_domino_config_element HF).
    - apply (leftof_domino_config_element HF HA).
    - apply (rightof_domino_config_element HF HA).
    - apply (midtape_domino_config_element HF HA).
    - apply in_app_iff in HA as [HA|HA].
      + now apply (type_2_sig_element HA).
      + now apply type_2_hash_element.
  Qed.

  Lemma mkdomino_fst (con: conf):
    concat (List.map fst (make_domino_config con)) = mconfig_pconfig con.
  Proof.
    unfold make_domino_config, mconfig_pconfig. destruct (ctape con) eqn: CC.
    - unfold make_niltape_domino_config.
      destruct (trans (cstate con, None)) as (q2, (o,m)) eqn: DT. destruct o,m; now cbn.
    - unfold make_leftof_domino_config.
      destruct (trans (cstate con, None)) as (q2, (o,m)) eqn: DT;
      destruct o,m; cbn[concat app map fst snd]; rewrite !map_app, concat_app;
      now rewrite remove_map_fst.
    - unfold make_rightof_domino_config.
      destruct (trans (cstate con, None)) as (q2, (o,m)) eqn: DT.
      destruct o,m; rewrite !map_app, !concat_app, !remove_map_fst; cbn;
        rewrite map_app; now rewrite <- !app_assoc.
    - unfold make_midtape_domino_config.
      destruct (trans (cstate con, Some e)) as (q2, (o,m)) eqn: DT.
      destruct o,m,l; rewrite !map_app, !concat_app, !remove_map_fst;
        cbn; try (rewrite map_app); try (now repeat rewrite <- app_assoc).
  Qed.

  Lemma mkdomino_snd (con: conf):
    concat (List.map snd (make_domino_config con)) = mconfig_pconfig (step con).
  Proof.
    unfold make_domino_config, mconfig_pconfig, step. destruct (ctape con) eqn: CC.
    - unfold make_niltape_domino_config. simpl.
      destruct (trans (cstate con, None)) as (q2, (o,m)) eqn: DT. destruct o,m; now cbn.
    - unfold make_leftof_domino_config. simpl.
      destruct (trans (cstate con, None)) as (q2, (o,m)) eqn: DT.
      destruct o,m; cbn; now rewrite map_app, concat_app, remove_map_snd.
    - unfold make_rightof_domino_config. simpl.
      destruct (trans (cstate con, None)) as (q2, (o,m)) eqn: DT.
      destruct o,m; cbn; rewrite !map_app, concat_app; cbn; rewrite remove_map_snd;
        try reflexivity; rewrite map_app; now rewrite <- !app_assoc.
    - unfold make_midtape_domino_config. cbn [current].
      destruct (trans (cstate con, Some e)) as (q2, (o,m)) eqn: DT. destruct o,m; cbn.
      + destruct l; cbn.
        * now rewrite map_app, concat_app, remove_map_snd.
        * rewrite !map_app, !concat_app, !remove_map_snd. cbn.
          now rewrite <- !app_assoc.
      + destruct l0; cbn; rewrite !map_app, !concat_app; cbn.
        * now rewrite remove_map_snd, <- !app_assoc.
        * rewrite map_app, concat_app, !remove_map_snd. cbn.
          now rewrite <- !app_assoc.
      + rewrite !map_app, !concat_app. cbn.
        now rewrite !remove_map_snd, <- !app_assoc.
      + destruct l; cbn.
        * now rewrite map_app, concat_app, remove_map_snd.
        * rewrite !map_app, !concat_app, !remove_map_snd. cbn.
          now rewrite <- !app_assoc.
      + destruct l0; rewrite !map_app.
        * rewrite !concat_app; cbn.
          now rewrite remove_map_snd, <- !app_assoc.
        * rewrite !map_cons. rewrite !concat_app.
          rewrite !remove_map_snd. cbn. now rewrite map_app, <- !app_assoc.
      + rewrite !map_app, !concat_app. cbn.
        now rewrite !remove_map_snd, <- !app_assoc.
  Qed.

  Theorem TM_Halt_solution (start: conf):
    Halt start -> exists (A: pcp psig), (solution ((type_1_first_card start)::A))
                                /\ A <<= snd (MPCP_instance start).
  Proof.
    intros HT. unfold Halt in HT. destruct HT as [f [HF HR]].
    induction HR.
    - destruct (deletion_dominoes HF) as [A [H1 H2]].
      exists (A++[get_type_5_final (cstate c)]). split.
      + unfold solution, get_type_5_final. cbn. f_equal.
        now rewrite !map_app, !concat_app.
      + intros a [HA|HA%in_sing]%in_app_iff.
        * auto.
        * subst. now apply get_type_5_element.
    - destruct (IHHR HF) as [S [SA SUB]]. exists ((make_domino_config c)++S). split.
      + clear IHHR HF SUB. revert SA. unfold solution, type_1_first_card.
        cbn. rewrite !map_app, !concat_app. rewrite mkdomino_fst, mkdomino_snd.
        inversion 1. now rewrite H1.
      + intros a [HD|HS]%in_app_iff. apply (make_domino_config_element H HD).
        now apply SUB.
  Qed.

  Theorem TM_Halt_MPCP_solution (start: conf):
    Halt start -> MPCP (MPCP_instance start).
  Proof.
    intros HT. apply (TM_Halt_solution) in HT as [A [SA SU]]. exists A.
    repeat split. inversion 1. intros a [<-|HA]. now left. right. now apply SU. exact SA.
  Qed.

MPCP Matches to Halting Computations


  Lemma halting_states_false (q: states T):
    halt q = false -> q el halting_states -> False.
  Proof.
    intros HQ HF. unfold halting_states in *.
    apply filter_In in HF as []. rewrite H0 in *. discriminate.
  Qed.

  Ltac split_element :=
    unfold type_2_copy, type_2_hash, left_some, right_some,
    stay_some, type_3_transitions, left_none_some, right_none_some, stay_none_some,
    type_4_del_left, type_4_del_right, type_5_final_pair,
    left_none_none, right_none_none, stay_none_none in *;
    cbn [ List.concat List.map fst snd];
    try match goal with
          | [ H : _ el _ :: _ |- _ ] => destruct H
          | [ H : _ el [] |- _ ] => inv H
          | [ H : _ el _ ++ _ |- _ ] => eapply in_app_iff in H as [H | H]
          | [ H : _ el [ _ ] |- _ ] => eapply in_sing in H; subst
          | [ H : _ el [ _;_ ] |- _ ] => destruct H as [<-| H]
          | [ H : _ el List.map _ _ |- _ ] => eapply in_map_iff in H as [ ? [] ]
          | [ H : _ el type_3_transitions_none |- _ ] => eapply in_concat_iff in H as [? [] ]
          | [ H : _ el type_3_transitions_some |- _ ] => eapply in_concat_iff in H as [? [] ]
          | [ H : _ el list_prod _ _ |- _ ] => eapply in_prod_iff in H as []
          | [ H : _ el halting_states |- _ ] => eapply halting_states_false in H
          | [ H : _ <<= ((type_1_first_card _)::_) |- _ <<= (type_1_first_card _)
                          ::TMdominoes ] => intros ? ?; apply H; right
        end;
    try (cbn in *;
         match goal with
         | [ H : _ :: _ = _ :: _ |- _ ] => now inv H
         end);
    subst.
  Ltac repSplit := repeat split_element.


  Lemma next_cards_niltape (S: pcp psig) (con start: conf):
    S <<= (type_1_first_card start)::TMdominoes
    -> ctape con = niltape sig -> halt (cstate con) = false
    -> solution (([],mconfig_pconfig con)::S)
    -> exists S', S = (make_niltape_domino_config (cstate con)) ++S'.
  Proof.
    unfold solution. cbn[concat List.map fst snd]. rewrite app_nil_l.
    intros Sub CT HF. destruct S. inversion 1. unfold mconfig_pconfig in H1.
    destruct (ctape con); inv H1. unfold mconfig_pconfig.
    rewrite CT. intros HH. destruct (Sub p (or_introl eq_refl)). subst. inv HH.
    unfold TMdominoes in *. repSplit.
    - inv HH. destruct S. inv H0.
      destruct (Sub p (or_intror (or_introl eq_refl))) as [ <- | ]; repSplit;
        destruct *; repSplit.
    - destruct * eqn: _; repSplit;inv HH; try (exists S;
      unfold make_niltape_domino_config; now rewrite H2); destruct S; try discriminate;
        destruct (Sub p (or_intror (or_introl eq_refl))) as [<- | ]; repSplit;
          try (destruct *; repSplit); exists S; unfold make_niltape_domino_config; now rewrite H2.
    - destruct *; repSplit.
    - destruct *; repSplit.
    - destruct *. inv HH.
  Qed.

  Lemma next_sigma_dominoes_left start S L A:
    S <<= (type_1_first_card start)::TMdominoes
    -> concat (List.map fst S) = map sym L ++ [#]++#::A
    -> exists S', S = (get_type_2_sig L)++[([#],[#])]++S'.
  Proof.
    revert S. induction L; intros S Sub HS.
    - cbn. destruct S. inv HS.
      destruct (Sub d (or_introl eq_refl)). subst. inv HS. unfold TMdominoes in *.
      repSplit.
      + exists S. reflexivity.
      + destruct *; repSplit.
      + destruct *; repSplit.
      + destruct *. inv HS.
      + destruct *. inv HS.
    - destruct S. inv HS. destruct (Sub d (or_introl eq_refl)).
      subst. inv HS. unfold TMdominoes in *. repSplit.
      + cbn in HS. inv HS. simpl. destruct (IHL S) as [S' HS]. intros s ES.
        apply Sub. now right. assumption. exists S'. rewrite HS. reflexivity.
      + destruct *; repSplit; inv HS; destruct L; inv H3.
      + destruct *; repSplit; inv HS; destruct L; inv H4.
      + destruct *; repSplit. inv HS. destruct L; inv H3.
      + destruct *; repSplit.
  Qed.

  Lemma next_cards_leftof (S: pcp psig) (con start: conf) e l:
    S <<= (type_1_first_card start)::TMdominoes
    -> ctape con = leftof e l -> halt (cstate con) = false
    -> solution (([],mconfig_pconfig con)::S)
    -> exists S', S = (make_leftof_domino_config (cstate con) e l ++ [([#], [#])]) ++ S'.
  Proof.
    unfold solution. cbn[concat List.map fst snd]. rewrite app_nil_l.
    intros Sub CT HF. destruct S. inversion 1. unfold mconfig_pconfig in H1.
    destruct (ctape con) in H1; inv H1. unfold mconfig_pconfig.
    rewrite CT. intros HH. destruct (Sub p (or_introl eq_refl)). subst. inv HH.
    unfold TMdominoes in *. repSplit.
    - inv HH. destruct S. inv H0.
      destruct (Sub p (or_intror (or_introl eq_refl))) as [ <- | ]; repSplit.
      destruct *; repSplit. destruct *; repSplit. destruct *; repSplit.
      destruct *; repSplit.
    - destruct * eqn: _; repSplit;
        try (inversion HH as [[H HI HII]]; subst; rewrite <- app_assoc in HII;
             apply (@next_sigma_dominoes_left start) in HII as [S' HS]);
        try (remember (e::l) as B; inversion HH as [[H HI]]; subst; rewrite <- app_assoc in HI;
             apply (@next_sigma_dominoes_left start) in HI as [S' HS]);
        try (unfold make_leftof_domino_config; rewrite H2; exists S'; rewrite HS;
             now rewrite !app_assoc); split_element.
    - destruct *; repSplit.
    - destruct *; repSplit.
    - destruct *. inv HH.
  Qed.

  Lemma next_sigma_dominoes_right start S B A s:
    S <<= (type_1_first_card start)::TMdominoes
    -> concat (List.map fst S) = map sym B ++[sym s]++A
    -> exists S', S = (get_type_2_sig B)++S'.
  Proof.
    revert S. induction B; intros S Sub HS.
    - cbn in *. now exists S.
    - simpl in *. destruct S. inv HS.
      destruct (Sub d (or_introl eq_refl)). subst. inv HS.
      unfold TMdominoes in *. repSplit.
      + inv HS. destruct (IHB S) as [S' HS]. intros se HE. apply Sub.
        now right. assumption. rewrite HS. exists S'. reflexivity.
      + destruct *; repSplit; inv HS; destruct B; inv H3.
      + destruct *; repSplit; inv HS; destruct B; inv H4.
      + destruct *; repSplit; inv HS; destruct B; inv H3.
      + destruct *. split_element.
  Qed.


  Lemma next_cards_rightof (S: pcp psig) (con start: conf) e r:
    S <<= (type_1_first_card start)::TMdominoes
    -> ctape con = rightof e r -> halt (cstate con) = false
    -> solution (([],mconfig_pconfig con)::S)
    -> exists S', S = ([([#], [#])] ++ make_rightof_domino_config (cstate con) e r) ++ S'.
  Proof.
    unfold solution. cbn[concat List.map fst snd]. rewrite app_nil_l.
    intros Sub CT HF. unfold mconfig_pconfig. destruct S. inversion 1.
    destruct (ctape con); inv H1.
    rewrite CT. intros HH. destruct (Sub p (or_introl eq_refl)). subst. inv HH.
    unfold TMdominoes in *. repSplit.
    - inv HH. destruct S. inv H0. now apply app_cons_not_nil in H1.
      rewrite <- !app_assoc in H0. rewrite map_app, <- !app_assoc in H0.
      destruct (@next_sigma_dominoes_right start (p::S) (List.rev r) ([state (cstate con)]
                                                    ++ [#] ++ # :: concat (List.map snd (p :: S))) e)
        as [S' HS]. split_element. assumption. assumption. rewrite HS in *. cbn in H0.
      rewrite !List.map_app, !concat_app in H0. rewrite remove_map_fst, remove_map_snd in H0.
      apply app_inv_head in H0. destruct S' as [ |a A]. inv H0.
      destruct (Sub a (in_or_app (([#], [#]) :: get_type_2_sig (List.rev r)) (a :: A)
                                 a (or_intror (or_introl eq_refl)))). subst. inv H0.
      repSplit; inv H0.
      + destruct A. inv H3.
        destruct (Sub p0 (in_or_app (([#], [#]) :: get_type_2_sig (List.rev r))
                                   (([(sym e)], [ (sym e)])
                                   :: p0 :: A)
                                   p0 (or_intror (or_intror (or_introl eq_refl))))).
        subst. inv H3. repSplit.
        * destruct * eqn: _; repSplit; inv H3; unfold make_rightof_domino_config;
            rewrite H4; exists A; simpl; unfold get_type_2_sig; rewrite List.map_app; simpl;
              now rewrite <- !app_assoc.
        * destruct *; repSplit.
        * destruct *; split_element.
        * destruct *; split_element.
      + destruct * eqn: _; repSplit; inv H3; unfold make_rightof_domino_config;
          rewrite H1; exists A; now rewrite <- !app_assoc.
      + destruct *; repSplit.
      + destruct *; repSplit.
      + destruct *; split_element.
    - simpl in HH. simpl in HH.
      destruct * eqn: _; repSplit; remember (List.rev r) as C; destruct C; inv HH.
    - simpl in HH. simpl in HH.
      destruct * eqn: _; repSplit; remember (List.rev r) as C; destruct C; inv HH.
    - destruct *; split_element.
    - destruct *; split_element.
    - inv HH. remember (rev r) as A. destruct A; inv H1.
  Qed.

  Lemma next_cards_midtape (S: pcp psig) (con start: conf) e l r:
    S <<= (type_1_first_card start)::TMdominoes
    -> ctape con = midtape l e r -> halt (cstate con) = false
    -> solution (([],mconfig_pconfig con)::S)
    -> exists S', S = (make_midtape_domino_config (cstate con) e l r
                                            ++ get_type_2_sig r ++ [([#], [#])]) ++ S'.
  Proof.
    unfold solution. cbn[concat List.map fst snd]. rewrite app_nil_l.
    intros Sub CT HF. unfold mconfig_pconfig. destruct S. inversion 1.
    destruct (ctape con); inv H1.
    rewrite CT. intros HH. destruct (Sub p (or_introl eq_refl)). subst. inv HH.
    unfold TMdominoes in *. repSplit.
    - simpl in HH. destruct l.
      + simpl in *. inv HH. destruct S. inv H0. destruct (Sub p (or_intror (or_introl eq_refl))).
        subst. inv H0. repSplit.
        * destruct * eqn:_; repSplit.
        * destruct * eqn:_; repSplit; inv H0; unfold make_midtape_domino_config;
            rewrite H4; simpl; rewrite <- app_assoc in H10;
              apply (@next_sigma_dominoes_left start) in H10 as [S' HS]; subst;
                try (exists S'; now rewrite <- app_assoc); intros a HA; apply Sub; right; now right.
        * destruct *; split_element.
        * destruct * eqn:_; repSplit.
      + inv HH. rewrite map_app in H0. rewrite <- !app_assoc in H0.
        assert (H1 := H0). apply (@next_sigma_dominoes_right start) in H0 as [S' HS]. subst.
        rewrite !List.map_app, !concat_app in H1. rewrite remove_map_fst, remove_map_snd in H1.
        apply app_inv_head in H1. destruct S'. inv H1.
        destruct (Sub p (in_or_app (([#], [#]) :: get_type_2_sig (List.rev l)) (p :: S')
                                    p (or_intror (or_introl eq_refl)))). subst. inv H1.
         repSplit.
        * inv H1. destruct S'. inv H3.
          destruct (Sub p (in_or_app (([#], [#]) :: get_type_2_sig (List.rev l))
                 (([ (sym e0)], [ (sym e0)])::p :: S')
                 p (or_intror (or_intror (or_introl eq_refl))))).
          subst. inv H3. repSplit.
          -- destruct * eqn:_; repSplit.
          -- destruct * eqn:_; repSplit; inv H3; rewrite <- app_assoc in H11;
               apply (@next_sigma_dominoes_left start) in H11 as [A HA]; subst;
                unfold make_midtape_domino_config; try (rewrite H5; exists A; simpl;
                unfold get_type_2_sig; rewrite !List.map_app; simpl;
                  now rewrite <- !app_assoc); split_element; apply in_app_iff; right; now repeat right.
          -- destruct *; split_element.
          -- destruct *; repSplit.
        * destruct *; repSplit.
        * destruct * eqn:_; repSplit; inv H1; rewrite <- app_assoc in H12;
            apply (@next_sigma_dominoes_left start) in H12 as [A HA]; subst;
          try (exists A; unfold make_midtape_domino_config; rewrite H4; simpl;
                 now rewrite <- !app_assoc); split_element; apply in_app_iff; right; now repeat right.
        * destruct *; repSplit.
        * destruct *; split_element.
        * split_element. assumption.
    - destruct * eqn:_;repSplit; inv HH; remember (List.rev l) as B;
        destruct B; simpl in H5; try inv H5. simpl in H6. inv H6. inv H6.
    - destruct * eqn:_; repSplit; inv HH; remember (List.rev l) as B;
        destruct B; inv H7; rewrite <- !app_assoc in H10;
          apply (@next_sigma_dominoes_left start) in H10 as [A HA]; subst;
            try (exists A; unfold make_midtape_domino_config; rewrite H3; destruct l);
            try (now split_element); try (now rewrite <- !app_assoc); simpl in HeqB;
              now apply app_cons_not_nil in HeqB.
    - destruct *; split_element.
    - destruct *; split_element.
    - inv HH. remember (rev l) as A. destruct A; inv H1.
  Qed.

  Lemma next_cards_solution_list (S: pcp psig) (con start: conf):
    S <<= (type_1_first_card start)::TMdominoes
    -> halt (cstate con) = false
    -> solution (([],mconfig_pconfig con)::S)
    -> exists S', S = (make_domino_config con)++S'.
  Proof.
    intros Sub HF. unfold make_domino_config.
    destruct (ctape con) eqn: CT.
    - apply (next_cards_niltape Sub CT HF).
    - apply (next_cards_leftof Sub CT HF).
    - apply (next_cards_rightof Sub CT HF).
    - apply (next_cards_midtape Sub CT HF).
  Qed.

  Lemma make_domino_config_not_nil (con: conf):
    (make_domino_config con) <> [].
  Proof.
    unfold make_domino_config. destruct (ctape con).
    - unfold make_niltape_domino_config. destruct (trans (cstate con, None)) as (q2, (o,m)) eqn: DT.
      destruct o,m; inversion 1.
    - intros [H G]%app_eq_nil. discriminate G.
    - intros [H G]%app_eq_nil. discriminate H.
    - intros [H [_ G]%app_eq_nil]%app_eq_nil. discriminate G.
  Qed.

  Lemma solution_Halt (start: conf):
   forall (A: pcp psig) con,
      solution (([],mconfig_pconfig con)::A) ->
      A <<= (type_1_first_card start)::TMdominoes ->
      Halt con.
  Proof.
    intros A. pattern A. apply (@size_induction (pcp psig) (@length (list psig* list psig))).
    intros B IH con sol sub. destruct (halt (cstate con)) eqn: HC.
    - exists con. split. assumption. constructor.
    - destruct (next_cards_solution_list sub HC sol) as [S' HS]. subst.
      assert (|S'| < | make_domino_config con ++ S' |) as HL.
      { rewrite app_length. destruct (|make_domino_config con|) eqn: ML.
        apply length_zero_iff_nil in ML. exfalso. apply (make_domino_config_not_nil ML).
        omega. }
      specialize (IH S' HL (step con)). destruct IH as [fin [HF RF]].
      + revert sol. unfold solution. rewrite !map_cons, !concat_cons. cbn.
        rewrite !map_app, !concat_app. rewrite mkdomino_fst, mkdomino_snd.
        cbn. intros H. apply app_inv_head in H. now rewrite H.
      + intros a HA. apply sub. apply in_app_iff. now right.
      + exists fin. split. assumption. apply reachS; assumption.
  Qed.

  Theorem MPCP_solution_TM_Halt (start: conf):
    MPCP (MPCP_instance start) -> Halt start.
  Proof.
    unfold MPCP_instance, pcp_solution. cbn[fst]. intros [S [NN [SB SL]]].
    unfold type_1_first_card in SL. unfold solution in SL. cbn[concat List.map fst snd] in SL.
    inv SL. apply (@solution_Halt start S start H0).
    intros a HA. apply SB. now right.
  Qed.

End Fix_TM.

Theorem reduction_halt_mpcp : red HaltD MPCPD.
Proof. unfold red. exists (fun (S:{sig : finType & sTM sig & tape sig}) =>
                        existT (fun X => mpcp X) (psig (projT2 (sigT_of_sigT2 S)))
                                   (MPCP_instance (initc (projT2 (sigT_of_sigT2 S))
                                                         (projT3 S)))).
       intros [sig [M c]]. unfold HaltD, MPCPD. cbn. split.
       apply TM_Halt_MPCP_solution. apply MPCP_solution_TM_Halt.
Qed.