Huỳnh Trần Khanh (Aug 04 2022 at 08:03): Huỳnh Trần Khanh (Aug 04 2022 at 08:03):Hello! This community surely has many competitive programmers, right? Where are you? Hint: if 1000000007 and 998244353 look familiar to you, you are a competitive programmer.
I am thinking about making a repository of formalized competitive programming code. I think Coq is a suitable language for this work. I know this is quite open ended, but could you give me advice on how to carry out this project?
A formalized KACTL might be a good idea. Competitive programmers are known for being quite creative. You can give me some other project ideas as well.
Alexander Gryzlov (Aug 04 2022 at 12:25):I'm actually not that familiar with competitive programming, but do you have in mind the kind of algorithms and theory you typically need for these tasks? I'm assuming it involves some number-theoretical tricks and pointer manipulation at the least, is that right?
Huỳnh Trần Khanh (Aug 04 2022 at 15:09):It is possible to solve all competitive programming problems without pointers and this is what most people do anyway. Check out https://usaco.guide for the most accurate information on competitive programming.
We do use some NT tricks but nothing advanced. Every high school student knows them.
The most important algorithm that competitive programmers use is brute force. You read that right. Before using more advanced techniques, we often write simple brute force programs to find properties hidden in the problem. These programs are also used to verify the correctness of a more efficient implementation. Of course, if we are strong enough to know the right algorithm for the problem, we implement it right away without brute forcing to explore the problem.
As figuring the algorithm is often much harder than implementing it, I think Coq is helpful for competitive programmers. Coq teaches us mathematical intuition. With Coq, we can prove theorems about the problem that might lead to a full solution.
Karl Palmskog (Aug 04 2022 at 17:34):one general piece of advice is to consider carefully if programs in Coq related to competitive programming are to be executed/evaluated or not [inside Coq as well as outside]. Depending on the libraries that people use, this may be really difficult (e.g., if a function depends on a well_founded proof that is opaque)
Karl Palmskog (Aug 04 2022 at 17:36):also, it's very likely that competitive programmers will find QuickChick useful
Karl Palmskog (Aug 04 2022 at 17:38):MathComp verified programs are usually represented in such a way as to make proof as easy as possible, and then one uses a refinement library like CoqEAL to make an equivalent program "faster" for evaluation
Malcolm Sharpe (Aug 05 2022 at 05:14):I used to be active in competitive programming, but I'm brand new to Coq, so I have no advice to give. I think competitive programming problems might make good exercises for formal verification, because they tend to have precise specifications and short but tricky solutions. That said, I hadn't thought of doing it in Coq, since the solutions express themselves most naturally in more C-like languages, but I'm ignorant of Coq's capabilities at that sort of programming.
Karl Palmskog (Aug 05 2022 at 08:55):some formalization problems by the creator of Isabelle is making the rounds, maybe useful for competitive stuff: https://lawrencecpaulson.github.io/2022/08/03/Small-Challenges-I.html
Huỳnh Trần Khanh (Aug 05 2022 at 09:43):Could I ask one quick question. QuickChick is bundled with Coq Platform, but because it depends on the OCaml compiler, I have to install the Coq Platform from source to use QuickChick right?
Huỳnh Trần Khanh (Aug 05 2022 at 09:44):And after installing the Coq Platform from source, I could use QuickChick immediately. Is that correct.
Huỳnh Trần Khanh (Aug 05 2022 at 09:45):I tried out a QuickChick command without installing anything except the Coq Platform. And the command was recognized, but I got an error saying that ocamlbuild was not found.
Li-yao (Aug 05 2022 at 10:28):Yes it must be from source, and if it doesn't work immediately after that you can complain here on Zulip or here https://github.com/QuickChick/QuickChick/issues/269
G Host (Aug 05 2022 at 11:33):https://github.com › mit-plv › fiat-cr...
mit-plv/fiat-crypto: Cryptographic Primitive Code Generation by Fiat - GitHub
Wtf am I seeing
G Host (Aug 05 2022 at 11:35):Ik little to nothing as to how to code yet I can only know when things are off. Someone help
Paolo Giarrusso (Aug 05 2022 at 16:42):@G Host we can’t tell what is the problem
Last updated: Oct 13 2024 at 01:02 UTC