finite set with default representation

Stream: Is there code for X?

[Paige Thomas]

Is there a type of finite set that has a builtin default representation, such as a requirement that the elements can be sorted and a representation of them as a sorted list?

[Paige Thomas]

Perhaps Batteries.RBSet.

[Johan Commelin]

@Kayla Thomas Something like docs#Fintype ?

[Johan Commelin]

If you want to be able to sort the elements, you additionally need to assume something like LinearOrder

[Yaël Dillies]

docs#FinEnum ?

[Paige Thomas]

I'm not sure. I'm trying to replace the Lists here in this representation of finite state automata with something equivalent to a finite set, but that is computable and displayable.

structure SymbolStepMultiple
  (α : Type)
  [DecidableEq α]
  (σ : Type)
  [DecidableEq σ] :
  Type :=
  (start_state : σ)
  (symbol : α)
  (stop_state_list : List σ)
  deriving Repr


structure EpsilonStepMultiple
  (σ : Type)
  [DecidableEq σ] :
  Type :=
  (start_state : σ)
  (stop_state_list : List σ)
  deriving Repr


structure EpsilonNFA
  (α : Type)
  [DecidableEq α]
  (σ : Type)
  [DecidableEq σ] :
  Type :=
  (symbol_step_list : List (SymbolStepMultiple α σ))
  (epsilon_step_list : List (EpsilonStepMultiple σ))
  (starting_state_list : List σ)
  (accepting_state_list : List σ)
  deriving Repr

[Paige Thomas]

That is, I want to be able to extract the result of evaluating it and display it.

[Paige Thomas]

I can do that with List, but trying to prove equivalence to a regular language isn't going so well, so trying to simplify it a bit.

[Daniel Weber]

Can't you define a representation for docs#Finset? Either have it unsafe, I'm not sure how that works, or assume some kind of order

[Eric Wieser]

Finset already has an (unsafe) representation, docs#Finset.instRepr

[Paige Thomas]

What are the implications of it being unsafe? Should I be worried about that?

[Eric Wieser]

It means you can't prove things about the string representation

[Eric Wieser]

If you want something safe, you can use docs#Finset.sort to get a list that you can print "safely"

[Paige Thomas]

I see. Thank you.