Stream: Constructive reals & analysis

Topic: formalization of Bishop's Constructive Analysis?

Ben Siraphob (May 13 2021 at 14:04):

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

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

Ben Siraphob (May 15 2021 at 07:43):

Thanks, that seems useful.

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?

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.

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

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.

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? ...

Ben Siraphob (Jul 03 2021 at 02:05):

@Hugo Herbelin Ok, here are some concrete examples.

• convergence of products and sums of sequences is given, but not for division or reciprocal
• Riemann integration lemmas are a mess, the naming is things like RiemannInt_P18 to express linearity
• lack of lemmas about inverses of continuous functions, nth roots

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.

Ben Siraphob (Jul 03 2021 at 02:07):

Yeah, I really need to try the other libraries.

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.

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

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.

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

Vincent Semeria (Jul 04 2021 at 08:24):

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

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: Jun 11 2023 at 00:30 UTC