The powerset DFA (as it is defined in Lecture 4) has subsets of Q (the states of the original NFA) as its states. However, the automaton definitions in this formalisation don't use finite sets of states but instead lists over a Fintype Q. So we need to define something like a powerset but for lists. We also need to prove that the resulting "powerlist" contains only finitely many elements because the states of an NFA have to be of a Fintype.

def List.power_upto {α : Type u_1} (l : List α) (n : Nat) : List (List α)

The powerset of a set X just contains all possible subsets of X. (See Set.lean) We define the power of a list l as the list containing all lists up to the length if l with elements from l. The following recursive function computes all lists with elements from a given list l that have a length up to n. This includes lists with duplicate elements and all possible sequences. We do this by repeatedly appending elements of l to all lists we currently have.

Equations

• l.power_upto n = List.power_upto.loop l n

def List.power_upto.loop {α : Type u_1} (l : List α) : Nat → List (List α)

Equations

• List.power_upto.loop l 0 = [[]]
• List.power_upto.loop l n.succ = List.power_upto.loop l n ++ List.flatMap (fun (l' : List α) => List.map (fun (e : α) => e :: l') l) (List.power_upto.loop l n)

This example shows how the power of a list is computed. As you can see, all the different lists are added to the powerlist multiple times.

After defining the power of a list, we can use this function to compute the Powertype of a Fintype and prove that it is also finite. As a reminder: a Fintype is a type with a corresponding list ("elems") containing all things of this type (refer to Fintype.lean for further information).

The following 4 theorems are auxiliary results required to prove that for a Fintype T with elements of type α T.elems.power_upto (T.elems.length) contains all lists of type List α that are at most of the same length as T.elems.

theorem nil_power {α : Type u_1} (n : Nat) (l : List α) : l = [] → l.power_upto n = [[]]

the result of [].power_upto n is [[]] for all n.

theorem mem_power_upto_n {α : Type u_1} (T : Fintype α) (l : List α) : l.length ≤ Fintype.elems.length → l ∈ Fintype.elems.power_upto l.length

T.elems.power_upto n contains every List α of length n

theorem mem_power_upto_n' {α : Type u_1} (T : Fintype α) (l : List α) (n : Nat) : n ≤ Fintype.elems.length → l.length = n → l ∈ Fintype.elems.power_upto n

theorem inclusion_succ {α : Type u_1} (T : Fintype α) (l : List α) (n : Nat) : l.length ≤ Fintype.elems.length → l ∈ Fintype.elems.power_upto n → l ∈ Fintype.elems.power_upto (n + 1)

If a list l is contained in T.elems.power_upto n, then it is also an element of l ∈ T.elems.power_upto (n+1).

theorem inclusion {α : Type u_1} (T : Fintype α) (l : List α) (n m : Nat) : n ≤ m → l ∈ Fintype.elems.power_upto n → l ∈ Fintype.elems.power_upto m

theorem powerlist {α : Type u_1} (T : Fintype α) (l : List α) : l.length ≤ Fintype.elems.length → l ∈ Fintype.elems.power_upto Fintype.elems.length

Now we can finally prove that the powerlist of T.elems contains all lists of length at most T.elems.length:

We use Finset instead of Set here because it enables easier proofs for (e.g.) DecidablePred (a ∈ X) and DecidableEq.

def Powertype (α : Type u) : Type u

Equations

• Powertype α = Finset α

instance instMembershipPowertype {α : Type u_1} : Membership α (Powertype α)

Equations

• instMembershipPowertype = { mem := fun (S : Powertype α) (a : α) => Finset.mem a S }

instance Finset.instFintypeOfFintype {α : Type u_1} [T : Fintype α] [DecidableEq α] : Fintype (Finset α)

Equations

• Finset.instFintypeOfFintype = { elems := List.map (fun (x : Finset' α) => Finset.mk x) (Fintype.elems.power_upto Fintype.elems.length), complete := ⋯ }

instance instFintypePowertypeOfDecidableEq {α : Type u_1} [T : Fintype α] [DecidableEq α] : Fintype (Powertype α)

Equations

• instFintypePowertypeOfDecidableEq = Finset.instFintypeOfFintype