Stream: math-comp analysis

Topic: Differences between MC analysis and num-analysis


view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Sep 09 2022 at 20:36):

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

view this post on Zulip Enrico Tassi (Sep 09 2022 at 20:37):

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

view this post on Zulip 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