subset refl weirdness

Stream: general

[Reid Barton]

Is this a bug?

set_option pp.all true
example {α : Type} (s : set α) : s ⊆ s := by refl
/-
error: invalid apply tactic, failed to unify
  @has_subset.subset.{0} (set.{0} α) (@set.has_subset.{0} α) s s
with
  @has_subset.subset.{?l_1} (list.{?l_1} ?m_2) (@list.has_subset.{?l_1} ?m_2) ?m_3 ?m_3
state:
α : Type,
s : set.{0} α
⊢ @has_subset.subset.{0} (set.{0} α) (@set.has_subset.{0} α) s s
-/

[Reid Barton]

I guess this actually does not exist anywhere...?

@[refl] lemma set.subset.refl {α : Type u} (s : set α) : s ⊆ s := λ x, id

[Simon Hudon]

You're probably right. You can try:

local attribute [refl] set.subset.refl -- if that's the name of the appropriate lemma

[Simon Hudon]

Then your proof will work

[Reid Barton]

Ah, the lemma does exist in mathlib, but without @[refl]

[Kevin Buzzard]

The proof of a refl lemma is often rfl, and conversely any proof which is proved with rfl is I think automatically tagged @[refl], but because the proof wasn't rfl here the tag is needed.

[Simon Hudon]

rfl is only for reflexivity of equality and the tag comes from the fact that rfl implies that the two terms are definitionally equal. But if we're talking of reflexivity of other relations than equality, it doesn't imply anything with regards to definitional equality

[Kevin Buzzard]

I just tried my theory and the lemma I proved with rfl was tagged @[_refl_lemma] not @[refl]

[Chris Hughes]

@[refl] means it's a proof that a relation is reflexive and is for the refl tactic. @[_refl_lemma] means it's a proof of equality proved using rfl for the dsimp tactic.