Idiomatic `use`

Stream: general

[Martin Dvořák]

I regularly use use when the goal starts with an existential quantifier.
Is it idiomatic to use use outside of plugging terms into existential quantifiers, too?
Or should refine be used in the other cases?

[Michael Rothgang]

Can you use use for goals not of the form \exists ...? This is the first time I learn about this.
I would find it quite surprising and consider it not-so-readable style.

[Michael Rothgang]

Or are you asking about using use as opposed to absorbing this into a refine on the next line?

[Michael Rothgang]

In my opinion, use a is certainly nicer than refine ⟨a, ?_⟩. On the other hand, I may preferrefine ⟨a, pf_a, b, ?_⟩ over use a; refine ⟨pf_a, b, ?_⟩. (Of course, these should be two lines; I'm using the semicolon for brevity.)

[Martin Dvořák]

Michael Rothgang said:

Can you use use for goals not of the form \exists ...?

import Mathlib.Tactic.Use

example (p : P) : P ∧ (3 + 2 ≤ 7) := by
  use p
  decide

[Michael Rothgang]

TIL, thanks! I'm not sure if I find this more readable than \<p, by decide\>.

[Martin Dvořák]

Yours is better.

I wanted to ask about situations where it is desirable to write either use p or refine ⟨p, ?_⟩ in the tactic mode because the proof continues with a sequence of tactics. Of course, I prefer use p when it is for an existential quantifier, but I am not sure which tactic is better when dealing with a conjunction whose LHS can be easily proved by a term but RHS is more complicated.

[Ruben Van de Velde]

I'm slightly inclined towards refine for that case

[Edward van de Meent]

i believe that what is "idiomatic" relies a lot on context; for example, for goals of the shape ∃ x, P x ∧ Q x, i personally am ok writing use x, hpx...

[Kyle Miller]

I don't see any problem using use here. I also think it's fine using use for any one-constructor type (it's designed for that after all).

[Jakub Nowak]

Kyle Miller said:

I don't see any problem using use here. I also think it's fine using use for any one-constructor type (it's designed for that after all).

The hover documentation suggests it's only for exists though. It could maybe at least include an example of using it with something else then Exists, if that's the intention?

[Kyle Miller]

Yeah, it would be nice if the docstrings were updated. When I made the current use/use! in #5350, I didn't think about how it would give the impression it's only for existentials.

In #32699, @Mirek Olšák's added a Nonempty example at least. This docstring change points out a convenient feature I'm not sure I was even aware of, where use will apply a Nonempty constructor for free — no need for use!.