please die `existsi`

Stream: general

[Kevin Buzzard]

I don't want to have to teach existsi, Rob wrote use precisely because existsi had some problems which mathematicians were running into. But I still know this one use case:

def h := ∃ (x : ℕ), x = x

example : h :=
begin
  -- use _, -- fails
  existsi _, -- Oh, says the student, it actually wants a *nat*"
  -- actual use case was `I.fg` for `I` an ideal
  repeat {sorry },
end

Is there a reason why use _ can't work?

[Johan Commelin]

Is refine ⟨_, _⟩ a suitable alternative?

[Anne Baanen]

What happens if h is reducible? Update: it results in the same error.

[Eric Rodriguez]

What if there is a nat in the local context?

[Anne Baanen]

use 0 works, use _ doesn't.

[Eric Rodriguez]

Or if the target type is an instance and its in the local context?

[Eric Rodriguez]

ok, even that fails.

[Eric Rodriguez]

seems to be deliberate: image.png

[Eric Rodriguez]

I guess it's like apply in that you can't always make it guess so well, because use ⟨0, rfl⟩ solves the goal

[Gabriel Ebner]

We've recently had a thread about this but I can't find it anymore (searching for use returns a lot of unrelated results as you might imagine).

[Gabriel Ebner]

The reason use _ doesn't work is because given the goal ⊢ ∃ x : ℕ × string, true you can use both use 1 "2" as well as use (1, "2") iirc.

[Kyle Miller]

I usually use tactic#fsplit for the use _ use case. It's the "split and preserve order" tactic.

[Gabriel Ebner]

I believe a few people, including me, thought that this special case is too surprising and not worth it.

[Arthur Paulino]

@Gabriel Ebner is this the discussion you're talking about?

This is how it was implemented in Mathlib4:

use e₁, e₂, ⋯ applies the tactic refine ⟨e₁, e₂, ⋯, ?_⟩ and then tries
to close the goal with trivial (which may or may not close it). It's
useful, for example, to advance on existential goals, for which terms as
well as proofs of some claims about them are expected.

[Kevin Buzzard]

Oh the refine solution works great for me