Upcoming closure results for regular languages in mathlib

Stream: CSLib

[Ching-Tsun Chou]

Hi, in view of mathlib#31247, the closure theorems of regular languages under complement, union, and intersection will appear in mathlib soon and their names will conflict with our versions of the same results in:
https://github.com/leanprover/cslib/blob/main/Cslib/Computability/Languages/RegularLanguage.lean
I'm wondering what we should do. I can think of two options:
(1) Delete our versions of those results when we start using the version of mathlib containing those results.
(2) Keep our versions of those results but rename them (say, with a prime) to avoid conflicts and add a comment to point out that the same results also appear in mathlib.
Personally I prefer (2) because I think the proofs using our definitions of DFA are of independent interest. What do you think?
I should point out that mathlib#31247 does not contain the indexed union and intersection versions of those results.

[Shreyas Srinivas]

I think those results are better placed in CSLib

[Shreyas Srinivas]

Namespacing will take care of these conflicts for the most part.

[Ching-Tsun Chou]

Cslib does not make its own version of a mathematical notion if it already exists in mathlib (except when the notion is a primary object of interest to cslib, such as automata). Since mathlib already has the notions of Language and Language.IsRegular, cslib inherits them from mathlib and only adds new definitions and theorems about them that are not (yet) in mathlib. Previously (for example) the theorem Language.IsRegular.compl was not in mathlib, but it is now. So the options are either (1) delete Language.IsRegular.compl from cslib or (2) rename it to something else. Wrapping Language.IsRegular.compl in the Cslib namespace is just one way of doing the renaming.

[Eric Wieser]

If the statements are identical then you should always just delete the cslib one

[Eric Wieser]

If the statements are different in a trivial way, you should align them (either by PRing to mathlib, or by adapting CSLib) then delete the cslib one.

[Eric Wieser]

If they are different in a non-trivial way (i.e. different definitions of NFAs) then you should try to rename one or both to avoid ambiguity

[Eric Wieser]

Which case is this?

[Chris Henson]

Yes, exactly what Eric says in general. In either case, can you make a PR to the nightly-testing branch with the required changes? I think the failure there is because of this.

[Eric Wieser]

It looks like the only one I can see causing trouble is docs#Language.isRegular_iff, which mentions a mathlib DFA on the RHS. I think if cslib wants the same notion for its own dfa, then Language.isRegular_iff_cslibDFA is reasonable enough as a new name

[Eric Wieser]

The mathlib one could quite reasonable rename to isRegular_iff_dfa

[Chris Henson]

Our now-duplicate Language.mem_inf is the failure in CI.

[Eric Wieser]

I assume it falls into the first case? (docs#Language.mem_inf)

[Ching-Tsun Chou]

They are exactly the same semantically, but one is proved using mathlib's definition of DFA and the other using cslib's definition of DA (which doesn't include the accepting states). Let me do this:
(1) I'll make a PR to rename the relevant theorems with comments saying that they will be removed after a future mathlib bump in cslib. This should fix the nightly-testing failures.
(2) After the mathlib bump, I'll do another PR to remove the theorems.

[Eric Wieser]

As far as Lean is concerned, two theorems are identical if they have the same statement. Generally mathlib doesn't keep around multiple ways to prove the same thing.

[Eric Wieser]

I assume you're not talking about mem_inf which is proved by Set.mem_inter_iff

[Chris Henson]

If theorems are to be removed on bumping Mathlib, it is preferable to make just a single PR to the nightly-testing branch.

[Ching-Tsun Chou]

I was talking about Language.IsRegular.{compl,add,inf}.

[Ching-Tsun Chou]

Never mind. I realized I was being stupid. I'll make a PR for the nightly-testing branch.

[Chris Henson]

Okay, thanks! I might have normally taken care of this already, but was busy with travel. Your thinking ahead is appreciated.

[Ching-Tsun Chou]

I'll do it tomorrow. Too late today.

[Ching-Tsun Chou]

PR: cslib#209

[Kim Morrison]

@Ching-Tsun Chou, could you please run lake exe shake --fix on your PR?

[Ching-Tsun Chou]

Thanks for pointing it out. I've just pushed a fix.

[Notification Bot]

8 messages were moved from this topic to #general > Using shake in new projects by Kim Morrison.