finite stuff

Stream: general

[Patrick Massot]

I'm really bad at manipulating finite sets in Lean. This is frustrating because everything about finite sets seem obvious. I'd be very grateful if someone could prove the following lemmas (the second one has the same assumption but a more precise conclusion):

import data.set.finite
open set

variables {ι : Type*} {α : Type*} {s : ι → set α} {t : set α}

lemma finite_stuff  (tfin : finite t) (h : t ⊆ ⋃ i, s i) :
  ∃ I : finset ι, t ⊆ ⋃ i ∈ I, s i :=
sorry

lemma finite_stuff' (tfin : finite t) (h : t ⊆ ⋃ i, s i) :
 ∃ I : finset ι, ∃ σ : {i | i ∈ I} → set α,
 (∀ i, finite (σ i)) ∧ (∀ i, σ i ⊆ s i) ∧ t ⊆ ⋃ i, σ i :=
sorry

Of course I'm also interested if someone explains those lemmas should be stated like this and will be a pain to use.

[Johan Commelin]

This reminds me of https://github.com/leanprover-community/mathlib/blob/51553e36ff9ae93ee4fbfb05a39e5d04c71be565/src/linear_algebra/finsupp.lean#L434

[Johan Commelin]

@Patrick Massot I think the statements are fine. (Maybe I would use t : finset _... To prove this, I would do something like

  have : \forall x : (t : Type*), \ex i, x \in s i,
  choose this using f hf,
  let I := finset.image f t,

modulo minor tweaks

[Kevin Buzzard]

apparently Lean can't synthesize decidable equality on iota. I am assuming that this isn't an issue for Patrick...

[Kevin Buzzard]

example (α : Type*) (t : set α) [finite t] : fintype t := by apply_instance -- fails

[Mario Carneiro]

I think you can do cases on the proof of finite t

[Mario Carneiro]

is finite even a typeclass?

[Kevin Buzzard]

no it isn't -- sorry. But still...

[Mario Carneiro]

yeah, it's defined as nonempty (fintype t) so just pop it open and use resetI

[Kevin Buzzard]

It's great that to prove this triviality I need to unfreeze local instances :-)

[Mario Carneiro]

hey, you're the one that wants to use instances that aren't present in the statement

[Mario Carneiro]

it's not needed for the statement and I'm not sure how it's being used in the proof

[Kevin Buzzard]

stupid mum_bUnion_iff wants the term to be in a set, not a finset :-)

[Kevin Buzzard]

How come mem_Union is an iff and mem_bUnion isn't?

[Mario Carneiro]

probably because mem_bUnion is too old

[Kevin Buzzard]

lemma finite_stuff  (tfin : finite t) (h : t ⊆ ⋃ i, s i) :
  ∃ I : finset ι, t ⊆ ⋃ i ∈ I, s i :=
begin
  have : ∀ x : t, ∃ i, x.1 ∈ s i,
    rintros ⟨x, hx⟩, rcases h hx with ⟨_, ⟨i, rfl⟩, hi⟩, exact ⟨i, hi⟩,
  choose f hf using this,
  tactic.unfreeze_local_instances,
  cases tfin,
  use finset.image f finset.univ,
  intros x hx,
  rw mem_Union,
  use f ⟨x, hx⟩,
  rw mem_Union,
  existsi _,
  apply hf,
  rw finset.mem_image,
  use ⟨x, hx⟩, simp,
end

[Kevin Buzzard]

That bit at the end could use some tidying

[Mario Carneiro]

it looks like a term mode proof written vertically

[Kevin Buzzard]

that's how I roll

[Kevin Buzzard]

you should see my codewars solutions

[Kevin Buzzard]

@Patrick Massot in the second one, why not have sigma mapping to finset alpha? it's finset.unbind then :-)

[Kevin Buzzard]

Did someone find a proof of finite t -> finite s \cap t?

[Kevin Buzzard]

There should be a mem_fUnion

[Kevin Buzzard]

or possibly a mem_fUnion_iff...

[Kevin Buzzard]

lemma finite_stuff' (tfin : finite t) (h : t ⊆ ⋃ i, s i) :
 ∃ I : finset ι, ∃ σ : {i | i ∈ I} → set α,
 (∀ i, finite (σ i)) ∧ (∀ i, σ i ⊆ s i) ∧ t ⊆ ⋃ i, σ i :=
