Huỳnh Trần Khanh (Sep 21 2022 at 10:15): Huỳnh Trần Khanh (Sep 21 2022 at 10:15):The "normal" tactic language in Coq is similar to what I am used to in Lean. By "normal", I mean the tactic language that is introduced in the first book of the Software Foundations series. However, Coq also has another tactic language called ssreflect. From what I've gathered, it is much shorter and much more concise, and it makes the development of math-comp much more efficient. Is this correct, and should I learn some ssreflect?
Huỳnh Trần Khanh (Sep 21 2022 at 10:17):Also, does "small scale reflection" mean I'll have to do a lot of metaprogramming? I honestly do not know what the term means, but reflection almost always means metaprogramming in other contexts.
Meven Lennon-Bertrand (Sep 21 2022 at 10:59):For your first question, it depends what you aim at. If you plan to use certain existing libraries, then the best idea is probably to learn whatever tactic language/proof patterns those libraries are using: libraries are often tailored for a certain proof style, and using that library with a different style is generally a source of subtle but annoying issues. Otherwise, especially if you are familiar with the "standard" Coq style due to your experience in Lean, I would advise to go with this style for now. Ssreflect definitely has advantages, but it also requires quite a bit of infrastructure and understanding that you might not want to set up yourself if you start in Coq.
Meven Lennon-Bertrand (Sep 21 2022 at 11:12):As for your second question, I’ll give it a try (maybe someone can give a better answer). The main idea of small scale reflection is to instrument two different ways to represent "truth", by switching between both in order to have the advantages of both. One representation is the "logical" one, using propositions, which is more structured. For instance, if you have a hypothesis A /\ B (/\ is logical and), then you can destruct it to obtain two hypotheses A and B. The second representation is more "computational", typically using booleans, and here you can instrument computation. For instance, if you have a hypothesis false || b = true (|| is boolean or), then by computation this simplifies to b = true without any need for reasoning. Ssreflect provides a lot of facilities to use both representations and switch between them, whenever required. So no, there is no need for metaprogramming, which usually comes with "large scale" reflection, where you implement complex bridges between logical and computational representations and decision procedures on the computational side.
Enrico Tassi (Sep 21 2022 at 13:00):If you want to know more you may look into https://math-comp.github.io/mcb/ and also into https://math-comp.github.io/documentation.html
Notification Bot (Sep 25 2022 at 08:52):Huỳnh Trần Khanh has marked this topic as resolved.
Last updated: Oct 03 2023 at 21:01 UTC