Understanding equality on Filter

Stream: mathlib4

[Esteban Martínez Vañó]

Hi everyone.

How does the proof of #filter_eq works?

In general, if you have a class where one field is the "base set" for the class, how can you prove that two terms of that class type are equal when the underlying sets are equal?

Thanks in advance for the answers.

[Patrick Massot]

All fields of the Filter structure except for sets are propositions so their values are equal by definition when you have two filters, and the Lean kernel knows this. That’s why the proof is so automatic.

[Patrick Massot]

The usual approach to such proofs is to use the ext attribute to auto-generate the proof. The reason why we don’t use it here is because we want the extensionality lemmas to be stated in terms of ∈ instead of .sets.

[Patrick Massot]

You can read documentation about the ext attribute at https://github.com/leanprover/lean4/blob/ffac974dba799956a97d63ffcb13a774f700149c/src/Lean/Elab/Tactic/Ext.lean

[Esteban Martínez Vañó]

I see.

So, for example, if I define the following class

@[ext]
class PFilter {X: Type*} (A: Set X) extends Filter X where
  point : Set X
  point_eq : point = A
  point_in : A ∈ sets

I know how to prove the lemma

lemma eq {X: Type*} (A: Set X): ∀ (F G: PFilter A), F.sets = G.sets → F = G

using the ext tactic, but how can it be proven if we don't use it?

[Kevin Buzzard]

You can do cases on F and G to start

[Patrick Massot]

As Kevin wrote, this kind of proof works by hitting everything in sight with cases. You can use rcases do recursively doing cases (that’s what the r stands for). You get

lemma eq {X: Type*} (A: Set X): ∀ (F G: PFilter A), F.sets = G.sets → F = G := by
  intros F G h
  rcases F with ⟨⟨A, B, C, D⟩, b, c, d⟩
  rcases G with ⟨⟨A', B', C', D'⟩, b', c', d'⟩
  dsimp at h
  subst c c' h
  rfl

This kind of proof is painful to write by hand everywhere, hence the existence of the ext attribute gadget.

[Patrick Massot]

And I hope your definition of PFilter is only an reduced version of your actual definition because otherwise it is a very bad idea.

[Esteban Martínez Vañó]

I see. I didn't know how to recover all the fields of F and G, but now I see it is by using rcases.

Everything understood. Thanks!

Patrick Massot ha dicho:

And I hope your definition of PFilter is only an reduced version of your actual definition because otherwise it is a very bad idea.

It is a dismiss definition because I've seen it is not worth it as some results (like the ones about the membership relation on filters) are not inferred and it is simplier to just take the desired element in a filter. Is that the reason it is a bad idea or are there more reasons? :sweat_smile:

Anyway, I think the doubt was interesting and, although I've dismissed the definition, I still wanted to know how it can be done.

[Patrick Massot]

The bad idea is to have a field point and immediately ask it is nothing but the parameter A. This point field is pure noise. But I guess the actual definition you have in mind is more interesting.

[Esteban Martínez Vañó]

Yes, it is not a good idea, and indeed that's now what I really wanted to express.