Stream: Coq users

Topic: Using Gallina in formal mathematics


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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 )

view this post on Zulip 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?)

view this post on Zulip 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 :-)

view this post on Zulip Hugo Herbelin (Dec 02 2021 at 18:20):

If not, you probably have bigger problems

Most probably yes!

view this post on Zulip 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?

view this post on Zulip 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: Jan 31 2023 at 14:03 UTC