set is too transparent

Stream: general

[Yaël Dillies]

It looks like set lemmas can rewrite goals with predicates in them. Here's a MWE minimized from #16435

import data.set.basic

example {α : Type*} {a : α} : (⊥ : α → Prop) a = ⊥ :=
begin
  rw set.bot_eq_empty, -- Why does this work?!?
  refl,
end

cc @Kyle Miller

[Eric Wieser]

Sounds like the same problem as the with_bot lemmas applying to option

[Reid Barton]

Here is a sort of "minimized" example, not involving type classes

def f {n : ℕ} (x : fin n → ℕ) : ℕ := 0
lemma f_def {x : fin 2 → ℕ} : f x = 0 := rfl

example {x : fin (1 + 1) → ℕ} : f x = 1 := begin
  rw f_def, -- succeeds; is that expected?
end

[Kyle Miller]

Here's an example as I ran into it, just to point out how docs#set.bot_eq_empty being a simp lemma leads to a breaking of the set API:

import data.set.basic

example (α : Type*) (x y : α) : (⊥ : α → α → Prop) x y = false :=
begin
  simp, -- simp only [pi.bot_apply, set.bot_eq_empty, eq_iff_iff, iff_false]
  -- ⊢ ¬∅ y
  -- (but we shouldn't see a `∅ y` term!)
  exact false.elim
end

[Kyle Miller]

I wonder if this has anything to do with the fact that implicit arguments are unified with semireducible transparency rather than reducible transparency? This doesn't explain Reid's example though.

[Gabriel Ebner]

Kyle's and Yaël's example are indeed due to the semireducible upgrade.

[Gabriel Ebner]

I'm not sure where Reid sees an issue in his example; note that 1 + 1 = 2 reducibly.

example : 1 + 1 = 2 := by tactic.reflexivity tactic.transparency.reducible

[Reid Barton]

Oh I just assumed that this needed to unfold some definition.

[Eric Wieser]

Which implicit argument is being made semireducible that's causing the issue?

[Reid Barton]

The arguments of has_bot.bot, I assume

[Gabriel Ebner]

⊥ has two implicit arguments: set α which is unfortunately defeq to α → Prop, and (by apply_instance : has_bot (set α)) which is defeq to (by apply_instance : has_bot (α → Prop)).

[Eric Wieser]

Would a gadget to tell simp not to reduce arguments help?

[Gabriel Ebner]

The gadget is called "make set a structure". :smile:

[Gabriel Ebner]

In Lean 4, simp will actually not apply that lemma because the discrimination tree filters it out. rw still has the issue though.

[Wrenna Robson]

I assume it would be quite a bit of work to make set a structure... but given the API is very developed, maybe not that much work?

[Wrenna Robson]

Like essentially anywhere where people apply a set as a predicate directly would break. But I assume in most places that doesn't happen.

[Anne Baanen]

You're not even supposed to do so anyway, so maybe this will actually be doable!

[Anne Baanen]

Although it will probably involve messing with the C++ code since set notation has its own custom parser.

[Yaël Dillies]

docs#set.boolean_algebra actually derives the instance from α → Prop. And I suspect this will be the same in other places too.

[Eric Wieser]

Making set a structure would mean that set_of (\mem s) = s is no longer true by definition

[Anne Baanen]

It would be true with definitional structure eta, right?

[Wrenna Robson]

What is definitional structure eta?

[Anne Baanen]

Older discussion, btw: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/with_top.20irreducible

[Wrenna Robson]

If set was a structure, maybe you could also change the definition of set_like so that set and finset both had set_like instances...

[Anne Baanen]

If you have an element x of some structure type, the equality (x.1, x.2, ...) = x, so constructing a new structure from the fields is just the original x, is called "eta reduction". Lean 4 will add this as a definitional equality, fixing many small annoyances.

[Wrenna Robson]

very nice