feat(Automata): Regular languages are closed under reversal.

[Lsonic233]

Proves that A^R = {w^R | w ∈ A} is regular if A is regular, i.e regular languages are closed under reversal. The proof takes the NFA for A and constructs a new NFA by swapping the accept and start states and reversing all the transition arrows.

Reverse.lean defines the reversal of a FinAcc and proves that it accepts the reverse of the language accepted by the original automaton. The Language reversal is defined in mathlib.

Added a theorem IsRegular.reverse in RegularLanguage.lean to prove that regular languages are closed under reversal.

AI Usage : I wrote down all the theorem statements and initial proofs with minimal. I then used claude to rewrite proofs for style compliance.

[ctchou]

Except for the minor import issue, I think this PR is ready for merge.

[eric-wieser]

Suggested change

	variable {Symbol State : Type*}
	variable {State Symbol : Type*}

to match the order of arguments to FinAcc

[eric-wieser]

Optional:

Suggested change

	open NA in
	/-- The reversal of a regular language is regular. -/
	theorem IsRegular.reverse {l : Language Symbol} (h : l.IsRegular) : (l.reverse).IsRegular := by
	rw [IsRegular.iff_nfa] at h ⊢
	obtain ⟨State, h_fin, nfa, rfl⟩ := h
	use State, inferInstance, nfa.reverse, FinAcc.reverse_language_eq nfa
	/-- A language is regular iff its reversal is regular. -/
	@[simp]
	theorem IsRegular.reverse_iff {l : Language Symbol} : (l.reverse).IsRegular ↔ l.IsRegular := by
	constructor
	· intro h
	simpa using IsRegular.reverse h
	· exact IsRegular.reverse
	open NA in
	/-- A language is regular iff its reversal is regular. -/
	@[simp]
	theorem IsRegular.reverse_iff {l : Language Symbol} : l.reverse.IsRegular ↔ l.IsRegular := by
	simp_rw [IsRegular.iff_nfa]
	congr! 4
	rw [FinAcc.reverse_involutive.surjective.exists]
	simp [FinAcc.reverse_language_eq, Language.reverse_injective.eq_iff]
	alias ⟨_, IsRegular.reverse⟩ := IsRegular.reverse_iff

[Lsonic233]

Your proof looks better - we could replace the congr! 4 line with refine exists₂_congr fun State _ => ?_.
Also the previous proof follows the same pattern that all other closure proofs follow (reversal stands out because its the only iff theorem of the closure ones). Would you recommend switching it out for this?

[ctchou]

See my comment on Execution.reverse.

[ctchou]

Actually Execution.reverse can be proved in two lines using grind:

  use by grind
  grind [reverse_tr]

Note that the definition of LTS.Execution consists of a universally quantified statement over successive pairs of states in ss plus some boundary conditions, which are the sort of things that grind is very good at using and proving. There are enough facts about List.reverse already in mathlib that you don't even need to think about them.

[chenson2018]

See my comment on Execution.reverse.

I'm not following this PR closely, but this suggestion of use by grind seems like a very odd style to me.

[ctchou]

What is a better solution? A single grind [reverse_tr] didn't work. The goal has the following form:

  ∃ _ : ss.length = μs.length + 1, ss[0] = s1 ∧ ss[ss.length - 1] = s2 ∧
  ∀ k, {_ : k < μs.length} → lts.Tr ss[k] μs[k] ss[k + 1]

[ctchou]

@chenson2018 Do you want to add anything concerning the proof of Execution.reverse which you are not very happy about? Personally I think this PR is ready to merge.

[ctchou]

LGTM now.

[chenson2018]

We typically have tried to standardize on using grind over aesop. I note that

Suggested change

	simp only [Accepts, reverse_mTr]
	aesop
	have : na.reverse.start = na.accept := rfl
	have : na.reverse.accept = na.start := rfl
	grind [Accepts, reverse_mTr]

works. Should the have here be lemmas?

[Lsonic233]

Yeah - I added them as lemmas.

[chenson2018]

Both uses of grind here are fragile in that grind? fails. (And for whatever reason linter.tacticAnalysis.verifyGrindOnly won't detect it, which is troubling). If you can turn these into a grind only that works that is fine, otherwise this becomes painful for maintenance.

(@ctchou I suppose I don't have a problem with use here looking at the signature. I had thought previously this would be nicer if Execution were a structure but had trouble with this refactor. If you ever feel like trying this out yourself please feel free.)

[ctchou]

In view of @chenson2018 's comment above, I just pushed a patch that replaced the first grind by simpa and the second by grind only [...]. It seems that explicitly unpacking the hypothesis h helped grind? find a grind only that actually works.