[Merged by Bors] - feat(computability/regular_expressions): define regular expressions

[foxthomson]

Very basic definitions for regular expressions

---

• depends on: [Merged by Bors] - feat(computability/language): define formal languages #5291

[eric-wieser]

Lifting this from a "resolved" comment so that it doesn't get lost...

---

You'll find when you try to prove (a + b) + c = a + (b + c) to form a monoid instance, as the page on Kleene algebras suggests is sensible notation, that you can't; you can only prove ∀ x, ((a + b) + c).rmatch x ↔ (a + (b + c)).rmatch x, which can't be put in a monoid instance.

If you instead work with quot (λ r s, ∀ l, r.rmatch l = s.rmatch l) or perhaps quotient if you fancy building a setoid, then you can prove that lemma.

[gebner]

I feel like the definitions go completely the wrong way here. First you define the Brzozowski derivative, and only at the end show that the algorithm matches the expected language.

I think it would be better to have it be the other way around, with the more fundamental definition first. First define the language of the regular expression, and only then show that it can be computed using the derivative:

def matches : regular_expression α → set (list α)
| zero := ∅
| null := {[]}
| (char x) = {[x]}
| (comp r1 r2) = r1.matches ∪ r2.matches
...

def deriv : regular_expression α → α → regular_expression α
...

def rmatch : regular_expression α → list α → bool
...

lemma rmatch_correct (r : regular_expression α) (xs : list α) :
  r.rmatch xs ↔ r.match xs :=
...

It might also be a good idea to introduce an explicit language type:

@[derive has_union, derive has_emptyc]
def language (α) := set (list α)

namespace language

instance : has_mul (language α) := -- composition

def star (l : language α) : language α := ...

end language

Then you can state properties about star more easily, like (star r).matches = r.matches.star (also makes for nice simp lemmas!).

You could also define the derivative on languages first, but I'm not sure how much this would help with the long proofs here.

[github-actions]

🎉 Great news! Looks like all the dependencies have been resolved:

• [Merged by Bors] - feat(computability/language): define formal languages #5291

💡 To add or remove a dependency please update this issue/PR description.

Brought to you by Dependent Issues (:robot: ). Happy coding!

[gebner]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests