Zulip Chat Archive

Stream: general

Topic: subset refl weirdness


view this post on Zulip 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
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
-/

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Simon Hudon (May 04 2018 at 18:53):

Then your proof will work

view this post on Zulip Reid Barton (May 04 2018 at 18:58):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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]

view this post on Zulip 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: May 14 2021 at 04:22 UTC