begin
  cases finite_stuff tfin h with I hI,
  use I,
  use (λ x, s x.1 ∩ t),
  split,
  { intro i, sorry}, -- finite t → finite s ∩ t
  split,
  { intro i, apply inter_subset_left},
  { intros x hx,
    rw mem_Union,
    replace hI := hI hx,
    rw mem_Union at hI,
    cases hI with i hi,
    rw mem_Union at hi,
    cases hi with hi hsi,
    use ⟨i, hi⟩,
    split,
      exact hsi,
    exact hx}
end

I'm not sure this is mathlib-ready </sarcasm>, and I assumed finite t -> finite s \cap t, but if it's just something you need now then there it is

[Kevin Buzzard]

I'm not sure these are term mode proofs really, because of the occasional rw mem_Union.

[Kevin Buzzard]

The proof of mem_Union doesn't seem to be rfl

[Mario Carneiro]

lemma finite_stuff' (tfin : finite t) (h : t ⊆ ⋃ i, s i) :
 ∃ I : finset ι, ∃ σ : (↑I:set ι) → set α,
 (∀ i, finite (σ i)) ∧ (∀ i, σ i ⊆ s i) ∧ t ⊆ ⋃ i, σ i :=
begin
  cases finite_stuff tfin h with I hI,
  use I,
  use (λ x, s x.1 ∩ t),
  split,
  { intro i,
    apply finite_subset tfin,
    apply inter_subset_right },
  split,
  { intro i, apply inter_subset_left },
  { intros x hx,
    rw mem_Union,
    replace hI := hI hx,
    rw mem_Union at hI,
    cases hI with i hi,
    rw mem_Union at hi,
    cases hi with hi hsi,
    use ⟨i, hi⟩,
    split,
    { exact hsi },
    { exact hx } }
end

[Patrick Massot]

Than you very much Kevin and Mario!

[Patrick Massot]

Mario, do you think we are missing intermediate lemmas here? It looks like a very long proof for such an obvious fact.

[Mario Carneiro]

here's kevin's proof in term mode:

