Christian Doczkal (Jul 02 2021 at 07:57): Christian Doczkal (Jul 02 2021 at 07:57):Topic for the first presentation
Reynald Affeldt (Jul 02 2021 at 08:47):@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!
Laurent Théry (Jul 02 2021 at 09:20):ok I don't have alzheimer ;-)
Reynald Affeldt (Jul 02 2021 at 09:23):well, it's not exactly 30 years ago though, but MIzar's stuff is even older
Reynald Affeldt (Jul 02 2021 at 09:25):
Ben Siraphob (Jul 02 2021 at 09:42):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
Reynald Affeldt (Jul 02 2021 at 09:46):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
Cyril Cohen (Jul 02 2021 at 09:47):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).
Meven Lennon-Bertrand (Jul 02 2021 at 10:21):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
Ben Siraphob (Jul 02 2021 at 12:35):@Reynald Affeldt Ah, I wasn't aware that one could use math-comp without using ssreflect in full, sounds useful.
Hugo Herbelin (Jul 02 2021 at 13:08):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
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.)?
Ben Siraphob (Jul 02 2021 at 13:09):Yes! The development is available here: https://github.com/siraben/math-3100/blob/master/analysis.v , I only use the stdlib
Hugo Herbelin (Jul 02 2021 at 13:32):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?
Ben Siraphob (Jul 02 2021 at 17:20):@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.
Hugo Herbelin (Jul 02 2021 at 22:57):@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!
Ben Siraphob (Jul 03 2021 at 02:06):@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.
Kevin Buzzard (Jul 05 2021 at 14:17):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.
Cyril Cohen (Jul 05 2021 at 14:39):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