finiteness

Stream: general

[Scott Morrison]

Do mathlib have something that behaves like:

class  Finite (α : Type u) :=
  (cardinality : nat)
  (bijection : trunc (equiv α (fin cardinality)))

[Scott Morrison]

Is this gross for some reason, and should be avoided?

[Kenny Lau]

It is in my category theory repo (the category “set”)

[Kenny Lau]

and it’s called fintype

[Scott Morrison]

It can't be called fintype, because mathlib already has a fintype which is slightly different (but equivalent, of course).

[Scott Morrison]

I guess I'm asking if there is a strong reason to (bite the bullet and learn how to use multisets and) use mathlib's fintype, or if it's okay to use something like this.

[Kenny Lau]

oops i meant the category is called set and uses fintype

[Kenny Lau]

but I guess I didn’t notice that you used trunc

[Mario Carneiro]

That's fintype. If you want to use such an interface to it, prove it and use it

[Scott Morrison]

Okay, I guess that's a good point. In the meantime I'm discovering fintype is pretty easy to use anyway.

[Scott Morrison]

What is the lemma that says fintype gives decidable_eq?

[Mario Carneiro]

I don't think it's true. So your formulation is a bit stronger, since it equips the set with a function to fin; in mathlib's fintype, this function is index_of, but it requires a separate proof of decidable_eq

[Mario Carneiro]

your Finite should be equivalent to the conjunction of fintype and decidable_eq

[Scott Morrison]

ah, okay.

[Reid Barton]

Is there any way we could get to a world in which

def finite {a : Type} (s : set a) : Prop := -- any definition of finiteness

structure finset (a : Type) :=
(s : set a)
(h : finite s)

class fintype (a : Type) : Prop :=
(h : finite (set.univ : set a))

[Reid Barton]

cons: all big_operators stuff becomes noncomputable
pros: API becomes comprehensible by humans, and no more instance diamonds for fintype

[Sebastien Gouezel]

(I also dream of a world where decidablewould disappear, but I know this won't happen)

[Mario Carneiro]

Up to proof irrelevance propositional equivalence, none of these definitions are different except you replaced fintype A with nonempty (fintype A). Maybe we should just have a class for that, replacing set.finite

[Bhavik Mehta]

actually do we lose anything by just changing fintype to the nonempty version of what it currently is? fintype.univ becomes noncomputable but it fixes the instance diamonds

[Mario Carneiro]

fintype.card also becomes noncomputable

[Reid Barton]

My bigger issue is that I find it really difficult to find what I'm looking for in data.finset/data.fintype/data.set.finite; it's possible this could be improved without any representation changes

[Reid Barton]

But a related issue is that there are three different ways to express the same ideas and they are connected by constructions that are not that simple

[Reid Barton]

It's my completely unsubstantiated opinion that if we proved a bunch of things for finite, say, we could systematically deduce the consequences for finset and fintype and end up with a more organized API

[Reid Barton]

Here is some pure fantasy: a universe level for only finite types

[Jalex Stark]

Type (1/2:\Q)

[Kenny Lau]

@Kevin Buzzard

[Kevin Buzzard]

We must make finiteness easier for mathematicians. Counting is all over Sylow's theorems and if people can't knock them off in Lean using what we have, then I think we don't have the right things. I recently had two distinct proofs that the trivial subgroup of a group was a fintype and it was annoying.

[Kevin Buzzard]

OK I have just spent some time trying to understand the issues here. I'm trying to prove Sylow's theorems with students. Sylow's theorems are theorems about finite groups with no mention of decidable equality or ever explicitly attempting to write down elements -- they apply to all finite groups. Hence it seems to me that computability is irrelevant, so fintype and finset are not the right classes. But set.finite isn't either, because it is unbundled finiteness. Reid is proposing a bundled version of finiteness which he also calls finset but how about for now we call it finset2.

structure finset2 (a : Type u) :=
(s : set a)
(h : finite s)

Is there an argument for developing an API for this? It is bundled noncomputable finiteness which seems to me to be the best for Lean and the best for Sylow. Have I understood things correctly? Are people just going to tell me to go ahead and try?

[Kevin Buzzard]

As for cardinality some non-cardinal options would be finset2.card, set.fincard : set X -> nat or fincard : Type u -> nat. These are all functions we don't have, right? @Patrick Massot you were complaining about fintype in another thread and it's got to the point where I just want to fix it. Sylow's theorems are about finite groups and I don't care whether they have decidable equality, I just want to be able to count subsets and not run into diamonds -- this is not an unreasonable request I don't think but perhaps the infrastructure is not yet there for this kind of thing.

[Kevin Buzzard]

More thoughts about finiteness and cardinality for sets and types.

Let's start with sets. Now set.finite exists in mathlib already; its definition is

def finite (s : set α) : Prop := nonempty (fintype s)

. It's not a class. Why is set.finite not a class? is_subgroup was a class. Could both set.finite and set.infinite be classes? This would be unbundled finiteness for sets (normal is unbundled Prop-valued normality for subgroups and we tried bundling it in the group theory game but it's quite inconvenient because you either reproduce a bunch of subgroup.* in normal.* or you put to_subgroup everywhere). The definition of bundled finiteness for sets I'm working with is

