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 #148, #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

coq-library-undecidability/theories/MuRec/Util/recalg.v

Line 51 in c486697

Fixpoint recalg_rect k f { struct f } : @P k f :=

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: rocq-prover/rocq#16731

[mrhaandi]

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

[DmxLarchey]

I am ok with the additions in vec.v and pos.v. Once Vector.nth is updated in the StdLib, we could switch to that definition, which is nearly the same as in the current vec.v. For the rest of the PR, it seems to me it mostly concerns stripping down the L subdir so @yforster and possibly @fakusb are better equipped for giving their opinions on those changes.

[yforster]

Apart from the conflict with the new CI file I'm happy to merge this now! (We can either merge #181 before or after, that should not matter)