Patrick Nicodemus (May 16 2022 at 01:44): Patrick Nicodemus (May 16 2022 at 01:44):I have been trying to prove a theorem in Coq for about two weeks now, I am coming in on the home stretch now but I feel like it would take me two to three hours to prove this theorem in a fairly precise level of detail on pencil and paper. I have written something like 1500 lines of code in pursuit of this one theorem. Is excess verbosity a typical problem for neophytes that I should expect to grow out of?
I find the work very slow and tedious. I can prove theorems competently given enough time but the amount of time it takes and the amount of code I have to write makes it prohibitive to adopt coq as a tool in the long term. I am looking for advice on how to use coq more efficiently, concisely, etc.
Patrick Nicodemus (May 16 2022 at 01:46):I have written a little bit of automation in Ltac so far but not really anything more than
repeat(match goal with
| (a bunch of simplifications for the goal or hypothesis; or a bunch of lemmas related to some specific topic like natural number arithmetic
end)
and i only know what Ltac to write after i have already written it out "the long way", i.e. in a detailed way, so that i can see what the patterns are in the tactics, it is difficult to know how the process should be automated before you see it done a few times manually.
Patrick Nicodemus (May 16 2022 at 01:47):I plan to start learning about SSReflect next.
Patrick Nicodemus (May 16 2022 at 01:49):What are your best high level tips?
I would ideally like to get to the point where i can use coq as a symbolic computation tool kind of like sage or macaulay2 but with support for much more abstract concepts then like, finitely generated abelian groups or other things which can be finitely presented by generators and relations.
Karl Palmskog (May 16 2022 at 08:16):if you listen to presentations on how people formalize complicated mathematics, they usually report that they spend a lot of time planning out the theorems and proofs to formalize on "pen and paper" before they jump into code. For example, Hales completely reorganized his original pen-and-paper proof of the Kepler conjecture to be more amenable to formalization in HOL Light.
On a smaller scale, people write informal "blueprints" which states the math they are going to do in the right order and in sufficient detail to begin coding. For example, here is a blueprint Dahmen et al. did before they formalized the cap set problem in Lean.
Karl Palmskog (May 16 2022 at 08:25):so rather than any specific Coq code tips, I think it generally helps to spend more time during planning phase, and in particular, planning out in detail how to use third-party Coq libraries (or stdlib) for needed definitions/results.
Alexander Gryzlov (May 16 2022 at 12:44):Yeah I think the situation here is not that different from software engineering in the sense that you have to come up with good modular architecture allowing you to compose new things out of your and other people's previous work. So the theorems you need end up being some specific cases that "fall out" of the theory that you've created, like algorithms "fall out" of cleverly designed data structures.
Last updated: Sep 26 2023 at 12:02 UTC