feat(Automata): Regular languages are closed under reversal. - #775
feat(Automata): Regular languages are closed under reversal. #775Lsonic233 wants to merge 11 commits into
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.
| obtain ⟨mid, h1, h2⟩ := LTS.MTr.split hmtr | ||
| simp only [LTS.MTr.singleton_iff] at h2 | ||
| exact ⟨mid, h2, ih.mpr h1⟩ | ||
|
|
There was a problem hiding this comment.
Can you add the result about CanReach too?
There was a problem hiding this comment.
Generally it would be good to write a theorem about every def in Cslib/Foundations/Semantics/LTS/Basic.lean, assuming there is something true to state!
There was a problem hiding this comment.
Will do. Would this be an exhaustive list of theorems to prove?
CanReach
UnlabelledTr - this relation gets flipped
image - image of a state in reverse is the preimage in original
imageMultistep - same as above
HasOutLabel - outgoing labels in the reverse are its incoming labels in the original.
BoundedUpTo - reversal preserves this
There was a problem hiding this comment.
Those all sound great!
There was a problem hiding this comment.
While you are at it, could you also add a corresponding theorem for LTS.Execution? I hope that doesn't require too much work.
There was a problem hiding this comment.
Wrote up proofs for the theorems stated above - please let me know if there is anything to be added.
For LTS.Execution I wrote down a long and not so reader friendly proof - claude helped use more automation and make it compact.
| obtain ⟨mid, h1, h2⟩ := LTS.MTr.split hmtr | ||
| simp only [LTS.MTr.singleton_iff] at h2 | ||
| exact ⟨mid, h2, ih.mpr h1⟩ | ||
|
|
There was a problem hiding this comment.
While you are at it, could you also add a corresponding theorem for LTS.Execution? I hope that doesn't require too much work.
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?
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 |
| ext xs | ||
| simp only [mem_language, mem_reverse, accepts_reverse] |
There was a problem hiding this comment.
Terminal simp should not be squeezed
| ext xs | |
| simp only [mem_language, mem_reverse, accepts_reverse] | |
| ext; simp |
| 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?
| 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 |
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.