New seed: halting of MM2 starting from the fixed state (1,(0,0))

[DmxLarchey]

This PR is a first step towards a proof of undecidability of Wang tilings with a fixed origin (ie tiling the North-East part of the plane). The intended reduction chain would be

1. MM2 halting, starting from the fixed state (1,(0,0));
2. PCTM on a half binary tape halting, starting from the empty tape;
3. Wang tiling of NE part of the plane.

Notice that undecidability of Wang tiling would then follow from the non co-enumerability of HALT, ie the chain is
1 => 2 (hence also ~1 => ~2) and then ~2 => ~3.

Notice that the changes in existing files are very small and only add new statements, ie they do not change existing statements

[mrhaandi]

I have two major comments.

• The proposed MM2 halting from (1,(0,0)) is already part of the prior, ready-to-merge PR No CM2 #169, and plays an important role there.
• The present PR targets the coq-8.15. The only reason coq-8.16 is currently not the main branch is because of the CI, however it compiles and works correctly. A lot of work is already invested in the coq-8.16 branch and new developments are to target it.

@DmxLarchey It would be good if you take a closer look at PR #169 and whether it already subsumes the present PR.

[DmxLarchey]

Ok I did not notice that this was already in. Does it also include TM (or equivalent) halting on the empty tape because that is my target ATM?

Btw, some of the code in deterministic simulation addresses the same questions with similar answers as those already present in the compiler used till the CPP'19 paper. May be in a slightly more abstract way. I did let a comment in #169 about it: https://github.com/uds-psl/coq-library-undecidability/pull/169/files#r996707608

Possibly we could merge those by reusing the deterministic simulation in the compiler correction, but this is not a lot of code in either cases.

The compiler was designed to be used with different models of computation, and it is what happened in the end. That is why there is a PC and the computation relation is described the way it is, ie not directly using the reflexive, transitive closure. I wanted to capture the number of steps also. Totality of the step relation could be weakened into forall s, (exists s', s -1> s') \/ (forall s', ~ s -1> s'). In the current PC based models, the above choice is made on the position on the PC wrt to the code, ie in_code or out_code.