Topic for the first presentation

@Laurent Théry the Isabelle/HOL paper mentions Joe Hurd in those terms "Hurd [6] formalizes a measure space on infinite boolean streams isomorphic

to the Lebesgue measure on the unit interval r [0, 1]." It looks specialized to probability theory. But Caratheodory's theorem was already there indeed!

ok I don't have alzheimer ;-)

well, it's not exactly 30 years ago though, but MIzar's stuff is even older

Adding on to discussion during the break on analysis in Coq, I was formalizing the content of the undergraduate analysis class at my university aimed for more vanilla Coq users, but at Riemann integration and beyond the stdlib was too painful to work with. Coquelicot required use of filters instead of epsilon-delta arguments, and math-comp analysis required knowledge of ssreflect, so even at the elementary level it's still hard

Ben Siraphob said:

Adding on to discussion during the break on analysis in Coq, I was formalizing the content of the undergraduate analysis class at my university aimed for more vanilla Coq users, but at Riemann integration and beyond the stdlib was too painful to work with. Coquelicot required use of filters instead of epsilon-delta arguments, and math-comp analysis required knowledge of ssreflect, so even at the elementary level it's still hard

For the ssreflect part, it is actually possible to carry out proofs in a hybrid style using mostly standard Coq tactics but indeed definitions have a ssreflect look and feel

Ben Siraphob said:

Adding on to discussion during the break on analysis in Coq, I was formalizing the content of the undergraduate analysis class at my university aimed for more vanilla Coq users, but at Riemann integration and beyond the stdlib was too painful to work with. Coquelicot required use of filters instead of epsilon-delta arguments, and math-comp analysis required knowledge of ssreflect, so even at the elementary level it's still hard

Mathcomp analysis also uses filters, however (and I think it's true in Coquelicot as well), there is always a way to translate the statement to a classic epsilon delta one if the topology is appropriate (pseudometric I guess).

Reynald Affeldt said:

For the ssreflect part, it is actually possible to carry out proofs in a hybrid style using mostly standard Coq tactics but indeed definitions have a ssreflect look and feel

I have been doing this to some extent, mixing Coq-like stuff for complex induction with reasoning using more ssreflecty things in subgoals, and the combination works quite well

@Reynald Affeldt Ah, I wasn't aware that one could use math-comp without using ssreflect in full, sounds useful.

Ben Siraphob said:

Hi, is there a paper or repository where to find more details about the technical aspects of formalizing real analysis which you encountered, or, more generally, which you are aware of. Typically, if ever someone comes and asks about advices on formalizing analysis in a proof assistant, to what kind of source can we direct them to help them to have a clear overview of the impact of this or that formalization choices (such as using filter or not, etc.)?

Yes! The development is available here: https://github.com/siraben/math-3100/blob/master/analysis.v , I only use the stdlib

Ben Siraphob said:

Yes! The development is available here: https://github.com/siraben/math-3100/blob/master/analysis.v , I only use the stdlib

Thanks. Don't know what is your conclusion though. Would it somehow be that, at least in the current state of advancement of proof assistants and libraries, an outsider willing to formalize analysis has to eventually prepare to a long and difficult road? Or is it a too caricatural view at it?

@Hugo Herbelin I'm not really concluding anything, just speaking from my experience in terms of wanting to formalize introductory analysis results but running into the inadequacy of the stdlib (which is well known) but seeing that the alternatives (mathcomp-analysis and coquelicot) would take some time to get used to due to their abstractions or proof style.

@Ben Siraphob I would say that it is the expectation of a standard library to be "adequate". Maybe there is no good solution at the moment to provide a standard library about analysis that fits all needs but since several people are working on libraries for analysis (such as math-comp and coquelicot) any hints on how to get the ideal library are welcome (whether it is about the choice of structures, the naming policy, the automation, the extent, the ability to compute, etc.)

Actually, I'm dreaming that one day, when you go to http://coq.inria.fr/distrib/current/stdlib, what you see is a browsable structured collection of all standard contents available in Coq (e.g. from the platform), with informed comments on the design choices of each library!

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

How to teach analysis using a theorem prover is an interesting question. I have tried it (using Lean, not Coq, but probably a lot of what I say goes over) by writing down my own definitions several times in the past and it is pretty horrible, because you can't use any library stuff and it's all done with filters in the library and probably in far more generality than one needs.

I have more recently tried a different approach. Here you do not make your own definitions. You simply say "well Lean/Coq has a definition of what it means for a sequence to tend to a limit, and I am not going to show you the internal definition, but here is the theorem that it's equivalent to the definition which you'll read in the textbooks" (we have this theorem in the Lean maths library and if you don't have it in exactly the form you want in Coq then of course you just prove it yourself and hide the proof away in an import). That way you have access to all the API and tactics but the students can still see that they're working with the definition they understand. I agree that Riemann integration is painful in dependent type theory; we just use Lebesgue integration in Lean.

Kevin Buzzard said:

I have more recently tried a different approach. Here you do not make your own definitions. You simply say "well Lean/Coq has a definition of what it means for a sequence to tend to a limit, and I am not going to show you the internal definition, but here is the theorem that it's equivalent to the definition which you'll read in the textbooks"

That's the approach in mathcomp-analysis: internally filters are used, but if you do not "unfold" you do not see it, and you can use equivalent phrasings if you are working inside a normed vector space for example.

Last updated: Sep 09 2024 at 06:02 UTC