concatenations of a pair of sets of lists

Stream: Is there code for X?

[Paige Thomas]

How would one go about defining this so that it type checks: def blah (α : Type) (R S : List α) := { r ++ s : List α | r ∈ R ∧ s ∈ S }? That is, the set of all concatenations of lists from two sets of lists, where the list that is first comes from the first set.

I get "invalid patterns, r is an explicit pattern variable, but it only occurs in positions that are inaccessible to pattern matching .(List.append r s)"

[Ruben Van de Velde]

First step would be to correct the types of R and S

[Ruben Van de Velde]

Then try (r ++ s) including the parentheses

[Paige Thomas]

def blah (α : Type) (R S : Set (List α)) := { (r ++ s) : List α | r ∈ R ∧ s ∈ S }
gives the same error.

[Kyle Miller]

def blah (α : Type) (R S : Set (List α)) := {r ++ s | (r ∈ R) (s ∈ S)}

[Ruben Van de Velde]

Thanks Kyle, I knew it was something with parentheses

[Paige Thomas]

huh, ok. I'm not sure what is going on there.

[Paige Thomas]

what does it mean without the ∧?

[Paige Thomas]

because this also fails def blah (α : Type) (R S : Set (List α)) := {(r ++ s) : List α | (r ∈ R) ∧ (s ∈ S)}.

[Ruben Van de Velde]

It's like \forall (r ∈ R) (s ∈ S), ...

[Paige Thomas]

I see. And it looks like the issue was that I put parentheses around the r ++ s, which I was doing in order to give the type to satisfy the type inference.

[Paige Thomas]

among other things

[Paige Thomas]

Thank you!

[Paige Thomas]

Is there a way to define the same thing but using Finset?

[Paige Thomas]

I'm trying to check that these definitions are what I want, but I can't #eval a Set.

def blah
  {α : Type}
  (R S : Set (List α)) :
  Set (List α) :=
  { r ++ s | (r ∈ R) (s ∈ S) }


def blah_n
  {α : Type}
  (R : Set (List α)) :
  ℕ → Set (List α)
  | Nat.zero => R
  | Nat.succ n => blah R (blah_n R n)

#eval blah_n {[('a' : Char)]} 2

[Paige Thomas]

And this is because I am trying to define a more concrete instance of docs#RegularExpression and I'm having trouble defining the language of the closure operator (Kleene star).

[Paige Thomas]

inductive RegExp (α : Type) : Type
  | char : α → RegExp α
  | epsilon : RegExp α
  | zero : RegExp α
  | union : RegExp α → RegExp α → RegExp α
  | concat : RegExp α → RegExp α → RegExp α
  | closure : RegExp α → RegExp α


def RegExp.languageOf (α : Type) : RegExp α → Set (List α)
  | char x => { [x] }
  | epsilon => { [] }
  | zero => ∅
  | union R S => R.languageOf ∪ S.languageOf
  | concat R S => { r ++ s | (r ∈ R.languageOf) (s ∈ S.languageOf) }
  | closure R => sorry

[Paige Thomas]

(unfolding the XY problem)