Since there was a release of coq-num-analysis, it would be interesting to see a breakdown of the current differences between this library and MC analysis. On a cursory glance:
I think you are correct. For topology, my understanding is that num-analysis builds on top of Coquelicot which offers that.
The main difference I see between both developments is that Analysis is built on top of MathComp whereas num-analysis uses the standard library, Coquelicot and ssreflect. I tend to prefer the uniformity of MathComp and Analysis but I'm definitely biased here. Anyway, this duplication of efforts is quite unfortunate IMHO.
well, in that case, it at least offers AI researchers (or Coq tooling dabblers like me) the opportunity to investigate how one can find mappings between concepts and possibly figure out automatic translations for different formalizations of the same thing. I don't think anyone is going to add any bridges between the libraries by hand, unfortunately.
Note that Analysis offers a
Rstruct.v file with links between stdlib and analysis real numbers, so part of the link is already there.
I'll probably bother people on the subject in the coming years - trying to add things left and things right to make things converge
at least I heard someone in AI was like: "we want tons of different proofs of the same thing [for training our models]" - which is kind of the opposite of what ITP researchers want
I don't think anyone is going to add any bridges between the libraries by hand, unfortunately.
in a recent chat between "MC people" and "NA people" I (provocatively) rephrased this challenge as "copy pasting a Word document into TeX or viceversa". It is sad, but that is really food for AI. It is not easy.
(and yes, we were looking at not-always-working canonical structure instances to use MC linear algebra library in NA)
maybe more realistic: there could at least be some "joint documentation" so we can see/compare what is done in each, possibly generated automatically from Coq annotations and the like
although this is arguably also AI problem ("summarize ITP libraries and their concepts")
[FTR, I dislike TeX as much as Word, they are just placeholders for very different languages]
What happened to crowdsourcing and wikis? I guess I'm just old-fashioned ...
Last updated: Feb 05 2023 at 14:02 UTC