The regular expression of the sublists of a word

The sublists of a word w form a regular language, matched by the product of the letters of w, each made optional. It is the dual of the shuffle ideal of w (Language.shuffleIdeal), the words of which w is a sublist.

Main definitions

• RegularExpression.sublists w: the letters of w in order, each optional.

Main results

• RegularExpression.matches'_sublists: sublists w matches exactly the sublists of w.

def RegularExpression.sublists {α : Type u_1} (w : List α) : RegularExpression α

The regular expression of the sublists of w: its letters in order, each optional.

Equations

• RegularExpression.sublists w = List.foldr (fun (a : α) (P : RegularExpression α) => (RegularExpression.char a + 1) * P) 1 w

@[simp]

theorem RegularExpression.sublists_nil {α : Type u_1} : sublists [] = 1

@[simp]

theorem RegularExpression.sublists_cons {α : Type u_1} (a : α) (w : List α) : sublists (a :: w) = (char a + 1) * sublists w

theorem RegularExpression.matches'_sublists {α : Type u_1} (w : List α) : (sublists w).matches' = {v : List α | v.Sublist w}

sublists w matches exactly the sublists of w.

theorem RegularExpression.mem_matches'_sublists {α : Type u_1} {v w : List α} : v ∈ (sublists w).matches' ↔ v.Sublist w