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.

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

Would it be desirable for the stdlib to conform to this list? This came up very recently and was apparently controversial (cc @Hugo Herbelin )

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?)

Copy-pasting the proof term is indeed my preference, if it's readable enough. If not, you probably have bigger problems :-)

If not, you probably have bigger problems

Most probably yes!

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?

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: Jan 31 2023 at 14:03 UTC