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

Have you looked at:

https://github.com/coq-community/corn

https://github.com/coq-community/math-classes

Thanks, that seems useful.

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

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.

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

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

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

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

Yeah, I really need to try the other libraries.

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.

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

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.

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

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

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