def finset2 (X : Type u) := {S : set X // finite S}

The idea would be to develop some API for set.finite and encourage mathematicians who don't #eval to either use set.finite or finset2 as their standard concept of finiteness for sets depending on whether they like bundled or unbundled -- and in particular to avoid finset completely because this is constructible finiteness.

For set cardinality the issue is that I don't know whether unbundled or bundled will be best, so I have had to introduce two nat-valued cardinalities -- firstly note that we have

noncomputable def equiv_finset (X : Type*) : finset2 X ≃ (finset X) := ...

and so we can define

noncomputable def finset2.card (F : finset2 X) : ℕ :=
((finset2.equiv_finset X).to_fun F).card

i.e. finset2.card is just finset.card but ported over the canonical bijection. This is cardinality for bundled finite sets. For unbundled finite sets there is the issue of trying to find the finite instance, and experience seems to show that this can be hard work, so I introduce

def sum [add_comm_monoid β] (s : set α) (f : α → β) : β :=
if h : finite s then h.to_finset.sum f else 37

and then define

def set.card (s : set α) : ℕ :=
s.sum (λ x, 1)

These functions are really easy to apply because they don't check finiteness. Under finiteness conditions you can relate the card to finset2.card and this is your route back to finset.card if you want to port API.

Earlier on in my Lean career I was concerned about all this noncomputable stuff because I didn't really know how important computability was. The thing to understand about noncomputable cards is that you can still prove Sylow's theorems which are all about cards, you just can't #eval, and because I never #eval anyway I'm not bothered.

---

Now onto types. For unbundled finiteness for types I'm using

def is_finite (X : Type u) : Prop := nonempty (fintype X)

attribute [class] is_finite

and again the idea is to encourage non-#eval mathematicians to use is_finite instead of fintype, because using it is strictly easier, modulo the fact that of course a whole load of the fintype library needs to be ported over.

Bundling finite types seems like the sort of thing that the category theory library might want to do, but I'm not doing it right now.

For cardinality again I follow the principle that the fewer inputs your function has, the easier it is to use it, so I have gone for

def fincard (X : Type*) : ℕ :=
if h : is_finite X then @fintype.card X (classical.choice h) else 0

and of course there's a route back to fintype.card in the is_finite setting, which enables noncomputational API (e.g. all theorems) to be ported.

All this work is piling up in the group-theory-game repo because we have got to the point where we want to prove Sylow's theorems. I think it might be sensible to start sending some of it to mathlib. Before I start, does anyone have any comments about the proposal, naming conventions, or anything else? I feel bad adding more definitions of finiteness but I think these are the things we need for reasoning. When I was refactoring subgroups I ran into an issue in the proof of Sylow's theorem where we are proving there are subgroups of order p^n for all n<=v_p(G); the n=0 case used bot and at some point I wanted to rewrite card_bot but unfortunately there are two proofs that the bot subgroup of a finite group is finite in mathlib -- one coming from the fact that it's the trivial group and one coming from the fact that a subset of a finite type is finite. This is just silly -- we don't need these subsingleton diamonds getting in the way when we are reasoning.

[Mario Carneiro]

What ever happened to definition irrelevance / API making? Instead of defining finset2, make an api that lets you treat a finset like a finset2

[Chris Hughes]

Agree with Mario here, nothing about finset forces you to be constructive.

[Mario Carneiro]

I think my definition of finsum is strictly more powerful than your sum too. If you are going to have no well definedness assumptions, you may as well have it give a reasonable result on the widest possible domain

[Mario Carneiro]

Oops, it appears this is a thread-spanning topic now. I'm referring to https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/universe.20hell.20in.20linear.20algebra/near/206415746

[Kevin Buzzard]

Yeah sorry, I had to choose whether to go with this thread or that one.

[Kevin Buzzard]

finsum is fine by me -- I was just using something Jeremy knocked up for MIL. I'm not sure I understand the finset2 thing though. I was 100% sure I used finset2 to make is_finite but I just removed the import and don't use it at all. So should I ditch finset2? I'm not sure I even need it now.

[Kevin Buzzard]

So is the point that we just don't define finset2 at all, prove that {S : set X // finite S} ≃ (finset X) and then for every lemma about finsets I prove some analogous lemma for set.finite?

[Mario Carneiro]

In what sense is that not already done in mathlib?

[Mario Carneiro]

set.finite has lots of lemmas generated exactly that way, and they are all very easy

[Mario Carneiro]

so you can add more if something is missing without too much trouble

[Kevin Buzzard]

I am confused about why we don't want finset2. What were the problems with is_subgroup which made us switch to subgroup? Were there actually no problems and we just decided that we wanted the cool dot notation?

[Reid Barton]

it was a class

[Kevin Buzzard]

So set.finite and set.infinite should not be classes? Here's the current definitions (mostly due to other people):

import data.finsupp

universe u

open_locale classical

attribute [class] set.finite set.infinite

noncomputable def finsum {ι α} [add_comm_monoid α] (f : ι → α) : α :=
if h : ∃ f' : ι →₀ α, f = f' then (classical.some h).sum (λ _ a, a) else 0

noncomputable def finsum_in {ι α} [add_comm_monoid α] (s : set ι) (f : ι → α) : α :=
finsum (λ i, if i ∈ s then f i else 0)

localized "notation `∑` binders `, ` r:(scoped:67 f, finsum f) := r" in finsum
localized "notation `∑` binders ` in ` s `, ` r:(scoped:67 f, finsum_in s f) := r" in finsum

noncomputable def set.card {ι} (s : set ι) := ∑ x in s, 1

def is_finite (X : Type u) : Prop := nonempty (fintype X)

attribute [class] is_finite

noncomputable def fincard (X : Type u) : ℕ :=
if h : is_finite X then @fintype.card X (classical.choice h) else 0

[Mario Carneiro]

I think set.card should be defined directly rather than by summing ones, but the definition will be equivalent regardless so it's not that important

[Mario Carneiro]

set.card s := fincard (\u s) for example

[Mario Carneiro]

also set.finite can be refactored on top of is_finite

[Mario Carneiro]

As for making is_finite a class, I think it will work okay, but it will be about as good as fintype for what it does

[Mario Carneiro]

In particular, AFAICT all the gripes about fintype are eliminated if it is excised from definitions such as fincard

[Kevin Buzzard]

wait -- are you telling me that the def of fincard should be rethought?

[Mario Carneiro]

no, I'm saying that it solves the bulk of the problems on its own

[Mario Carneiro]

As long as the fintype instance doesn't occur in the statement of theorems using finiteness, it should be fine to appear as a hypothesis

[Mario Carneiro]

so perhaps the is_finite class isn't so important

[Kevin Buzzard]

This is not just navel-gazing for its own sake -- I'm trying to use finiteness to prove results in group theory. The idea of decreeing that "we will only take sizes of sets" or "...of types" sounded appealing to me, but I've seen explicit examples today where you really have to move between sets and types.

[Mario Carneiro]

I'm still not convinced that you can't just use fintype (\u s) for talking about sets in a world of classes on types

[Mario Carneiro]

The main use of is_finite is not as a class but as a hypothesis, a proposition to be used however you use propositions

[Kevin Buzzard]

How are you proposing saying things like "if p is a partition of the finite type X then the sum of the sizes of the blocks of p equals the size of X"?

[Mario Carneiro]

theorem foo [fintype X] : ... fincard X

[Kevin Buzzard]

But you need to count all the subsets too

[Kevin Buzzard]

you have a set of subsets -- you don't really want to convert all of these to types, do you?

[Mario Carneiro]

finsum (\lam p, fincard p) = fincard X

[Mario Carneiro]

it's fine, let coercion do its magic

[Kevin Buzzard]

In practice I was using is_finite in the fincard proofs because most of them are case splits on whether something is finite or not. So it was very convenient to have is_finite as a class because i could just dump it into the inference system and then not worry about it. But I guess that given that I had it, I could just feed it into the theorems I need rather than doing the resetI dance

[Kevin Buzzard]

Amusing thing: when doing some set lemmas I realised I was constantly splitting on whether something was finite or infinite, and they were both classes, so I proved that every set was finite or infinite and then was doing cases; resetI. I then joked that I should just be doing casesI so I wrote it for a joke and then it turned out that it existed :P

[Mario Carneiro]

def partition (X : Type*) := {P : set (set X) // ∀ x, ∃! p, p ∈ P ∧ x ∈ p}

theorem partition_sum {X} [fintype X] (P : partition X) :
  finsum_in P.1 (λ p, fincard p) = fincard X := sorry

easy peasy

[Mario Carneiro]

(I won't prove it right now because fincard et al don't have an API yet)

[Kevin Buzzard]

that's a bad theorem, it uses the forbidden fintype

[Mario Carneiro]

No, the fintype does not appear in the statement of the theorem, so you can just get it from wherever you like

[Mario Carneiro]

you won't have unification problems as a result

[Kevin Buzzard]

Oh I see. But you should prove this for is_finite because it's more general

[Mario Carneiro]

it's (constructively, even) equivalent

[Kevin Buzzard]

then you should prove it for is_finite because fintype is deprecated?

[Mario Carneiro]

the idea with this proposal is that you use fintype for your typeclass needs and reserve is_finite as a regular hypothesis that you can pop open when you want to teach the typeclass system

[Kevin Buzzard]

I thought I never wanted to use fintype ever again?

[Mario Carneiro]

It already has all the "structural" instances you want

[Mario Carneiro]

the bad thing about fintype is that because it is a Type, you can get into unification issues like patrick mentioned at the start of the other thread

[Mario Carneiro]

but as long as you use fincard instead of fintype.card that problem goes away

[Reid Barton]

Kevin Buzzard said:

I then joked that I should just be doing casesI so I wrote it for a joke and then it turned out that it existed :P

on a related note, I just discovered fconstructor

[Kevin Buzzard]

Jason wanted to make an API for finsum (which was defined by Mario to be)

noncomputable def finsum {ι α} [add_comm_monoid α] (f : ι → α) : α :=
if h : ∃ f' : ι →₀ α, f = f' then (classical.some h).sum (λ _ a, a) else 0

and he realised that what he wanted was to prove that it equalled finset.sum. This would be easier if we used the following definition:

noncomputable def finsum2 {ι α} [add_comm_monoid α] (f : ι → α) : α :=
if h : (function.support f).finite then ∑ x in h.to_finset, f x else 0

Are there disadvantages to finsum2 @Mario Carneiro ?

[Mario Carneiro]

which one has less imports?

[Mario Carneiro]

Either way you want to prove both definitions are the same

[Kevin Buzzard]

import data.finsupp data.support

noncomputable theory

open_locale classical big_operators

noncomputable def finsum {ι α} [add_comm_monoid α] (f : ι → α) : α :=
if h : ∃ f' : ι →₀ α, f = f' then (classical.some h).sum (λ _ a, a) else 0

noncomputable def finsum2 {ι α} [add_comm_monoid α] (f : ι → α) : α :=
if h : (function.support f).finite then ∑ x in h.to_finset, f x else 0

theorem finsum_eq_finsum2 {ι α} [add_comm_monoid α] (f : ι → α) : finsum f = finsum2 f :=
begin
  unfold finsum,
  unfold finsum2,
  split_ifs with h1 h2 h3,
  { unfold finsupp.sum,
    congr',
    { ext x,
      rw finsupp.mem_support_iff,
      rw (classical.some_spec h1).symm,
      rw set.finite.mem_to_finset,
      refl },
    { exact (classical.some_spec h1).symm } },
  { exfalso,
    apply h2,
    clear h2,
    rcases h1 with ⟨h1, rfl⟩,
    exact h1.finite_supp },
  { exfalso,
    apply h1,
    clear h1,
    let f' : ι →₀ α :=
    { support := h3.to_finset,
      to_fun := f,
      mem_support_to_fun := begin
        intro i,
        simp only [function.mem_support, set.finite.mem_to_finset],
      end },
    use f',
    refl },
  { refl }
end .

[Mario Carneiro]

what is finiteness.is_finite?

[Mario Carneiro]

wow, I thought function.support would have an easy definition but the file that defines it has a ton of imports

[Kenny Lau]

I thought we stopped caring about the import hierarchy 37 days ago

[Yury G. Kudryashov]

This file has many imports because it was added after these imports

[Yury G. Kudryashov]

It's easy to remove all imports if you move lemmas to other files

[Kevin Buzzard]

Another insight from Chris at Xena this evening; how about this:

def finset.univ' (ι : Type*) : finset ι := if h : nonempty (fintype ι) then
  (classical.choice h).elems else ∅

def fincard' (X : Type u) : ℕ := finset.card $ finset.univ' X

@Mario Carneiro you had suggested

def fincard (X : Type*) : ℕ :=
if h : nonempty (fintype X) then @fintype.card X (classical.choice h) else 0

-- does this variant meet with your approval?

[Mario Carneiro]

ha, clever

[Kenny Lau]

@Kevin Buzzard @Mario Carneiro I would go as far as saying that the finset.univ in mathlib should be replaced with your new finset.univ' etc.

[Mario Carneiro]

that finset.univ' could be useful for many things

[Kenny Lau]

(etc. = the same for other definitions depending directly on fintype)

[Kevin Buzzard]

OK so @Jason KY. and I have been hacking away on this stuff, and we ran into something which presumably has been run into before. Recall we've been talking about these definitions (either will do for me but the finset one is easier to port with):

noncomputable def finsum {ι α} [add_comm_monoid α] (f : ι → α) : α :=
if h : ∃ f' : ι →₀ α, f = f' then (classical.some h).sum (λ _ a, a) else 0

noncomputable def finsum2 {ι α} [add_comm_monoid α] (f : ι → α) : α :=
if h : (function.support f).finite then ∑ x in h.to_finset, f x else 0

Jason pointed out that we should probably do products too -- but then we run into the following issue: finsupp and support both want a zero. Is there an analogous construction in Lean which does either of these things but with a 1?

[Kevin Buzzard]

We can make one_support or whatever -- function.one_support f is the things which don't get mapped to one -- but then to_additive will turn this into zero_support. Presumably we can work around this? But do we want one_support at all?

[Reid Barton]

Kevin Buzzard said:

so I proved that every set was finite or infinite and then was doing cases; resetI. I then joked that I should just be doing casesI so I wrote it for a joke and then it turned out that it existed :P

I also just learned you can use it instead of unfreezing local instances.

[Yury G. Kudryashov]

We can define set.to_finset using the same trick, then finset.univ = univ.to_finset, fincard = finset.univ.card

[Kevin Buzzard]

There's a fincard branch of mathlib by the way.

[Adam Topaz]

Reid Barton said:

Is there any way we could get to a world in which

def finite {a : Type} (s : set a) : Prop := -- any definition of finiteness

structure finset (a : Type) :=
(s : set a)
(h : finite s)

class fintype (a : Type) : Prop :=
(h : finite (set.univ : set a))

I hereby sign this petition.

[Patrick Massot]

I sign any petition that could make finiteness manageable.

[Johan Commelin]

Reid Barton said:

It's my completely unsubstantiated opinion that if we proved a bunch of things for finite, say, we could systematically deduce the consequences for finset and fintype and end up with a more organized API

What would this systematic deduction look like? It should be possible to do that with current definitions, right?

I think the only design choice that is not trivial upto Prop-eq is whether fintype is Type or Prop valued.

[Johan Commelin]

Otoh, I do wish quite often that we had

def finite (s : set α) : Prop := ∃ t : finset α, s = ↑t
-- instead of
def finite (s : set α) : Prop := nonempty (fintype s)

[Johan Commelin]

@Reid Barton If you want to start with set.finite instead of finset, I guess

def finite' {α : Type*} (s : set α) : Prop :=
∃ l : list α, ∀ x, x ∈ l ↔ x ∈ s

would be an obvious way to start.

[Johan Commelin]

But it's not yet clear to me how set.finite and finset would become much easier to handle than with what we have now. (Not saying the current setup is easy.)

[Adam Topaz]

Johan Commelin said:

Reid Barton If you want to start with set.finite instead of finset, I guess

def finite' {α : Type*} (s : set α) : Prop :=
∃ l : list α, ∀ x, x ∈ l ↔ x ∈ s

would be an obvious way to start.

You don't even need an if and only if, only that l surjects onto s.

[Adam Topaz]

def finite' {α : Type*} (s : set α) : Prop :=
∃ l : list α, ∀ x, x ∈ s → x ∈ l

[Adam Topaz]

This makes it easier to prove that the intersection / union of two finite sets are finite.

[Reid Barton]

It really doesn't matter how you define finite. The right place to start would be constant finite : set \a -> Prop. At some point you'll have collected a bunch of proof obligations like finite_union, finite_fin, ... and then you can think about what definition would be best to prove them all.
A more important question might be whether finite or fintype should be the primitive one, with the other one defined in terms of it. But I think it doesn't matter too much.

[Johan Commelin]

Currently finset is the primitive one. Is that bad?

[Adam Topaz]

Oh? Why isn't set.finite defined as "there exists a finset such that..."?

[Reid Barton]

Johan Commelin said:

But it's not yet clear to me how set.finite and finset would become much easier to handle than with what we have now. (Not saying the current setup is easy.)

One advantage is everything just becomes more straightforward.

• If you have (s : set T) (h : finite s), you don't need to go hunt down finite.to_finset. You can just write ⟨s, h⟩.
• More importantly, when you extract the underlying set of this finset, it's now defeq to what you started with.
• That means if we define all the has_mem, has_union etc. on finset using the corresponding set definition on the first component, then everything becomes defeq. You don't even really need to prove a theorem like (s t : finset α) : s ⊆ s ∪ t because you can just apply the set version. All lemmas about bounded quantification over set also apply to bounded quantification over finset, etc.

[Reid Barton]

(The other, more substantial advantage is that all the decidable_eq stuff disappears, but that comes with tradeoffs.)

[Reid Barton]

I think the current definition of finset probably comes from Coq or something but it doesn't fit the mathematician's idea of a finite set, which is first and foremost a set, that happens to be finite.

[Reid Barton]

Actually, we could probably achieve much of these "everything becomes more straightforward" advantages just by changing the definition of finsetto have an underlying set field, without simultaneously making things classical.

[Johan Commelin]

So it would have a set field and a multiset and a proof that they are "equal"?

[Johan Commelin]

But I guess that breaks the "everything is straightforward" part of the multiset-finset interface

[Johan Commelin]

Not saying that's a dealbreaker

[Reid Barton]

I guess if you wanted to do the constructive version of this then you would consider s : set together with a "finiteness structure" on s, which would be some kind of subsingleton (e.g. trunc (\Sigma n, s \~- fin n))

[Reid Barton]

But yeah, you could also do what you suggested.

[Reid Barton]

But I'd rather go completely classical. I'm just worried about what the story is going to be for computing, say, finset.sum over a singleton.

[Reid Barton]

As far as I can tell, effectively the only purpose of this decidable_eq stuff in finset/fintype is so that finset.sum+relatives will reduce on things like empty sets and singletons (is that it? I thought about finset.insert too but finset.sum_insert doesn't seem to be true by rfl actually).

[Mario Carneiro]

To my mind, the reason finset has a separate name is because it's not just the same as a finite set. If you want a finite set you can say that - a set that is finite

[Reid Barton]

But in that case we should port all the finset.sum, finset.min etc stuff to set + finite where it would be used

[Mario Carneiro]

Well yes, I thought we had made plans about that as well (c.f. finsum)

[Mario Carneiro]

In particular I think that in most cases you can leave off the finiteness assumptions in the definitions

[Reid Barton]

I still really hate this style.

[Mario Carneiro]

I don't think that partial functions does anyone any favors

[Mario Carneiro]

particularly when they get involved in stating structures and things, and you need to write proofs inline

[Reid Barton]

I don't understand how the proposed changes (change argument of sum from finset to set and pass finiteness assumptions to lemmas) won't make long calc manipulations of sums a lot messier.

[Reid Barton]

Particularly when the indexing set of the sum is changing through the calculation

[Mario Carneiro]

If each index set is "structurally" finite, then we can use a typeclass on set.finite to discharge it

[Reid Barton]

Oh boy you might have found something I hate even more :upside_down:

[Mario Carneiro]

importantly, we won't have to worry about carrying the original finiteness proof through all the manipulations and getting a mismatch when a new proof also applies

[Mario Carneiro]

Then again, in a case like this it seems like finset might be more your cup of tea. So why the use of sets?

[Reid Barton]

Well, for example, because I have a set R which is definable in an o-minimal structure and so I know either it's finite or contains an interval. If it's finite I want to take the smallest element (I also know it's nonempty), if it contains an interval I want to do something else.

[Reid Barton]

Currently I think what I do is: if it's finite then I use set.finite.to_finset to get a finset, then take the min of that, and then I need to do a bit of arguing to show how it relates to my original set.

[Mario Carneiro]

simp?

[Reid Barton]

I don't remember exactly what I had to do, but it was effort that served no apparent real purpose.

[Reid Barton]

In this case it was just a local let inside a proof, so simp wouldn't be too bad, but if it was an auxiliary top-level definition, then the "no partial functions" style is really annoying because the proof of finiteness now becomes a second top-level thing that you have to pass around as well

[Mario Carneiro]

I mean you could use {s // finite s} in some of these applications, but I don't know about giving this type the full mathlib treatment because it is isomorphic to finset and the API is the same

[Reid Barton]

Replacing finset with this is exactly what I want to do, and I don't agree that the API is the same.

[Mario Carneiro]

the functions are the same, the lemmas are the same

[Mario Carneiro]

don't come to me about defeq

[Mario Carneiro]

For <s, h> I'd rather see that as a lean limitation that we can't customize the function that this invokes

[Reid Barton]

Well this is very frustrating. All I can say is that I find finset consistently more difficult to deal with than the set equivalent. For a long time I thought it was just me, but finally I realized that it doesn't have to be this way.

[Mario Carneiro]

If you really want to do it, the API would have to be at least as large as finset.lean. Half baked APIs make me sad

[Reid Barton]

Of course, my intention was to replace finset entirely

[Reid Barton]

so that's why I'm more interested in the question: what will break?

[Mario Carneiro]

But I don't see that as an option, because finset has its place as a nodups multiset

[Mario Carneiro]

Perhaps that's a niche thing, but it's distinct

[Mario Carneiro]

we can change the name if it makes it easier

[Mario Carneiro]

As I said: the API is the same, so nothing should break, in particular if fintype remains based on the old finset

[Mario Carneiro]

fintype instances need to compute

[Mario Carneiro]

and they are occasionally defeq-forced, so replacing them with something noncomputable isn't going to fly

[Reid Barton]

Ideally fintype would become a proposition as well, and where something computational is really needed, we would use fin_enum. However I'm not sure how important this is.

[Mario Carneiro]

That seems reasonable; the fact that fintype instances lose the order is occasionally problematic

[Mario Carneiro]

so what would be the typeclass for finiteness of sets? would you reuse fintype (\u s) or would set.finite s be a class?

[Reid Barton]

I wasn't intending to change the status quo in terms of having finite as an unbundled predicate and finset as a bundled structure for set, and fintype as a class for types... it seems fairly reasonable to me

[Reid Barton]

in particular finiteness of sets is often non-structural, e.g., if s ⊆ t and t is finite then s is finite... I guess the same thing can happen with an injective map of types but maybe it's less important there?

[Mario Carneiro]

I mean would the type in instances be [fintype (\u s)] : fintype (\u (s \cap t)) or [set.finite s] : set.finite (s \cap t)

[Johan Commelin]

I think injective maps are important enough to please let set.finite not be a class.

[Mario Carneiro]

both would work I think, the second one requires set.finite to be a class which has occasional consequences for freezing which are sometimes undesirable for a proposition

[Reid Barton]

I see, I think the first one is okay. But now I also realize I think I haven't had so much experience with fintype directly.

[Reid Barton]

If you want fintype on \u of some set though then it makes sense to have structural instances for this that are parallel to finite.union, ... I guess.

[Mario Carneiro]

but now maybe we're losing the whole {s // finite s} thing this way

[Reid Barton]

I'm not sure what these instances would bottom out to though

[Mario Carneiro]

I would still prefer that finite s be defined as it is now, in terms of old finset

[Reid Barton]

Like why would you have any instance of fintype (\u s) in the first place (aside from if s : set t where fintype t)

[Mario Carneiro]

you might have finite s and haveI a fintype (\u s) instance

[Mario Carneiro]

maybe that's too much trouble?

[Mario Carneiro]

Working with finite sets in this way is probably always going to be a little brittle. It's easy to misplace the finiteness proofs

[Mario Carneiro]

I have always found it very easy to work with finset as currently defined because of its robust API, but that's only when dealing with them as finsets and not necessarily when interfacing with sets

[Mario Carneiro]

aagh I hate defeq

[Reid Barton]

I think finite would end up sort of like is_subgroup in that (besides maybe being used to implement finset) it ends up getting used mainly to mediate between the set world and the finset world

[Reid Barton]

like in the definable set example I gave before, where you have a set and then later you acquire the information that it's finite

[Mario Carneiro]

I mean you can do all that with the current API

[Mario Carneiro]

I'm sorry the function that does it has a name

[Reid Barton]

right, and you end up with 100-character long simp onlys instead of nothing

[Mario Carneiro]

nothing, he says

[Reid Barton]

I guess I don't understand the apparent opposition. Like is it a problem that (x, y).fst is defeq to x? Should we have only a propositional equality?

[Reid Barton]

Why would it be unreasonable to think "finite set" = subtype set.finite?

[Mario Carneiro]

I really hate this aspect of lean, that it makes one look so much worse than the other even though they are about the same complexity

[Mario Carneiro]

If defeq wasn't a thing then they would be the same, and you could set up the "refl"-equivalent tactic to work with whatever you say

[Mario Carneiro]

in lean that tool is simp but it does just a bit too much

[Reid Barton]

Right, I agree that this whole conversation is somehow an artifact of DTT

[Mario Carneiro]

Is there a way we can fix this with more notation?

[Mario Carneiro]

like make the constructor easier to call, and add a custom simp set to make the simp only more palatable

[Mario Carneiro]

I think if we start bending over backwards to make all the defeqs work out we will lose, because it is impossible to please everyone

[Mario Carneiro]

all equalities should be defeqs

[Reid Barton]

Already Johan's suggestion of adding "... and a set, such that it's equal to the multiset" would be an improvement. Then all the lemmas that say that union commutes with taking the underlying sets get baked into the definitions of those operations.

[Reid Barton]

But since (independently of this issue) it's also quite annoying to deal with finset.inter and so on having these decidable_eq instances which may or may not be coherent, and considering that in the end, it's unclear how much working constructively really buys us, it seems to me that doing things classically would be better anyways. And at that point just using subtype set.finite seems like a welcome simplification.

[Kyle Miller]

I wonder if this might be a good setup. It lets you reuse all the fintype machinery, so it might make fleshing out the interface easier.

import data.fintype.basic

structure new_finset (α : Type*) :=
(to_set : set α)
(finite : fintype to_set)

def set.to_new_finset {α : Type*} (s : set α) [fintype s] : new_finset α :=
new_finset.mk s (by apply_instance)

instance {α : Type*} : has_coe (new_finset α) (set α) :=
⟨new_finset.to_set⟩

@[simp]
lemma new_finset.coe {α : Type*} (s : new_finset α) : s.to_set = s := rfl

instance new_finset.fintype {α : Type*} (s : new_finset α) : fintype s :=
s.finite

[Kyle Miller]

The current finset would still exist somewhere but with a new name.

[Kyle Miller]

You also get a fairly nice new_finset.univ:

def new_finset.univ {α : Type*} [fintype α] : new_finset α :=
{ to_set := set.univ,
  finite := by apply_instance }

[Adam Topaz]

Wouldn't this get annoying because you would have to deal with the coercion from the set to the associated subtype?

[Kyle Miller]

If you want to go between set and finset you already have to use set.to_finset and finset's lift to set.

But something that would likely be a problem is that there are non-defeq fintype instances... so I retract this proposal. (Maybe it'd be ok with nonempty (fintype to_set).)

[Kyle Miller]

Reviving this thread, I'm wondering whether there's a reason the first definition was chosen over the second:

def set.finite (s : set α) : Prop := nonempty (fintype s)
-- versus
def set.finite (s : set α) : Prop := ∃ (t : finset α), s = ↑t

[Kyle Miller]

Also, in case it changes the calculus of including a noncomputable finset, docs#set_like would be a way to implement one with a little less boilerplate (but still, it would be an undertaking to do it this way):

import tactic

universes u

structure finset' (α : Type u) :=
(s : set α)
(finite' : ∃ (t : finset α), s = ↑t)

namespace finset'
variables {α : Type u}

instance : set_like (finset' α) α :=
⟨finset'.s, λ p q h, by { cases p, cases q, congr' }⟩

@[simp] lemma mem_coe {s : finset' α} {x : α} : x ∈ s.s ↔ x ∈ (s : set α) := iff.rfl

@[ext] theorem ext {s t : finset' α} (h : ∀ x, x ∈ s ↔ x ∈ t) : s = t := set_like.ext h

/-- Copy of a `finset'` with a new `s` equal to the old one. Useful to fix definitional
equalities. See See Note [range copy pattern]. -/
protected def copy (s : finset' α) (t : set α) (hs : t = ↑s) : finset' α :=
{ s := t,
  finite' := hs.symm ▸ s.finite' }

lemma finite (s : finset' α) : ∃ (t : finset α), (s : set α) = (t : set α) := s.finite'

noncomputable instance : has_coe (finset' α) (finset α) := ⟨λ s, s.finite.some⟩

@[simp] lemma coe_set_finset (s : finset' α) : ((s : finset α) : set α) = s :=
s.finite.some_spec.symm

noncomputable instance (s : finset' α) : fintype s :=
(set.finite_mem_finset (s : finset α)).fintype

end finset'