I am aware that coq users have been writing verifications of proofs. I would like to see how they looks like in specific subjects, particularly analysis. Are there any such files around ?

https://github.com/huynhtrankhanh/CoqCP/blob/main/docs/RepeatCompare.md https://github.com/huynhtrankhanh/CoqCP/blob/main/theories/RepeatCompare.v

This is a fun proof that's quite easy to read

There are many Coq packages under the coq-community organization https://github.com/orgs/coq-community/repositories

corn and coqtail-math might interest you

the most actively developed library for analysis in Coq these days is likely MathComp Analysis: https://github.com/math-comp/analysis

Wait. @Heime what do you call "writing verifications of proofs"? Usually people write "proofs" in coq format, and coq verifies.

I mean the files in coq-format that verifies a proof. Would like to see them verify

specific theorems.

https://madiot.fr/coq100/ - has links to Coq files stating and proving many well-known theorems

How would one order them in terms of importance ?

Perhaps like this

- MathComp Analysis
- Corn
- Coqtail Math

Wondering whether verifying a new proof requires coq programming. Does one need to program coq functionality, then call them when devising the proof verification ?

@Karl Palmskog Could coqtail-math start having version numbers ?

You don't need to change Coq code at all

BTW when you're learning a new field that's so different from what you're familiar with you should expect your mental model and your preconceptions to be wrong

Like you said "verification of proofs", I don't know what that means and other community members don't either

What do you describe the process of proof verification using the coq system ?

what process are you referring to exactly?

writing proofs, or running completed proofs?

The process of having machine-checked proofs of theorems. What do you call such a process ? In my view there are two aspects

- Writing the theorem in some coq format
- Writing the commands that machine-checks its proof

Having proofs isn't a process

These questions indicate that you haven't even tried the very basics yet. Writing the theorem statements in Coq is more or less identical to what you would write in math using logical symbols. Writing the proofs in Coq is very different since Coq uses a special language ("tactics") for proofs. There is no separate verification process, or at least, there isn't any such process that you need to worry about at this stage. Coq verifies the proofs for you automatically as you go along.

As you write the proof, Coq verifies it. If the proof does not verify successfully, then you have not written it correctly. You seem to think that writing and verifying proofs are separate processes. They are not, at least, not as far as you're concerned.

Yes, quite identical but with text such as "forall" that is specific to coq. Yes. Coq uses tactics which you can run. The tactics provide a proof, not like a proof in a mathematical book, but a proof nonetheless. If I want to verify one of my proofs on a new topic, I might need to write some coq tactics myself, am I right ?

I never write "forall" in my proofs, I just write ∀, which means the same thing (assuming you have loaded the Utf8 package) but looks more normal to a mathematician.

Verifying a proof doesn't require you to do anything other than run Coq on your file.

"coqc file.v" and you're done. This assumes that you've written the proofs in file.v correctly.

I can write a proof in terms of tactics, but that does not mean that it verifies successfully.

Correct, in a way, but I would argue that in that case you haven't written a "proof"

to write a "proof" means that the proof verifies correctly. Otherwise it is not a proof.

Put another way, running coq on a coq proof is not fundamentally any different from running gcc on C code

if your so-called proof does not verify then I would call it a failed attempt at a proof, not a proof

