(Universal) Turing machine halting

[mrhaandi]

Goals of this PR:

• Top-level (universal) Turing machine halting Definition HaltUTM : tape (finType_CS bool) -> Prop := fun t => HaltsTM UTM [t]. and Lemma HaltUTM_undec : undecidable HaltUTM. where the boolean single-tape machine UTM is fixed.
• Cleanup internal TM files which are not necessary for the decision problems in the library. This has several benefits.
  • Less pervasive dependencies on MetaCoq. This PR makes only L depend on MetaCoq.
  • Less historically breaking code for the same top-level results.
  • Faster compilation. Previously real 8m15.765s, user 50m4.791s, Now real 5m50.301s, user 37m34.350s. EDIT: Now down to real 3m55.015s, user 24m23.905s.
  • Faster vos compilation. Previously real 1m57.135s, user 9m51.042s, Now real 1m26.193s, user 6m41.955s.
• Replaced ComputableTime result by Computable results, removing additional time analysis. This does not change top-level results in the library, and speeds up proofs.
• Removed Smpl dependency.

[yforster]

This looks good, and the 20% reduction in compilation time is great!

I think the best way to merge this is to first let Fabian port the files and results that we remove to https://github.com/uds-psl/coq-library-complexity. That way, we can make sure that nothing gets lost and all results stay under CI. Fabian agreed to do this in the next ~2 weeks.

Are you fine with that Andrej?

[mrhaandi]

Are you fine with that Andrej?

Yes, I like the separation of complexity and computability. I also now removed the L/Complexity framework to reason about compilation time up to a bound. This does not change the top-level computability results. As a benefit, now MetaCoq is local to L for extraction and Smpl is local to TM for simplification. So if a plugin breaks (or when porting to the next Coq version) one can keep the impact local.

[mrhaandi]

After removal of the ComputableTime framework (Computable suffices) the compilation time went further down to real 5m11.080s, user 31m13.067s. Here we start hitting diminishing returns because the critical path is now in HOU instead of L. (Without HOU I get real 3m18.730s, user 19m51.220s.)

[yforster]

Meaning HOU makes up for 30% of the whole computation power needed? That's surprising. I knew it was high, but not that high.

[mrhaandi]

@yforster @fakusb The main results on TM are the Arbitrary_to_Binary.v compression and the Single/StepTM.v compression. For these, Smpl is not really necessary and I replaced the remaining TM_Correct code by smaller and faster eauto with tm. tm is essentially the same database as the previous TM_Correct but without the additional tactics. Especially Single/StepTM.v benefits from the faster eauto (previously 54s, now 29s on my machine). As a result, we do not have Smpl as a library dependency anymore.