Patrick Nicodemus (Dec 02 2021 at 17:24): Patrick Nicodemus (Dec 02 2021 at 17:24):Say that I want to prove A and B are isomorphic.
Is there a tradeoff between trying to define the map from A to B by writing it out in detail in Gallina vs constructing it in proof mode as a term of type A -> B? Is one of these recommended in general?
For me tactic mode is certainly easier as it lets me build the function interactively line by line and the goal reminds me what I am trying to construct, it seems much harder to write the function correctly in straight Gallina without the assistant. But I am wondering if the use of tactics causes problems later on, perhaps the handwritten function is simpler than the term constructed using tactics and simpler to reason about, i.e. to prove it has an inverse.
Gaëtan Gilbert (Dec 02 2021 at 17:30):there is a little discussion of this in the hott style guide https://github.com/HoTT/HoTT/blob/master/STYLE.md#17-transparency-and-opacity
Paolo Giarrusso (Dec 02 2021 at 17:43):Would it be desirable for the stdlib to conform to this list? This came up very recently and was apparently controversial (cc @Hugo Herbelin )
Hugo Herbelin (Dec 02 2021 at 18:13):Would it be desirable for the stdlib to conform to this list?
Indeed, conforming to this list may address the argument of proof stability and resolve the controversy. (Also, just wondering, in some cases, copy-pasting the resulting proof term once it is proven with the help of tactics might also work?)
Paolo Giarrusso (Dec 02 2021 at 18:19):Copy-pasting the proof term is indeed my preference, if it's readable enough. If not, you probably have bigger problems :-)
Hugo Herbelin (Dec 02 2021 at 18:20):If not, you probably have bigger problems
Most probably yes!
Paolo Giarrusso (Dec 02 2021 at 18:29):I guess another tradeoff, both for @Patrick Nicodemus's question and for our discussion in https://github.com/coq/coq/pull/15254, is about how much annoyance you accept for clients. Say you define f: A -> B and g: B -> A using tactics, and your proof that f (g x) = x must deal with the extra complexities. How much annoyance do you accept?
Paolo Giarrusso (Dec 02 2021 at 18:33):and how much unpredictability do you accept when updating your proofs? One school of thought is to only use "robust" features, so that the impact of changes is as predictable as in a conventional programming language. (Or as in mathematical proofs!).
Last updated: Oct 13 2024 at 01:02 UTC