feat: proof of Myhill-Nerode theorem for DFAs

[akhilesh-balaji]

Re-opening #479 which was accidentally closed. Thanks very much, @ctchou, for going through it and making edits.

This PR adds a proof of the Myhill-Nerode theorem. It builds on the definition of right congruence (and associated definitions and theorems) in #278. These are the main results shown (the statement of the theorem has been taken from Wikipedia and amended slightly):

(1) L regular iff. ∼_L (distinguishability by L, also called the Nerode
congruence) has a finite number of equivalence classes N.
(2) N is the number of states in the minimal DFA accepting L.
(3) The minimal DFA is unique up to unique isomorphism. That is, for any
minimal DFA acceptor, there exists exactly one isomorphism from it to the
following one:

Let each equivalence class ⟦ x ⟧ correspond to a state, and let state
transitions be a : ⟦ x ⟧ → ⟦ x a ⟧ for each a ∈ Σ.
Let the starting state be ⟦ ϵ ⟧, and the accepting states be ⟦ x ⟧ where
x ∈ L.

[ctchou]

Thanks for re-opening the PR. I have a few more comments.

[akhilesh-balaji]

I have made all the changes. Also, in RegularLanguage, we have:

theorem IsRegular.iff_dfa {l : Language Symbol} :
    l.IsRegular ↔ ∃ State : Type, ∃ _ : Finite State,
      ∃ dfa : DA.FinAcc State Symbol, language dfa = l

At some point, we should ideally change this to use ∃ State : Type*, as ∃ State : Type makes proving theorems with State: Type* much more difficult. For now, I have used (in MyhillNerode):

theorem dfa_num_state_min {State : Type} {M : DA.FinAcc State α} [Finite State] :
    Nat.card State ≥ Nat.card (language M).NerodeQuotient

rather than State: Type*. Otherwise, when showing Finite (language M).NerodeQuotient, I would have to downcast the type universe, etc. The other theorems still use State: Type*.

[ctchou]

The State in the theorem IsRegular.iff_dfa is only a Type and not a Type* because this is how Language.IsRegular is defined in mathlib:
https://leanprover-community.github.io/mathlib4_docs/Mathlib/Computability/DFA.html#Language.IsRegular
And mathlib does this for a good reason: changing State : Type to State : Type* simply does not work in Leen's type system. We have a similar pattern in the definition of OmegaLanguage.IsRegular as well:
https://api.cslib.io/docs/Cslib/Computability/Languages/OmegaRegularLanguage.html#Cslib.%CF%89Language.IsRegular
You can try changing the Type to Type* and see what happens.

There are theorems that let you "lift" the state spaces to Type*:
https://leanprover-community.github.io/mathlib4_docs/Mathlib/Computability/DFA.html#Language.isRegular_iff
https://api.cslib.io/docs/Cslib/Computability/Languages/OmegaRegularLanguage.html#Cslib.%CF%89Language.isRegular_iff
But I usually don't bother with them, because we are dealing with finite types here and there seems no loss of generality in having those finite types living in Type 0, rather than some higher Type u.

[ctchou]

We are getting close to an approvable shape in the organization and statements of definitions and theorems.

@chenson2018: maybe you want to take a look as well? I have not tried any proof golfing.

[ctchou]

@akhilesh-balaji Please mark those comments which you have fixed as resolved. Thanks!

[akhilesh-balaji]

Done.

Please explain what "Nerode congruence" means. Later you talk about c_l without explaining what it means. Also, be consistent with the use of lowercase vs uppercase: either all l or all L. Don't mix them.

I have defined c_l now when stating the three parts of the theorem. Also, c_l has been defined when instance NerodeCongruence appears, and so I keep referring to this c_l. I can of course rephrase all the docstrings to be in plain English but this would arguably make it harder to read.

[ctchou]

Thanks for making the changes. I just pushed a commit to re-word the main comment a bit. I also turned on the CI.

I'm pretty happy with the overall structure of this PR now. I would like to take a closer look at the proofs, but that will take a few days. I hope @chenson2018 will be able to take a look as well.

[ctchou]

I removed some redundant lines. Please do not add redundant -- lines.

[ctchou]

@akhilesh-balaji There are some CI failures which you should look into. I always run locally the following steps for any PR of my own:

lake exe mk_all --module
lake build
lake lint
lake test

and correct all errors or warnings reported by them.

[akhilesh-balaji]

The linter appears to have failed here:

  /- The `impossibleInstance` linter reports:
  SOME INSTANCES HAVE ARGUMENTS THAT ARE IMPOSSIBLE TO INFER
  These are arguments that are not instance-implicit and do not appear in
  another instance-implicit argument or the return type. -/
  -- Cslib.Computability.Languages.MyhillNerode
  /home/runner/work/cslib/cslib/Cslib/Computability/Languages/MyhillNerode.lean:48:1: error: @Language.NerodeCongruence argument 2 l : Language
    α
  /home/runner/work/cslib/cslib/Cslib/Computability/Languages/MyhillNerode.lean:192:1: error: @Cslib.Automata.DA.FinAcc.StateCongruence argument 3 M : Cslib.Automata.DA.FinAcc
    State α

This can be fixed easily if instance is changed back to def. I am unsure of how else to get around this; I would appreciate your advice on the same.

The other errors are suggestions to change existing proofs in other files to use NerodeQuotient. For instance:

Try to change the left-hand side to the simplified term!
  /home/runner/work/cslib/cslib/Cslib/Computability/Languages/RegularLanguage.lean:154:1: error: @Cslib.Language.IsRegular.mul Left-hand side simplifies from
    (l1 * l2).IsRegular
  to
    Finite (l1 * l2).NerodeQuotient
  using
    simp only [*, @Language.IsRegular.iff_finite_nerodeQuotient]
  Try to change the left-hand side to the simplified term!

Wouldn't this affect the readability of these other theorems, or should I go ahead and implement the changes suggested by the linter?

Thank you.

[ctchou]

@akhilesh-balaji I just pushed a commit that fixes the linter errors. I changed the instances to defs and added the @[impliict_reducible] attributes to those new defs. I also removed a number of @[simp] attributes. Some of them triggered the simpNF errors, while the others of them are probably useless because the conclusion of the tbeorem is not something you would typically try to rewrite. In general, I prefer to add theorems to the simp database sparingly and add @[simp] only when I expect the theorem will be used outside the current file for rewriting.

Note that the old code in the existing files have already been linted. So the errors reported by the linter are almost always caused by the new code.

[akhilesh-balaji]

Thank you for fixing the linter errors, @ctchou.

[chenson2018]

@ctchou If you'll ping me once you approve, I can take a last look at any golfing/style before merging.

[ctchou]

@chenson2018 I just merged in the latest "main" branch.