Zulip Chat Archive

Stream: maths

Topic: rfl lemma


view this post on Zulip Thomas Browning (Dec 23 2020 at 21:47):

The lemma adjoin_empty in field_theory/adjoin is actually a rfl-lemma. Is it worth making a PR?

@[simp] lemma adjoin_empty (F E : Type*) [field F] [field E] [algebra F E] :
  adjoin F ( : set E) =  :=
eq_bot_iff.mpr (adjoin_le_iff.mpr (set.empty_subset _))
@[simp] lemma adjoin_empty (F E : Type*) [field F] [field E] [algebra F E] :
  adjoin F ( : set E) =  := rfl

view this post on Zulip Patrick Massot (Dec 23 2020 at 21:52):

There is no problem at all with PRs that are easy to review.

view this post on Zulip Bryan Gin-ge Chen (Dec 23 2020 at 22:04):

@Mario Carneiro once gave some reasons why we shouldn't replace all possible proofs with rfl when possible; not sure whether that advice applies in this case though.

view this post on Zulip Mario Carneiro (Dec 23 2020 at 22:05):

The question is whether the defeq can be proven using only "public" defeq facts

view this post on Zulip Mario Carneiro (Dec 23 2020 at 22:07):

I think it is fair to say that bot = empty = {x | false] is public, but I don't know much about adjoin

view this post on Zulip Mario Carneiro (Dec 23 2020 at 22:09):

Looking around it seems like you have to dig through many layers to get this result, so I would say that it shouldn't be public

view this post on Zulip Mario Carneiro (Dec 23 2020 at 22:10):

it seems like adjoin_le_iff is the API for adjoin

view this post on Zulip Eric Wieser (Dec 23 2020 at 22:53):

Using rfl vs not affects whether dsimpapplies this lemma, right?


Last updated: May 12 2021 at 07:17 UTC