What are canonical examples for refine, _, ?_

Stream: new members

[Dan Abramov]

I roughly understand what these do:

• refine is like a more general version of apply / exact / use
• _ is like "try to fill this in using inference"
• ?_ is like "let me fill this in later as a goal"

However whenever I try to use them I tend to get a mess in the tactic state and give up. I'm not sure why that is (and unfortunately I don't have a ready example at the moment).

But I was wondering if there's a good crash course showing canonical examples for using them. I mean, like, literal two or three-liners that show "before" and "after" so that I can get a good intuition for when I'd want to reach for them. Right now I don't have an intuition for when they're most useful, so I end up not using them, and I feel like at this point it's a disadvantage for me.

Thanks!

[Dan Abramov]

I guess it would also be helpful to understand what they cannot do. For example in which case is _ placeholder possible to fill in? Also, where to look for documentation for these questions? It's very hard to google.

[Dan Abramov]

Also, which of these are compatible with which ones? E.g. is _ only usable with refine or also with apply? How about with exact? Is it usable with everything? What about ?_?

[Dan Abramov]

Also, is it possible to express use / exact / apply in terms of refine? I.e. do they "desugar" to refine? If yes, is this documented anywhere? It would be nice to not have to guess. I've seen this documentation but it doesn't give a clear complete picture, just a patchwork of concrete cases.

[Damiano Testa]

I would say that a terminal refine is almost the same as exact. If I remember correctly, there are situations where they cannot be replaced by one another, but they are "rare".

[Damiano Testa]

apply and refine are also close, but refine requires every explicit argument to be marked as _ or ?_, while apply tries to be more independent.

[Damiano Testa]

This comes with a cost, though: refine uses the type of the goal to unify, while apply tries on its own and then performs a check.

[Damiano Testa]

This leads to somewhat more common situations where one of apply or refine works, but not the other.

[Damiano Testa]

Finally, use x is pretty similar to refine \<x, ?_\>, though use tries a (very) little to solve the trivial leftover goal.

[Damiano Testa]

In general, it is almost never the case that two tactics can be replaced for one another: there are usually situations where one works but the other does not.

[Chris Bailey]

About _ and ?_: https://lean-lang.org/doc/reference/latest/Terms/Holes/#The-Lean-Language-Reference--Terms--Holes

About refine: https://lean-lang.org/doc/reference/latest/Tactic-Proofs/Tactic-Reference/#refine

There are certainly more expert users of refine here who may chime in, but I find it's very useful when you know the general structure of a proof and want to set up a sketch of it with the missing pieces marked as holes, or when you just want to be sure you're even going in the right direction ("does refine x ?_ y ?_ z ?_ ?_ work here as long as I can eventually fill in the holes or am I getting a type error", that kind of thing).

Very contrived example, but maybe illustrative if you imagine the principles applied to a more complex problem:

example (p q : Prop) (h1 : p → q) (h2 : q → p) : p ↔ q := by
  refine ⟨?mp, ?mpr⟩
  /-
  The state after refine tells you the remaining cases /obligations:
    case mp
    p q r : Prop
    h1 : p → q
    h2 : q → p
    ⊢ p → q
    case mpr
    p q r : Prop
    h1 : p → q
    h2 : q → p
    ⊢ q → p
  -/
  case mp => assumption
  case mpr => assumption

[Kyle Miller]

Damiano Testa said:

Finally, use x is pretty similar to refine \<x, ?_\>, though use tries a (very) little to solve the trivial leftover goal.

It's a bit more complicated than that — use a, b, c is like doing exact a; exact b; exact c with at most one constructor before and between the exacts, and then it does something like try trivial on remaining goals. The use! tactic modifies the strategy, where it can use constructor more than once.

[Kyle Miller]

@Dan Abramov I think the best source here might be to grep mathlib for these tactics and move your cursor around to inspect the before/after states. You'll see the patterns I think.

[Kyle Miller]

Dan Abramov said:

is it possible to express use / exact / apply in terms of refine

Yes, and furthermore, pretty much every tactic can be rewritten as refine in some way. Not a fixed refine of course, since tactics generally look at the local context and the goal to decide how to proceed, but there's some term you can use with refine.

constructor/use are similar, and are like using refine with an appropriate constructor expression with ?_'s per constructor field.

I see you noticed that _ works with apply. I personally think this is an oversight, but it's hard to fix at the moment. Only ?_ is really meant to be the way you create new goals. (The oversight is that apply turns all unassigned placeholders ("metavariables") into new goals.)

The relationship between exact and refine is that exact must close the goal.