Stream: coq-community devs & users

Topic: Listing bitrotted math on coq-community wiki


view this post on Zulip Karl Palmskog (Aug 19 2020 at 11:33):

I can't think of any other way of getting started with collecting bitrotted Coq math than using the coq-community wiki: https://github.com/coq-community/manifesto/wiki/List-of-disused-formalized-mathematics-in-Coq - other suggestions welcome, though

view this post on Zulip Bas Spitters (Aug 19 2020 at 12:05):

https://github.com/roglo/puiseuxth compiles with 8.11, apparently
This is also bitrotting:
https://github.com/Eelis/hybrid

view this post on Zulip Karl Palmskog (Aug 19 2020 at 12:09):

sigh, Madiot's list is out of date

view this post on Zulip Bas Spitters (Aug 19 2020 at 12:12):

Also the work by Carlos Simson and his group, which is quite close to what Kevin is trying to do:
https://math.unice.fr/%7Ecarlos/themes/verif.html

view this post on Zulip Bas Spitters (Aug 19 2020 at 12:13):

In case you want it extend it to CS:
https://github.com/EasyCrypt/certicrypt

view this post on Zulip Karl Palmskog (Aug 19 2020 at 12:15):

CS fits more for "move project" issues

view this post on Zulip Bas Spitters (Aug 19 2020 at 12:20):

What's the difference between math and CS in this respect?

view this post on Zulip Karl Palmskog (Aug 19 2020 at 12:23):

I think of CS as more holistic, one formalizes a whole program / language, and the program is generally not something known before

view this post on Zulip Karl Palmskog (Aug 19 2020 at 12:24):

if you look in coq-community issues, we already have certicrypt and hybrid issues there. But math results may be just a small part of other projects.

view this post on Zulip Karl Palmskog (Aug 19 2020 at 12:25):

basically I'm not going to put an issue with "move proof that pi is transcendental to coq-community", so second best thing is to list it in wiki

view this post on Zulip Karl Palmskog (Aug 19 2020 at 12:27):

I think Simpson's Coq work is (maybe with some exception) available in the coq-contribs, which I would at least would consider "preserved"

view this post on Zulip Karl Palmskog (Aug 19 2020 at 13:49):

A lot of things in ForMath that appears to fit: https://wiki.portal.chalmers.se/cse/pmwiki.php/ForMath/ProofExamples

view this post on Zulip Bas Spitters (Aug 19 2020 at 14:19):

@Cyril Cohen and @Maxime Dénès were involved in this project from Sophia, and may know more.
I lead the Nijmegen part of WP4, corn and math-classes are part of the community.
CoqEAL is still available.
I think WP3 was mostly done in Isabelle. I'd be happy to provide more information, if you think other things are missing.

view this post on Zulip Karl Palmskog (Aug 19 2020 at 14:39):

for precision if Cyril and Maxime see this, we are interested in listing results that may be of interest to researchers that are not currently included in any modern library.

view this post on Zulip Karl Palmskog (Aug 19 2020 at 17:28):

@Bas Spitters do you know what happened to the other stuff in WP4 (if anything happened at all), like "Rohn's theorem, a sketch of Perron-Frobenius, and canonical forms" (https://wiki.portal.chalmers.se/cse/uploads/ForMath/formath-4.3.zip)

view this post on Zulip Bas Spitters (Aug 20 2020 at 07:08):

@Yves Bertot and his team worked on that. There's quite an extensive PDF report in the zip file you linked.
P-F was the work by:
https://www-sop.inria.fr/marelle/Guillaume.Cano/
These slides tell me that it is now in math-comp analysis.
https://perso.crans.org/cohen/CoqWS2018.pdf
There was also work by Ioana (https://www-sop.inria.fr/marelle/Ioana.Pasca/phd/ https://www-sop.inria.fr/marelle/Ioana.Pasca/publications.html).
Other parts are available in CoqEAL.
I believe some parts have also been subsumed by @Cyril Cohen s work on robotics.
( Incidentally, https://github.com/aa755/ROSCoq by @Abhishek Anand is another fun application of Coq to robotics.)

view this post on Zulip Bas Spitters (Aug 20 2020 at 07:13):

About WP4.1
http://coq.io/opam/coq-pi-agm.1.2.6.html
But follow-up work in:
https://www-sop.inria.fr/marelle/distant-decimals-pi/
https://github.com/thery/Plouffe

view this post on Zulip Bas Spitters (Aug 20 2020 at 07:14):

About WP3, I see quite a bit of the code is actually in Coq. Do you think it's worth following up?

view this post on Zulip Karl Palmskog (Aug 20 2020 at 07:26):

thanks, so it seems the rest of WP4 is indeed covered. I'll take a look at WP3 later this week


Last updated: Feb 05 2023 at 13:02 UTC