feat(Computability/Languages): regular languages have matching regular expressions through Kleene’s Algorithm

[chiyunhsu]

We introduce IsRegular.iff_regex, a language is regular if and only if it matches a regular expression. It is a combination of the existing IsRegular.regex, a language matching a regular expression is regular and our new direction. The new direction is proven through Kleene’s algorithm.

It is the result that was anticipated in PR#846 by @ctchou.       

The pull request introduces a new file, KleeneAlgorithm.lean. In it, we proved a language defined by a DFA on Fin n with one accepting state has a matching regular expression. The algorithm applies induction on a bound which restricts which interior states that a run may pass through.  

Implemented collaboratively by Brooke Gill and Chi-Yun Hsu

[ctchou]

This is the first batch of my comments. I will have more in the future.

My general point is that by defining FLTS.execution, you can express directly the concepts in the textbook proof, rather than using bespoke recursive definitions. This allows you to leverage the large number of results about lists in mathlib.

[ctchou]

I think you can benefit from having the following functions about List:

namespace List

variable {α : Type*}

def AllButFirstLast (p : α → Bool) (as : List α) : Prop :=
  ∀ i, ∀ _ : 0 < i ∧ i + 1 < as.length, p as[i]

def findIdxButFirst (p : α → Bool) (as : List α) : ℕ :=
  as.tail.findIdx p + 1

def revFindIdxButLast (p : α → Bool) (as : List α) : ℕ :=
  as.length - as.reverse.findIdxButFirst p

end List

Then not only a lot of your definitions can be simplified (see the inline comments), but you can state and prove properties about the above List functions without distractions.

I have not looked into the proofs in detail.

[ctchou]

I think this whole block of code can be replaced by:

namespace Cslib.LTS

variable {Symbol : Type*} {n : ℕ}

def BddExec (lts : LTS (Fin n) Symbol) (bound : ℕ)
    (start : Fin n) (xs : List Symbol) (last : Fin n) (ss : List (Fin n)) : Prop :=
  lts.Execution start xs last ss ∧ ss.AllButFirstLast (· < bound)

def bddLang (lts : LTS (Fin n) Symbol) (bound : ℕ) (start last : Fin n) : Language Symbol :=
  { xs | ∃ ss, lts.BddExec bound start xs last ss }

end Cslib.LTS

Note that your main proof will refer to different starts, lasts, and bounds in the same statement, so it is better to have them as explicit parameters rather than as fields of structures which you need to construct and destruct all the time.

[ctchou]

Just a nitpick: use i instead of idx. I understand that you want to use i, j, k etc to denote states from Fin n. But I think it is clearer to keep denoting the latter using s, t, r, etc.

[ctchou]

It is in general a good idea to include only those parameters which are actually needed:

def splitFirst (xs : List Symbol) (ss : List (Fin n)) (k : Fin n) : List Symbol :=
  xs.take (ss.findIdxButFirst (· = k))

def splitFirstCompl (xs : List Symbol) (ss : List (Fin n)) (k : Fin n) : List Symbol :=
  xs.drop (ss.findIdxButFirst (· = k))

The same comment applies to SplitLast[Compl] above.

[ctchou]

I think it is probably better to put the splitLast section after the splitFirst section, because the latter seems easier to reason about than the former.