proposition: Lemma M_to_P_step s y : MPM2.step M (to_Config s) = Some y -> exists t, y = to_Config t /\ sss_step (@mm_sss _) (1, P) s t.
proof: Proof. rewrite /MPM2.step. case Hi: (nth_error M (MPM2.state (to_Config s))) => [i|]; last done. case: i Hi. - done. - rewrite /M. move=> ? /(@nth_error_In MPM2.Instruction) /in_map_iff. by move=> [[]] /= => [?|??] []. - move=> c. rewrite /M nth_error_map. case Hi: (nth_error P (MPM2.state (to_Config s))) => [i|]; last done. move: Hi => /(@nth_error_split (mm_instr _)) [P1] [P2] [HP HP1] [Hi] [<-]. move: s HP1 => [p v] HP1. have Hp : p = S (p - 1). { move: p HP1 => [|p]. { rewrite (decompose_vec2 v) /= HP app_length /=. lia. } move=> ? /=. lia. } exists (S (S (MPM2.state (to_Config (p, v)))), ((if c then 0 else 1) + MPM2.value1 (to_Config (p, v))) ## ((if c then 1 else 0) + MPM2.value2 (to_Config (p, v))) ## vec_nil). split; first done. exists 1, P1, i, P2, v. split; first by congr pair. split. { move: HP1. by rewrite (decompose_vec2 v) Hp /= => <-. } have -> : i = INC (if c then pos1 else pos0). { move: i Hi {HP} => []; last done. move=> d /=. by case: (case_pos2 d) => /= -> [<-]. } have := @in_mm_sss_inc 2 p (if c then pos1 else pos0) v. congr mm_sss. congr pair. { by rewrite (decompose_vec2 v) Hp. } case: c {Hi}. + by rewrite (decompose_vec2 v) Hp /=. + by rewrite (decompose_vec2 v) Hp /=. - move=> c q. rewrite /M nth_error_map. case Hi: (nth_error P (MPM2.state (to_Config s))) => [i|]; last done. move: Hi => /(@nth_error_split (mm_instr _)) [P1] [P2] [HP HP1] [Hi] [<-]. move: s HP1 => [p v] HP1. have Hp : p = S (p - 1). { move: p HP1 => [|p]. { rewrite (decompose_vec2 v) /= HP app_length /=. lia. } move=> ? /=. lia. } move: HP1. rewrite (decompose_vec2 v) Hp /= => HP1. move: i HP Hi => [] /=; first done. move=> d r. move: (case_pos2 d) => [|] /= -> HP [] <- <-. + exists (if (vec_head v) is S a then (S p, a ## vec_head (vec_tail v) ## vec_nil) else (r, 0 ## vec_head (vec_tail v) ## vec_nil)). split. { case: (vec_head v). - by case: (r). - move=> ?. by rewrite [in to_Config _]Hp /to_Config. } case Hv: (vec_head v) => [|a]. * exists 1, P1, (DEC pos0 r), P2, v. split; first by congr pair. split. { by rewrite [in (_, v)](decompose_vec2 v) /= HP1 Hv. } have := @in_mm_sss_dec_0 2 p pos0 r v. rewrite [in vec_pos v](decompose_vec2 v) /=. move=> /(_ Hv). by congr mm_sss; rewrite -?Hp [in (_, v)](decompose_vec2 v) Hv. * exists 1, P1, (DEC pos0 r), P2, v. split; first by congr pair. split. { by rewrite [in (_, v)](decompose_vec2 v) /= HP1 Hv. } have := @in_mm_sss_dec_1 2 p pos0 r v. rewrite [in vec_pos v](decompose_vec2 v) /=. move=> /(_ a Hv). congr mm_sss; rewrite -?Hp. ** by rewrite -Hv -(decompose_vec2 v). ** by rewrite [in vec_change v](decompose_vec2 v). + exists (if (vec_head (vec_tail v)) is S b then (S p, vec_head v ## b ## vec_nil) else (r, vec_head v ## 0 ## vec_nil)). split. { case: (vec_head (vec_tail v)). - by case: (r). - move=> ?. by rewrite [in to_Config _]Hp /to_Config. } case Hv: (vec_head (vec_tail v)) => [|b]. * exists 1, P1, (DEC pos1 r), P2, v. split; first by congr pair. split. { by rewrite [in (_, v)](decompose_vec2 v) /= HP1 Hv. } have := @in_mm_sss_dec_0 2 p pos1 r v. rewrite [in vec_pos v](decompose_vec2 v) /=. move=> /(_ Hv). by congr mm_sss; rewrite -?Hp [in (_, v)](decompose_vec2 v) Hv. * exists 1, P1, (DEC pos1 r), P2, v. split; first by congr pair. split. { by rewrite [in (_, v)](decompose_vec2 v) /= HP1 Hv. } have := @in_mm_sss_dec_1 2 p pos1 r v. rewrite [in vec_pos v](decompose_vec2 v) /=. move=> /(_ b Hv). congr mm_sss; rewrite -?Hp. ** by rewrite -Hv -(decompose_vec2 v). ** by rewrite [in vec_change v](decompose_vec2 v). Qed.
imports: PeanoNat Lia List Undecidability.MinskyMachines(MM MM_sss) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss) ssreflect ssrbool ssrfun