Computability: L -> MMA /\ MMA -> TM

[mrhaandi]

As previously discussed with @yforster, this PR replaces the laborious, direct L_computable -> TM_computable proof by a shorter L_computable -> MMA_computable, MMA_computable -> TM_computable variant with several benefits.

• no Hoare framework required
• no Smpl plugin required
  • Smpl is entirely removed as a dependency
  • fixes CI
  • now the library is easy to integrate into Coq's CI
• no L on boolean lists required
• no complexity considerations required (which distract from the actual argument)
• short: 4000 LOC vs. 20000 LOC
• fast: local library total compilation time real 4m21s vs. real 6m30s

Supercedes https://github.com/uds-psl/coq-library-undecidability/pull/148, https://github.com/uds-psl/coq-library-undecidability/pull/171

[mrhaandi]

@DmxLarchey since TMs are working with Coq vector primitives and MMAs work with your vector primitives (vec_pos, vec_change) the code is more cumbersome than necessary due to conversions. I also added missing vec_change_app_left, vec_change_app_right, pos_list_NoDup to your shared library.

[DmxLarchey]

@mrhaandi The vec(tors) and pos(itions) I use in the Shared/Libs/DLW/vec are the same as Vector.t and Fin.t so it is possible to use the tools of the StdLib on them. By the same, I mean eg Notation vec := Vector.t. This was not the case initially but the identification occurred a several years ago.

Using pos.v and vec.v is more convenient (from my point of view) but not mandatory at all.

[mrhaandi]

use the tools of the StdLib on them. By the same, I mean eg Notation vec := Vector.t

Yes, vec := Vector.t definitely helps. Still, some functionality like vec_pos which is extensionally (but not definitionally) equal to Vector.nth requires rewrites back and forth. I understand that asking to set vec_pos := Vector.nth and vec_change := Vector.replace would induce too much work. Basically, it only matters when a reduction between two models use different vector primitives.

[DmxLarchey]

Still, some functionality like vec_pos which is extensionally (but not definitionally) equal to Vector.nth requires rewrites back and forth.

@mrhaandi Interesting point: that is intended! Unfortunately, the way Vector.nth is written clashes with the guardedness condition. Indeed, vec_pos v j is accepted/recognized as a structural sub-term of v but Vector.nth v j is not. In particular, in the fixpoint recalg_rect at

https://github.com/uds-psl/coq-library-undecidability/blob/c486697da8cfa4b9bb11b4c53eea7d57781c0deb/theories/MuRec/Util/recalg.v#L51

replacing vec_pos with Vector.nth will break the guardedness condition (you also need to update the induction hypothesis Pcomp five lines above). This is why I needed to rewrite Vector.nth carefully; this dates back to 2014 if I recall correctly. FYI, that specific point was pointed out in my ITP 2017 paper on µ-recursive functions vs Coq, but I can understand this subtlety is not very widely known.

Using Vector.nth, the Braga method would still be available as a workaround though. But much heavier that the smooth vec_pos because the fixpoint equation holds definitionally with vec_pos. If it where up to me, I would rewrite Vector.nth in the StdLib to match the code of vec_pos instead of the converse ;-)

[DmxLarchey]

I understand that asking to set vec_pos := Vector.nth and vec_change := Vector.replace would induce too much work.

Concerning vec_change this issue would not pop up so I think it would be possible to define it as a notation for Vector.replace. I do not think I use vec_change so much anyway but I would definitely need to check the Trahktenbrot code though. Also the interaction btw vec_pos and vec_change would need to be updated because of vec_pos.

[mrhaandi]

If it where up to me, I would rewrite Vector.nth in the StdLib to match the code of vec_pos instead of the converse ;-)

I proposed this change to Coq's stdlib: https://github.com/coq/coq/pull/16731

[mrhaandi]

@DmxLarchey are you ok with the added MMA files and additions to your vec library?