Zulip Chat Archive

Stream: general

Topic: simp lemma for subtype.property


Johan Commelin (Feb 26 2019 at 08:50):

Should this be a simp lemma in mathlib?

import data.subtype

universe u

@[simp] lemma val_prop {X : Type u} {S : set X} (x : {x // x  S}) : x.val  S := x.property

Mario Carneiro (Feb 26 2019 at 08:51):

I'm not sure if it will work right as a simp lemma, but you are welcome to try

Kenny Lau (Feb 26 2019 at 08:52):

I would prefer this:

import data.set.basic

universe u

@[simp] lemma val_prop {X : Type u} {S : set X} (x : S) : x  S := x.property

Mario Carneiro (Feb 26 2019 at 08:52):

I'm guessing that the unfolding of x : S was performed by dsimp

Mario Carneiro (Feb 26 2019 at 08:53):

the simp lemma should be something that is in simp normal form already

Kenny Lau (Feb 26 2019 at 08:53):

only if you do dsimp *

Kenny Lau (Feb 26 2019 at 08:53):

how about we include both S and {x // x in S}

Kenny Lau (Feb 26 2019 at 08:54):

is x.val in simp normal form or \u x?

Mario Carneiro (Feb 26 2019 at 08:54):

I think they are both valid

Kenny Lau (Feb 26 2019 at 08:54):

so we have 4 versions!

Mario Carneiro (Feb 26 2019 at 08:54):

I don't think S vs {x // x in S} affects simp applicability

Kenny Lau (Feb 26 2019 at 08:55):

you're right

Kenny Lau (Feb 26 2019 at 08:55):

so 2 versions

Johan Commelin (Feb 26 2019 at 08:57):

I've succesfully applied the current version in the perfectoid project. I'll prepare a PR that adds both versions to data/subtype.


Last updated: Dec 20 2023 at 11:08 UTC