Agda-like "refine" tactic in Coq

In Agda, one can build up an expression piece-by-piece, by repeatedly using the “refine” Emacs command (C-c C-r).

It’s not possible to write Gallina interactively in this manner in Coq. However, something similar can be achieved in Coq’s proof mode/Ltac mode.

With Coq’s refine tactic, one can write an arbitrary expression, leaving underscores for holes to be filled in later. It has the same name as Agda’s “refine” tactic, and superficially seems similar. However, there is a very important difference.

First of all, if you leave a hole for a variable which appears in the type of another hole, Coq will not create a subgoal to allow you to fill in that variable. As of Coq 8.5, there is a simple resolution for this problem: there is a tactic called simple refine which will create the subgoal regardless. And more generally, one can prefix any tactic invocation with unshelve to force the tactic to make subgoals for the evars that it creates.

But there is a second issue: any hole that you leave inside of a refine expression will be passed to Coq’s inference mechanisms, which can be arbitrarily agressive (essentially due to typeclasses). If you leave several holes in your expression, it is likely that you are leaving the inference problem underconstrained, and that Coq will make a “wrong” choice.

Here’s a simple concrete example where simple refine goes wrong: Refine.v Github Gist.

The above file also shows what the solution is: use unshelve eapply rather than simple refine. I believe unshelve eapply is the closest thing in Coq to Agda’s “refine”.