regexp.concrete.universe

In the construction of an automata for a given regular expression, we build the state space inductively starting at the singleton set and taking the disjoint union at each step. We define the inductive type sort which is the reification of finite types build thus. Having these finite types reified thus ensures easy extraction and subsequent synthesis of subsets, relations, and transition functions on these finite sets.

Inductive sort :=
| Unit : sort
| CoProd : sort → sort → sort.

We use the following notation for sorts for ease of readability

Notation "'𝟙'" := Unit : concrete_scope.
Notation "A '∐' B" := (CoProd A B) (at level 50, left associativity) : concrete_scope.

The denotational semantics of sort is given by the function denote given below

Fixpoint denote (s : sort) : finType :=
  match s with
  | 𝟙 ⇒ unit
  | s1 ∐ s2 ⇒ denote s1 + denote s2
  end%type.

For the sort s, unless there is ambiguity, we use s to also denote the associated finite type given by denote