I'm very new to Coq, hence the question :-) When using dependent types, is it considered "best practice" to use
As I understand it, there's a pretty compelling argument for liberally using
Program (e.g. the
match ergonomics alone) over raw
refine, but are there drawbacks that I'm not aware of?
Program both seem to me to make dependently-typed programming more ergonomic; is one preferred over the other in cases where both would work?)
there are very subtle tradeoffs between
Program. The latter is basically a whole "framework", while the former is just a tactic that can be used anywhere.
Equations is basically state of the art for any dependently typed programming in Coq right now, but it's a standalone plugin, while Program/refine are built in
Gotcha, many thanks @Karl Palmskog !
I tend to prefer
Program when I don't need something very complex, but there are some cases where Program doesn't work, e.g., I couldn't get it to recognize that a recursive call was on a subterm, while
refine is usually very predictable
another thing that
Program gives you for free are all the matching-term-equality facts (remember which branch was taken in a match so it shows up in the proof goal). Equations gives all that kind of stuff and also the kitchen sink
Actually, Program's match behavior is the first thing I disable (with Unset Program Cases.) before using it. It does have usecases, but it can cause a quadratic blowup in pattern-matching compilation (at least when using wildcards).
Moreover, that behavior is not something that I'd usually want to expose in a transparent definition. As a rule of thumb, if a definition is transparent, you want it to be elaborated predictably. Equations fixes that by hiding the definition and exposing only propositional equalities (and tactics to use them).
@Paolo Giarrusso how big functions do you have to have for the Program blowup to be noticeable? My maximum is usually about three matches deep with maybe 5-10 branches each, so I don't think I've ever noticed it.
7 * 2 is apparently enough:
that combines (1) wildcard matches (they make the blow-up worse) (2) well-founded recursion — that alone makes it almost necessary to write unfolding lemmas by hand, using the semi-documented
I think those
_ are probably hiding 20+ cases in that example
I tried to count the constructors — 7 ( https://github.com/TiarkRompf/minidot/blob/master/ecoop17/dsubsup_total_rec.v#L28-L40 ) and 2 (https://github.com/TiarkRompf/minidot/blob/master/ecoop17/dsubsup_total_rec.v#L55-L60)
I haven't looked at that code in 3 years, and I did manage to get acceptable performance with some effort
I had little clue what I was doing, and I could do much better now
but relative to what's explained by e.g. Software Foundations or the manual, I'm confident on not blaming the authors.
but also, Equations fixes almost all the complaints I had.
also, that Fixpoint could have been written with
refine for sure, with some extra boilerplate
with well-founded recursion?
I'm sure so, and one of my colleague from Paris 7 did it, but it didn't look too pleasant
only nitpick on Equations: it used to use
Opaque for definitions, but you'd often want stronger sealing (no def. eq.) in these cases.
I mean, there's nothing stopping you from declaring
Fixpoint fp (x : Y) : bla. refine ( ). Defined.
but to be clear, my point is _not_ "never use Program", just that it has footguns and Equations has fewer ones.
@Karl Palmskog I'm confused on what
fp is showing — I'm aware of
refine, but that example uses
Program because it uses well-founded recursion.
if your point is
I couldn't get it to recognize that a recursive call was on a subterm, while refine is usually very predictable
I can reassure you that function isn't structurally recursive. I had to recheck, but here it's because it's calling locally-nameless's
open on the type it is recursing into:
ah, I guess I would have defined that one using
BTW just for completeness, beyond tactic-based definition (
refine), the use of
Equations (the recommended approach in most cases, as you said), there is also
Function (https://coq.inria.fr/refman/using/libraries/funind.html?highlight=function#coq:cmd.function), which is the other built-in way to define non-structural recursive functions with a measure or more generally by well-founded recursion, but it is less powerful than
Equations, but it might by handy in some simple cases...
Last updated: Feb 04 2023 at 21:02 UTC