contribute lemma to mathlib

Stream: general

[Bernd Losert]

Here is the lemma:

lemma ultrafilter_comap_set (f : X → Y) (A : set X) (𝒱 : ultrafilter Y) (h : f '' A ∈ 𝒱) :
∃ 𝒰 : ultrafilter X, 𝒰.map f = 𝒱 ∧ A ∈ 𝒰 := begin
  -- 𝒰 will be the ultrafilter generated by the filter base { (f ⁻¹' V ∩ A) | V ∈ 𝒱 }
  let B₀ : set X := f⁻¹' (f '' A) ∩ A,
  let ℬ : filter_basis X := {
    sets := { (f ⁻¹' V ∩ A) | V ∈ 𝒱 },
    nonempty := ⟨B₀, f '' A, h, rfl⟩,
    inter_sets := begin
      assume B : set X,
      assume B' : set X,
      rintro ⟨V : set Y, h₁ : V ∈ 𝒱, h₂ : f ⁻¹' V ∩ A = B⟩,
      rintro ⟨V' : set Y, h₁' : V' ∈ 𝒱, h₂' : f ⁻¹' V' ∩ A = B'⟩,
      let B'' := B ∩ B',
      use B'',
      split,
      have h' : f ⁻¹' (V ∩ V') ∩ A = B'', from calc
        f ⁻¹' (V ∩ V') ∩ A = (f ⁻¹' V ∩ f ⁻¹' V') ∩ A : by rw set.preimage_inter
        ... = (f ⁻¹' V ∩ A) ∩ (f ⁻¹' V' ∩ A) : by {ext, simp, tauto}
        ... = B ∩ B' : by rw [h₂, h₂'],
      exact ⟨V ∩ V', 𝒱.inter_sets h₁ h₁', h'⟩,
      simp [set.subset.rfl],
    end,
  },
  let ℱ := ℬ.filter,
  have : A ∈ ℱ := ℬ.mem_filter_iff.mpr ⟨B₀, ⟨f '' A, h, rfl⟩, set.inter_subset_right (f⁻¹' (f '' A)) A⟩,
  haveI : ℱ.ne_bot := begin
    rw ℬ.has_basis.ne_bot_iff,
    assume B : set X,
    rintro ⟨V : set Y, h₁ : V ∈ 𝒱, h₂ : f ⁻¹' V ∩ A = B⟩,
    rw (set.inter_comm (f⁻¹' V) A) at h₂,
    rw ← h₂,
    unfold id,
    rw ← set.image_inter_nonempty_iff,
    have : f '' A ∩ V ∈ 𝒱, from 𝒱.inter_sets h h₁,
    exact ultrafilter.nonempty_of_mem this,
  end,
  let 𝒰 := ultrafilter.of ℱ,
  use 𝒰,
  split,

  show 𝒰.map f = 𝒱, begin
    have : ∀ (V : set Y), V ∈ 𝒱 → f ⁻¹' V ∈ ℱ, begin
      assume V : set Y,
      assume hV : V ∈ 𝒱,
      rw filter_basis.mem_filter_iff ℬ,
      let B := f ⁻¹' V ∩ A,
      use B,
      split,
      show B ∈ ℬ, from ⟨V, hV, rfl⟩,
      show B ⊆ f ⁻¹' V, from set.inter_subset_left (f ⁻¹' V) A,
    end,
    have : map f 𝒰 ≤ 𝒱, from calc
      map f 𝒰 ≤ map f ℱ : filter.map_mono (ultrafilter.of_le ℱ)
      ... ≤ 𝒱 : by exact (filter.tendsto_def.mpr this),
    have : map f 𝒰 = 𝒱, from (𝒱.unique this),
    exact_mod_cast this,
  end,

  show A ∈ 𝒰, from filter.le_def.mp (ultrafilter.of_le ℱ) A (by assumption : A ∈ ℱ),
end

I couldn't find anything like this in mathlib. I thought proving it would be simple, but it turned out not to be the case. I was thinking about contributing this since it is a non-trivial result. Any thoughts? Should I just open a PR?

[Eric Wieser]

Can you promote that from an existential to a construction?

[Eric Wieser]

That is, something like

def ultrafilter_comap_set (f : X → Y) (A : set X) (𝒱 : ultrafilter Y) (h : f '' A ∈ 𝒱) :
  ultrafilter X

lemma map_ultrafilter_comap_set (f : X → Y) (A : set X) (𝒱 : ultrafilter Y) (h : f '' A ∈ 𝒱) :
  (ultrafilter_comap_set f A𝒱 h).map f = 𝒱

lemma mem_ultrafilter_comap_set (f : X → Y) (A : set X) (𝒱 : ultrafilter Y) (h : f '' A ∈ 𝒱) :
  A ∈ ultrafilter_comap_set f A𝒱 h

[Bernd Losert]

Yes I can.

[Bernd Losert]

I know I will also need to change the variable names to fit the style of order.filter.ultrafilter. Also, I'm not sure about the name of this thing.

[Patrick Massot]

I think this proof is needlessly complicated, I'll try to find time to write a shorter proof.

[Bernd Losert]

Yeah, my tactic skills (or lack thereof) shows.

[Patrick Massot]

This is not a question of tactic skills. You need to get used to how much structure we use on filters, especially push-forward, pull-back, inf and sup. And of course you need to know the library.

import order.filter.bases order.filter.ultrafilter

open filter set
open_locale filter

variables {X Y : Type*}

lemma ultrafilter.eq_of_le {a b : ultrafilter X} (h : (a : filter X) ≤ b) : a = b :=
ultrafilter.coe_injective (b.unique h)

open ultrafilter

lemma ultrafilter_comap_set {f : X → Y} {A : set X} {V : ultrafilter Y} (h : f '' A ∈ V) :
  ∃ 𝒰 : ultrafilter X, 𝒰.map f = V ∧ A ∈ 𝒰 :=
begin
  haveI : (comap f V ⊓ 𝓟 A).ne_bot := comap_inf_principal_ne_bot_of_image_mem V.ne_bot h,
  refine ⟨of (comap f V ⊓ 𝓟 A), _, of_le _ (mem_inf_of_right $ mem_principal_self A)⟩,
  apply eq_of_le,
  calc filter.map f (of (comap f V ⊓ 𝓟 A))
      ≤ map f (comap f V ⊓ 𝓟 A) : map_mono (of_le _)
  ... ≤ (map f $ comap f V) ⊓ map f (𝓟 A) : map_inf_le
  ... = (map f $ comap f V) ⊓ (𝓟 $ f '' A) : by rw map_principal
  ... ≤ V ⊓ (𝓟 $ f '' A) : inf_le_inf_right _ map_comap_le
  ... = V : inf_of_le_left (le_principal_iff.mpr h)
end

[Patrick Massot]

As you can see, the core of the proof is a computation using all the structure I mentioned. As far as I know, this doesn't exist anywhere else (it certainly doesn't exist in Bourbaki).

[Bernd Losert]

I did try to make it work with comap f V ⊓ 𝓟 A, but I ran into problems when I wanted to show the equality 𝒰.map f = V, so I tried a different approach.
I have not used the refine tactic yet, so I'm not sure what magic it does.

[Bernd Losert]

And of course you need to know the library.

Yeah, this is a major issue I have.

[Kyle Miller]

@Bernd Losert refine is like exact but any holes you leave (the underscores) become new goals if Lean doesn't otherwise figure them out for you.

[Kyle Miller]

For example, say f has two arguments, then apply f and refine f _ _ have a similar effect.

[Bernd Losert]

Ah, that's interesting.

[Kyle Miller]

It's also useful for using custom induction lemmas since it gives you more control (and also the induction tactic seems to have some longstanding bugs...). Setting up strong induction, for example: refine nat.strong_induction_on n (λ n' ih, _)

[Patrick Massot]

refine isn't doing anything fancy here. You could write the exact same proof as:

lemma ultrafilter_comap_set {f : X → Y} {A : set X} {V : ultrafilter Y} (h : f '' A ∈ V) :
  ∃ 𝒰 : ultrafilter X, 𝒰.map f = V ∧ A ∈ 𝒰 :=
begin
  haveI : (comap f V ⊓ 𝓟 A).ne_bot := comap_inf_principal_ne_bot_of_image_mem V.ne_bot h,
  use of (comap f V ⊓ 𝓟 A),
  split,
  { apply eq_of_le,
    calc filter.map f (of (comap f V ⊓ 𝓟 A)) ≤ map f (comap f V ⊓ 𝓟 A) : map_mono (of_le _)
    ... ≤ (map f $ comap f V) ⊓ map f (𝓟 A) : map_inf_le
    ... = (map f $ comap f V) ⊓ (𝓟 $ f '' A) : by rw map_principal
    ... ≤ V ⊓ (𝓟 $ f '' A) : inf_le_inf_right _ map_comap_le
    ... = V : inf_of_le_left (le_principal_iff.mpr h) },
  { exact of_le _ (mem_inf_of_right $ mem_principal_self A) }
end

[Patrick Massot]

If anything is fancy here then it's the anonymous constructor notation (the angle brackets) and its convenient "associativity".

[Patrick Massot]

refine is a really fundamental tactic. In a very real sense, every tactic is a special case of refine.

[Bernd Losert]

I don't remember seeing refine in "Theorem proving with Lean". Most of my tactic knowledge comes from there.

[Adam Topaz]

Isn't refine the only tactic that exists in agda? (This is only partially a joke)

[Bernd Losert]

The only tactic I know of in Agda is rewrite.

[Arthur Paulino]

I'm not aware of how updated this list is, but https://leanprover-community.github.io/mathlib_docs/tactics.html contains a more complete set of possibilities available in mathlib

(tip: it's a bit overwhelming, so don't worry too much)

[Adam Topaz]

@Bernd Losert refine is the analogue of agda's C-c C-r (in emacs)

[Bernd Losert]

Ah, I don't use emacs with Agda, so no clue.

[Adam Topaz]

Is it possible to write agda without emacs?

[Bernd Losert]

Of course. I'm also writing Lean without emacs or vscode.

[Bernd Losert]

I use vim.

[Adam Topaz]

" C-c C-r -> \r
nnoremap <buffer> <LocalLeader>r :call AgdaRefine("False")<CR>
nnoremap <buffer> <LocalLeader>R :call AgdaRefine("True")<CR>

[Bernd Losert]

:)
My vim setup is very plain. I just run agda on the files, so no hole-driven development for me.

[Julian Berman]

Bernd Losert said:

I use vim.

Are you using lean.nvim or doing something similarly barebones for lean

[Bernd Losert]

Barebones. I basically run !lean % to type check the file I'm working on.

[Julian Berman]

Brave.

[Yakov Pechersky]

By doing so, you've really decreased the "interactive" in interactive theorem prober

[Yakov Pechersky]

Because you've lost the ability to see the goal automatically at different places in your tactic proofs

[Yakov Pechersky]

So you're basically limited to constructing proofs that are basically the equivalent of term mods proofs with holes.

[Yakov Pechersky]

Which is now explains why your proof at the beginning of the thread is the way it is

[Bernd Losert]

Yes. I tried using vscode (again). The feedback in goals is super fast. Unfortunately, vscode has the bad habit of dying on me and sending all my cpus to 100%.

[Bernd Losert]

It's also a giant time sink to be honest.

[Bernd Losert]

I used to use emacs before too. But after I while I also realized it was a giant time sink.

[Adam Topaz]

Have you tried doom emacs? It works pretty much right out of the box.

[Adam Topaz]

Bernd Losert said:

Barebones. I basically run !lean % to type check the file I'm working on.

This is definitely not recommended.

[Bernd Losert]

Never tried doom emacs. Maybe I'll give it a try again at some point. I'm doing fine with vim at the moment.

[Julian Berman]

Any reason you're not using lean.nvim I suppose I should ask (even just for feedback)?

[Julian Berman]

Is it because you're using vanilla vim?

[Bernd Losert]

Correct.

[Julian Berman]

Seems like switching to neovim should be easier than switching to emacs :) -- but even if you stick with your current thing, even just using coc is going to be lots more fun than !lean %, but it's your party.

[Bernd Losert]

What's coc?

[Julian Berman]

An LSP client (one that works for vanilla vim).

[Bernd Losert]

Ah, OK. There was a time when I used neovim with LSP and all sorts of customizations. But at some point I realized that the benefit I got from it was marginal and started reverting to a more simpler setup. I work as developer, so I've gone through a couple of IDEs. And I've always abandoned them for vim in the end.

[Julian Berman]

Sure, I understand, I hate IDEs and don't use anything but (neo)vim :), but I've never done so quite as barebones as you're doing now, I think it'd get quite annoying to me not seeing the goal state.Do what makes you happy (says the guy who ignored people who said lean doesn't support vim and did it anyway :P) but you may try something else for a bit just to see what you're missing from Lean, and then if you're really happy the way you were you go back. And in a biased way I'd try lean.nvim as the closest to what you're doing now :P.

[Julian Berman]

Or watch the demo at least maybe -- https://github.com/Julian/lean.nvim/ it's out of date, things look nicer now, but it's close to what my setup looks like.

[Bernd Losert]

Looks pretty good. Thanks for suggesting it. The only thing that would annoy me is the pop-ups. I've grown to dislike pop-ups.

[Julian Berman]

None of that is required (and in my own setup, no popups at this point happen automatically, they're all key driven).

[Arthur Paulino]

The discussion has turned into a talk about text editors (someone might split this thread). So I am going to say something: learning vim/neovim is an old dream of mine and I'd love to learn how to use it with Lean :smiley:

[Bernd Losert]

@Eric Wieser : I have broken-up the proof by @Patrick Massot like this:

namespace ultrafilter

lemma eq_of_le {f g : ultrafilter α} (h : (f : filter α) ≤ g) : f = g :=
coe_injective (g.unique h)

def comap_inf_principal_ne_bot_of_image_mem {m : α → β} {s : set α} {g : ultrafilter β} (h : m '' s ∈ g) : (filter.comap m g ⊓ 𝓟 s).ne_bot :=
filter.comap_inf_principal_ne_bot_of_image_mem g.ne_bot h

noncomputable def of_comap_inf_principal {m : α → β} {s : set α} {g : ultrafilter β} (h : m '' s ∈ g) : ultrafilter α :=
begin
  haveI : (filter.comap m g ⊓ 𝓟 s).ne_bot := comap_inf_principal_ne_bot_of_image_mem h,
  exact of (filter.comap m g ⊓ 𝓟 s)
end

def of_comap_inf_principal_ultrafilter_mem {m : α → β} {s : set α} {g : ultrafilter β} (h : m '' s ∈ g) : s ∈ of_comap_inf_principal h :=
begin
  haveI : (filter.comap m g ⊓ 𝓟 s).ne_bot := comap_inf_principal_ne_bot_of_image_mem h,
  have : s ∈ filter.comap m g ⊓ 𝓟 s := mem_inf_of_right (mem_principal_self s),
  exact filter.le_def.mp (of_le _) s this
end

def of_comap_inf_principal_ultrafilter_eq_of_map {m : α → β} {s : set α} {g : ultrafilter β} (h : m '' s ∈ g) : (of_comap_inf_principal h).map m = g :=
begin
  haveI : (filter.comap m g ⊓ 𝓟 s).ne_bot := comap_inf_principal_ne_bot_of_image_mem h,
  apply eq_of_le,
  calc filter.map m (of (filter.comap m g ⊓ 𝓟 s)) ≤ filter.map m (filter.comap m g ⊓ 𝓟 s) : filter.map_mono (of_le _)
  ... ≤ (filter.map m $ filter.comap m g) ⊓ filter.map m (𝓟 s) : filter.map_inf_le
  ... = (filter.map m $ filter.comap m g) ⊓ (𝓟 $ m '' s) : by rw filter.map_principal
  ... ≤ g ⊓ (𝓟 $ m '' s) : inf_le_inf_right _ filter.map_comap_le
  ... = g : inf_of_le_left (le_principal_iff.mpr h)
end

end ultrafilter

One thing that bugs me is that I have to keep repeating the haveIpart. Is there a way to prevent this?

If anyone has any other feedback about this code, please let me know.

[Eric Wieser]

Most of those defs should be lemmas, only the actual construction (of_comap_inf_principal) should be a def. I'm not familiar with this part of mathlib so can't really advise much beyond that.

[Bernd Losert]

Ah, good point.

[Bernd Losert]

Any thoughts on the haveI issue?

[Eric Wieser]

There might be a trick - this works, but is uglier than what you have:

lemma of_comap_inf_principal_ultrafilter_mem {m : α → β} {s : set α} {g : ultrafilter β} (h : m '' s ∈ g) : s ∈ of_comap_inf_principal h :=
begin
  have : s ∈ filter.comap m g ⊓ 𝓟 s := mem_inf_of_right (mem_principal_self s),
  exact filter.le_def.mp (@of_le _ _ (id _)) s this,  -- find the instance by unification rather than typeclass search
end

There might be a nicer way to spell that.

[Bernd Losert]

I made a PR: https://github.com/leanprover-community/mathlib/pull/11445.