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