feat(Automata): Regular languages are closed under reversal. - #775
Conversation
The commit adding Cslib/Foundations/Semantics/LTS/Reverse.lean did not add the corresponding import to Cslib.lean, so lake exe mk_all --check failed in CI.
ctchou
left a comment
ctchou
left a comment
There was a problem hiding this comment.
Except for the minor import issue, I think this PR is ready for merge.
|
|
||
| open Acceptor Language | ||
|
|
||
| variable {Symbol State : Type*} |
There was a problem hiding this comment.
| variable {Symbol State : Type*} | |
| variable {State Symbol : Type*} |
to match the order of arguments to FinAcc
| 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 |
There was a problem hiding this comment.
Optional:
| 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 |
There was a problem hiding this comment.
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?
There was a problem hiding this comment.
I don't think it matters much!
ctchou
left a comment
ctchou
left a comment
There was a problem hiding this comment.
See my comment on Execution.reverse.
ctchou
left a comment
ctchou
left a comment
There was a problem hiding this comment.
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.
I'm not following this PR closely, but this suggestion of |
|
What is a better solution? A single |
|
@chenson2018 Do you want to add anything concerning the proof of |
| simp only [Accepts, reverse_mTr] | ||
| aesop |
There was a problem hiding this comment.
We typically have tried to standardize on using grind over aesop. I note that
| 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?
There was a problem hiding this comment.
Yeah - I added them as lemmas.
| use by grind | ||
| grind [reverse_tr] |
There was a problem hiding this comment.
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.)
|
In view of @chenson2018 's comment above, I just pushed a patch that replaced the first |
|
Hi @eric-wieser and @chenson2018 Have all your concerns been addressed in this PR? It seems to me ready to merge. Thanks in advance! |
| public import Cslib.Computability.Automata.NA.Basic | ||
| public import Cslib.Foundations.Semantics.LTS.Reverse | ||
|
|
||
| /-! # Reversal of nondeterministic automata. -/ |
There was a problem hiding this comment.
Perhaps this should have a few sentences noting that this defines Cslib.Automata.NA.FinAcc.reverse, and that reverse_language_eq proves that the language accepted by this automata is the Language.reverse of the one accepted by the original.
In general, it's handy for module docstring to call out the key results.
Same for the other files.
There was a problem hiding this comment.
Addressed - for NA/Reverse.lean and LTS/Reverse.lean.
eric-wieser
left a comment
eric-wieser
left a comment
There was a problem hiding this comment.
Just minor documentation nits; otherwise this now looks great!
chenson2018
left a comment
chenson2018
left a comment
There was a problem hiding this comment.
It looks like Eric's last comments were addressed. Thanks for the contribution!
|
Thanks everyone! |
4 participants
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.leandefines the reversal of aFinAccand 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.reverseinRegularLanguage.leanto 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.