refine vs refine'

Stream: mathlib4

[Yaël Dillies]

Why do we have both refine and refine'? Why do we have to put interrogation marks before holes in refine now?

[Yaël Dillies]

Also, why am I see a handful of terminal refine' in mathlib4?

[Jireh Loreaux]

refine' is equivalent to Lean 3 refine.

[Yaël Dillies]

Why is it primed if we're going to use this one mainly?

[Jireh Loreaux]

In Lean 4, refine won't create goals for natural holes and will fail if it can't fill them in.

[Jireh Loreaux]

I use refine generally.

[Scott Morrison]

It's possible we'll even deprecate refine' after the port.

[Yaël Dillies]

But what is a natural hole? Why do we not want them?

[Jireh Loreaux]

It's nice because you can distinguish between holes you want goals for and holes Lean should fill.

[Jireh Loreaux]

?_ for the former and _ for the latter.

[Yaël Dillies]

So whatever the option, the refine syntax got longer?

[Johan Commelin]

Or put differently, whatever the option, the refine syntax got more precise.

[Thomas Murrills]

One user-side nice thing about refine vs. refine' is that you can name your goals to keep track of them in the tactic state as different cases, e.g. refine (?x, ?y)

[Thomas Murrills]

(Which is especially useful for clarity/interactivity if you have a few goals and the resulting types of those goals depend on each other, e.g. maybe one of your goals winds up with type ?x = ?y!)

[Michael Rothgang]

Is there a preference between using refine and refine'? For instance, is the latter a mathport-ism or did I dream this :wink: ? (If the latter, is this documented anywhere? I find it quickly.)

[Ruben Van de Velde]

refine' was added for mathport, yeah. I don't see a reason to use it for new code, but there's at least one person who seems to prefer it

[Eric Wieser]

Rarely the primed version is useful for when you want goals from implicit variables and don't want to add an @

[Scott Morrison]

I would prefer if we could remove refine'. Best not to have too many ways to say the same thing.

[Scott Morrison]

A few @s are not really worth another tactic to learn.

[Floris van Doorn]

Presumably you can also write refine my_lemma (implicitArg := ?_) (if the implicit argument is named)? (edit: this syntax is indeed allowed)

[Eric Wieser]

Does refine? know how to do that?

[Eric Wieser]

(assuming it actually exists)

[Eric Rodriguez]

refine? doesn't seem to exist, but I think it'd be really good to have!

[Floris van Doorn]

apply? gives refine suggestions. I doubt that it will get this syntax correct, but if it gets the lemma name, that's most of its usage anyway.

[Yaël Dillies]

refine' is really useful to build a refine call.

[Eric Rodriguez]

Floris van Doorn said:

apply? gives refine suggestions. I doubt that it will get this syntax correct, but if it gets the lemma name, that's most of its usage anyway.

Sometimes you already have a lemma ready, though

[Floris van Doorn]

If I already know what lemma I want to apply next, I never use apply? anymore. Do you?

[Eric Rodriguez]

no, but I would like to generate a full refine statement!

[Eric Rodriguez]

i.e. apply X works, but I want it as refine X ?_ _ ?_ ..., and sometimes with long lemmas that isn't the most fun thing to figure out:)

[Damiano Testa]

Does show_term do what you would like?

import Mathlib.Tactic

theorem X (a b c d : ℕ) : a + c = 0 := sorry

example (a b c d : ℕ) : a + c = 0 := by
  show_term apply X
  -- Try this: refine X a ?b c ?d

[Eric Wieser]

Unfortunately that fails for

import Mathlib.Tactic

theorem X (a : ℕ) {b : ℕ} (c d : ℕ) : a + c = 0 := sorry

example (a b c d : ℕ) : a + c = 0 := by
  show_term apply X
  -- Try this: refine X a c ?d

[Eric Wieser]

That sounds pretty fixable though

[Eric Wieser]

It works with set_option pp.analyze true in

[Damiano Testa]

Ah, we could have a syntax extension refine? X that does set_option pp.analyze true in show_term X.

[Damiano Testa]

Or maybe even fill_term! and fill_term, if you want/do not want implicit arguments to be made explicit.

[Eric Wieser]

Well, if you don't make the implicit argument explicit in this example it just fails.

[Eric Wieser]

Do you have an example where pp.analyze prints something different but both work?

[Damiano Testa]

