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

Cslib.lean

@@ -21,6 +21,7 @@ public import Cslib.Computability.Automata.NA.Hist
 public import Cslib.Computability.Automata.NA.Loop
 public import Cslib.Computability.Automata.NA.Pair
 public import Cslib.Computability.Automata.NA.Prod
+public import Cslib.Computability.Automata.NA.Reverse
 public import Cslib.Computability.Automata.NA.Sum
 public import Cslib.Computability.Automata.NA.ToDA
 public import Cslib.Computability.Automata.NA.Total
@@ -106,6 +107,7 @@ public import Cslib.Foundations.Semantics.LTS.MapLabel
 public import Cslib.Foundations.Semantics.LTS.Notation
 public import Cslib.Foundations.Semantics.LTS.OmegaExecution
 public import Cslib.Foundations.Semantics.LTS.Relation
+public import Cslib.Foundations.Semantics.LTS.Reverse
 public import Cslib.Foundations.Semantics.LTS.Simulation
 public import Cslib.Foundations.Semantics.LTS.Termination
 public import Cslib.Foundations.Semantics.LTS.Total

Cslib/Computability/Automata/NA/Reverse.lean

@@ -0,0 +1,61 @@
+/-
+Copyright (c) 2026 Vignesh Karri. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Vignesh Karri
+-/
+
+module
+
+public import Cslib.Computability.Automata.NA.Basic
+public import Cslib.Foundations.Semantics.LTS.Reverse
+
+/-! # Reversal of nondeterministic automata. -/
+
+@[expose] public section
+
+namespace Cslib.Automata.NA
+
+open Acceptor Language
+
+variable {State Symbol : Type*}
+
+namespace FinAcc
+
+/-- `na.reverse` reverses every transition of `na` and swaps its start and accept states,
+so that it accepts exactly the reversals of the words accepted by `na`. -/
+def reverse (na : FinAcc State Symbol) : FinAcc State Symbol where
+  toLTS := na.toLTS.reverse
+  start := na.accept
+  accept := na.start
+
+/-- Reversing an automaton twice gives back the original automaton. -/
+@[simp]
+theorem reverse_reverse (na : FinAcc State Symbol) : na.reverse.reverse = na := rfl
+
+/-- Reversal of an automaton is an involution. -/
+theorem reverse_involutive : Function.Involutive (reverse (State := State) (Symbol := Symbol)) :=
+  reverse_reverse
+
+/-- The multistep transitions of `na.reverse` are exactly the reversed multistep transitions
+of `na`. -/
+@[simp]
+theorem reverse_mTr (na : FinAcc State Symbol) {xs : List Symbol} {s s' : State} :
+    na.reverse.MTr s' xs s ↔ na.MTr s xs.reverse s' := LTS.reverse_mTr
+
+/-- `na.reverse` accepts a word iff `na` accepts its reversal. -/
+@[simp]
+theorem accepts_reverse {na : FinAcc State Symbol} {xs : List Symbol} :
+    Accepts na.reverse xs ↔ Accepts na xs.reverse := by
+  simp only [Accepts, reverse_mTr]
+  aesop
+
+/-- `na.reverse` accepts exactly the reversals of the words accepted by `na`. -/
+@[simp]
+theorem reverse_language_eq (na : FinAcc State Symbol) :
+    language na.reverse = (language na).reverse := by
+  ext xs
+  simp only [mem_language, mem_reverse, accepts_reverse]
+
+end FinAcc
+
+end Cslib.Automata.NA

Cslib/Computability/Languages/RegularLanguage.lean

@@ -11,6 +11,7 @@ public import Cslib.Computability.Automata.DA.Prod
 public import Cslib.Computability.Automata.DA.ToNA
 public import Cslib.Computability.Automata.NA.Concat
 public import Cslib.Computability.Automata.NA.Loop
+public import Cslib.Computability.Automata.NA.Reverse
 public import Cslib.Computability.Automata.NA.ToDA
 public import Mathlib.Computability.DFA
 public import Mathlib.Computability.RegularExpressions
@@ -190,6 +191,21 @@ theorem IsRegular.congr_fin_index {Symbol : Type}
   use Quotient c.eq, inferInstance, ⟨c.toDA, {a}⟩
   exact DA.FinAcc.congr_language_eq
 
+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
+
 /-- The language containing only the one character string `a` is regular. -/
 @[simp]
 theorem IsRegular.char (a : Symbol) : ({[a]} : Language Symbol).IsRegular := by

Cslib/Foundations/Semantics/LTS/Reverse.lean

@@ -0,0 +1,112 @@
+/-
+Copyright (c) 2026 Vignesh Karri. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Vignesh Karri
+-/
+
+module
+
+public import Cslib.Foundations.Semantics.LTS.Execution
+
+/-!
+# Reverse operation for LTS.
+-/
+
+@[expose] public section
+
+namespace Cslib.LTS
+
+variable {State Label : Type*}
+
+section Reverse
+
+/-- Constructs an LTS by reversing the transitions of an existing LTS. -/
+def reverse (lts : LTS State Label) : LTS State Label where
+  Tr s μ s' := lts.Tr s' μ s
+
+/-- The transitions of `lts.reverse` are exactly the reversed transitions of `lts`. -/
+@[simp]
+theorem reverse_tr {lts : LTS State Label} :
+    (lts.reverse).Tr s μ s' ↔ lts.Tr s' μ s := by rfl
+
+/-- Reversing an LTS twice gives back the original LTS. -/
+@[simp]
+theorem reverse_reverse (lts : LTS State Label) : lts.reverse.reverse = lts := rfl
+
+/-- Reversal of an LTS is an involution. -/
+theorem reverse_involutive : Function.Involutive (reverse (Label := Label) (State := State)) :=
+  reverse_reverse
+
+/-- The multistep transitions of `lts.reverse` are exactly the reversed multistep transitions of
+`lts`. -/
+@[simp]
+theorem reverse_mTr {lts : LTS State Label} :
+    lts.reverse.MTr s' μs s ↔ lts.MTr s μs.reverse s' := by
+  induction μs generalizing s s' with
+  | nil =>
+    simp [eq_comm]
+  | cons x xs ih =>
+    simp_rw [List.reverse_cons, MTr.append_iff, MTr.singleton_iff, MTr.cons_iff, and_comm, ih,
+      reverse_tr]
+
+/-- `lts.reverse` can reach `s'` from `s` iff `lts` can reach `s` from `s'`. -/
+@[simp]
+theorem reverse_canReach {lts : LTS State Label} :
+    lts.reverse.CanReach s s' ↔ lts.CanReach s' s := by
+  simp only [CanReach, reverse_mTr]
+  conv_rhs => rw [List.reverse_involutive.surjective.exists]
+
+/-- The unlabelled transitions of `lts.reverse` are those of `lts` with the endpoints swapped. -/
+@[simp]
+theorem reverse_unlabelledTr {lts : LTS State Label} :
+    lts.reverse.UnlabelledTr s s' ↔ lts.UnlabelledTr s' s := Iff.rfl
+
+/-- The `μ`-image of a state in `lts.reverse` is its `μ`-preimage in `lts`. -/
+@[simp]
+theorem reverse_image {lts : LTS State Label} :
+    lts.reverse.image s μ = {s' | lts.Tr s' μ s} := rfl
+
+/-- Membership form of `reverse_image`. -/
+theorem mem_reverse_image {lts : LTS State Label} :
+    s' ∈ lts.reverse.image s μ ↔ s ∈ lts.image s' μ := Iff.rfl
+
+/-- The `μs`-image of a state in `lts.reverse` is its `μs.reverse`-preimage in `lts`. -/
+@[simp]
+theorem reverse_imageMultistep {lts : LTS State Label} :
+    lts.reverse.imageMultistep s μs = {s' | lts.MTr s' μs.reverse s} :=
+  Set.ext fun _ => reverse_mTr
+
+/-- Membership version of `reverse_imageMultistep`. -/
+theorem mem_reverse_imageMultistep {lts : LTS State Label} :
+    s' ∈ lts.reverse.imageMultistep s μs ↔ s ∈ lts.imageMultistep s' μs.reverse := reverse_mTr
+
+/-- A state has `μ` as an outgoing label in `lts.reverse` iff it has `μ` as an incoming
+label in `lts`. -/
+@[simp]
+theorem reverse_hasOutLabel {lts : LTS State Label} :
+    lts.reverse.HasOutLabel s μ ↔ ∃ s', lts.Tr s' μ s := Iff.rfl
+
+/-- `lts.reverse` is bounded up to `n` iff `lts` is. -/
+@[simp]
+theorem reverse_boundedUpTo {lts : LTS State Label} {n : ℕ} :
+    lts.reverse.BoundedUpTo n ↔ lts.BoundedUpTo n := by
+  constructor <;> intro h s₁ μs s₂ hmtr <;> simpa using h s₂ μs.reverse s₁ (by simpa using hmtr)
+
+/-- Reversing an execution of `lts` gives an execution of `lts.reverse`, with the labels, states
+and endpoints reversed. -/
+theorem Execution.reverse {lts : LTS State Label} (h : lts.Execution s μs s' ss) :
+    lts.reverse.Execution s' μs.reverse s ss.reverse := by
+  obtain ⟨_, _, _, _⟩ := h
+  use by simpa
+  grind only [reverse_tr, = List.getElem_reverse, = List.length_reverse]
+
+/-- An execution of `lts.reverse` is an execution of `lts` with the labels, states
+and endpoints reversed. -/
+@[simp]
+theorem reverse_execution {lts : LTS State Label} :
+    lts.reverse.Execution s μs s' ss ↔ lts.Execution s' μs.reverse s ss.reverse :=
+  ⟨fun h => by simpa using h.reverse, fun h => by simpa using h.reverse⟩
+
+end Reverse
+
+end Cslib.LTS