Changing the implicitness of `∀ (x ∈ s)` binders

Stream: general

[Eric Wieser]

Right now, when lean sees ∀ (x ∈ s) it generates ∀ (x : X) (H : x ∈ s). I think it might be more useful to generate ∀ ⦃x : X⦄ (H : x ∈ s), since when it actually comes to applying the lemma chances are you will pass an _ as x. What do people think about this?

This came up when reviewing #6785.

[Johan Commelin]

I think it would be a major refactor to remove all the explicit variables pass around in mathlib (-;

[Johan Commelin]

But I agree that the pattern you describe makes sense.

[Gabriel Ebner]

I dislike the {x : X} (h : p x) pattern in general. I think it should always be (x : X) (h : p x). I often want to specify the element explicitly, so that Lean shows the correct goal for p x and I can then work on the proof for that subgoal (or use by simp or by ring, etc., on it).
Sometimes this works if x is left as a metavariable. But when it doesn't work, it's very cumbersome to work around using @ or show p x, from ....

[Eric Wieser]

Do you object to my suggestions in that PR then?

[Gabriel Ebner]

I added a comment to that effect on the PR.

[Eric Wieser]

Would you go as far as advocating for changing the implicitness of the binders in src#function.injective and src#set.inj_on?

[Gabriel Ebner]

I'd also prefer to make them explicit. We'll have them to change them in Lean 4 anyways, since ⦃⦄ is gone now.

[Eric Wieser]

Is that worth opening a github issue about, with a mathport tag?

[Gabriel Ebner]

It doesn't hurt to open an issue.

[Damiano Testa]

This may be an irrelevant comment, but sometimes, when working with sets and their members, using show_term on a solve_by_elim gives a term of the form hx x z and the x should not be there, since it is implicit. Is this also an issue with some implicit/explicit business? I can try to replicate an example, if needed, but do not have one at hand right now.

[Gabriel Ebner]

https://github.com/leanprover-community/lean/issues/394 ?

[Damiano Testa]

Exactly!

I decided to work an explicit example out and came up with exactly this:

lemma set_members {α : Type*} {s t : set α} (h : s ⊆ t) {x : α} (hx : x ∈ s) : x ∈ t :=
begin
  solve_by_elim,
end

[Damiano Testa]

Using show_term on solve_by_elim produces exact h x hx, which does not work, while exact h hx does.

[Damiano Testa]

In the general theme of this thread, I agree with Gabriel that often I want to tell Lean the element, before I supply a proof that it satisfies some property. This is mostly at the level of manufacturing the proof term, once that step is done, I can usually supply directly the proof. I sometimes leave explicit some assumptions that could be figured out by later ones, exactly for this reason. However, I am not sure what is the best strategy overall.