Require Import List Lia.
Require Import Undecidability.TM.SBTM.
Require Undecidability.StringRewriting.SR.
Require Import Undecidability.StringRewriting.Util.Definitions.
Require Import Undecidability.Synthetic.Definitions.
Require Import Undecidability.Synthetic.ReducibilityFacts.
Import ListNotations.
Set Default Proof Using "Type".
Lemma nil_app_tail {X} (x : X) l : ~ [] = l ++ [x]. Proof. destruct l; cbn; firstorder congruence. Qed.
Lemma nil_app_tail' {X} (x : X) l : ~ l ++ [x] = []. Proof. destruct l; cbn; firstorder congruence. Qed.
Definition SRH' '(Rs, x, A) := exists y : list nat, SR.rewt Rs x y /\ exists a, In a A /\ In a y.
Section FixM.
Variable M : SBTM.
Notation X := 1.
Notation "⦇" := 2.
Notation "⦈" := 3.
Notation tt := 4.
Notation ff := 5.
Notation "!! b" := (if b then tt else ff) (at level 1).
Definition enc_state (q : Fin.t (S (num_states M))) := ((S ff) + proj1_sig (Fin.to_nat q)).
Notation "! p" := (enc_state p) (at level 1).
Fixpoint all_fins (n : nat) : list (Fin.t n) :=
match n with
| 0 => nil
| S n => Fin.F1 :: map Fin.FS (all_fins n)
end.
Lemma in_all_fins n i :
In i (all_fins n).
Proof.
induction i.
- cbn. eauto.
- cbn. right. eapply in_map_iff. eauto.
Qed.
Definition all_states {B} f : list B := flat_map f (all_fins (S (num_states M))).
Definition all_syms {B} f : list B := [f tt ; f ff].
Definition encode_sym (o : option bool) := match o with None => X | Some true => tt | Some false => ff end.
Definition encode_trans (c : option (state M * option bool * move)) (q : Fin.t (S (num_states M))) : option (nat * nat * nat * move) :=
option_map (fun '(s,o,m) => (!q, !s, encode_sym o, m)) c.
Definition rules q₁ : list (list nat * list nat):=
match encode_trans (trans M (q₁, None)) q₁ with
| Some (q₁, q₂, X, Lmove) => all_syms (fun l => ([l;q₁;X], [q₂;l])) ++ [([⦇;q₁;X],[⦇;q₂;X])]
| Some (q₁, q₂, X, Nmove) => [([q₁;X], [q₂;X])]
| Some (q₁, q₂, X, Rmove) => all_syms (fun r => ([q₁;X;r], [q₂;r])) ++ [([q₁;X;⦈],[q₂;X;⦈])]
| Some (q₁, q₂, c, Lmove) => all_syms (fun l => ([l;q₁;X], [q₂;l;c])) ++ [([⦇;q₁;X],[⦇;q₂;X;c])]
| Some (q₁, q₂, c, Nmove) => [([q₁;X], [q₂;c])]
| Some (q₁, q₂, c, Rmove) => all_syms (fun r => ([q₁;X;r], [c;q₂;r])) ++ [([q₁;X;⦈],[c;q₂;X;⦈])]
| None => []
end ++
let a := tt in
match encode_trans (trans M (q₁, Some true)) q₁ with
| Some (q₁, q₂, X, Lmove) => all_syms (fun l => ([l;q₁;a], [q₂;l;a])) ++ [([⦇;q₁;a],[⦇;q₂;X;a])]
| Some (q₁, q₂, X, Nmove) => [([q₁;a], [q₂;a])]
| Some (q₁, q₂, X, Rmove) => all_syms (fun r => ([q₁;a;r], [a;q₂;r])) ++ [([q₁;a;⦈],[a;q₂;X;⦈])]
| Some (q₁, q₂, c, Lmove) => all_syms (fun l => ([l;q₁;a], [q₂;l;c])) ++ [([⦇;q₁;a],[⦇;q₂;X;c])]
| Some (q₁, q₂, c, Rmove) => all_syms (fun r => ([q₁;a;r], [c;q₂;r])) ++ [([q₁;a;⦈],[c;q₂;X;⦈])]
| Some (q₁, q₂, c, Nmove) => [([q₁;a], [q₂;c])]
| None => []
end ++
let a := ff in
match encode_trans (trans M (q₁, Some false)) q₁ with
| Some (q₁, q₂, X, Lmove) => all_syms (fun l => ([l;q₁;a], [q₂;l;a])) ++ [([⦇;q₁;a],[⦇;q₂;X;a])]
| Some (q₁, q₂, X, Rmove) => all_syms (fun r => ([q₁;a;r], [a;q₂;r])) ++ [([q₁;a;⦈],[a;q₂;X;⦈])]
| Some (q₁, q₂, X, Nmove) => [([q₁;a], [q₂;a])]
| Some (q₁, q₂, c, Lmove) => all_syms (fun l => ([l;q₁;a], [q₂;l;c])) ++ [([⦇;q₁;a],[⦇;q₂;X;c])]
| Some (q₁, q₂, c, Rmove) => all_syms (fun r => ([q₁;a;r], [c;q₂;r])) ++ [([q₁;a;⦈],[c;q₂;X;⦈])]
| Some (q₁, q₂, c, Nmove) => [([q₁;a], [q₂;c])]
| None => []
end.
Definition R : SR.SRS nat := all_states rules.
Lemma rules_incl q :
incl (rules q) R.
Proof.
unfold R, all_states.
intros r Hr.
eapply in_flat_map.
exists q. split; [ | assumption].
eapply in_all_fins.
Qed.
Definition enc_conf '(ls, o, rs) (q : Fin.t (S (num_states M))) : list nat :=
[⦇] ++ map (fun b : bool => !!b) (rev ls) ++ [!q] ++ [encode_sym o] ++ map (fun b : bool => !!b) rs ++ [⦈].
Lemma simulation q1 q2 t1 t2 :
eval M q1 t1 q2 t2 -> SR.rewt R (enc_conf t1 q1) (enc_conf t2 q2).
Proof.
induction 1.
- econstructor.
- econstructor. 2:eassumption. clear - H.
destruct t as [[ls o] rs]. cbn in H.
eapply rew_subset with (2 := @rules_incl q).
unfold rules.
destruct o as [ [] | ] eqn:Eo; rewrite H; clear H.
1: eapply rew_subset; [ | eapply incl_appr, incl_appl, incl_refl ].
2: eapply rew_subset; [ | eapply incl_appr, incl_appr, incl_refl ].
3: eapply rew_subset; [ | eapply incl_appl, incl_refl ].
all:destruct w as [[] | ] eqn:Ew, m eqn:Em; cbn -[Nat.add].
all:try match goal with [ |- context[enc_conf match ?l with _ => _ end]] => destruct l as [ | [] ] eqn:El end; cbn -[Nat.add].
all: rewrite ?map_app; cbn [map app].
all:unfold all_syms.
Ltac inst_left := match goal with [ |- ?L = ?R ] =>
match L with
context C [?x1 :: ?x2 :: ?x3 :: ?r] => let t := context C [@nil nat] in instantiate (2 := t)
| context C [?x1 :: ?x2 :: ?r] => let t := context C [@nil nat] in instantiate (2 := t)
end
end.
Ltac help1 := cbn -[Nat.add]; simpl_list; cbn -[Nat.add];inst_left; cbn; now simpl_list.
Ltac help2 := cbn -[Nat.add]; now simpl_list.
all: eapply do_rew; [ (now left + (right; now left) + (right; right; now left) + (right; right; right; now left)) | help1 | help2].
Qed.
Lemma enc_conf_inv' xs q ys ls o rs q' :
xs ++ !q ++ ys = enc_conf (ls, o, rs) q' ->
xs = [⦇] ++ map (fun b : bool => !!b) (rev ls) /\
q = q' /\
ys = encode_sym o :: map (fun b : bool => !!b) rs ++ [⦈].
Proof.
intros. pose proof (H' := H). cbn - [Nat.add] in H.
destruct xs; cbn -[Nat.add] in H; inversion H; subst n; clear H.
eapply list_prefix_inv' in H2 as (H1 & -> & H3).
- subst. repeat split. eapply Fin.to_nat_inj. unfold "!" in H1. lia.
- clear H'. induction xs in ls, H2 |- *.
+ firstorder.
+ cbn -[Nat.add]. destruct ls as [ | ? ? _] using rev_ind.
* cbn -[Nat.add] in H2. inversion H2. subst. destruct xs; inversion H1; subst.
destruct o as [ [] | ]; cbn in H0; lia.
assert (In (!q) (map (fun b : bool => !! b) rs ++ [⦈])). rewrite <- H3. rewrite in_app_iff. cbn[In]. solve [eauto].
eapply in_app_iff in H as [ (? & ? & ?) % in_map_iff | [ | []]]; try destruct x; cbn in H; lia.
* rewrite rev_app_distr in H2. cbn -[Nat.add] in H2. inversion H2; subst.
intros [ | ].
-- destruct x; cbn in *; lia.
-- eapply IHxs. 2:eauto. rewrite H1. reflexivity.
- intros (? & ? & ?) % in_map_iff. destruct x; cbn in *; lia.
Qed.
Lemma enc_state_inv q t q' :
In (enc_state q) (enc_conf t q') -> q = q'.
Proof.
destruct t as [[ls o] rs].
now intros (xs & ys & (-> & -> & ->) % eq_sym % enc_conf_inv') % in_split.
Qed.
Lemma enc_conf_inv xs q c ys ls o rs q' :
xs ++ !q ++ [c] ++ ys = enc_conf (ls, o, rs) q' ->
xs = [⦇] ++ map (fun b : bool => !!b) (rev ls) /\
q = q' /\
c = encode_sym o /\
ys = map (fun b : bool => !!b) rs ++ [⦈].
Proof.
intros. eapply enc_conf_inv' in H as (-> & -> & [= -> ->]). eauto.
Qed.
Lemma rev_sim t q z :
SR.rew R (enc_conf t q) z -> exists q' w m, trans M (q, curr t) = Some (q', w, m) /\ z = enc_conf (mv m (wr w t)) q'.
Proof.
intros H. inversion H as [x y u v Hin HL HR]; subst z.
destruct t as [[ls o] rs].
eapply in_flat_map in Hin as (q_ & _ & Hq2).
unfold rules in Hq2.
rewrite ! in_app_iff in Hq2.
destruct Hq2 as [ Hq2 | [Hq2 | Hq2]].
all: destruct (trans M (q_, _)) as [ [[q' w] m] | ] eqn:Etrans; try destruct m eqn:Em;
try destruct w as [[] | ] eqn:Ew; cbn -[Nat.add] in Hq2; (exists q', w, m || exfalso); rewrite ?Em, ?Ew.
all: repeat match type of Hq2 with _ \/ _ => destruct Hq2 as [Hq2 | Hq2] end; inversion Hq2; subst u v; clear Hq2; cbn -[Nat.add].
cbn [app] in HL.
all:
cbn [app] in HL;
match type of HL with
| ?L = ?R => match L with context C [! ?q :: ?c :: ?rs] => let ls := context C [@nil nat] in
replace L with (ls ++ !q ++ [c] ++ rs) in HL; [ | cbn; now simpl_list]
end
end.
all:
match type of HL with _ = enc_conf (?ls,?o,?rs) ?q =>
let H1 := fresh "H" in let H2 := fresh "H" in let H3 := fresh "H" in let H4 := fresh "H" in let HH := fresh "H" in
eapply enc_conf_inv in HL as (H1 & -> & H3 & H4); try rewrite H4 in *; destruct o as [ [] | ]; inversion H3; clear H3; cbn in H1;
rewrite ?app_nil_r in H1; subst;
split ; try eassumption; try reflexivity;
(let x := match type of H1 with ?x ++ _ = _ => x end in
destruct x; try (now inversion H1); cbn in H1; eapply cons_inj in H1 as [HH H1]; try rewrite HH in *; clear HH;
now destruct ls as [ | []]; cbn in H1;
[ reflexivity || destruct x; now inversion H1 | try rewrite map_app in H1; cbn in H1; (eapply app_inj_tail in H1 as [-> [=]] + (try eapply nil_app_tail in H1 as []) + (try eapply nil_app_tail' in H1 as []) ).. ])
+ (destruct rs as [ | [] rs]; cbn in H4; eapply cons_inj in H4 as [ [=] H4]; rewrite ?H4 in *; clear H4;
now cbn; simpl_list)
end.
Qed.
End FixM.
Lemma reduction :
HaltSBTMu ⪯ SR.SRH.
Proof.
unshelve eexists. { intros [(M & q & H) t]. exact (R M, @enc_conf M t Fin.F1, enc_state M q). }
intros [(M & q & Hq) t]. split.
- cbn -[enc_state]. intros (t' & H).
exists (enc_conf M t' q). split.
+ now eapply simulation.
+ destruct t' as [[ls o] rs].
cbn -[Nat.add]. right. rewrite !in_app_iff. cbn; eauto.
- cbn -[R Nat.add]. intros (x & H1 & H2). revert H1.
generalize (@Fin.F1 (num_states M)). intros q1 H.
revert q Hq H2. remember (enc_conf M t q1) as y.
induction H in q1, Heqy, t |- *; subst; intros q Hq H2.
+ exists t. eapply enc_state_inv in H2. subst. econstructor. eapply Hq.
+ eapply rev_sim in H as (q' & w & m & H1 & H3). subst.
edestruct IHrewt as (H4 & H5); [reflexivity | eauto | eauto |].
eexists. econstructor. 2:eassumption. eassumption.
Qed.
Require Import Undecidability.TM.SBTM.
Require Undecidability.StringRewriting.SR.
Require Import Undecidability.StringRewriting.Util.Definitions.
Require Import Undecidability.Synthetic.Definitions.
Require Import Undecidability.Synthetic.ReducibilityFacts.
Import ListNotations.
Set Default Proof Using "Type".
Lemma nil_app_tail {X} (x : X) l : ~ [] = l ++ [x]. Proof. destruct l; cbn; firstorder congruence. Qed.
Lemma nil_app_tail' {X} (x : X) l : ~ l ++ [x] = []. Proof. destruct l; cbn; firstorder congruence. Qed.
Definition SRH' '(Rs, x, A) := exists y : list nat, SR.rewt Rs x y /\ exists a, In a A /\ In a y.
Section FixM.
Variable M : SBTM.
Notation X := 1.
Notation "⦇" := 2.
Notation "⦈" := 3.
Notation tt := 4.
Notation ff := 5.
Notation "!! b" := (if b then tt else ff) (at level 1).
Definition enc_state (q : Fin.t (S (num_states M))) := ((S ff) + proj1_sig (Fin.to_nat q)).
Notation "! p" := (enc_state p) (at level 1).
Fixpoint all_fins (n : nat) : list (Fin.t n) :=
match n with
| 0 => nil
| S n => Fin.F1 :: map Fin.FS (all_fins n)
end.
Lemma in_all_fins n i :
In i (all_fins n).
Proof.
induction i.
- cbn. eauto.
- cbn. right. eapply in_map_iff. eauto.
Qed.
Definition all_states {B} f : list B := flat_map f (all_fins (S (num_states M))).
Definition all_syms {B} f : list B := [f tt ; f ff].
Definition encode_sym (o : option bool) := match o with None => X | Some true => tt | Some false => ff end.
Definition encode_trans (c : option (state M * option bool * move)) (q : Fin.t (S (num_states M))) : option (nat * nat * nat * move) :=
option_map (fun '(s,o,m) => (!q, !s, encode_sym o, m)) c.
Definition rules q₁ : list (list nat * list nat):=
match encode_trans (trans M (q₁, None)) q₁ with
| Some (q₁, q₂, X, Lmove) => all_syms (fun l => ([l;q₁;X], [q₂;l])) ++ [([⦇;q₁;X],[⦇;q₂;X])]
| Some (q₁, q₂, X, Nmove) => [([q₁;X], [q₂;X])]
| Some (q₁, q₂, X, Rmove) => all_syms (fun r => ([q₁;X;r], [q₂;r])) ++ [([q₁;X;⦈],[q₂;X;⦈])]
| Some (q₁, q₂, c, Lmove) => all_syms (fun l => ([l;q₁;X], [q₂;l;c])) ++ [([⦇;q₁;X],[⦇;q₂;X;c])]
| Some (q₁, q₂, c, Nmove) => [([q₁;X], [q₂;c])]
| Some (q₁, q₂, c, Rmove) => all_syms (fun r => ([q₁;X;r], [c;q₂;r])) ++ [([q₁;X;⦈],[c;q₂;X;⦈])]
| None => []
end ++
let a := tt in
match encode_trans (trans M (q₁, Some true)) q₁ with
| Some (q₁, q₂, X, Lmove) => all_syms (fun l => ([l;q₁;a], [q₂;l;a])) ++ [([⦇;q₁;a],[⦇;q₂;X;a])]
| Some (q₁, q₂, X, Nmove) => [([q₁;a], [q₂;a])]
| Some (q₁, q₂, X, Rmove) => all_syms (fun r => ([q₁;a;r], [a;q₂;r])) ++ [([q₁;a;⦈],[a;q₂;X;⦈])]
| Some (q₁, q₂, c, Lmove) => all_syms (fun l => ([l;q₁;a], [q₂;l;c])) ++ [([⦇;q₁;a],[⦇;q₂;X;c])]
| Some (q₁, q₂, c, Rmove) => all_syms (fun r => ([q₁;a;r], [c;q₂;r])) ++ [([q₁;a;⦈],[c;q₂;X;⦈])]
| Some (q₁, q₂, c, Nmove) => [([q₁;a], [q₂;c])]
| None => []
end ++
let a := ff in
match encode_trans (trans M (q₁, Some false)) q₁ with
| Some (q₁, q₂, X, Lmove) => all_syms (fun l => ([l;q₁;a], [q₂;l;a])) ++ [([⦇;q₁;a],[⦇;q₂;X;a])]
| Some (q₁, q₂, X, Rmove) => all_syms (fun r => ([q₁;a;r], [a;q₂;r])) ++ [([q₁;a;⦈],[a;q₂;X;⦈])]
| Some (q₁, q₂, X, Nmove) => [([q₁;a], [q₂;a])]
| Some (q₁, q₂, c, Lmove) => all_syms (fun l => ([l;q₁;a], [q₂;l;c])) ++ [([⦇;q₁;a],[⦇;q₂;X;c])]
| Some (q₁, q₂, c, Rmove) => all_syms (fun r => ([q₁;a;r], [c;q₂;r])) ++ [([q₁;a;⦈],[c;q₂;X;⦈])]
| Some (q₁, q₂, c, Nmove) => [([q₁;a], [q₂;c])]
| None => []
end.
Definition R : SR.SRS nat := all_states rules.
Lemma rules_incl q :
incl (rules q) R.
Proof.
unfold R, all_states.
intros r Hr.
eapply in_flat_map.
exists q. split; [ | assumption].
eapply in_all_fins.
Qed.
Definition enc_conf '(ls, o, rs) (q : Fin.t (S (num_states M))) : list nat :=
[⦇] ++ map (fun b : bool => !!b) (rev ls) ++ [!q] ++ [encode_sym o] ++ map (fun b : bool => !!b) rs ++ [⦈].
Lemma simulation q1 q2 t1 t2 :
eval M q1 t1 q2 t2 -> SR.rewt R (enc_conf t1 q1) (enc_conf t2 q2).
Proof.
induction 1.
- econstructor.
- econstructor. 2:eassumption. clear - H.
destruct t as [[ls o] rs]. cbn in H.
eapply rew_subset with (2 := @rules_incl q).
unfold rules.
destruct o as [ [] | ] eqn:Eo; rewrite H; clear H.
1: eapply rew_subset; [ | eapply incl_appr, incl_appl, incl_refl ].
2: eapply rew_subset; [ | eapply incl_appr, incl_appr, incl_refl ].
3: eapply rew_subset; [ | eapply incl_appl, incl_refl ].
all:destruct w as [[] | ] eqn:Ew, m eqn:Em; cbn -[Nat.add].
all:try match goal with [ |- context[enc_conf match ?l with _ => _ end]] => destruct l as [ | [] ] eqn:El end; cbn -[Nat.add].
all: rewrite ?map_app; cbn [map app].
all:unfold all_syms.
Ltac inst_left := match goal with [ |- ?L = ?R ] =>
match L with
context C [?x1 :: ?x2 :: ?x3 :: ?r] => let t := context C [@nil nat] in instantiate (2 := t)
| context C [?x1 :: ?x2 :: ?r] => let t := context C [@nil nat] in instantiate (2 := t)
end
end.
Ltac help1 := cbn -[Nat.add]; simpl_list; cbn -[Nat.add];inst_left; cbn; now simpl_list.
Ltac help2 := cbn -[Nat.add]; now simpl_list.
all: eapply do_rew; [ (now left + (right; now left) + (right; right; now left) + (right; right; right; now left)) | help1 | help2].
Qed.
Lemma enc_conf_inv' xs q ys ls o rs q' :
xs ++ !q ++ ys = enc_conf (ls, o, rs) q' ->
xs = [⦇] ++ map (fun b : bool => !!b) (rev ls) /\
q = q' /\
ys = encode_sym o :: map (fun b : bool => !!b) rs ++ [⦈].
Proof.
intros. pose proof (H' := H). cbn - [Nat.add] in H.
destruct xs; cbn -[Nat.add] in H; inversion H; subst n; clear H.
eapply list_prefix_inv' in H2 as (H1 & -> & H3).
- subst. repeat split. eapply Fin.to_nat_inj. unfold "!" in H1. lia.
- clear H'. induction xs in ls, H2 |- *.
+ firstorder.
+ cbn -[Nat.add]. destruct ls as [ | ? ? _] using rev_ind.
* cbn -[Nat.add] in H2. inversion H2. subst. destruct xs; inversion H1; subst.
destruct o as [ [] | ]; cbn in H0; lia.
assert (In (!q) (map (fun b : bool => !! b) rs ++ [⦈])). rewrite <- H3. rewrite in_app_iff. cbn[In]. solve [eauto].
eapply in_app_iff in H as [ (? & ? & ?) % in_map_iff | [ | []]]; try destruct x; cbn in H; lia.
* rewrite rev_app_distr in H2. cbn -[Nat.add] in H2. inversion H2; subst.
intros [ | ].
-- destruct x; cbn in *; lia.
-- eapply IHxs. 2:eauto. rewrite H1. reflexivity.
- intros (? & ? & ?) % in_map_iff. destruct x; cbn in *; lia.
Qed.
Lemma enc_state_inv q t q' :
In (enc_state q) (enc_conf t q') -> q = q'.
Proof.
destruct t as [[ls o] rs].
now intros (xs & ys & (-> & -> & ->) % eq_sym % enc_conf_inv') % in_split.
Qed.
Lemma enc_conf_inv xs q c ys ls o rs q' :
xs ++ !q ++ [c] ++ ys = enc_conf (ls, o, rs) q' ->
xs = [⦇] ++ map (fun b : bool => !!b) (rev ls) /\
q = q' /\
c = encode_sym o /\
ys = map (fun b : bool => !!b) rs ++ [⦈].
Proof.
intros. eapply enc_conf_inv' in H as (-> & -> & [= -> ->]). eauto.
Qed.
Lemma rev_sim t q z :
SR.rew R (enc_conf t q) z -> exists q' w m, trans M (q, curr t) = Some (q', w, m) /\ z = enc_conf (mv m (wr w t)) q'.
Proof.
intros H. inversion H as [x y u v Hin HL HR]; subst z.
destruct t as [[ls o] rs].
eapply in_flat_map in Hin as (q_ & _ & Hq2).
unfold rules in Hq2.
rewrite ! in_app_iff in Hq2.
destruct Hq2 as [ Hq2 | [Hq2 | Hq2]].
all: destruct (trans M (q_, _)) as [ [[q' w] m] | ] eqn:Etrans; try destruct m eqn:Em;
try destruct w as [[] | ] eqn:Ew; cbn -[Nat.add] in Hq2; (exists q', w, m || exfalso); rewrite ?Em, ?Ew.
all: repeat match type of Hq2 with _ \/ _ => destruct Hq2 as [Hq2 | Hq2] end; inversion Hq2; subst u v; clear Hq2; cbn -[Nat.add].
cbn [app] in HL.
all:
cbn [app] in HL;
match type of HL with
| ?L = ?R => match L with context C [! ?q :: ?c :: ?rs] => let ls := context C [@nil nat] in
replace L with (ls ++ !q ++ [c] ++ rs) in HL; [ | cbn; now simpl_list]
end
end.
all:
match type of HL with _ = enc_conf (?ls,?o,?rs) ?q =>
let H1 := fresh "H" in let H2 := fresh "H" in let H3 := fresh "H" in let H4 := fresh "H" in let HH := fresh "H" in
eapply enc_conf_inv in HL as (H1 & -> & H3 & H4); try rewrite H4 in *; destruct o as [ [] | ]; inversion H3; clear H3; cbn in H1;
rewrite ?app_nil_r in H1; subst;
split ; try eassumption; try reflexivity;
(let x := match type of H1 with ?x ++ _ = _ => x end in
destruct x; try (now inversion H1); cbn in H1; eapply cons_inj in H1 as [HH H1]; try rewrite HH in *; clear HH;
now destruct ls as [ | []]; cbn in H1;
[ reflexivity || destruct x; now inversion H1 | try rewrite map_app in H1; cbn in H1; (eapply app_inj_tail in H1 as [-> [=]] + (try eapply nil_app_tail in H1 as []) + (try eapply nil_app_tail' in H1 as []) ).. ])
+ (destruct rs as [ | [] rs]; cbn in H4; eapply cons_inj in H4 as [ [=] H4]; rewrite ?H4 in *; clear H4;
now cbn; simpl_list)
end.
Qed.
End FixM.
Lemma reduction :
HaltSBTMu ⪯ SR.SRH.
Proof.
unshelve eexists. { intros [(M & q & H) t]. exact (R M, @enc_conf M t Fin.F1, enc_state M q). }
intros [(M & q & Hq) t]. split.
- cbn -[enc_state]. intros (t' & H).
exists (enc_conf M t' q). split.
+ now eapply simulation.
+ destruct t' as [[ls o] rs].
cbn -[Nat.add]. right. rewrite !in_app_iff. cbn; eauto.
- cbn -[R Nat.add]. intros (x & H1 & H2). revert H1.
generalize (@Fin.F1 (num_states M)). intros q1 H.
revert q Hq H2. remember (enc_conf M t q1) as y.
induction H in q1, Heqy, t |- *; subst; intros q Hq H2.
+ exists t. eapply enc_state_inv in H2. subst. econstructor. eapply Hq.
+ eapply rev_sim in H as (q' & w & m & H1 & H3). subst.
edestruct IHrewt as (H4 & H5); [reflexivity | eauto | eauto |].
eexists. econstructor. 2:eassumption. eassumption.
Qed.