Joshua Grosso (Aug 27 2020 at 22:16): Joshua Grosso (Aug 27 2020 at 22:16):I'm very new to Coq, hence the question :-) When using dependent types, is it considered "best practice" to use refine or Program?
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?
Joshua Grosso (Aug 27 2020 at 22:19):(Relatedly: Equations and Program both seem to me to make dependently-typed programming more ergonomic; is one preferred over the other in cases where both would work?)
Karl Palmskog (Aug 27 2020 at 22:21):there are very subtle tradeoffs between refine and Program. The latter is basically a whole "framework", while the former is just a tactic that can be used anywhere.
Karl Palmskog (Aug 27 2020 at 22:22):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
Joshua Grosso (Aug 27 2020 at 22:23):Gotcha, many thanks @Karl Palmskog !
Karl Palmskog (Aug 27 2020 at 22:25):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
Karl Palmskog (Aug 27 2020 at 22:26):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
Paolo Giarrusso (Aug 28 2020 at 06:14):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).
Paolo Giarrusso (Aug 28 2020 at 06:18):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).
Karl Palmskog (Aug 28 2020 at 12:45):@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.
Paolo Giarrusso (Aug 28 2020 at 12:57):7 * 2 is apparently enough:
https://github.com/TiarkRompf/minidot/blob/master/ecoop17/dsubsup_total_rec.v#L494-L550
Paolo Giarrusso (Aug 28 2020 at 12:59):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 unfold_sub tactic
Karl Palmskog (Aug 28 2020 at 13:00):I think those _ are probably hiding 20+ cases in that example
Paolo Giarrusso (Aug 28 2020 at 13:01):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)
Paolo Giarrusso (Aug 28 2020 at 13:01):I haven't looked at that code in 3 years, and I did manage to get acceptable performance with some effort
Paolo Giarrusso (Aug 28 2020 at 13:02):I had little clue what I was doing, and I could do much better now
Paolo Giarrusso (Aug 28 2020 at 13:03):but relative to what's explained by e.g. Software Foundations or the manual, I'm confident on not blaming the authors.
Paolo Giarrusso (Aug 28 2020 at 13:03):but also, Equations fixes almost all the complaints I had.
Karl Palmskog (Aug 28 2020 at 13:04):also, that Fixpoint could have been written with refine for sure, with some extra boilerplate
Paolo Giarrusso (Aug 28 2020 at 13:05):with well-founded recursion?
Paolo Giarrusso (Aug 28 2020 at 13:05):I'm sure so, and one of my colleague from Paris 7 did it, but it didn't look too pleasant
Paolo Giarrusso (Aug 28 2020 at 13:06):only nitpick on Equations: it used to use Opaque for definitions, but you'd often want stronger sealing (no def. eq.) in these cases.
Karl Palmskog (Aug 28 2020 at 13:07):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.
Paolo Giarrusso (Aug 28 2020 at 13:09):@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.
Paolo Giarrusso (Aug 28 2020 at 13:13):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:
https://github.com/TiarkRompf/minidot/blob/master/ecoop17/dsubsup_total_rec.v#L445
Karl Palmskog (Aug 28 2020 at 13:16):ah, I guess I would have defined that one using well_founded_induction_type with refine.
Erik Martin-Dorel (Sep 11 2020 at 18:04):BTW just for completeness, beyond tactic-based definition (refine), the use of Program, or 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 Program and Equations, but it might by handy in some simple cases...
Last updated: Sep 26 2023 at 11:01 UTC