Set.Finite and Finset

Stream: new members

[Tobias Leichtfried]

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]

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

[Tobias Leichtfried]

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]

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]

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]

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

[Tobias Leichtfried]

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.