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]

Instead of defining this specialized notion PathSupp, I think you should define the following general notion:

namespace Cslib.FLTS
def execution (flts : FLTS State Label) (s : State) : List Label → List State
  | [] => [s]
  | μ :: μs => s :: flts.execution (flts.tr s μ) μs
end Cslib.FLTS

which you can place in the file FLTS/Basic.lean. So far as I can tell, you need PathSupp only to define BddPath in the following expression:

∀ i ∈ PathSupp p.toFLTS p.start xs, i < p.bound

whch you can express as:

let ss := p.toFLTS.execution p.start xs
∀ k, ∀ _ : 0 < k ∧ k + 1 < ss.length, ss[k] < p.bound

Other expressions involving membership in PathSupp can be similarly translated.

I make this suggestion because execution is a cleaner notion which will have simpler properties and can have more general applications in the future. The above expression is also a more direct translation of the informal proof. Lean's grind tactic is very good at reasoning about simple properties of natural numbers, so you shouldn't have any problem working with list indices.

Also, this whole section should be in the namespace Cslib.FLTS.

[ctchou]

BTW, you may want to consider doing the proof using NFA rather than DFA. (Dexter Kozen's textbook has the proof.) LTS.Execution is already defined and a number of theorems proved about it. I suspect there may be less "noise" in that setup.

[chiyunhsu]

I agree with the suggestion of using Execution than PathSupp.

I am now contemplating on the reasons whether NFA approach would be more preferable than DFA approach.
More preferble:

• LTS.Execution is defined. Defining FLTS.Execution duplicates the code (unless there might other usages? I feel that FLTS.Execution would not be huge.)
• Explicit NFA -> Regex rather than implicit NFA -> DFA -> Regex as currently is (but is it needed?)

Less preferable:

• The current LTS/Execution.lean has no lemmas about bounding the states. Everything should be rewritten and strengthened, so back to the previous question, is explicit NFA -> Regex so preferable? And would this strengthened (probably longer codes) worth not defining FLTS.Execution?

I am all ears to hear what you think before we start to rewrite the codes for better applications in the future.

[ctchou]

It seems to me that the crux of the proof is to formalize Figure 3.3 of Hopcroft et al's textbook. Given an execution in the sense of LTS.Execution and the additional assumption that no state in the execution is > k, you can obtain the indices of the occurrences of k using Nat.nth p, where the predicate p is something like:

fun j => ∃ _ : 0 < j ∧ j + 1 < ss.length, ss[j] = k

Then using those indices you can extract the relevant segments of ss and xs using List.extract (which degenerates to List.take and List.drop for the first and last of them). Then you need to show that those extracted segments are LTS.Execution in their own right and have the necessary properties to make them members of the various R_ij^(k) sets. But there are a lot of results about Nat.nth, List.extract, LTS.Execution, etc in mathlib and cslib that you can leverage and Lean's grind tactic is very good at reasoning about list indices.

Alternatively, you can continue to use concepts like splitFirst and splitLast. Here I would suggest that instead of splitting the list directly, you use List.findIdx to find the index of the occurrence of k and then split the list using List.take and List.drop with that index. Your theorems like split{First,Last}_append are then just instances of the existing theorem List.take_append_drop.

[chiyunhsu]

Thanks for making more detailed suggestions. To clarify, it sounds like there are multiple routes to change the code:

1. Define new FLTS.Execution to replace the role of PathSupp.
2. Use existing LTS.Execution to replace the role of PathSupp. This will involve FLTS.toLTS.
3. Upgrade the PR to prove Kleene's algorithm for NFA -> Regex. Use existing LTS.Execution.

Which route are you suggesting us to take?

[ctchou]

Number 3. I think the determinism of FLTS is a distraction.

The hard part of the proof is to identify the occurrences of k in an execution and reason about them. It doesn't really matter whether the execution is from a deterministic or nondeterministic machine. There just happens to be more infrastructure already developed for the latter in cslib.

[ctchou]

See my comment about splitFirst below.

[ctchou]

Using the notion of FLTS.execution mentioned above, I think splitFirst can be defined more directly without recursion: just use List.findIdx or its variants to search for k in FLTS.execution and then use the returned index to extract the sub-list via List.take. For splitFirstCompl, use List.drop instead of List.take. Mathlib has a lot of theorems about List.{findIdx,take,drop} which I suspect can simplify many of your proofs or even make some of your theorems unnecessary.

For splitLast[Compl], reverse FLTS.execution before applying List.findIdx.

Alternatively, Nat.nth and Nat.count let you talk about the occurrences of k directly:
https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Nat/Nth.html