added MuRec_computable_to_MM_computable using existing MuRec to MM co…

…mpiler

theories/L/Reductions/MMA_HALTING_to_HaltLclosed.v

@@ -743,6 +743,6 @@ Proof.
         (sync P)
         L_facts.uniform_confluence
         (@sss_step_transport _ P)
-        (fun p => sss_step_or_stuck (@mma_sss_total_ni _) p 1 P)
+        (sss_step_or_stuck (@mma_sss_total_ni _) 1 P)
         (1, v) _ eq_refl Ht).
 Qed.

theories/L/Reductions/MMA_computable_to_L_computable_closed.v

@@ -203,7 +203,7 @@ Proof.
         move E: (apps _ _) => t H.
         elim: H i v E {H' Hi}.
         move=> {}t IH1 IH2 i v ?. subst t.
-        have [[[j w]]|] := sss_step_or_stuck (@mma_sss_total_ni _) (i, v) 1 P.
+        have [[[j w]]|] := sss_step_or_stuck (@mma_sss_total_ni _) 1 P (i, v).
         ** move=> /[dup] Hvw /enc_run_spec /=.
            move=> /(@t_steps_app_r _ _ (enc_nth (@Fin.F1 (k + n)))).
            move=> /[dup] /(@clos_trans_clos_refl_trans term) /eval_rt_steps_eval H' + /H'.
@@ -234,7 +234,7 @@ Proof.
       move E: (apps _ _) => t H.
       elim: H i v E {H'}.
       move=> {}t IH1 IH2 i v ?. subst t.
-      have [[[j w]]|] := sss_step_or_stuck (@mma_sss_total_ni _) (i, v) 1 P.
+      have [[[j w]]|] := sss_step_or_stuck (@mma_sss_total_ni _) 1 P (i, v).
       * move=> /enc_run_spec /=.
         move=> /(@t_steps_app_r _ _ (enc_nth (@Fin.F1 (k + n)))).
         move=> /[dup] /(@clos_trans_clos_refl_trans term) /eval_rt_steps_eval H' + /H'.

theories/MinskyMachines/MM/mm_defs.v

@@ -50,6 +50,12 @@ Section Minsky_Machine.
     * exists (j,v); constructor; auto.
     * exists (1+i,v[k/x]); constructor; auto.
   Qed.
+
+  Fact mm_sss_total_ni ii s :
+    exists t, ii // s -1> t.
+  Proof.
+    apply (ex_of_sig (mm_sss_total _ _)).
+  Qed.
 
   Fact mm_sss_INC_inv x i v j w : INC x // (i,v) -1> (j,w) -> j=1+i /\ w = v[(S (v#>x))/x].
   Proof. inversion 1; subst; auto. Qed.

theories/MinskyMachines/Reductions/MMA_computable_to_MMA_mon_computable.v

@@ -359,13 +359,6 @@ Proof.
   apply: sss_step_fun. by apply: mma_sss_fun.
 Qed.
 
-Lemma step1_intro s : (exists t, step1 s t) \/ (Sim.stuck step1 s).
-Proof.
-  have [|] := subcode.in_out_code_dec (fst s) (1, P).
-  - move=> /(in_code_step (@mma_sss_total_ni num_counters)) ?. by left.
-  - move=> /(out_code_iff (@mma_sss_total_ni num_counters)) ?. by right.
-Qed.
-
 Lemma simulation v v' w' c m :
   (1, P) // (1, 0 ## Vector.append v (Vector.const 0 k')) ->> (c, m ## (Vector.append v' w')) ->
   c < 1 \/ S (length P) <= c ->
@@ -398,6 +391,6 @@ Proof.
     rewrite /= length_P' /=. lia.
   - move=> v /(sss_terminates_iff (@mma_sss_total_ni _)) Hv. apply: H2P.
     apply /(sss_terminates_iff (@mma_sss_total_ni _)). move: Hv.
-    apply /(Sim.terminates_reflection (Sim.deterministic_uniformly_confluent _ step2_det) fstep step1_intro).
+    apply /(Sim.terminates_reflection (Sim.deterministic_uniformly_confluent _ step2_det) fstep (sss_step_or_stuck (@mma_sss_total_ni _) 1 P)).
     rewrite -vec_append_const. by apply: sync_intro.
 Qed.

theories/MinskyMachines/Reductions/MM_computable_to_MMA_computable.v

@@ -9,7 +9,7 @@
   If a relation R is MM_computable then it is MMA_computable
 *)
 
-From Undecidability.MinskyMachines Require Import MM MMA MMA.mma_defs Util.MMA_computable Util.MMA_facts Util.MM_computable MM.mm_defs.
+From Undecidability.MinskyMachines Require Import MM MMA MMA.mma_defs MM.mm_defs Util.MMA_computable Util.MMA_facts Util.MM_computable MM.mm_defs.
 Require Import Undecidability.MinskyMachines.Util.MM_sss.
 
 From Undecidability.Shared.Libs.DLW
@@ -131,12 +131,6 @@ Definition sync : nat * Vector.t nat num_counters -> nat * Vector.t nat num_coun
 #[local] Notation step1 := (sss_step (@mm_sss num_counters) (1, P)).
 #[local] Notation step2 := (sss_step (@mma_sss num_counters) (1, P')).
 
-Fact mm_sss_total_ni {n : nat} (ii : mm_instr (pos n)) (s : MM.mm_state n) :
-  exists t : MM.mm_state n, mm_sss ii s t.
-Proof.
-  have [t ?] := mm_sss_total ii s. by exists t.
-Qed.
-
 Lemma fstep s t s' : step1 s t -> sync s s' ->
   exists t', clos_trans _ step2 s' t' /\ sync t t'.
 Proof.
@@ -151,13 +145,6 @@ Proof.
   apply: sss_step_fun. by apply: mma_sss_fun.
 Qed.
 
-Lemma step1_intro s : (exists t, step1 s t) \/ (stuck step1 s).
-Proof.
-  have [|] := subcode.in_out_code_dec (fst s) (1, P).
-  - move=> /(in_code_step mm_sss_total_ni) ?. by left.
-  - move=> /(out_code_iff mm_sss_total_ni) ?. by right.
-Qed.
-
 Lemma simulation v v' c :
   sss_compute (mm_sss (n:= num_counters)) (1, P) (1, v) (c, v') ->
   c < 1 \/ S (length P) <= c ->
@@ -185,6 +172,6 @@ Proof.
     rewrite /= MM_MMA.length_P' MM_MMA.addr_spec.
     move: Hc => /=. lia.
   - move=> v /(sss_terminates_iff (@mma_sss_total_ni _)) Hv. apply: H2P.
-    apply /(sss_terminates_iff MM_MMA.mm_sss_total_ni). move: Hv.
-    by apply /(terminates_reflection (deterministic_uniformly_confluent _ MM_MMA.step2_det) MM_MMA.fstep MM_MMA.step1_intro).
+    apply /(sss_terminates_iff (@mm_sss_total_ni _)). move: Hv.
+    by apply /(terminates_reflection (deterministic_uniformly_confluent _ MM_MMA.step2_det) MM_MMA.fstep (sss_step_or_stuck (@mm_sss_total_ni _) 1 P)).
 Qed.