SetoidRewrite.v #2316
Description
I'm looking again at the file contrib/SetoidRewrite.v that @patrick-nicodemus kindly contributed to the library in late 2022. See #1684 and #1695 .
I think this is going to be quite handy for some work in progress with @ThomatoTomato .
A couple of updates to the discussion from back then:
At least as of Rocq 9.0, SetoidRewrite.v builds fine without having the Rocq standard library installed. You just need the core part of Rocq. So this is promising, and makes me think we should consider moving it back to the main library.
However, adding Require Coq.Init.Tactics at the top of Basics/Settings.v does cause at least one build failure, in Spaces/Nat/Core.v. The line inversion leq_m_Sn as [p | k H p] produces a p of type Logic.eq instead of a path. This isn't the end of the world, as we could just import SetoidRewrite.v when needed, but it would be better if we had full compatibility with the library. Does anyone know a (robust) fix for this particular issue?
Even better, can someone see if they can make the whole library build with SetoidRewrite loaded? I'd estimate that around half of the library built fine (with no warnings) with Coq.Init.Tactics loaded, so it's probably not too hard to get the whole library to build. I'm still on Coq 8.20.1, so that's what I tested with. So another question is whether things are already better with Rocq 9.0 or 9.1.