(in the same way that C code with a syntax or type error isn't really C code)

UTF8 is just about rendering, but the actual source code is "forall", is that right ?

no

If you want to get started with proofs, I recommend http://michaeldnahas.com/doc/nahas_tutorial -- yes, it is old, and out of date, but so what? It at least focuses on proofs, whereas most other introductory Coq documentation starts with computation.

The actual source code file contains the UTF8 character ∀. The Utf8 package aliases this character to "forall"

now please, go start working through some tutorials. Asking questions is useless if you don't ever actually use the system.

I think of all this differently. You describe a theorem that coq can interpret. You come up with a proof that has not been machine verified yet. You then come up with a new proof that has been machine verified. You might also need to write new constructs and tactics as well before being able to have a verification to succeed.

It's really obvious that you have never used Coq. What you are describing is perhaps theoretically possible, but completely alien to anyone who uses Coq. We don't use Coq that way!

What actually happens is: we have a proof. It is not machine verified. We break it down into small steps that we think we can individually achieve on the machine. We then write each small step on the machine, first one step, then the next, then the next, and so on. As we go along, we check what we write. Almost never does it work the first time. We look at what Coq says and then we change our proof, adjust, refine, improve, until that small step succeeds. Then we do the next step. After many hours, days, or weeks, we have a complete proof. It is an interactive, back-and-forth process. There is not a separate concept of proofs and verification. Both go together hand in hand simultaneously.

I use emacs, I do write "forall" and not the UTF symbol.

it doesn't matter really what you write, as long as Coq can read it. The larger point stands. Your mental model is wrong.

@djao I understand it as you described. You have a proof you think does work, but then use your computer to be sure each step is successful. If not successful, you make the changes. When the steps succeed, you have the proof that you stick with.

Suppose I have some proof for a new wavelet transform technique. Would coq have all the tactics I need ? That's my question.

You can get very far in Coq without ever needing to write new tactics. If you do encounter a situation where you need to write new tactics, hopefully you are advanced enough in Coq to know how to do that.

It seems very odd to be asking such questions when you haven't even learned the very basics.

If one never wrote new tactics, is there some manual to learn ? Can't one just start straight away - learning coq and learning how to write tactics at the same time ?

Do you know any programming languages at all? When you're learning C, do you need to write language extensions? Yes, perhaps, at some point, but that point is very far from the beginner level. Start at the beginner level and work your way up from there. It is the same with everything else.

It's just absolutely bizarre for anyone to be worrying about this at the very start of their journey.

Some books do cover the tactical language alongside the Coq language, for example http://adam.chlipala.net/cpdt/ (which you should feel free to read); however in my experience these books tend to focus more on computation and software verification than on mathematical proofs.

How long does it normally take to use coq without knowing how to write any tactics ? I am unsure whether my work is too advanced for coq to handle. And therefore would need to do more work myself. Do you know if there are any libraries listing proofs involving signal analysis, fourier and wavelet transforms ? Am quite fed up working with toy problems such as arithmetic and logic.

I really doubt that your problem is tactics. Tactics are never *necessary*. In theory you can write any proof using lambda calculus proof terms. Almost always the problem is that math itself is hard to formalize.

Hard to formalise for a machine to understand ?

If you are unable to progress beyond simple arithmetic and logic, new tactics are not going to magically allow you to make further progress.

You have to understand the problem domain much more deeply than you think in order to formalize a proof, tactics or no tactics.

I really need to see how people handle proofs from calculus, particularly integral equations.

You have to train in order to climb the mountain. Yes, there is a risk that no matter how hard you train the mountain will be too hard.

People have already pointed you to many existing libraries containing hundreds if not thousands of examples of proofs. A library is just a collection of proofs. Look inside the source code. Look for the word "Proof."

https://github.com/math-comp/analysis/blob/master/theories/lebesgue_integral.v Here's another place to start. Dozens of occurrences of "Proof." in that file.

There are thousands, but I want to focus on topics that would actually be of use to me.

The formal proofs community is only a small fraction the size of the larger mathematical community. It is possible, indeed likely, that your specific niche has not been covered yet.

First you ask simply for examples of proofs (which we have given), and now you want proofs that are of use to you (which we do not have).

That's my worry, that it could well be that it has not been covered sufficiently for me yet.

well, I must admit, I have no interest in wavelets, so you are on your own here. I will say that you have no chance of accomplishing anything with Coq until you start actually using it.

You cannot learn formal proofs from book reading. You have to DO THE PROOFS. And if the only proofs you do are simple arithmetic and logic proofs, then that is all you will ever be able to do.

I asked for examples of proofs in analysis - thinking about special functions and integral equations.

The entire mathcomp-analysis library is about analysis.

It might not be your particular brand of analysis, but it is analysis.

If you insist on only working through examples in your specific niche area, you probably are at a dead end.

Fine then. I was curious to know how far people have got on topics close to my area and what to expect in terms of work and effort.

It's possible that your topic did not attract the people who might know about your field though. You could try asking in the #math-comp analysis stream about what people think of what you are considering formalising and whether it seems achievable to them.

Heime said:

Karl Palmskog Could coqtail-math start having version numbers ?

Coqtail does have version numbers, they are based on Coq's version number such as `8.14`

and `8.18`

. See https://github.com/coq/opam/tree/master/released/packages/coq-coqtail

See also https://github.com/coq-community/awesome-coq and in particular for learning resources: https://github.com/coq-community/awesome-coq?tab=readme-ov-file#books

I am not familiar with the topic of integral equations but as a contributor to MathComp-Analysis it looks to me that there are enough special functions and integration theory to at least get started, there are a few papers available online about Lebesgue integration in MathComp-Analysis and these lecture notes that I definitely should be working on https://staff.aist.go.jp/reynald.affeldt/documents/karate-coq.pdf

@Reynald Affeldt is there any landing website/repository for those lecture notes or is the PDF the canonical reference? (Looks useful to link from Awesome Coq)

this is the canonical reference (there was a short homepage for the lecture but the pdf there is not updated)

I think the only thing that needs to be said is: coq provide an INTERACTIVE mode (coqtop) that allows to develop the proof interactively. Virtually no one develops coq proofs without it. coqc is basically a silent coqtop which generates .vo files that can then be loaded as libraries by coqtop and coqc.

@Reynald Affeldt I was looking to avoid getting started randomly because I could easily waste too much time on things that would be irrelevant to me to think about. For instance, I do not want to delve into mathematical topics to understand the framework before getting to follow a proof.

@Pierre Courtieu I agree fully with that assertion. It is quite easy to understand.

@Karl Palmskog If I click upon coq-coqtail.8.18, there is no way to download the source.

https://github.com/coq-community/coqtail-math/releases/tag/8.18 which has this archive: https://github.com/coq-community/coqtail-math/archive/refs/tags/8.18.tar.gz

@Karl Palmskog You should include the version number in the readme and not have the users figure out what version is it.

So it is coqtail-math rather than coq-coqtail. It is very confusing if one does not clean things up.

I'm afraid you won't get anywhere with that attitude. Not wanting to delve into mathematical topics is the opposite of what is needed to use a proof assistant.

`coqtail-math`

is the name of the repository. `coq-coqtail`

is the name of the *opam package*. The repository has the name `coqtail-math`

to distinguish it from this unrelated project: https://github.com/whonore/Coqtail

Coq uses the opam package manager to distribute code. Version numbers are used primarily for/in opam.

From what I understand, some people use UTF8 characters in the actual source code. But then in reality, some UTF package in coq would convert to actual words such as forall. Correct ?

It's like #define in C.

@djao That is how the old school mathematicians used to function. But for some of us, mathematics is not done for mathematical interest or knowledge, but to get some job done. I cannot just pick any topic and simply delve into it for no work benefit.

Can you be a bit more precise about your goal?

@djao If you open your files with a text editor without UTF capability, do you see forall or an unrecognised glyph ?

Hard disagree. I use mathematics for a job (cryptography). I could not do this without deep knowledge of the involved mathematics. If you don't need deep knowledge, then you also don't need proofs, and you would have no reason to be here in the first place, since the only purpose of Coq is to provide the proofs.

A mathematical proof is not needed if you only want to use the mathematics to get a job done and for no other purpose.

For your UTF8 question, I assure you, the bits in the file are UTF8. I'm not sure what exactly would happen in a "text editor without UTF capability" since opening a UTF8 file in such a text editor would result in undefined behavior.

My interests are on topics that have engineering value particularly about signal processing. Thus areas such as Fourier Analysis, Wavelet Decomposition, Special Functions, Functional Analysis, Linear Algebra, Probability. Lot of other mathematical topics are simply disregarded and I put no effort into them (e.g. logic, arithmetic, booleon algebra, geometry, algebraic structures, topology, and so on). And I do not teach, no courses, no anything - just normal work like other people.

the whole topic about character encoding and meaning of glyphs has been discussed in the literature many times before, see for example http://cs.ru.nl/~freek/pubs/rap.pdf - the short answer is that proof assistants are generally not "safe" against symbol confusion and trickery. But professionals will easily find these issues if serious audits are done.

see https://math.andrej.com/asset/data/formalizing-invisible-mathematics.pdf#page=16 for the general proof assistant workflow

I think it is simply not tenable to claim interest in formal proofs while also claiming no interest in logic. This stance is self-contradictory.

@djao Right because you require traditional mathematics. I am not in cryptography. We do need to come up with proofs because I work on the development of algorithms. Otherwise an algorithm becomes useless. I also don't care about publication. Our work areas are too far apart.

It is logically (!) impossible to prove anything without logic.

I don't care where or what you work on.

@djao You should think about it some more. Godel told you about the limits of logic, which many people today fail to comprehend. They heard about it but failed to understand its meaning. David Hilbert was wrong !

@djao Stop everything you're doing, and go through the limits of provability in axiomatic theories. The world does not work like that. Ramanujan also knew this but did not need a proof to convince himself.

That's why one should bow down to Ramanujan.

I don't need to convince you of anything. I have given you good advice, if you don't take it then I am done giving advice.

I feel like a doctor in an insane asylum where the patients think they are normal and the doctor is crazy. Ramanujan was right, you are wrong.

Looks like you don't need my advice. That's totally fine.

I just do not need to go through many proofs on logic and other toy problems. Just wanted to see the work already done on topics in my area and focus on that so I can extend them. I got some links to specific libraries, which could be helpful. But general discussions are not focused enough for me to entertain.

@Karl Palmskog The Yves Bertot article is fantastic. Thank you for that.

One thing is for sure. The ANSSI is correct in its statements about accountability - as we at the Gnu Project have been telling the world for decades.

maybe relevant that we also wrote an article on the Coq Platform, which is the official distribution of Coq together with many plugins and libraries such as MathComp-Analysis

@Karl Palmskog Very relevant actually. Of importance is the Coq Test Suite. Are there relatively simple tests categorised by mathematical topic ? Not only for purposes of compatibility, but also as a way for users to use those tests in a way that aids their experience writing and understanding coq proofs and their requirements. Such a test scheme would be of great benefit to everyone. With the added benefit of not requiring so many people asking beginning level questions. Users could then focus more an real problems involving new work instead.

as partly explained in the paper, there are many "test suites" for Coq.

- first there are the many small-scale tests that are run for essentially every commit to the
`coq`

repository: https://github.com/coq/coq/tree/master/test-suite - second, there is Coq's CI, which consists of many third-party plugins and libraries that are continually tested in the
`coq`

repository: https://github.com/coq/coq/tree/master/dev/ci - third, there is the Coq Platform CI, that continually tests Coq Platform packages (not necessarily with the
`master`

branch of Coq): https://github.com/coq/platform/actions

