Zulip Chat Archive

Stream: new members

Topic: Set.Finite and Finset


Tobias Leichtfried (Nov 07 2024 at 14:59):

Hi! I'm new to Mathlib.
I need some way to express that a collection of elements is finite. The Mathematics in Lean Book makes heavy use of Fintype/Finset so I tried using Finset. I found working with it however cumbersome, because constructing at new Finset is somewhat difficult. I discovered now the Set.Finite predicate in the library, with a note that it should be preferred in theorems. My questions is now, which to use when?

Yaël Dillies (Nov 07 2024 at 15:33):

Hey! In what context do you want to work with finite sets?

Tobias Leichtfried (Nov 07 2024 at 16:27):

I am formalizing nondeterministic pushdown automata. These have a transition function which when given the state at a point in time return a set of possible new states.

Philippe Duchon (Nov 07 2024 at 17:10):

From what you are describing, it looks like your finite sets are all subsets of a finite set? So you could probably work with a S: Fintype for your global set of states, and X: Set S for a set X of states?

Tobias Leichtfried (Nov 08 2024 at 06:41):

No, that is not possible, as the automaton can push a list of arbitrary length on the stack, so there is a non finite amount of possible next states

Eric Wieser (Nov 08 2024 at 06:55):

Can you give an example of a Finset that you are finding difficult to construct?

Tobias Leichtfried (Nov 08 2024 at 12:24):

A very concrete example would be the following snippet

abbrev transition_fun' (G : ContextFreeGrammar T) [Fintype G.NT] (_ : Q) (Z : S G) : Set (Q × List (S G)) :=
  match Z with
  | nonterminal N => { (Q.loop, α) | (α : List (S G)) (_ : N, α  G.rules) }
  | _ => 

The set which this function returns is finite, because G.rules is a list. But more generally a ordinary Set I can construct just using a predicate, a finset can not be constructed this way if there is no obvious finite superset.


Last updated: May 02 2025 at 03:31 UTC