proposition: Theorem ra_mm_compiler (n : nat) (f : recalg n) : { m & { P : list (mm_instr (pos (n+S m))) | (forall x v, ⟦f⟧ v x -> (1,P) /v/ (1,vec_app v vec_zero) ->> (1+length P,vec_app v (x##vec_zero))) /\ (forall v, (1,P) /v/ (1,vec_app v vec_zero) ↓ -> ex (⟦f⟧ v)) } }.
proof: Proof. destruct ra_mm_env_simulator with (f := f) as (P & HP). set (k := Nat.max (S n) (mm_nat_bound P)). assert (S n <= k) as H3 by apply Nat.le_max_l. assert { m | k = n+S m } as H4. { exists (k-S n); lia. } clear H3. destruct H4 as (m & Hm). exists m. destruct mm_nat_pos with (n := k) (l := P) as (Q & HQ). + apply Nat.le_max_r. + revert Q HQ; rewrite Hm; clear k Hm; intros Q HQ. exists Q; split. * intros x v H. destruct (HP v (fun j => match le_lt_dec n j with left _ => 0 | right Hj => vec_pos v (nat2pos Hj) end)) as [ H1 _ ]. - intros p; generalize (pos2nat_prop p); intros H0; unfold get_env. destruct (le_lt_dec n (pos2nat p)); try lia. f_equal; apply nat2pos_pos2nat. - intros j Hj; unfold get_env. destruct (le_lt_dec n j); lia. - destruct (H1 _ H) as (e' & G1 & k & G2); auto. exists k. rewrite HQ in G2 at 1. apply sss_steps_mm_pos_nat_inv with (v1 := vec_app v vec_zero) in G2. ++ destruct G2 as (v2 & G2 & G3); simpl in G3. eq goal G3; do 2 f_equal. { rewrite HQ; unfold mm_pos_nat; rewrite map_length; auto. } apply vec_pos_ext, pos_left_right_rect. ** intros p; rewrite G2, vec_pos_app_left, G1; simpl. rewrite pos2nat_left. generalize (pos2nat_prop p); intros G4. rewrite get_set_env_neq; try lia. unfold get_env. destruct (le_lt_dec n (pos2nat p)); try lia. f_equal; apply nat2pos_pos2nat. ** intros p. rewrite vec_pos_app_right, G2, pos2nat_right; simpl snd. rewrite Nat.add_comm. analyse pos p. -- rewrite pos2nat_fst; simpl. rewrite G1; rew env. -- rewrite pos2nat_nxt; simpl. unfold vec_zero; rewrite vec_pos_set. rewrite G1, get_set_env_neq; try lia. unfold get_env; simpl. destruct (le_lt_dec n (S (pos2nat p+n))); lia. ++ simpl; apply pos_left_right_rect. ** intros p; rewrite vec_pos_app_left, pos2nat_left. unfold get_env. generalize (pos2nat_prop p); intros. destruct (le_lt_dec n (pos2nat p)); try lia; f_equal. rewrite nat2pos_pos2nat; auto. ** intros p; rewrite vec_pos_app_right, pos2nat_right. unfold vec_zero; rewrite vec_pos_set. unfold get_env. destruct (le_lt_dec n (n+pos2nat p)); try lia. * intros v ((j,w) & (k & G1) & G2); simpl in G2. set (e1 := fun j => match le_lt_dec n j with left _ => 0 | right Hj => vec_pos v (nat2pos Hj) end). apply sss_steps_mm_pos_nat with (e1 := e1) in G1. destruct G1 as (e2 & G1 & G3); simpl in G3. apply HP with e1. - intros p; unfold e1, get_env. generalize (pos2nat_prop p); intros. destruct (le_lt_dec n (pos2nat p)); try lia. rewrite nat2pos_pos2nat; auto. - intros p Hp. unfold e1, get_env. destruct (le_lt_dec n p); lia. - rewrite HQ; exists (j,e2); split. ++ exists k; auto. ++ simpl; unfold mm_pos_nat; rew length; auto. - simpl; apply pos_left_right_rect. ++ intros p; rewrite vec_pos_app_left, pos2nat_left. unfold e1, get_env. generalize (pos2nat_prop p); intros. destruct (le_lt_dec n (pos2nat p)); try lia. rewrite nat2pos_pos2nat; auto. ++ intros p; rewrite vec_pos_app_right, pos2nat_right, vec_zero_spec. unfold e1, get_env. destruct (le_lt_dec n (n+pos2nat p)); try lia. Qed.
imports: List Arith Lia Max Undecidability.Shared.Libs.DLW(utils pos vec subcode sss) Undecidability.MinskyMachines(env mm_defs mme_defs mme_utils) Undecidability.MuRec.Util(recalg ra_mm_env)