Working with finite subsets of a set

Stream: new members

[Adam Topaz]

Hi everyone. I'm trying to figure out whether there is a "standard" way to work with finite sets using what already exists in mathlib.

Specifically, I want to do some things with finite subsets of a given arbitrary subset of a type, and (eventually) to be able to prove lemmas by induction on the elements of a given finite subset.

I can think of at least three ways to define this in lean. See the code below for the three possible definitions of the set of finite subsets U of a given set S.

import data.set.finite
variables {T : Type*} (S : set T)

def finite_subsets_1 :=
{ U : set T | U ⊆ S ∧ set.finite U }

def finite_subsets_2 :=
{ U : set T | U ⊆ S ∧ ∃ V : finset T, ↑V = U }

def finite_subsets_3 :=
{ U : set T | U ⊆ S ∧ ∃ L : list T, ∀ u ∈ U, u ∈ L }

I'm sure there are some benefits and/or pitfalls with using one definition over another, and I hope someone with more experience with lean and mathlib can point be in the right direction!

My initial guess is to use definition 3, since it allows to immediately access a list which enumerates the elements of the finite subset (possibly with repetition). I know that finset is defined as a subtype of multiset which is a quotient of list T so definition 2 is not far off from 3, and mathlib might have a better api for finsets. But I suspect that producing a finite subset with definition 2 would be more annoying due to the overhead necessary in defining finset from list.

[Mario Carneiro]

I would suggest finite_subsets_2, except that you should forget about U and only use V (and S if you must)

[Mario Carneiro]

Using either set.finite or finset there is a recursion principle that allows you to prove theorems by induction by adding elements one at a time to the empty list. For list this is built in.

[Mario Carneiro]

would be more annoying due to the overhead necessary in defining finset from list

This is the wrong way to think about it. The overhead has nothing to do with the stack of definitions that bring the target API down to the axioms, because these proofs are not "run" when you use them, they were proved once and now you reuse them. The overhead instead depends on how closely the provided API matches your use case

[Mario Carneiro]

(or, to turn it around, how easily you can adapt your use case to fit the provided API)

[Adam Topaz]

Thanks Mario. I should mention that, unfortunately, in my use I don't think I can avoid the coersion from finset T to set T, since I have a function, say f which must be defined for all of set T, and I need to write down an axiom roughly similar to the shape of my_axiom in the code below:

import data.set.finite
import data.finset
variables {T : Type*} (T' : Type*)
variables (P : T' → T' → Prop) (f : set T → T')

def finite_subsets (S : set T) :=
{ U : set T | U ⊆ S ∧ ∃ V : finset T, ↑V = U }

def my_axiom := ∀ {S : set T}, ∃ U ∈ finite_subsets S, P (f S) (f U)

Anyway, I'll try to look through the finset api in mathlib. I did notice the to_finset function which which probably be enough for what I need anyway :)

[Mario Carneiro]

I didn't mean avoid the coercion, I mean to avoid having a variable of type set

[Mario Carneiro]

like this:

def my_axiom := ∀ {S : set T}, ∃ U : finset T, ↑U ⊆ S ∧ P (f S) (f ↑U)

[Adam Topaz]

Ah. Yes, I completely agree. Thanks!