Stream: math-comp analysis

Topic: Differences between MC analysis and num-analysis

Karl Palmskog (Sep 09 2022 at 11:52):

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:

• both have the Lebesgue integral, but probably encoded very differently
• num-analysis has the Bochner integral, but MC analysis does not(?)
• num-analysis has Lax-Milgram theorem, MC does not(?)
• num-analysis has Tonelli theorem, so does MC(?)
• MC analysis has a bunch of topology, I think this is not part of num-analysis but might be found elsewhere in that style

Pierre Roux (Sep 09 2022 at 12:44):

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.

Karl Palmskog (Sep 09 2022 at 12:48):

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.

Pierre Roux (Sep 09 2022 at 12:55):

Note that Analysis offers a Rstruct.v file with links between stdlib and analysis real numbers, so part of the link is already there.

Julien Puydt (Sep 09 2022 at 12:57):

I'll probably bother people on the subject in the coming years - trying to add things left and things right to make things converge

Karl Palmskog (Sep 09 2022 at 13:08):

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

Enrico Tassi (Sep 09 2022 at 20:32):

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.

Enrico Tassi (Sep 09 2022 at 20:33):

(and yes, we were looking at not-always-working canonical structure instances to use MC linear algebra library in NA)

Karl Palmskog (Sep 09 2022 at 20:35):

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

Karl Palmskog (Sep 09 2022 at 20:36):

although this is arguably also AI problem ("summarize ITP libraries and their concepts")

Enrico Tassi (Sep 09 2022 at 20:37):

[FTR, I dislike TeX as much as Word, they are just placeholders for very different languages]

Bas Spitters (Sep 10 2022 at 11:49):

What happened to crowdsourcing and wikis? I guess I'm just old-fashioned ...

Last updated: Feb 05 2023 at 14:02 UTC