Zulip Chat Archive

Stream: general

Topic: subset refl weirdness

Reid Barton (May 04 2018 at 18:47):

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
  @has_subset.subset.{?l_1} (list.{?l_1} ?m_2) (@list.has_subset.{?l_1} ?m_2) ?m_3 ?m_3
α : Type,
s : set.{0} α
⊢ @has_subset.subset.{0} (set.{0} α) (@set.has_subset.{0} α) s s

Reid Barton (May 04 2018 at 18:52):

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

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

Simon Hudon (May 04 2018 at 18:53):

You're probably right. You can try:

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

Simon Hudon (May 04 2018 at 18:53):

Then your proof will work

Reid Barton (May 04 2018 at 18:58):

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

Kevin Buzzard (May 04 2018 at 22:01):

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 (May 04 2018 at 22:03):

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 (May 04 2018 at 22:10):

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

Chris Hughes (May 05 2018 at 19:59):

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

Last updated: Aug 03 2023 at 10:10 UTC