Zulip Chat Archive

Stream: new members

Topic: Subset of subset


view this post on Zulip Thomas Browning (Jul 29 2020 at 23:46):

If B : set C, and A : set B, how do you get (a version of) A in set C?

view this post on Zulip Adam Topaz (Jul 29 2020 at 23:51):

Try something like subtype.val '' A

view this post on Zulip Yury G. Kudryashov (Jul 30 2020 at 03:45):

We recently decided that the simp-normal form is coe, not subtype.val.

view this post on Zulip Yury G. Kudryashov (Jul 30 2020 at 03:45):

So, (coe '' A : set C)

view this post on Zulip Eric Wieser (Aug 08 2020 at 10:13):

By this, you mean that we should never type subtype.val or x.val in a proof or lemma?

view this post on Zulip Reid Barton (Aug 08 2020 at 11:41):

No, this is much too strong. Just don't use it in the statement of a simp lemma, especially on the left-hand side. You might find it useful to avoid using it in other places too.

view this post on Zulip Kevin Buzzard (Aug 10 2020 at 12:09):

@Eric Wieser do you know about simp normal form? The idea is that if you want to get simp working for you, you should know what the form is which the lemmas are trying to normalise towards. The idea is that when your goal is in the "right" form when you can just apply standard theorems, but all the theorems need to be stated in the "right" form too. So you need to make some design decision about what all your lemmas will look like, and then try and stick to this notation in the middle of proofs.


Last updated: May 16 2021 at 05:21 UTC