Zulip Chat Archive

Stream: Is there code for X?

Topic: set.univ is \top


view this post on Zulip Eric Wieser (Nov 10 2020 at 13:38):

I ended up stuck with this as a subgoal, which was quite annoying:

example  (A : Type*) (a : A) : a  ( : set A) := sorry

The solution is set.mem_univ a, but neither simp nor library_search were able to find it. Should there be a lemma for this?

view this post on Zulip Anne Baanen (Nov 10 2020 at 13:40):

I'd like to see a @[simp] lemma : (⊤ : set A) = univ.

view this post on Zulip Eric Wieser (Nov 10 2020 at 13:53):

Looks like it was just forgotten, docs#set.bot_eq_empty` is there

view this post on Zulip Eric Wieser (Nov 10 2020 at 13:54):

I'll make a PR

view this post on Zulip Eric Wieser (Nov 10 2020 at 14:01):

#4963

view this post on Zulip Kevin Buzzard (Nov 10 2020 at 14:15):

I guess the "canonical form" for (⊤ : set A) is univ in the library. simp is usually something which proves equalities and <->s rather than random simple facts, I guess.

view this post on Zulip Eric Wieser (Nov 10 2020 at 14:24):

My reading was that simp has a second job, which is to turn things into canonical forms

view this post on Zulip Eric Wieser (Nov 10 2020 at 14:24):

(eg how we have docs#monoid_hom.to_fun_eq_coe)

view this post on Zulip Kevin Buzzard (Nov 10 2020 at 14:39):

Yeah you're dead right, and Anne's simp lemma is doing exactly that. I guess I'm saying that Anne's approach is the correct one for simp, rather than adding your original subgoal as a simp lemma.


Last updated: May 07 2021 at 21:10 UTC