proposition: Lemma bsm_instr_compile_sound : instruction_compiler_sound bsm_instr_compile (@bsm_sss _) (@mm_sss _) bsm_state_enc.
proof: Proof. Proof using Hvr1 Hvr2 Hvr3 Hv12 Hv13 Hv23 Hreg. intros lnk I i1 v1 i2 v2 w1 H; revert H w1. change v1 with (snd (i1,v1)) at 2. change i1 with (fst (i1,v1)) at 2 3 4 6 7 8. change v2 with (snd (i2,v2)) at 2. change i2 with (fst (i2,v2)) at 2. generalize (i1,v1) (i2,v2); clear i1 v1 i2 v2. induction 1 as [ i p j k v Hv | i p j k v ll Hll | i p j k v ll Hll | i p [] v ]; simpl; intros w1 H0 H; generalize H; intros (H1 & H2 & Htmp3 & H3). + exists w1; split; auto. apply mm_pop_void_progress; auto using Hv12, Hvr1, Hvr2. rewrite H3, Hv; auto. + exists (w1[(stack_enc ll)/reg p]); repeat split; auto; rew vec. * apply mm_pop_Zero_progress; auto using Hv12, Hvr1, Hvr2. rewrite H3, Hll; auto. * rewrite vec_change_neq. 2: congruence. eauto. * rewrite vec_change_neq. 2: congruence. eauto. * rewrite vec_change_neq. 2: congruence. eauto. * intros q; dest p q. assert (reg p <> reg q); rew vec. + exists (w1[(stack_enc ll)/reg p]); repeat split; auto; rew vec. * apply mm_pop_One_progress; auto using Hv12, Hvr1, Hvr2. rewrite H3, Hll; auto. * rewrite vec_change_neq. 2: congruence. eauto. * rewrite vec_change_neq. 2: congruence. eauto. * rewrite vec_change_neq. 2: congruence. eauto. * intros q; dest p q. assert (reg p <> reg q); rew vec. + exists (w1[(stack_enc (One::v#>p))/reg p]); repeat split; auto; rew vec. 2:{ rewrite vec_change_neq. 2: congruence. eauto. } 2:{ rewrite vec_change_neq. 2: congruence. eauto. } 2:{ rewrite vec_change_neq. 2: congruence. eauto. } rewrite H0; apply mm_push_One_progress; auto using Hv12, Hvr1, Hvr2. intros q; dest p q. assert (reg p <> reg q); rew vec. + exists (w1[(stack_enc (Zero::v#>p))/reg p]); repeat split; auto; rew vec. rewrite H0; apply mm_push_Zero_progress; auto using Hv12, Hvr1, Hvr2. * rewrite vec_change_neq. 2: congruence. eauto. * rewrite vec_change_neq. 2: congruence. eauto. * rewrite vec_change_neq. 2: congruence. eauto. * intros q; dest p q. assert (reg p <> reg q); rew vec. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss compiler_correction) Undecidability.StackMachines.BSM(bsm_defs) Undecidability.MinskyMachines.MM(mm_defs mm_utils)