Type theory construct

Stream: new members

[Dan Stanescu]

Trying to formalize some notes by Pete Clark on filters I came up with a question mark. The problem is exemplified in the code below, which I tried to keep to a minimum. Basically the principal_filter definition needs a proof that the set is not empty. If I try to use it later in principal_of_finite, I want to obtain that there is such nonempty set, but then how do I feed that back into the same statement later on? In other words, how to fill the _ in the lemma statement?

import data.set.basic
import order.filter.basic
import tactic.basic

namespace peteClark

-- A filter is a non-empty collection of non-empty subsets of X with the following properties:
structure filter (X : Type) :=
( f_sets          : set (set X) )  -- a collection of subsets of X
( f_nonempty      : f_sets.nonempty )
( f_mem_nonempty  : ∀ (A : set X), A ∈ f_sets → A.nonempty )
( f_mem_inter_in  : ∀ (A B : set X), A ∈ f_sets ∧ B ∈ f_sets →  A ∩ B ∈ f_sets )
( f_container_in  : ∀ (A B : set X), A ∈ f_sets ∧ A ⊆ B →  B ∈ f_sets )
( f_univ_in              : set.univ ∈ f_sets )

variables {X : Type}

-- Example: a principal filter
def principal_filter (Y : set X) (hY : Y.nonempty) : filter X := sorry -- code not shown
variables (Xf : Type) [fintype Xf]

lemma principal_of_finite (F : filter Xf) :
   ∃ (Y : set Xf), Y.nonempty ∧ principal_filter Y _ = F :=   -- the underscore here??
begin                                                            -- should be the Y.nonempty from the first part
   sorry,                                                         -- of the conjunction
end


end peteClark

This is probably not a desirable situation in type theory. I guess it's better not to ask for Y.nonempty in principal_filter, and that can easily be taken care of. I'm just wondering if there is a way to proceed in this setting. Any help appreciated!

[Bryan Gin-ge Chen]

Maybe you want:

lemma principal_of_finite (F : filter Xf) :
   ∃ (Y : set Xf), ∃ (hY : Y.nonempty), principal_filter Y hY = F

[Dan Stanescu]

I guess that is what I wanted! Thanks @Bryan Gin-ge Chen

[Bhavik Mehta]

Dan Stanescu said:

( f_mem_inter_in  : ∀ (A B : set X), A ∈ f_sets ∧ B ∈ f_sets →  A ∩ B ∈ f_sets )
( f_container_in  : ∀ (A B : set X), A ∈ f_sets ∧ A ⊆ B →  B ∈ f_sets )

By the way, you can write these as A ∈ f_sets → B ∈ f_sets → A ∩ B ∈ f_sets and A ∈ f_sets → A ⊆ B → B ∈ f_sets which is sometimes easier to work with in practice!

[Dan Stanescu]

That one I knew, but I'm writing these to be legible by someone with zero knowledge of type theory.

[Dan Stanescu]

Or functional programming.

[Dan Stanescu]

Thank you both!

[Patrick Massot]

Having both f_nonempty and f_univ_in in the definition is a bit silly. Those conditions are equivalent using f_container_in. And in pratice f_univ_in is much more convenient both when constructing filters and when using the definition.

[Patrick Massot]

I'm almost sure you know but just to make sure: mathlib doesn't put f_mem_non_empty in the definition of filters. So your definition is not equivalent to the definition in mathlib. Both choices have pros and cons, but mathlib's version is far superior in the long run (this is probably irrelevant to whatever you are trying to do).

[Dan Stanescu]

@Patrick Massot Thanks and agreed! I eventually default to mathlib's version in my proofs. This was just me playing around preparing some formalization notes. Actually P. Clark doesn't have f_univ_in in his definition, it just got there after I considered a few variants and I forgot to remove it. Then he only considers proper filters, there you go for f_mem_non_empty.

[Dan Stanescu]

@Patrick Massot As a follow-up question, we don't seem to have nets in mathlib. Would it make sense to add them?

[Patrick Massot]

If you plan to eventually use mathlib filters then you probably shouldn't put that properness condition in your main definition.

[Patrick Massot]

You are right that we don't have nets in mathlib. It seems that, beyond the illusion of familiarity that they provide at first, they are simply inferior to filters in every aspect. There is no harm in adding an isolated file nets.lean, but I don't think we should start duplicating everything in those terms. Our topology library is already pretty big hence difficult to navigate.

[Dan Stanescu]

Patrick Massot said:

If you plan to eventually use mathlib filters then you probably shouldn't put that properness condition in your main definition.

Just making sure, proper filters in mathlib are those F such that F ≠ ⊥ --- ?

[Yury G. Kudryashov]

Yes, and many theorems assume F ≠ ⊥.

[Yury G. Kudryashov]

As far as I understand, the main reason to deal with ⊥ is to have a complete_lattice structure.

[Kevin Buzzard]

It also enables you to do pushforwards and pullbacks (or map and comap as they're called in lean)