feat(computability/*FA): is_regular

[foxthomson]

---

• depends on: [Merged by Bors] - feat(computability/epsilon_nfa): epsilon-NFA definition #6108

[foxthomson]

This still shows remnants of #6108, I will merge master when that one goes through.

[bryangingechen]

This structure's fields contain data in σ and M, and we usually only name structures is_X when they are Props.

Also, you're using is_regular l hypotheses below in square brackets, and these are usually instantiated via type class search, so either those arguments should be made explicit, or this structure should be turned into a class.

Maybe you can say a little bit about how you envision using this structure, as the right design will depend on what you plan to do with it, and the usages below are all fairly trivial.

[eric-wieser]

I would guess that this probably should be a Prop

[gebner]

Indeed, is_regular should be a Prop. (And it should have a single universe parameter.) There are a lot of equivalent properties that describe regular languages (accepted by a DFA, matched by a regex, generated by a regular grammar, having finite index, ...). The idea is that is_regular should provide an API that is independent of the concrete model.

Probably the easiest way around the universe issues is to define regularity in terms of regular expressions (though we're still missing the equivalence between regexps and DFAs for the pumping lemma then):

@[irreducible] def is_regular (l : language α) : Prop :=
∃ R : regular_expression α, l = R.matches

If we want to stick with DFAs for the definition, then σ should be in Type, as Eric commented:

@[irreducible] def is_regular (l : language α) : Prop :=
∃ (σ : Type) [fintype σ] (M :  DFA α σ), l = M.accepts

(Note that you can't use structure to define this type if it is in Prop, because then Lean can't create the projection to the fields σ, _inst_1 and M.)

[eric-wieser]

I think ∃ (n : nat) (M : DFA α (fin n)), l = M.accepts might be slightly easier to work with, as it avoids dealing with instances in quantifiers

[eric-wieser]

You can then add a lemma to say that the universe-polymorphic statement is equivalent.

[github-actions]

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

• [Merged by Bors] - feat(computability/epsilon_nfa): epsilon-NFA definition #6108

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

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

[eric-wieser]

This universe polymorphism is likely to cause you unnecessary pain - it means that "regular in universe u" and "regular in universe u+1" are different statements. Since all fintypes are isomorphic to a type in Type, the statements are all equivalent so you may as well just quantify over Type or just fin n

[gebner]

You define is_regular as a structure, but then use it like a class [is_regular l]. I don't know if it is a good idea to make is_regular a class or not. I think both options could work. But it is important to stay consistent.

If you keep is_regular as it is and don't make it a class (which is probably the safe choice), then please don't use it in brackets [is_regular l].

On the other hand, if you make is_regular a class, then please (1) make it class when you define it, (2) consistently use [is_regular l], and (3) make DFA.is_regular an instance.

[gebner]

Indeed, is_regular should be a Prop. (And it should have a single universe parameter.) There are a lot of equivalent properties that describe regular languages (accepted by a DFA, matched by a regex, generated by a regular grammar, having finite index, ...). The idea is that is_regular should provide an API that is independent of the concrete model.

Probably the easiest way around the universe issues is to define regularity in terms of regular expressions (though we're still missing the equivalence between regexps and DFAs for the pumping lemma then):

@[irreducible] def is_regular (l : language α) : Prop :=
∃ R : regular_expression α, l = R.matches

If we want to stick with DFAs for the definition, then σ should be in Type, as Eric commented:

@[irreducible] def is_regular (l : language α) : Prop :=
∃ (σ : Type) [fintype σ] (M :  DFA α σ), l = M.accepts

(Note that you can't use structure to define this type if it is in Prop, because then Lean can't create the projection to the fields σ, _inst_1 and M.)

[gebner]

Suggested change

	lemma pumping_lemma (l : language α) [hreg : is_regular l] {x : list α} (hx : x ∈ l)
	(hlen : fintype.card hreg.σ + 1 ≤ list.length x) :
	∃ a b c, x = a ++ b ++ c ∧ a.length + b.length ≤ fintype.card hreg.σ + 1 ∧ b ≠ [] ∧
	lemma pumping_lemma (l : language α) (hreg : is_regular l) :
	∃ n, ∀ x ∈ l, n ≤ x.length →
	∃ a b c, x = a ++ b ++ c ∧ a.length + b.length ≤ n ∧ b ≠ [] ∧

In the spirit of "don't leak implementation details".

[foxthomson]

Perhaps it may be better to leave this until we have equivalence of regular expressions and DFA's. Then the definition can be in terms of regular_expression.