mem_image

Stream: mathlib4

[Yury G. Kudryashov]

I think that this was discussed some time ago but I can't quickly find the thread. What do you think about removing @[simp] from lemmas like docs#Set.mem_image and moving it to lemmas like docs#Set.ball_image_iff and docs#Set.biUnion_image ?

[Yury G. Kudryashov]

IMHO, in case of docs#Set.mem_image, docs#Set.mem_range, and docs#Set.mem_image2, the RHS is not simpler than LHS.

[Yury G. Kudryashov]

Also, this creates simp confluence issues when we have something like ⋃ y ∈ f '' s, g y but there is a simp lemma for ⋃ x ∈ s, _ that stops Lean from applying docs#Set.iUnion_iUnion_eq_right

[Eric Wieser]

I think this was discussed before, perhaps pre-lean4. It would be good to find the old thread.

[Yury G. Kudryashov]

I tried and failed.

[Yaël Dillies]

I'm a priori not super happy with such a change, but good alternative simp lemmas could convince me otherwise.

[Yaël Dillies]

My hunch is that a lot of proofs of the form by ext; simp will break.

[Yaël Dillies]

For confluence on ⋃ y ∈ f '' s, g y, I would think this just means that we're missing simp lemmas for ⋃ mimicking the basic logic ones

[Yury G. Kudryashov]

We do have docs#Set.iUnion_iUnion_eq_right but it doesn't work if Lean can simplify x ∈ s. The same happens in a simpler case:

import Mathlib.Data.Set.Lattice

example {f : ℕ → ℕ} {s t : Set ℕ} :
    (∀ y ∈ f '' (s ∩ t), y = 0) ↔ ∀ x ∈ s ∩ t, f x = 0 := by
  simp
  guard_target =ₛ (∀ y x : ℕ, x ∈ s → x ∈ t → f x = y → y = 0) ↔ ∀ x ∈ s, x ∈ t → f x = 0

example {f : ℕ → ℕ} {s t : Set ℕ} :
    (∀ y ∈ f '' (s ∪ t), y = 0) ↔ ∀ x ∈ s ∪ t, f x = 0 := by
  simp -- success

example {f : ℕ → ℕ} {s : ℕ → Set ℕ} {t : Set ℕ} :
    (∀ y ∈ f '' (⋃ i ∈ t, s i), y = 0) ↔ ∀ x ∈ ⋃ i ∈ t, s i, f x = 0 := by
  simp
  guard_target =ₛ (∀ (y x x_1 : ℕ), x_1 ∈ t → x ∈ s x_1 → f x = y → y = 0) ↔
    ∀ (x x_1 : ℕ), x_1 ∈ t → x ∈ s x_1 → f x = 0

example {f : ℕ → ℕ} {s : ℕ → Set ℕ} {t : Set ℕ} :
    (∀ y ∈ f '' (⋂ i ∈ t, s i), y = 0) ↔ ∀ x ∈ ⋂ i ∈ t, s i, f x = 0 := by
  simp -- success

[Eric Wieser]

Here's one old message I found:

Gabriel Ebner said:

Another one that annoys me greatly is Set.mem_image, which I always have to disable because what I actually want is Set.ball_image_iff.

[Eric Wieser]

And another

Sebastien Gouezel said:

By the way, is this really a good simp lemma? It turns something into an existential, which is not very good as a normal form because it is hard to manipulate (Lean will almost never be able to guess the right y to discharge such a proof obligation).

[Yaël Dillies]

We certainly can try removing it

[Yury G. Kudryashov]

I'll try after #9275

[Kyle Miller]

I'm wondering if this is suggesting a different design for "cute" binders. For example, if we had a separate notation and definition for bounded quantifiers

def BForall {α β : Type*} [Membership α β] (dom : β) (p : (x : α) → Prop) : Prop :=
  ∀ x, x ∈ dom → p x

macro (priority := high) "∀ " n:ident " ∈ " s:term ", " p:term : term =>
  `(BForall $s (fun $n => $p))

-- LHS is `BForall (Set.Icc 0 1) fun x ↦ x < 2`
#check (rfl : (∀ x ∈ Set.Icc 0 1, x < 2) = (∀ x, x ∈ Set.Icc 0 1 → x < 2))

then we could be sure that Set.ball_image_iff would get applied rather than Set.mem_image.

The tradeoff would be needing specialized lemmas for handling BForall as well as potentially needing to modify tactics to be BForall-aware. While intro would be able to see through it for example, intros would not...

[Yury G. Kudryashov]

Do you suggest introducing BForall, BExists, Set.biUnion etc?

[Mario Carneiro]

another alternative is for simp to just "get good" at handling forall x, (exist y, x = f y) -> P x simplification. Isabelle is able to simplify this using a simpproc

[Kyle Miller]

@Yury G. Kudryashov Yeah, that's the suggestion. It's just an idea I thought I'd mention which didn't seem immediately bad. I came up with it because it's something I noticed is necessary when making a framework for binders over different types of containers -- not everything can use the nesting trick, for example Finset.sum can't, and it's easier to handle when binders have both a raw type for the bound variable along with some object representing its domain.

I'm not suggesting this very seriously though.