Zulip Chat Archive

Stream: general

Topic: Transparent has_mem instance

Patrick Massot (Mar 06 2019 at 15:52):

Following conversation in Amsterdam, I'm trying to use the instance instance {α : Type*}: has_mem (set α) (filter α) := ⟨λ U F, U ∈ F.sets⟩ so that, if F is a filter on α, and U a subset of α then we can write U ∈ F as we do on paper. But this leads to huge mess of failing proofs in filter.basic because s ∈ F is not syntactically equal to s ∈ F.sets, although it is defeq. Is there anything I could do to improve this? Should I give up on having this instance? It would be very sad, because this s ∈ F.sets reads really weird

Patrick Massot (Mar 07 2019 at 15:19):

I was too pessimistic. It turns out that marking the instance as reducible goes a long way towards solving those issues. I'm working on it

Patrick Massot (Mar 07 2019 at 18:02):

@Johannes Hölzl I did it! https://github.com/leanprover-community/mathlib/pull/799 This was super tedious work, but the result looks great.

Patrick Massot (Mar 07 2019 at 18:03):

I think this will bring less conflicts than moving stuff around, but it should still be merged pretty quickly if we don't want any inconvenience.

Johan Commelin (Mar 18 2019 at 12:01):

@Patrick Massot I still see .sets here: https://github.com/leanprover-community/mathlib/blob/e8bdc7fc14c6d56d4040892d16929f310e9d03d5/src/order/filter/basic.lean#L415-L417
Is that because removing it causes some breakage?

Johannes Hölzl (Mar 18 2019 at 18:34):

The change only added a instance to filter. But in the proposition, sets is used for the projection from filter to set. While in the proof the .sets notation is required for the rewrite.

Johannes Hölzl (Mar 18 2019 at 18:34):

So the lemma is not affected by the change.

Johan Commelin (Mar 18 2019 at 18:44):

Aah, so this is not made "transparent" by some coercion.

Patrick Massot (Mar 18 2019 at 19:25):

I'm not sure which .sets you are talking about. In the statement of the lemma, it's clearly needed. The notation is not a generic one like or , it specifically means set.Union. So the binded expression must be a set, a filter is not good enough. In the show at beginning of the proof, the situation is different. Here we are indeed fighting the rigidity of rw, which really work on the syntactic level: a transparent instance of a defeq quantity is not good enough. This problem is almost hidden in this change because I changed almost all definition and statements to use this has_mem instance, so almost everything is syntactically what we want. This is why it was crucial to make the replacement everywhere at once. The only exceptions arise in statements like the one we pointed out where we really want to talk about the sets of a filter, and not talk about something belonging to these sets.

Patrick Massot (Mar 18 2019 at 19:25):

Does it make sense?

Johan Commelin (Mar 18 2019 at 19:27):

I think it makes sense. I find that erw can often succeed when rw fails.

Johan Commelin (Mar 18 2019 at 19:27):

Also, would a coercion help to get rid of the .sets in the statement?

Patrick Massot (Mar 18 2019 at 19:27):

I never used erw

Johan Commelin (Mar 18 2019 at 19:28):

Because statements like these will introduce .sets and then it doesn't compose nicely with all the statements where you did remove the .sets

Patrick Massot (Mar 18 2019 at 19:28):

Coercions rarely help in delicate situations. We are already happy when they work in situations that look straightforward

Johan Commelin (Mar 18 2019 at 19:28):

Hmm... never mind. A coe wouldn't solve that.

Johan Commelin (Mar 18 2019 at 19:29):

Ok... my confusion is cleared up. Thanks!

Last updated: Aug 03 2023 at 10:10 UTC