```lean
lemma finite_stuff' (tfin : finite t) (h : t ⊆ ⋃ i, s i) :
 ∃ I : finset ι, ∃ σ : (↑I:set ι) → set α,
 (∀ i, finite (σ i)) ∧ (∀ i, σ i ⊆ s i) ∧ t ⊆ ⋃ i, σ i :=
let ⟨I, hI⟩ := finite_stuff tfin h in
⟨I, λ x, s x.1 ∩ t,
  λ i, finite_subset tfin (inter_subset_right _ _),
  λ i, inter_subset_left _ _,
  λ x hx, mem_Union.2 $
    let ⟨i, hi, hsi⟩ := mem_bUnion_iff.1 (hI hx) in
    ⟨⟨i, hi⟩, hsi, hx⟩⟩

[Kevin Buzzard]

Nice :-)

[Mario Carneiro]

although I did swap in the use of mem_bUnion_iff

[Kevin Buzzard]

To do that I would have had to understand how supr was implemented and I couldn't be bothered to dig

[Mario Carneiro]

I don't think this is an unreasonably long proof, given the complexity of the statement itself. Once you set the logical manipulation aside the only actually interesting part is the last 3 lines of my version of the proof

[Mario Carneiro]

I ctrl-clicked on mem_bUnion and looked for neighbors

[Mario Carneiro]

it was two lemmas previous

[Patrick Massot]

Do you think we should keep both version finite_stuff and finite_stuff'?

[Patrick Massot]

(with better names of course)

[Mario Carneiro]

If you find it useful, I don't see why not

[Mario Carneiro]

I usually try to find an appropriate constructive analogue for these sorts of things, that is, a function with the stated properties, since existentials have to be unpacked and lack global coherence of choices

[Patrick Massot]

In my question the first lemma was really meant as training for the second one.

[Patrick Massot]

I want to use only the second one.

[Patrick Massot]

If you can turn this lemma into a function that would be even better of course.

[Patrick Massot]

(in order to avoid unpacking the existential)

[Mario Carneiro]

I feel like there is a simpler core underlying principle here

[Patrick Massot]

That was my question about missing lemmas.

[Mario Carneiro]

like, you can swap forall and exists a la skolemization for finite sets

[Sebastien Gouezel]

In the conclusion of finite_stuff', it would be better to replace t ⊆ ⋃ i, σ iwith t = ⋃ i, σ i.

[Patrick Massot]

I didn't need this, but feel free to prove that stronger version!

[Mario Carneiro]

what do you think of this formulation:

lemma finite_stuff'' (s : finset α) (P : α → ι → Prop)
  (h : ∀ x ∈ s, ∃ i, P x i) :
  ∃ t : finset ι, ∀ x ∈ s, ∃ i ∈ t, P x i := sorry

[Patrick Massot]

That certainly looks cleaner. Can you prove it and deduce Sébastien's version of the original question?

[Mario Carneiro]

I think it's not quite enough to get the second version of the statement

[Kevin Buzzard]

Do we have an equiv e between finset X and Pi (s : set X), finite s, and the lemma that for x : X, x \in s iff x \in e s?

[Mario Carneiro]

Hey, isn't this just the collection principle from zfc?

[Kevin Buzzard]

All I know is that it's a mathematical triviality so it wouldn't surprise me if the logicians called it a principle

[Mario Carneiro]

I'm thinking of the version where you replace "finite" with "is a set" and depending on how you set things up it might be a theorem or an axiom

[Kevin Buzzard]

Like most principles

[Mario Carneiro]

it's essentially a souped up version of replacement without the assumption that the relation is a function

[Kevin Buzzard]

Replacement says the image of a set is a set

[Mario Carneiro]

right

[Mario Carneiro]

here it's the image under a relation

[Kevin Buzzard]

A relation on X

[Mario Carneiro]

and it's not really an image because you can take a subset

[Mario Carneiro]

but you have to preserve "enough" of the original relation

[Kevin Buzzard]

is_monoid_hom f is unbundled monoid homs and it's a class. monoid_hom is bundled and it's a structure

[Kevin Buzzard]

finite s is unbundled finiteness and it's a structure. finset is bundled and a structure

[Patrick Massot]

Do we have a version sInter s when s : finset (set X)? This is why I used finite everywhere instead of finset.

[Kevin Buzzard]

I mentioned fUnion earlier (which doesn't exist)

[Patrick Massot]

I know I can write ⋂₀ s.to_set but it looks silly.

[Mario Carneiro]

you can use the coercion as I did above

[Mario Carneiro]

If we did have something like that, I would prefer it generalize to lattices. I would call it finset.inf

[Mario Carneiro]

ok hey look what I found

[Johan Commelin]

Kevin Buzzard said:

finite s is unbundled finiteness and it's a structure. finset is bundled and a class

Whut?? Is finset a class?

[Mario Carneiro]

finset isn't a class

[Johan Commelin]

It should be just a structure, right?

[Kevin Buzzard]

Fixed

[Kevin Buzzard]

It's the wrong way around

[Mario Carneiro]

arguably, finite s should be called is_finite s. Is that your point?

[Mario Carneiro]

I think the problem, grammatically, is that finite is an adjective and monoid_hom is a noun

[Kevin Buzzard]

I am saying that the class/structure choice is different in the two situations for both the unbundled and the bundled concepts

[Kevin Buzzard]

I think I have this straight now

[Mario Carneiro]

Oh I see. Well, using typeclasses for these things has always been dubious, that's why we're moving away from them

[Kevin Buzzard]

I'm saying that either finset should be a structure or subgroup should be a class

[Kevin Buzzard]

Reasoning purely by analogy

[Mario Carneiro]

finset is a structure

[Mario Carneiro]

subgroup is also a structure

[Kevin Buzzard]

I see so I still have one error

[Mario Carneiro]

I'm failing to see past the typo to the point

[Kevin Buzzard]

Is finite a class?

[Kevin Buzzard]

I'm on mobile right now

[Kevin Buzzard]

Because is_subgroup is a class

[Mario Carneiro]

finite is not a class, is_subgroup is a class, and yes this is inconsistent

[Mario Carneiro]

my proposed solution is to delete is_subgroup and call it a day

[Kevin Buzzard]

Is finite deprecated? Because is_subgroup is, kinda

[Mario Carneiro]

finite is not deprecated, it is meant to be a proposition to talk about finiteness in other positions

[Mario Carneiro]

for example you can meaningfully negate it

[Kevin Buzzard]

This is some sort of indication that one should stick to finsets where one can though

[Kevin Buzzard]

Bundled ftw

[Kevin Buzzard]

We should have infinset

[Reid Barton]

import topology.subset_properties
import data.set.finite
open set

variables {ι : Type*} {α : Type*} {s : ι → set α} {t : set α}

lemma finite_stuff  (tfin : finite t) (h : t ⊆ ⋃ i, s i) :
  ∃ I : finset ι, t ⊆ ⋃ i ∈ I, s i :=
begin
  letI : topological_space α := ⊥,
  haveI : discrete_topology α := ⟨rfl⟩,
  exact tfin.compact.elim_finite_subcover _ (λ i, is_open_discrete _) h
end

[Johan Commelin]

Brilliant hack!

[Patrick Massot]

Too bad this topology stuff come too late.

[Patrick Massot]

You still get the jury special honorary mention.

[Patrick Massot]

It's too late because I want to put this below order.filter.basic. But it's also good to see that the form of the statement is used elsewhere in mathlib.

[Reid Barton]

Yes, I expected it to be easy but I didn't realize it would be quite this easy.

[Ryan Lahfa]

Mario Carneiro said:

for example you can meaningfully negate it

BTW, is it normal that push_neg on not set.finite cannot rename it as set.infinite, I guess it has to do with simp (?) ?

[Ryan Lahfa]

(I had to do a rw set.infinite in order to get the nice infinite S rather than not set.finite S)

[Mario Carneiro]

push_neg needs explicit support for each of these things. Seems like a good PR

[Ryan Lahfa]

Mario Carneiro said:

push_neg needs explicit support for each of these things. Seems like a good PR

Sounds good, thanks

[Patrick Massot]

Yes, every end-game negation in push_neg is hardcoded.

[Patrick Massot]

Damn, I was trying to put this finite stuff in the proper place before PRing, and guess what? https://leanprover-community.github.io/mathlib_docs/data/set/finite.html#set.finite_subset_Union

[Kenny Lau]

[Johan Commelin]

So... why did library_search not find this?

[Mario Carneiro]

It's very unlikely that library_search will find longer statements, because the probability that you spell the theorem the same way as the library decreases exponentially with the length of the theorem

[Mario Carneiro]

Because of our rigid naming convention and fairly deterministic file organization it's much likely to notice a collision the way Patrick did, by putting it in its proper place and seeing something already there, or getting a name conflict with a duplicate of your theorem

[Patrick Massot]

Yes, I'm trying to fit in the more precise version, and it's a pain.

[Patrick Massot]

Because of mathematically empty differences between my statement and the one already in mathlib.

[Mario Carneiro]

this is also why I highly recommend looking at sources for relevant files as a theorem discovery strategy

[Patrick Massot]

Let's try that Zulip tactic. For our experts in finiteness:

lemma set.finite.fin_param {α : Type*} {s : set α} (h : finite s) :
  ∃ f : fin (h.to_finset.card) → α, injective f ∧ range f = s :=
sorry

[Johan Commelin]

@Patrick Massot voila

open function

lemma set.finite.fin_param {α : Type*} {s : set α} (h : s.finite) :
  ∃ f : fin (h.to_finset.card) → α, injective f ∧ set.range f = s :=
begin
  classical,
  unfreezingI { cases h },
  obtain ⟨e⟩ := fintype.equiv_fin s,
  have : fintype.card s = (finset.card $ set.finite.to_finset ⟨h⟩),
  { symmetry,
    refine finset.card_congr (λ a ha, ⟨a, _⟩) _ _ _,
    { simpa only [set.finite.mem_to_finset] using ha },
    { intros, exact finset.mem_univ _ },
    { intros a b ha hb H, simpa only [subtype.mk_eq_mk] using H },
    { rintro ⟨a, ha⟩ -, refine ⟨a, _, rfl⟩, simpa only [set.finite.mem_to_finset] using ha } },
  rw ← this,
  refine ⟨λ x, e.symm x, subtype.coe_injective.comp e.symm.injective, _⟩,
  ext x,
  simp only [set.mem_range],
  split,
  { rintro ⟨i, rfl⟩, exact (e.symm i).2 },
  { intro h, refine ⟨e ⟨x, h⟩, _⟩, rw e.symm_apply_apply, refl }
end

[Patrick Massot]

Thanks Johan! This is much more complicated than what I hoped for :sad:

[Patrick Massot]

I massaged a bit into:

lemma set.finite.finset_card_eq_fintype_card {α : Type*} {s : set α} (h : finite s) :
  h.to_finset.card = @fintype.card ↥s h.fintype:=
begin
  letI := h.fintype,
  refine finset.card_congr (λ a ha, ⟨a, _⟩) _ _ _,
  { simpa only [set.finite.mem_to_finset] using ha },
  { intros, exact finset.mem_univ _ },
  { intros a b ha hb H, simpa only [subtype.mk_eq_mk] using H },
  { rintro ⟨a, ha⟩ -, refine ⟨a, _, rfl⟩, simpa only [set.finite.mem_to_finset] using ha }
end

noncomputable
lemma set.finite.equiv_fin {α : Type*} {s : set α} (h : finite s) : s ≃ fin h.to_finset.card :=
begin
  classical,
  rw h.finset_card_eq_fintype_card,
  letI := h.fintype,
  exact classical.some (fintype.equiv_fin s).exists_rep
end

lemma set.finite.fin_param {α : Type*} {s : set α} (h : finite s) :
  ∃ f : fin (h.to_finset.card) → α, injective f ∧ range f = s :=
let e := h.equiv_fin in
⟨λ x, e.symm x, subtype.coe_injective.comp e.symm.injective, by simp [e.symm.surjective.range_comp]⟩

lemma set.finite.fin_param' {α : Type*} {s : set α} (h : finite s) :
  ∃ (n : ℕ) (f : fin n → α), injective f ∧ range f = s :=
⟨_, h.fin_param⟩

Now I'm sure @Mario Carneiro will explain why we are writing nonsense.

[Eric Wieser]

noncomputable lemma strikes me as nonsense

[Eric Wieser]

Probably the conclusion should be nonempty (s \equiv fin _), which also eliminates the classical

[Bhavik Mehta]

Patrick Massot said:

Thanks Johan! This is much more complicated than what I hoped for :sad:

open_locale classical

lemma set.finite.fin_param' {α : Type*} {s : set α} (h : finite s) :
  ∃ (n : ℕ) (f : fin n → α), injective f ∧ range f = s :=
let f := (fintype.equiv_fin (h.to_finset : set α)).out in
⟨_, coe ∘ f.symm, subtype.coe_injective.comp (equiv.injective _),
 set.ext $ λ x, ⟨λ ⟨y, h⟩, by simpa [←h] using (f.symm y).2, λ hs, ⟨f ⟨x, by simpa⟩, by simp⟩⟩⟩

[Eric Wieser]

Presumably you can avoid choice there by using docs#trunc.rec instead of trunc.out?

[Eric Wieser]

Or better, docs#nonempty_of_trunc

[Patrick Massot]

I don't see how any of this could avoid choice here.

[Eric Wieser]

Your conclusion is in prop, so you don't need to ever construct anything

[Patrick Massot]

Indeed, it's in prop

[Eric Wieser]

You're correct though, docs#fintype.equiv_fin already uses classical logic

[Eric Wieser]

Which seems ridiculous, because isn't the whole point of trunc to be a computable version of nonempty?

[Patrick Massot]

Yes, that's the issue. Maybe a proof exists in classical logic without going through that lemma, but I'm not very interested in avoiding classical logic anyway...

[Eric Wieser]

The docs specifically list that lemma as being computable

[Eric Wieser]

Oh, I guess functions can still be computable but use classical logic in internal proofs

[Mario Carneiro]

@Eric Wieser There is a difference between being computable and avoiding choice entirely. The former means that any uses of AC are confined to proof arguments where they don't hamper code generation. Large parts of mathlib are computable, but only a small fraction is AC-free

[Mario Carneiro]

In principle most of the things that are computable are also AC-free, but there aren't too many people besides me making any attempt to actually make it happen, and there are several foundational bits that need adjustment before there is any hope of making, say, finsets AC-free. I made another push toward AC-freedom in lean core recently, so we should see some improvement in mathlib when the next minor version is released.