Require Import Prelim Single_TM String_rewriting Reductions.

Section Fix_TM.
  Variable sig : finType.
  Variable T : (sTM sig).
  Definition conf :Type := mconfig sig (states T).

  Instance eq_dec_states : eq_dec (states T).
  Proof. exact _. Defined.

  Inductive rsig' : Type := hash | dollar | sigma (s: sig).

  Instance eq_dec_rsig' : eq_dec rsig'.
  Proof.
    intros. hnf. decide equality. apply eq_dec_sig.
  Defined.

  Instance finType_rsig': finTypeC (EqType rsig').
  Proof.
    exists (hash::dollar::(List.map (fun s => sigma s) (elem sig))).
    intros x. destruct x; cbn. induction (elem sig); auto. induction (elem sig); auto.
    apply inductive_count. intros x y; now inversion 1. apply (@enum_ok sig (class sig) s).
  Defined.


  Inductive rsig : Type := state (q: states T) | symb (s: (FinType (EqType rsig'))).
  Definition sym : sig -> rsig := fun s => symb (sigma s).
  Notation "#" := (symb hash).
  Notation "$" := (symb dollar).

  Instance eq_dec_rsig : eq_dec rsig.
  Proof.
    intros. hnf. decide equality. apply eq_dec_states.
    apply eq_dec_rsig'.
  Defined.

  Lemma state_count_one q:
    count (map (fun s : states T => state s) (elem (states T))) (state q) = 1.
  Proof.
    apply inductive_count. intros x y; now inversion 1.
    apply (@enum_ok (states T) (class (states T)) q).
  Qed.

  Lemma symb_count_one s:
    count (map (fun s0 : FinType (EqType rsig') => symb s0)
               (elem (FinType (EqType rsig')))) (symb s) = 1.
  Proof.
    apply inductive_count. intros x y; now inversion 1.
    apply (@enum_ok (FinType (EqType rsig')) (class (FinType (EqType rsig'))) s).
  Qed.


  Instance finType_rsig: finTypeC (EqType rsig).
  Proof.
    exists ((List.map (fun s => state s) (elem (states T)))
         ++ (List.map (fun s => symb s) (elem (FinType (EqType rsig'))))).
    intros x. destruct x.
    - rewrite in_count_app. rewrite state_count_one.
      remember (elem (FinType (EqType (rsig')))) as B.
      now rewrite (@diff_constructors_count_zero (FinType (EqType rsig'))
                                                 (EqType rsig) (states T) B symb state).
    - rewrite in_count_app. rewrite symb_count_one. remember (elem (states T)) as B.
      now rewrite (@diff_constructors_count_zero (states T)).
  Defined.

  Definition rsig_finType : finType := (@FinType (EqType rsig) finType_rsig).

  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)).

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

  Lemma halting (q: states T) :
    halt q = true <-> q el halting_states.
  Proof.
    split. unfold halting_states. rewrite filter_In.
    intros H. split. auto. now rewrite H. unfold halting_states.
    rewrite filter_In. intros []. auto.
  Qed.

  Definition mk_srconf (c: conf): list rsig :=
    match (ctape c) with
    | niltape _ => [state (cstate c);#;$]
    | leftof s r => [state(cstate c); #]++ (List.map sym (s::r))++[$]
    | rightof s l => [#]++(List.map sym (List.rev (s::l)))++[state(cstate c);$]
    | midtape l s r => [#]++(List.map sym (List.rev l))++ [(state(cstate c))]
                                ++ (List.map sym (s::r))++[$]
    end.

  Lemma sym_inj : Injective sym.
  Proof.
    intros x y. now inversion 1.
  Qed.

  Lemma state_not_sym A B q e l:
    A++[state q] = B ++sym e::(List.map sym l) -> False.
  Proof.
    revert B e. induction l; intros B e H; cbn in *.
    - apply last_app_eq in H as [H HE]. inv HE.
    - apply (IHl (B++[sym e]) a). now rewrite <- app_assoc.
  Qed.

  Lemma midtape_state A B q1 q2 l r:
    A ++ (state q1)::B = List.map sym l++(state q2)::(List.map sym r)
            -> A = List.map sym l /\ B = (List.map sym r) /\ q1 = q2.
  Proof.
    revert r A B. induction l; intros r A B H; cbn in *.
    - destruct A. rewrite app_nil_l in H. inv H. now split. inv H. exfalso.
      assert ((state q1) el (A++(state q1)::B) -> False). intros H. rewrite H2 in H.
      apply in_map_iff in H as [x [? ?]]. inv H. apply H. auto.
    - destruct A. rewrite app_nil_l in H. inv H. inv H. destruct (IHl r A B H2).
      subst. now split.
  Qed.

  Lemma mk_srconf_inj (c1 c2: conf) :
    mk_srconf c1 = mk_srconf c2 <-> c1 = c2.
  Proof.
    split.
    - unfold mk_srconf. destruct (ctape c1) eqn: H,(ctape c2) eqn: H'; try inversion 1;
                         subst; destruct c1,c2; cbn in *; subst; try reflexivity.
      + apply app_inv_tail in H4. apply map_inj in H4. now subst. apply sym_inj.
      + change [state cstate;$] with ([state cstate]++[$]) in H2.
        change [state cstate0;$] with ([state cstate0]++[$]) in H2.
        rewrite !app_assoc in H2. apply app_inv_tail in H2.
        apply last_app_eq in H2 as [H3 H2]. repeat rewrite map_app in H3.
        apply last_app_eq in H3 as [H3 HE]. inv H2. inv HE. rewrite map_inj in H3.
        rewrite rev_eq in H3. now subst. apply sym_inj.
      + change [state cstate; $] with ([state cstate]++[$]) in H2.
        rewrite !app_assoc, !app_comm_cons in H2. rewrite app_assoc in H2.
        apply last_app_eq in H2 as [H2 _]. exfalso.
        change (state cstate0::sym e0::List.map sym l1)
                   with ([state cstate0]++sym e0::List.map sym l1) in H2.
        rewrite app_assoc in H2. apply (state_not_sym H2).
      + change [state cstate0; $] with ([state cstate0]++[$]) in H2.
        rewrite !app_assoc, !app_comm_cons in H2. rewrite app_assoc in H2.
        apply last_app_eq in H2 as [H2 _]. symmetry in H2.
        change (state cstate::sym e::List.map sym l0)
                          with ([state cstate]++sym e::List.map sym l0) in H2.
        rewrite app_assoc in H2. exfalso. apply (state_not_sym H2).
      + rewrite !app_comm_cons in H2. rewrite! app_assoc in H2. apply last_app_eq in H2 as [H2 _].
        assert (List.map sym (List.rev l) ++ state cstate :: List.map sym (e::l0) =
                List.map sym (List.rev l1) ++ state cstate0 :: List.map sym (e0::l2)) as H3 by auto.
        apply midtape_state in H3 as [H3 [H4 H5]]. inv H4. apply map_inj in H6.
        subst. apply map_inj in H3. rewrite rev_eq in H3. now subst. apply sym_inj. apply sym_inj.
    - now intros <-.
  Qed.

   Definition get_rules_left (q1 q2: states T) (old new: option sig) : list (list rsig * list rsig):=
    match old,new with
    |None,None => List.map (fun c => ([sym c; state q1; $], [state q2; sym c; $])) (elem sig)
    |None,Some b => List.map (fun c => ([sym c; state q1; $], [state q2; sym c; sym b; $])) (elem sig)
    |Some a,None => List.map (fun c => ([sym c; state q1; sym a], [state q2; sym c; sym a])) (elem sig)
    |Some a,Some b => List.map (fun c => ([sym c; state q1; sym a], [state q2; sym c; sym b])) (elem sig)
    end.

   Definition get_rules_right (q1 q2: states T) : list (list rsig * list rsig) :=
     List.map (fun a => ([state q1; #; sym a],[#; state q2; sym a])) (elem sig).

   Definition get_rules (q1 q2: states T) (old new: option sig) (m: move) :
     list (list rsig * list rsig) :=
    match old,new,m with
    |None,None,L => [([state q1; #],[state q2; #])] ++ (get_rules_left q1 q2 None None)
    |None,None,N => [([state q1; #],[state q2; #]);([state q1; $],[state q2; $])]
    |None,None,R => [([state q1; #;$],[state q2; #;$]); ([state q1; $],[state q2; $])]
                     ++ (get_rules_right q1 q2)
    |None,Some b,L => [([state q1; #],[state q2; #; sym b])] ++ (get_rules_left q1 q2 None (Some b))
    |None,Some b,N => [([state q1; #],[#; state q2; sym b]); ([state q1; $],[state q2; sym b; $])]
    |None,Some b,R => [([state q1; #],[#; sym b; state q2]); ([state q1; $],[sym b; state q2; $])]
    |Some a,None,L => [([#;state q1; sym a],[state q2; #; sym a])]
                       ++ (get_rules_left q1 q2 (Some a) None)
    |Some a,None,N => [([state q1; sym a],[state q2; sym a])]
    |Some a,None,R => [([state q1; sym a],[sym a; state q2])]
    |Some a,Some b,L => [([#; state q1; sym a],[state q2; #; sym b])]
                         ++ (get_rules_left q1 q2 (Some a) (Some b))
    |Some a,Some b,N => [([state q1; sym a],[state q2; sym b])]
    |Some a,Some b,R => [([state q1; sym a],[sym b; state q2])]
    end.


   Definition TMrules : list (list rsig * list rsig) :=
     List.concat ((List.map (fun q1 => match trans (q1,None) with
                      |(q2,(o,m)) => get_rules q1 q2 None o m
                                   end) not_halting_states) ++
                 (List.map (fun (P: states T * sig) => let (q1,s) := P in match trans (q1,Some s) with
                                                    |(q2,(o,m)) => get_rules q1 q2 (Some s) o m
                                                    end)
                           (list_prod not_halting_states (elem sig)))).

   Lemma get_rules_el_TMrules (q1 q2: states T) (old new: option sig) (m: move) :
     halt q1 = false -> (trans (q1,old) = (q2,(new,m)))
     -> get_rules q1 q2 old new m <<= TMrules.
   Proof.
     intros HF HT. intros s HS. apply in_concat_iff. exists (get_rules q1 q2 old new m).
     split. assumption. apply in_app_iff. destruct old.
     - right. apply in_map_iff. exists (q1,e). rewrite HT. split. reflexivity.
       apply in_prod_iff. split. now apply not_halting. auto.
     - left. apply in_map_iff. exists q1. rewrite HT. split. auto. now apply not_halting.
   Qed.

   Lemma rewrite_step_conf (c1: conf) :
    (halt (cstate c1) = false) -> rew TMrules (mk_srconf c1) (mk_srconf (step c1)).
   Proof.
     intros H. unfold mk_srconf. destruct (ctape c1) eqn: CT; unfold step; rewrite CT; cbn.
     - destruct (trans (cstate c1, None)) as (q2,(new,mov)) eqn: TC;
         assert (Sub: get_rules (cstate c1) q2 None new mov <<= TMrules)
         by (now apply get_rules_el_TMrules). destruct new as [new| ]; destruct mov; cbn.
       + apply rewR with (x:=[]) (u:= [state (cstate c1);#]) (v:=[state q2;#;sym new]).
         firstorder.
       + apply rewR with (x:=[]) (u:= [state (cstate c1);#]) (v:= [#;sym new; state q2]).
         firstorder.
       + apply rewR with (x:=[]) (u:= [state (cstate c1); #]) (v:=[#; state q2; sym new]).
         firstorder.
       + apply rewR with (x:=[]) (u:= [state (cstate c1); #]) (v:=[state q2; #]).
         firstorder.
       + apply rewR with (x:=[]) (u:= [state (cstate c1); #; $])(v:=[state q2; #; $]).
         firstorder.
       + apply rewR with (x:=[]) (u:= [state (cstate c1); #]) (v:=[state q2; #]).
         firstorder.
     - destruct (trans (cstate c1, None)) as (q2,(new,mov)) eqn: TC;
         assert (Sub: get_rules (cstate c1) q2 None new mov <<= TMrules)
         by (now apply get_rules_el_TMrules). destruct new as [new| ]; destruct mov; cbn.
       + apply rewR with (x:=[]) (u:= [state (cstate c1); #]) (v:=[state q2; #; sym new]).
         firstorder.
       + apply rewR with (x:=[]) (u:= [state (cstate c1); #]) (v:=[#; sym new; state q2]).
         firstorder.
       + apply rewR with (x:=[]) (u:= [state (cstate c1); #]) (v:=[#; state q2; sym new]).
         firstorder.
       + apply rewR with (x:=[]) (u:= [state (cstate c1); #])(v:=[state q2; #]).
         firstorder.
       + apply rewR with (x:=[]) (u:= [state (cstate c1); #; sym e]) (v:=[#; state q2; sym e]).
         apply Sub. cbn. right. right. unfold get_rules_right. apply in_map_iff. exists e. now split.
       + apply rewR with (x:=[]) (u:= [state (cstate c1); #]) (v:=[state q2; #]).
         firstorder.
     - destruct (trans (cstate c1, None)) as (q2,(new,mov)) eqn: TC;
         assert (Sub: get_rules (cstate c1) q2 None new mov <<= TMrules)
         by (now apply get_rules_el_TMrules). destruct new as [new| ]; destruct mov; cbn.
       + rewrite map_app. rewrite <- app_assoc.
         apply rewR with (x:=#::List.map sym (List.rev l)) (u:= [sym e; state (cstate c1); $])
                       (v:=[state q2; sym e; sym new;$]).
         apply Sub. cbn. right. apply in_map_iff. exists e. now split.
       + rewrite !map_app. setoid_rewrite <- app_assoc at 2.
         apply rewR with (x:=#::List.map sym (List.rev l) ++[sym e]) (u:= [state (cstate c1); $])
                       (v:=[sym new; state q2;$]). firstorder.
       + apply rewR with (x:=#::List.map sym (List.rev l++[e])) (u:= [state (cstate c1); $])
                       (v:=[state q2; sym new; $]). firstorder.
       + rewrite map_app. rewrite <- app_assoc.
         apply rewR with (x:=#::List.map sym (List.rev l)) (u:= [sym e; state (cstate c1); $])
                       (v:=[state q2; sym e;$]).
         apply Sub. cbn. right. apply in_map_iff. exists e. now split.
       + apply rewR with (x:=#::List.map sym (List.rev l++[e])) (u:= [state (cstate c1); $])
                       (v:=[state q2; $]). firstorder.
       + apply rewR with (x:=#::List.map sym (List.rev l++[e])) (u:= [state (cstate c1); $])
                       (v:=[state q2; $]). firstorder.
     - destruct (trans (cstate c1, Some e)) as (q2,(new,mov)) eqn: TC;
         assert (Sub: get_rules (cstate c1) q2 (Some e) new mov <<= TMrules)
         by (now apply get_rules_el_TMrules). destruct new as [new| ]; destruct mov; cbn.
       + destruct l; cbn.
         * apply rewR with (x:=[]) (u:= [#; state (cstate c1) ; sym e]) (v:=[state q2; #; sym new]).
           firstorder.
         * rewrite map_app. rewrite <- app_assoc.
           apply rewR with (x:=#::List.map sym (List.rev l))
                           (u:= [sym e0; state (cstate c1) ; sym e])
                           (v:=[state q2; sym e0; sym new]).
           apply Sub. cbn. right. apply in_map_iff. exists e0. now split.
       + destruct l0; cbn.
         * rewrite map_app. rewrite <- app_assoc.
           apply rewR with (x:= # :: List.map sym (List.rev l))
                           (u:= [state (cstate c1) ; sym e]) (y:=[$])
                           (v:=[sym new; state q2]). firstorder.
         * rewrite map_app. rewrite <- app_assoc.
           apply rewR with (x:=#::List.map sym (List.rev l))
                           (u:= [state (cstate c1) ; sym e])
                           (v:=[sym new; state q2]). firstorder.
       + apply rewR with (x:=# :: List.map sym (List.rev l)) (u:= [state (cstate c1); sym e])
                         (v:=[state q2; sym new]). firstorder.
       + destruct l; cbn.
         * apply rewR with (x:=[])
                           (u:= [#;state (cstate c1) ; sym e])
                           (v:=[state q2; #; sym e]). firstorder.
         * rewrite map_app. rewrite <- app_assoc.
           apply rewR with (x:=#::List.map sym (List.rev l))
                           (u:= [sym e0; state (cstate c1) ; sym e])
                           (v:=[state q2; sym e0; sym e]).
           apply Sub. cbn. right. apply in_map_iff. exists e0. now split.
       + destruct l0; cbn.
         * rewrite map_app. rewrite <- app_assoc.
            apply rewR with (x:=# :: List.map sym (List.rev l))
                            (u:= [state (cstate c1) ; sym e])
                            (v:=[sym e; state q2]). firstorder.
         * rewrite map_app. rewrite <- app_assoc.
           apply rewR with (x:=#::List.map sym (List.rev l))
                           (u:= [state (cstate c1) ; sym e])
                           (v:=[sym e; state q2]). firstorder.
       + apply rewR with (x:=# :: List.map sym (List.rev l))
                         (u:= [state (cstate c1); sym e])
                       (v:=[state q2; sym e]). firstorder.
  Qed.

  Lemma state_eqlist A B C D q1 q2:
    A ++(state q1)::B = C++(state q2)::D
    -> (exists (E F: list rsig'), C = List.map symb E /\ D = List.map symb F)
    -> A = C /\ B = D /\ q1 = q2.
  Proof.
    revert C. induction A; intros C H HA; destruct C; try rewrite !app_nil_l in H.
    - inv H. now split.
    - inv H. destruct HA as [E [F [H1 H2]]]. destruct E; inv H1.
    - rewrite <- app_comm_cons in H. inv H. destruct HA as [E [F [H1 H2]]].
      exfalso. assert ((state q1) el (A++(state q1)::B) -> False). intros H.
      rewrite H2 in H. apply in_map_iff in H as [x [? ?]]. inv H. apply H. auto.
    - inv H. specialize (IHA C H2). destruct HA as [E [F [H3 H4]]]. destruct E,F.
      inv H3. inv H3. cbn in H3. inv H3. destruct IHA as [<- [<- <-]]. exists E, []. now split.
      now split. cbn in H3. inv H3. destruct IHA as [<- [<- <-]]. exists E, (r1::F). now split.
      now split.
  Qed.

  Fact map_symb_sigma A :
    List.map symb (List.map sigma A) = List.map sym A.
  Proof.
    induction A. auto. cbn. now rewrite <- IHA.
  Qed.

  (* Automation for rewrite_step_halt Lemma. ListInv mainly eliminates contradictory
     assumptions while state_inv also solves cases *)

  Ltac listInv :=
    cbn in *;
    match goal with
    | [H: sym _ = sym _ |- _ ] => inv H
    | [H: [] = _ ::_ |- _ ] => inv H
    | [H: _::_ = _::_ |- _ ] => inv H
    | [H: []++ _ = _ |- _ ] => rewrite app_nil_l in H
    | [H: _ ++[] = _ |- _ ] => rewrite app_nil_r in H
    | [H: _ = []++ _ |- _ ] => rewrite app_nil_l in H
    | [H: _ = _ ++[] |- _ ] => rewrite app_nil_r in H
    | [H: [] = List.map sym ?L |- _ ] => destruct L eqn: ?
    | [H: List.rev ?L = [] |- _] => apply rev_nil in H
    | [H: _ ++ _::_ = [] |- _ ] => symmetry in H; now apply app_cons_not_nil in H
    | [H: [] = List.map _ (List.rev (_) ++ ?e) |- _ ] =>
      apply map_app in H; now apply app_cons_not_nil in H
    | [H: _ ++ [#] = List.map sym (List.rev _ ++ ?e) |- _ ] =>
      rewrite map_app in H; let E:= fresh "E" in apply last_app_eq in H as [_ E]; inv E
    | [H: ?x ++ [_] = #::(List.map sym ?L) |- _ ] => destruct x eqn: ?
    | [H: _ ++ [#] = List.map sym (List.rev ?L) |- _ ] => destruct L eqn: ?
    | [H: _ ++ [sym _] = List.map sym (List.rev ?L) |- _ ] => destruct L eqn:?
    | [H: _ ++ [sym _] = List.map sym (_ ++ [_]) |- _ ] =>
      rewrite map_app in H; apply last_app_eq in H as [? ?]
    | [H: ?A ++ _::_ = _::_ |- _ ] => destruct A eqn: ?
    end; subst.
  Ltac rep_listInv := repeat listInv.

  Ltac confeq :=
    unfold step; unfold mk_srconf;
    match goal with
      | [ |- (_::_ = _::_) /\ _ ] => split
      | [ |- (_::_ = _::_)] => reflexivity
      | [H: ctape _ = _ |- (_ = _) /\ _ ] => rewrite H
      | [H: trans(_,_) = _ |- _ ] => rewrite H
      | [H: _ |- mk_mconfig _ _ = mk_mconfig _ _ /\ _ ] => split
      | [ |- mk_mconfig _ _ = mk_mconfig _ _ ] => reflexivity
      | [H: (?q,_) el list_prod not_halting_states _ |- halt ?q = false ] =>
        apply in_prod_iff in H as [? _]; now apply not_halting
      | [H: _ el not_halting_states |- halt _ = false] => now apply not_halting
        end; subst; cbn in *; try now rewrite !map_app, <- !app_assoc.
  Ltac rep_confeq := repeat confeq.

  Ltac state_inv :=
    unfold get_rules_right in *;
    match goal with
    |[H: ?x ++ ?z::(state ?q)::?y = ?a::(?A++(state _ )::_) |- _] =>
     cbn in H; change (x++z::state q::y) with (x++[z]++(state q)::y) in H; rewrite app_assoc in H;
     rewrite app_comm_cons in H; eapply state_eqlist in H as [? [? ?]]
|[H: ?x ++ state _ :: ?y = state _ ::_ |- _ = _ /\ _ ] =>
     apply state_eqlist with (A:= x) (B:= y) (C:= []) in H as [? [? ?]]
|[H: ?x ++ ?z::state ?q :: ?y = state _ ::_ |- _ = _ /\ _ ] =>
     change (x++z::state q::y) with (x++[z]++state q::y) in H; rewrite app_assoc in H;
     apply state_eqlist with (A:=x++[z]) (B:= y) (C:= []) in H as [? [? ?]]
|[H: ?x ++(state _ )::?y = ?a::(?A ++ (state _ )::_) |- _ ] =>
     cbn in H; rewrite app_comm_cons in H; eapply state_eqlist in H as [? [? ?]]
|[H: _::_ = _::_ |- _ ] => inv H
    |[H: (_,_) el List.map _ _ |- (_ = _) /\ _] => apply in_map_iff in H as [? [? ?]]
|[H: (_,_) = (_,_) |- _ ] => inv H
    |[H: _ |- exists E F, [] = _ /\ [#;$] = _ ] => exists [],[hash; dollar]; now split
    |[H: _ |- exists E F, [] = _ /\ #::sym ?e::List.map sym ?L++[$] = _ ] =>
     exists [],(hash::sigma e::List.map sigma L++[dollar]); split; auto; cbn;
     rewrite map_app, map_symb_sigma; now cbn
    |[H: _ |- exists E F, #::(List.map sym ?A) = _ /\ [$] = _ ] =>
     exists (hash::(List.map sigma A)), [dollar]; split; auto; cbn;
     rewrite !map_app, map_symb_sigma; now cbn
    |[H: _ |- exists E F, #::(List.map sym ?A) = _ /\ sym ?e::(List.map sym ?L)++[$] = _ ] =>
     exists (hash::(List.map sigma A)), (sigma e::(List.map sigma L)++[dollar]);
     split; cbn; try rewrite map_app; now rewrite map_symb_sigma
    end.

  Ltac solve_inv := repeat (state_inv || confeq || listInv).

  Lemma rewrite_step_halt (c1: conf) y:
    rew TMrules (mk_srconf c1) y -> (y = (mk_srconf (step c1)) /\ (halt (cstate c1) = false)).
  Proof.
    intros H. remember (mk_srconf c1) as a. inv H.
    apply in_concat_iff in H0 as [L [EL HL]]. unfold mk_srconf in H2.
    destruct (ctape c1) eqn: CT1; cbn in *; apply in_app_iff in HL as [HL|HL];
      try apply in_map_iff in HL as [z [HZ ZF]]; try (destruct z as (q1, old));
        try (destruct (trans(z,None)) as (qz,(o,m)) eqn: TZ +
            destruct (trans (q1, Some old)) as (q2, (o, m)) eqn: TZ);
        destruct o as [new| ]; destruct m; cbn in HZ; subst; destruct EL;
          try apply in_sing in H; try inv H; solve_inv; destruct l0; cbn; rep_confeq.
  Qed.

  Theorem reach_rewrite (c1 c2:conf):
    reach c1 c2 <-> rewt TMrules (mk_srconf c1) (mk_srconf c2).
  Proof.
    split.
    - induction 1. constructor. apply rewtRule with (y:=(mk_srconf (step c))).
      + now apply rewrite_step_conf.
      + assumption.
    - remember (mk_srconf c1) as y. remember (mk_srconf c2) as b.
       intros H. revert Heqy. revert c1. induction H; intros c1 Heqy; subst.
       + apply mk_srconf_inj in Heqy. subst. constructor.
       + apply rewrite_step_halt in H as [H1 H]. subst.
         apply reachS. apply IHrewt; auto. assumption.
  Qed.

  Definition reduction_reach_rewrite (p: conf * conf) :=
      let (c1,c2) := p in (TMrules, mk_srconf c1, mk_srconf c2).

    Section abstract_epsilon.
    Variable gam: finType.
    Variable fin: list gam.

    Definition get_rule_l (f: gam) (r: gam) := ([r;f],[f]).
    Definition get_rule_r (f: gam) (r: gam) := ([f;r],[f]).
    Definition get_rule_fin (f: gam) : rule gam := ([f],[]).

    Definition del_rules_l : srs gam:=
      List.map (fun (P: (gam * gam)) => let (f, s) := P
                                     in get_rule_l f s) (list_prod fin (elem gam)).

    Definition del_rules_r : srs gam :=
      List.map (fun (P: (gam * gam)) => let (f, s) := P
                                     in get_rule_r f s) (list_prod fin (elem gam)).

    Definition del_rules_fin : srs gam := List.map get_rule_fin fin.
    Definition Drules := del_rules_r ++ del_rules_l ++ del_rules_fin.

    Lemma del_rule_r_el q r: q el fin -> get_rule_r q r el Drules.
    Proof.
      intros HT. apply in_app_iff. left. apply in_map_iff.
      exists (q,r). split. auto. apply in_prod_iff. auto.
    Qed.

    Lemma del_rule_l_el q r: q el fin -> get_rule_l q r el Drules.
    Proof.
      intros HT. apply in_app_iff. right. apply in_app_iff. left.
      apply in_map_iff. exists (q,r). split. auto. apply in_prod_iff. auto.
    Qed.

    Lemma del_rule_fin_el q: q el fin -> get_rule_fin q el Drules.
    Proof.
      intros HT. apply in_app_iff. right. apply in_app_iff. right.
      apply in_map_iff. exists q. now split.
    Qed.

    Lemma delete_list_right (A B: list gam) q:
      q el fin -> rewt Drules (A++q::B) (A++[q]).
    Proof.
      intros Hq. induction B.
      - constructor.
      - apply rewtRule with (y:= (A++q::B)).
        + eapply rewR with (x:=A) (u:= [q;a]) (v:=[q]). apply in_app_iff.
          left. apply in_map_iff. exists (q,a). split. auto. apply in_prod_iff. now split.
        + assumption.
    Qed.

    Lemma delete_list_left (A B: list gam) q:
      q el fin -> rewt Drules (A++q::B) (q::B).
    Proof.
      intros Hq. pattern A. apply (@size_induction (list gam) (@length gam)).
      intros C IH. replace C with (rev (rev C)) by (apply rev_involutive).
      remember (rev C) as D. destruct D; cbn. constructor.
      rewrite <- app_assoc. change ((rev D)++[e]++q::B) with (rev D++([e;q])++B).
      apply rewtRule with (y:= (rev D++q::B)).
      apply rewR with (x:=rev D) (u:= [e;q]) (v:=[q]). apply in_app_iff. right.
      apply in_app_iff. left. apply in_map_iff. exists (q,e). split. auto. apply in_prod_iff.
      now split. apply IH. destruct C. inv HeqD. rewrite rev_length.
      setoid_rewrite <- rev_length at 2. rewrite <- HeqD. cbn. omega.
    Qed.

    Lemma delete_fin q:
      q el fin -> rewt Drules [q] [].
    Proof.
      intros HF. apply rewtRule with (y:=[]).
        + eapply rewR with (x:=[]) (y:=[]) (u:=[q]) (v:=[]). now apply del_rule_fin_el.
        + constructor.
    Qed.

    Theorem fin_rewrite_nil (A: list gam) q:
      q el fin -> q el A -> rewt Drules A [].
    Proof.
      intros QF QA. apply in_split in QA as [a1 [a2 HA]].
      destruct a1, a2; try rewrite app_nil_l in HA; subst.
      - now apply delete_fin.
      - apply rewtTrans with (y:=[q]). now apply delete_list_right with (A:=[]).
        now apply delete_fin.
      - apply rewtTrans with (y:=[q]). now apply delete_list_left.
        now apply delete_fin.
      - apply rewtTrans with (y:=q::e0::a2).
        + now apply delete_list_left.
        + apply rewtTrans with (y:=[q]).
          * now apply delete_list_right with (A:=[]).
          * now apply delete_fin.
    Qed.

    Lemma rewrite_drules (A B: list gam) :
      rew Drules A B -> exists q, q el fin /\ q el A.
    Proof.
      inversion 1. apply in_app_iff in H0 as [B1|[B2|B3]%in_app_iff].
      - unfold del_rules_r in B1. apply in_map_iff in B1 as [[q s] [B1 B2]].
        inv B1. apply in_prod_iff in B2 as [B4 B5]. exists q. split; auto.
      - unfold del_rules_l in B2. apply in_map_iff in B2 as [[q s] [B1 B2]].
        inv B1. apply in_prod_iff in B2 as [B2 B3]. exists q. split; auto.
        apply in_app_iff. right. auto.
      - unfold del_rules_fin in B3. apply in_map_iff in B3 as [q [B5 B4]].
        inv B5. exists q. split; auto.
    Qed.

    End abstract_epsilon.

  Definition delRules := (Drules (List.map (fun s => state s) halting_states)).

  Theorem reach_rewrite_nil (c: conf):
     halt (cstate c) = true -> rewt delRules (mk_srconf c) [].
   Proof.
     intros H. apply fin_rewrite_nil with (q:= (state (cstate c))).
     apply in_map_iff. exists (cstate c). split. auto. now apply halting.
     unfold mk_srconf. destruct (ctape c); try (now left); apply in_app_iff.
     - right. apply in_app_iff. right. now left.
     - right. apply in_app_iff. right. apply in_app_iff. left. now left.
   Qed.

  Lemma mk_srconf_not_nil (con: conf):
    (mk_srconf con) <> [].
  Proof.
    unfold mk_srconf. destruct (ctape con); inversion 1.
  Qed.

  Lemma rew_delRules_halt c A:
    rew delRules (mk_srconf c) A -> halt (cstate c) = true.
   Proof.
     intros H. apply rewrite_drules in H as [q [H1 H2]]. unfold mk_srconf in H2.
     apply in_map_iff in H1 as [a [H4 H3]]. subst. destruct (ctape c).
     - inv H2. inv H. now apply halting. repeat (inv H; inv H0).
     - inv H2. inv H. now apply halting. repeat inv H; inv H0. inv H.
       apply in_app_iff in H as [H|H]. apply in_map_iff in H as [x [M N]]. inv M.
       apply in_sing in H. inv H.
     - repeat (apply in_app_iff in H2 as [H2|H2]).
       + apply in_sing in H2. inv H2.
       + apply in_map_iff in H2 as [x [M _]]. inv M.
       + inv H2. inv H. now apply halting. apply in_sing in H. inv H.
     - repeat (apply in_app_iff in H2 as [H2|H2]).
       + apply in_sing in H2. inv H2.
       + apply in_map_iff in H2 as [x [M _]]. inv M.
       + apply in_sing in H2. inv H2. now apply halting.
       + apply in_map_iff in H2 as [x [M _]]. inv M.
       + apply in_sing in H2. inv H2.
   Qed.

  Theorem rewrite_nil (c:conf):
    rewt (TMrules++delRules) (mk_srconf c) [] -> exists c1, reach c c1 /\ (halt (cstate c1) = true).
  Proof.
    remember (mk_srconf c) as y. remember [] as b. intros H. revert Heqy.
    revert c. induction H; intros c Heqc; subst.
    - exfalso. symmetry in Heqc. now apply mk_srconf_not_nil in Heqc.
    - remember (mk_srconf c) as a. assert (H' := H). inv H. apply in_app_iff in H1 as [H1|H1].
      + assert (rew TMrules (mk_srconf c) (x++v++y0)) as HR.
        { rewrite <- H3. now apply rewR with (x:=x) (u:=u). }
        apply rewrite_step_halt in HR as [HR1 HR2].
        destruct (IHrewt (eq_refl) (step c) HR1) as [c1 [RC HC]].
        exists c1. split. apply reachS; assumption. assumption.
      + assert (rew delRules (x++u++y0) (x++v++y0)) as HD.
        { now apply rewR with (x:=x) (u:=u) (v:=v). }
        rewrite H3 in HD. apply rew_delRules_halt in HD. exists c. split. constructor. assumption.
  Qed.

  Definition tm_srs_reduction (c: conf) : ((srs rsig * (list rsig)) * (list rsig)):=
    (TMrules ++ delRules, mk_srconf c, []).

  Theorem halt_iff_rewriting (c: conf) :
    (exists f :conf , halt (cstate f) = true /\ reach c f) <->
    rewt (TMrules ++ delRules) (mk_srconf c) [].
  Proof.
    split.
    - intros [fin [H1 H2]]. apply rewtTrans with (y:= mk_srconf fin).
      + assert (rewt TMrules (mk_srconf c) (mk_srconf fin)).
        apply (reach_rewrite c fin). assumption.
        apply (@subset_rewriting rsig TMrules). auto. assumption.
      + apply (@subset_rewriting rsig delRules). auto. now apply reach_rewrite_nil.
    - intros HR. apply rewrite_nil in HR as [c2 [H1 H2]]. exists c2. now split.
  Qed.

End Fix_TM.

Theorem reduction_reach_sr : red Reach SR.
Proof. unfold red. exists (fun S
                      => existT (fun (sig:finType) => (prod (prod (srs sig) (list sig)) (list sig)))
                               (rsig_finType (projT1 (projT2 S)))
                               (reduction_reach_rewrite (projT2 (projT2 S)))).
       intros [sig [M [c1 c2]]]. unfold Reach, SR. cbn. apply reach_rewrite.
Qed.

Theorem reduction_halt_sr : red HaltD SR.
Proof.
  unfold red. exists (fun (S: {sig : finType & sTM sig & tape sig})
                 => existT (fun (sig:finType) => (prod (prod (srs sig) (list sig)) (list sig)))
                          (rsig_finType (projT2 (sigT_of_sigT2 S)))
                          (tm_srs_reduction (initc (projT2 (sigT_of_sigT2 S)) (projT3 S)))).
  intros [sig [M con]]. unfold HaltD, SR. cbn. apply halt_iff_rewriting.
Qed.