Zulip Chat Archive

Stream: new members

Topic: Working with finite subsets of a set


view this post on Zulip Adam Topaz (Jun 05 2020 at 23:12):

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.

view this post on Zulip Mario Carneiro (Jun 06 2020 at 00:01):

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

view this post on Zulip Mario Carneiro (Jun 06 2020 at 00:03):

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.

view this post on Zulip Mario Carneiro (Jun 06 2020 at 00:05):

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

view this post on Zulip Mario Carneiro (Jun 06 2020 at 00:07):

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

view this post on Zulip Adam Topaz (Jun 06 2020 at 00:40):

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 :)

view this post on Zulip Mario Carneiro (Jun 06 2020 at 01:07):

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

view this post on Zulip Mario Carneiro (Jun 06 2020 at 01:09):

like this:

def my_axiom :=  {S : set T},  U : finset T, U  S  P (f S) (f U)

view this post on Zulip Adam Topaz (Jun 06 2020 at 01:48):

Ah. Yes, I completely agree. Thanks!


Last updated: May 08 2021 at 10:12 UTC