Zulip Chat Archive

Stream: general

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


view this post on Zulip Eric Wieser (Mar 29 2021 at 10:48):

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.

view this post on Zulip Johan Commelin (Mar 29 2021 at 10:49):

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

view this post on Zulip Johan Commelin (Mar 29 2021 at 10:49):

But I agree that the pattern you describe makes sense.

view this post on Zulip Gabriel Ebner (Mar 29 2021 at 11:27):

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 ....

view this post on Zulip Eric Wieser (Mar 29 2021 at 11:31):

Do you object to my suggestions in that PR then?

view this post on Zulip Gabriel Ebner (Mar 29 2021 at 11:40):

I added a comment to that effect on the PR.

view this post on Zulip Eric Wieser (Mar 29 2021 at 11:47):

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

view this post on Zulip Gabriel Ebner (Mar 29 2021 at 11:57):

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

view this post on Zulip Eric Wieser (Mar 29 2021 at 12:18):

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

view this post on Zulip Gabriel Ebner (Mar 29 2021 at 12:20):

It doesn't hurt to open an issue.

view this post on Zulip Damiano Testa (Mar 29 2021 at 12:31):

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.

view this post on Zulip Gabriel Ebner (Mar 29 2021 at 12:33):

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

view this post on Zulip Damiano Testa (Mar 29 2021 at 12:35):

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

view this post on Zulip Damiano Testa (Mar 29 2021 at 12:35):

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

view this post on Zulip Damiano Testa (Mar 29 2021 at 12:37):

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.


Last updated: May 15 2021 at 02:11 UTC