Karl Palmskog (Aug 19 2020 at 11:33): 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
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
Karl Palmskog (Aug 19 2020 at 12:09):sigh, Madiot's list is out of date
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
Bas Spitters (Aug 19 2020 at 12:13):In case you want it extend it to CS:
https://github.com/EasyCrypt/certicrypt
Karl Palmskog (Aug 19 2020 at 12:15):CS fits more for "move project" issues
Bas Spitters (Aug 19 2020 at 12:20):What's the difference between math and CS in this respect?
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
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.
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
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"
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
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.
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.
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)
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.)
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
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?
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: Jun 03 2023 at 18:01 UTC