Stream: Constructive reals & analysis

Topic: formalization of Bishop's Constructive Analysis?


view this post on Zulip Ben Siraphob (May 13 2021 at 14:04):

Has anyone worked on/is aware of a formalization of Bishop's Constructive Analysis in Coq?

view this post on Zulip Bas Spitters (May 13 2021 at 15:05):

Have you looked at:
https://github.com/coq-community/corn
https://github.com/coq-community/math-classes

view this post on Zulip Ben Siraphob (May 15 2021 at 07:43):

Thanks, that seems useful.

view this post on Zulip Bas Spitters (May 15 2021 at 09:39):

@Vincent Semeria has recently been contributing a lot to the libraries and has even integrated it in the stdlib.

What would you like to do with constructive analysis?

view this post on Zulip Ben Siraphob (May 16 2021 at 12:54):

I've just taken a undergrad real analysis course at my university and formalized parts of it (up to Riemann integration at which point the stdlib was too difficult to work with), but I was also interested to see how much analysis one could do without LEM.

view this post on Zulip Bas Spitters (May 16 2021 at 13:53):

One can develop and formalize a lot of it without LEM.
We also did (Riemann) integration a while ago:
https://arxiv.org/abs/0809.1552

view this post on Zulip Hugo Herbelin (Jul 02 2021 at 23:12):

The "Mesure et Int├ęgrale de Lebesgue en Coq" (https://lipn.univ-paris13.fr/MILC/, in French) is also developing integration in Coq.

view this post on Zulip Hugo Herbelin (Jul 02 2021 at 23:17):

@Ben Siraphob: By the way, I'm not sure to exactly grasp what you intend by "too difficult to work with" (even if I'm ready to believe it!). Do you main too pedestrian? Do you mean lacking appropriate lemmas? Lacking automation? Lacking structure? ...

view this post on Zulip Ben Siraphob (Jul 03 2021 at 02:05):

@Hugo Herbelin Ok, here are some concrete examples.

Automation is OK in terms of having linear solvers, I wrote some Ltac to make proving limits easier. IIRC differentiation in coquelicot is nice in this regard.

view this post on Zulip Ben Siraphob (Jul 03 2021 at 02:07):

Yeah, I really need to try the other libraries.

view this post on Zulip Bas Spitters (Jul 03 2021 at 20:32):

Which part of the stdlib are you talking about. I believe the constructive measure theory that is there was written by @Vincent Semeria , so you can ask him directly.

view this post on Zulip Ben Siraphob (Jul 04 2021 at 03:39):

@Bas Spitters ah this is a continuation of discussion from #Coq Workshop 2021, repasted in reply to @Hugo Herbelin

view this post on Zulip Vincent Semeria (Jul 04 2021 at 07:51):

I agree with @Ben Siraphob critiques about the Riemann integration in the stdlib. The missing lemmas should be added and the existing lemmas should be renamed. For backward compatibility, the current _PXYZ names can be kept as notations.

view this post on Zulip Ben Siraphob (Jul 04 2021 at 07:54):

I'm thinking that some of the names could be taken from coqtail-math (e.g. https://github.com/coq-community/coqtail-math/blob/master/Reals/Rintegral/Riemann_integrable.v) also

view this post on Zulip Vincent Semeria (Jul 04 2021 at 08:24):

Those names make sense to me. You can submit a pull request to the stdlib.

view this post on Zulip Vincent Semeria (Jul 04 2021 at 08:52):

An implementation of constructive measure theory is here, https://github.com/coq-community/corn/tree/master/reals/stdlib. It uses no axioms (in particular it avoids LEM) but it's not very user-friendly at the moment.


Last updated: Feb 06 2023 at 06:29 UTC