Transparent has_mem instance

Stream: general

[Patrick Massot]

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]

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]

@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]

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]

@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]

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]

So the lemma is not affected by the change.

[Johan Commelin]

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

[Patrick Massot]

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]

Does it make sense?

[Johan Commelin]

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

[Johan Commelin]

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

[Patrick Massot]

I never used erw

[Johan Commelin]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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