macro "refine?" t:tacticSeq : tactic => `(tactic| set_option pp.analyze true in show_term $t)

example (a b c d : ℕ) : a + c = 0 := by
  refine? apply X
  -- refine X a (b := ?b) c ?d

[Damiano Testa]

Eric Wieser said:

Do you have an example where pp.analyze prints something different but both work?

I do not know...

The refine? macro uses your solution!

[Damiano Testa]

I edited the name above to be refine?, since it seems more in line with the naming conventions/expectations.

[Eric Wieser]

I think the feature request here is that the current refine' should be renamed to refine?, and should emit the diagnostics of your show_term!

[Damiano Testa]

So... simply renaming show_term! to refine?? :smile:

[Eric Wieser]

No, because there's also the request to remove refine', which would make show_term! refine' oh _ no stop working

[Eric Wieser]

apply isn't a substitute for refine'

[Damiano Testa]

Ok, though removing refine' seems like a much bigger PR than just adding refine?.

[Damiano Testa]

(besides, for the next several hours I will not be able to PR anything anyway!)

[Damiano Testa]

$ git grep "refine'" '*.lean' | wc
  12301  107506 1226928

I can look into this, but not soon.

[Jireh Loreaux]

Because no one seems to know this PR exists: Thomas started refine? in #8364

[Jireh Loreaux]

@Thomas Murrills see the discussion above.

[Mario Carneiro]

I would be opposed to removing refine' altogether, although I would be fine with a lint/style proscription against it. It is very useful when debugging proofs and "using lean in anger"

[Mario Carneiro]

I don't know whether there are any cases that actually need it though in a completed proof, unlike let' / have'

[Damiano Testa]

Given the PR that Thomas has, I will not then add a PR for the simple macro above: I am sure that dealing with edge cases would take a long time and it seems that Thomas has already invested quite a bit of effort into it!

And in the meantime, show_term is a good option that requires no further effort!

[Thomas Murrills]

Having refine? <tactic> is a really cool idea! However, I think some care ought to be taken before using this as a solution for the term version, where the syntax ought to be refine? <term>

Mainly, show_term has the unfortunate effect of instantiating _’s. In the middle of complicated proofs—exactly when we probably want to use refine?—terms might be really long, and we ought to use _ where possible. (As such, it also uses assignments produced by tactics which might come after refine?, which can be confusing.)

Further, as you anticipate @Damiano Testa, I found quite a few edge cases! :P show_term doesn’t seem to work in all cases, even with pp.analyze true: it gets delayed mvars wrong, for instance, and loses goals in type ascriptions. It also uses headBeta, which isn’t appropriate in this case, since we might accidentally put a ?_ in a function application position (where it then fails).

It also doesn’t seem to insert goals for unsynthesizable implicit arguments all the time? E.g. set_option pp.analyze true in show_term f ?_ _ where def f {A} : A → (p : Prop) → p := sorry.

[Mario Carneiro]

what does that print?

[Thomas Murrills]

refine f ?refine'_2 (a + c = 0)

[Thomas Murrills]

(Using the a + c = 0 example goal above)

[Mario Carneiro]

what's wrong with that?

[Thomas Murrills]

Can’t synthesize the implicit argument A (type of ?refine'_2)! :)

[Mario Carneiro]

oh so this is a pp.analyze issue?

[Thomas Murrills]

I’m not sure…I mean, if ?refine'_2 has a pre-existing type, it makes sense not to include it. I think maybe the issue is pp.analyze doesn’t know what refine needs, and that refine is creating (and needs to synthesize) this argument (and therefore needs it to be explicit to become a goal).

[Thomas Murrills]

Like, pp.analyze is happening “after the fact” (of refine') here

[Thomas Murrills]

Going back to the original topic for a sec: it seems like one way or another there’s interest here in making refine? insert implicit arguments!

[Thomas Murrills]

Currently #8364 is awaiting review, but tacitly regards turning implicit arguments into goals as a job for refine' (it only replaces unassigned syntactic _’s with ?_’s). I’d like to avoid delaboration if possible, but delaboration will be necessary in the presence of notation or macros. Still, maybe it would be best to only delaborate as a fallback.

[Thomas Murrills]

More broadly, I wonder if it would make sense to have custom delaborators to refinable syntax, which could be passed the necessary information on which mvars must be explicit for refine to work.