Then also most serious individual projects use CI based on the official Coq Docker images

the `test-suite`

is organized by topic, but not necessarily "mathematical domain". The Coq Platform breaks down packages by topic for example here

I find the possibility of criticism here particularly on the word "many". This is just a gentle comment about having a basic general mathematics test suite (categorised in a few categorisations in pure and applied mathematics ), not too big or small, and which is customarily unchanging. And with all needed libraries provided.

it can be argued that MetaCoq is the greatest test devised for Coq itself (a formalization of Coq's calculus and type checking algorithm in Coq itself). However, MetaCoq doesn't currently drive Coq, it's downstream of Coq.

our general view is that anyone who wants to use Coq for mathematics should start from the Coq Platform, and from there branch out as needed into even more specialized libraries that are available on `released`

part the Coq opam archive (and then possibly further into libraries "in the wild" on GitHub, GitLab, etc.)

Heime said:

Karl Palmskog Very relevant actually. Of importance is the Coq Test Suite. Are there relatively simple tests categorised by mathematical topic ? Not only for purposes of compatibility, but also as a way for users to use those tests in a way that aids their experience writing and understanding coq proofs and their requirements. Such a test scheme would be of great benefit to everyone. With the added benefit of not requiring so many people asking beginning level questions. Users could then focus more an real problems involving new work instead.

Don't you mean examples? I don't think of tests as being aimed at users.

We have had a similar experience with emacs. As the thing got bigger and bigger, and as the old timers vanish, nobody can really figure it in its low level stuff. Big Problem.

@Gaëtan Gilbert Ok. Proof examples as a test suite for coq users before going into the wild. And possibly of use to some who may want to go beyond the normal use - so they can get some idea of what could be involved. But the scope must be quite contained for it to work out.

I mean there are people who learned how to use Ltac2 by reading the test suite

based on my observations, the consensus among Coq developers/researchers is that *interactively* working through highly organized "book-level" material (such as MCB and Logical Foundations) is the best way for new users to get started. Then there are more specialized tutorials and examples they can work through.

if you study through Software Foundations you might find this UI convenient https://coq.vercel.app/ext/sf/

that's what I used to learn Coq

the most productive thing for you to do right now is just go through Software Foundations and play with the exercises. the equivalent in Lean is the Natural Number Game

after going through introductory material you'll be better informed and can pose better questions

Think about this. If the Coq Platform could go a bit further and provide a specific example suite that people can use whose scope is not so basic. In this way, the transition towards specialised libraries and possibly further could became softer. This means that people could stay working with the Coq Platform tools a bit longer whilst getting their skills sharper. I am quite sure that the Coq Platform is better suited for this, because other libraries could have a diverse set of priorities which cannot be completely relied upon without getting unnecessarily confused at the start of the journey.

at the end of the day the math is hard :( I don't think there's much the Coq Platform can do

I feel the primary bottleneck is having the right proof strategy, the technical details of dealing with Coq are not as hard

If I am able to progress enough to my satisfaction, perhaps I could provide some useful things to make the process joyful.

I feel it's too early for you to talk about this

learn the basics first :)

we have discussed having "Platform tutorials" that show different combinations of techniques available through Platform packages. However, I think it's essentially niche content at this point, since most people get stuck earlier on more "trivial" things, such as UI and grappling with tactics and the specification language (Gallina)

@Karl Palmskog I see. Hopefully it will progress and become a useful and established way once the earlier blocks stop being a problem in future. From your description, generally people need to go through extremely simple proofs, otherwise they immediately get stuck.

Could be a long road till all this becomes mainstream. And I want to help as I find such an endeavor meaningful. To me at least. But to convince others - quite hard. Even harder to have them help me.

well, you usually need to go through very simple proofs *to know what to do to get unstuck*. The classic case is someone trying to formalize a pen-and-paper proof and failing deep inside the Coq proof attempt due to some small fact that should be obvious not holding.

if you are using some highly automated tactics, you then drop to more elementary tactics and find the smallest possible step where you fail, and that's typically where the missing piece becomes obvious

but more generally, just making the statement to prove in the "right" form can be very challenging. And if you state it in the wrong form, the difficulty of formal proof can increase several orders (e.g., take an order of magnitude longer to complete, minutes vs. days)

When I looked at it in more detail in 2019, proof assistant user productivity was not addressed in any serious way (compared to software developer productivity) in the literature (p. 214 in https://arxiv.org/abs/2003.06458)

I come from the industrial mathematics software engineering productivity. So at this point quite critical of the typical university mathematician. I find that they do a lot of mistakes and they get angry as they feel better than they actually are. Of course, they can be quite capable if they put their mind to it.

@Karl Palmskog I noticed that. The problems involved in getting to the "right form" required.

Heime said:

I come from the industrial mathematics software engineering productivity. So at this point quite critical of the typical university mathematician. I find that they do a lot of mistakes and they get angry as they feel better than they actually are. Of course, they can be quite capable if they put their mind to it.

Kevin Buzzard highlighted an example where the same math journal to this day has papers published that directly contradict each other, and you have to get access to a paywalled math paper review site to know which one is correct (slide 6-7 in https://www.andrew.cmu.edu/user/avigad/meetings/fomm2020/slides/fomm_buzzard.pdf)

Yes, I have talked to Kevin. I also have found many mistakes in publications - but few have talked about it. I have now stopped reviewing to concentrate on my own work only. Rather than read papers, it is more productive to work directly with others without spending time on peer-review publishing.

Today, I give this advice - if you have to get access to a paywalled math paper to know which one is correct, don't bother with it. Work on topics you can do without using paywalled papers, but work directly with the individuals involved. The current evolution of the university system will became extinct - it has no value even today.

as of right now, there are still very few employment opportunities outside academia to work with any of Coq, Lean, Isabelle, etc. (at least consistently)

It is my wish and my blessing for more opportunities for the energetic young ones. I am one of the old sods from the early 80's. You have the power today to go beyond our bull.

the free market is my ultimate judge :)

I don't want to be in academia. I feel formal verification has a lot of potential in the brutal free market

It is the future. I am all for free enterprise myself. Do what is important to you, the result is not up to you.

Last updated: Jun 13 2024 at 21:01 UTC