From 559a00e9e55e6d7bbbe30e476b2ceb3f5fdc17e2 Mon Sep 17 00:00:00 2001
From: Vignesh Karri <vigneshkarri5@gmail.com>
Date: Tue, 4 Aug 2026 22:50:47 +0530
Subject: [PATCH 01/11] feat(Automata): reversal of NFA

---
 Cslib.lean                                    |  1 +
 Cslib/Computability/Automata/NA/Reverse.lean  | 62 +++++++++++++++++++
 .../Languages/RegularLanguage.lean            |  9 +++
 3 files changed, 72 insertions(+)
 create mode 100644 Cslib/Computability/Automata/NA/Reverse.lean

diff --git a/Cslib.lean b/Cslib.lean
index d74457919..8557261bc 100644
--- a/Cslib.lean
+++ b/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
diff --git a/Cslib/Computability/Automata/NA/Reverse.lean b/Cslib/Computability/Automata/NA/Reverse.lean
new file mode 100644
index 000000000..ac62640f1
--- /dev/null
+++ b/Cslib/Computability/Automata/NA/Reverse.lean
@@ -0,0 +1,62 @@
+/-
+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
+
+/-! # Reversal of nondeterministic automata. -/
+
+@[expose] public section
+
+namespace Cslib.Automata.NA
+
+open Acceptor Language
+
+variable {Symbol State : Type*}
+
+/-- `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 FinAcc.reverse (na : FinAcc State Symbol) : FinAcc State Symbol where
+  Tr s x t := na.Tr t x s
+  start := na.accept
+  accept := na.start
+
+/-- Reversing an automaton twice gives back the original automaton. -/
+@[simp]
+theorem FinAcc.reverse_reverse (na : FinAcc State Symbol) : na.reverse.reverse = na := rfl
+
+/-- The multistep transitions of `na.reverse` are exactly the reversed multistep transitions
+of `na`. -/
+theorem reverse_mtr (na : FinAcc State Symbol) {xs : List Symbol} {s s' : State}
+    (hmtr : na.MTr s xs.reverse s') : na.reverse.MTr s' xs s := by
+  induction xs generalizing s s' with
+  | nil =>
+    simp_all
+  | cons x xs ih =>
+    simp only [List.reverse_cons] at hmtr
+    simp only [LTS.MTr.cons_iff]
+    obtain ⟨mid, h1, h2⟩ := LTS.MTr.split hmtr
+    simp only [LTS.MTr.singleton_iff] at h2
+    exact ⟨mid, h2, ih h1⟩
+
+/-- `na.reverse` accepts exactly the reversals of the words accepted by `na`. -/
+theorem reverse_language_eq (na : FinAcc State Symbol) :
+    language (na.reverse) = (language na).reverse := by
+  ext xs
+  simp only [mem_language, mem_reverse]
+  constructor
+  · intro h
+    simp only [Accepts] at h ⊢
+    obtain ⟨s, hs, s', hs', hmtr⟩ := h
+    rw [← List.reverse_reverse xs] at hmtr
+    exact ⟨s', hs', s, hs, reverse_mtr na.reverse hmtr⟩
+  · intro h_na
+    simp only [Accepts] at h_na ⊢
+    obtain ⟨s, hs, s', hs', hmtr⟩ := h_na
+    exact ⟨s', hs', s, hs, reverse_mtr na hmtr⟩
+
+end Cslib.Automata.NA
diff --git a/Cslib/Computability/Languages/RegularLanguage.lean b/Cslib/Computability/Languages/RegularLanguage.lean
index f97e124b8..e42acadd2 100644
--- a/Cslib/Computability/Languages/RegularLanguage.lean
+++ b/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
@@ -206,6 +207,14 @@ theorem IsRegular.char (a : Symbol) : ({[a]} : Language Symbol).IsRegular := by
     · induction xs using List.reverseRec <;> grind
     · simp_all [flts, List.append_eq_cons_iff]
 
+open NA in
+/-- The reversal of a regular language is regular. -/
+@[simp]
+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, reverse_language_eq nfa
+
 /-- Languages matching regular expressions are regular. -/
 theorem IsRegular.regex {r : RegularExpression Symbol} :
     r.matches'.IsRegular := by

From 44c23e76afbdf44ea529ca04df736b54dc942cd4 Mon Sep 17 00:00:00 2001
From: Vignesh Karri <vigneshkarri5@gmail.com>
Date: Wed, 5 Aug 2026 01:52:38 +0530
Subject: [PATCH 02/11] feat(Automata): theorems in FinAcc namespace, closure
 iff for regular languages

---
 Cslib/Computability/Automata/NA/Reverse.lean  | 37 +++++++++++++------
 .../Languages/RegularLanguage.lean            | 10 ++++-
 2 files changed, 34 insertions(+), 13 deletions(-)

diff --git a/Cslib/Computability/Automata/NA/Reverse.lean b/Cslib/Computability/Automata/NA/Reverse.lean
index ac62640f1..006c13a92 100644
--- a/Cslib/Computability/Automata/NA/Reverse.lean
+++ b/Cslib/Computability/Automata/NA/Reverse.lean
@@ -18,30 +18,37 @@ open Acceptor Language
 
 variable {Symbol State : 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 FinAcc.reverse (na : FinAcc State Symbol) : FinAcc State Symbol where
+def reverse (na : FinAcc State Symbol) : FinAcc State Symbol where
   Tr s x t := na.Tr t x s
   start := na.accept
   accept := na.start
 
 /-- Reversing an automaton twice gives back the original automaton. -/
 @[simp]
-theorem FinAcc.reverse_reverse (na : FinAcc State Symbol) : na.reverse.reverse = na := rfl
+theorem reverse_reverse (na : FinAcc State Symbol) : na.reverse.reverse = na := rfl
 
 /-- The multistep transitions of `na.reverse` are exactly the reversed multistep transitions
 of `na`. -/
-theorem reverse_mtr (na : FinAcc State Symbol) {xs : List Symbol} {s s' : State}
-    (hmtr : na.MTr s xs.reverse s') : na.reverse.MTr s' xs s := by
+theorem reverse_mtr_iff (na : FinAcc State Symbol) {xs : List Symbol} {s s' : State} :
+    na.reverse.MTr s' xs s ↔ na.MTr s xs.reverse s' := by
   induction xs generalizing s s' with
   | nil =>
-    simp_all
+    simp_all [eq_comm]
   | cons x xs ih =>
-    simp only [List.reverse_cons] at hmtr
+    simp only [List.reverse_cons]
     simp only [LTS.MTr.cons_iff]
-    obtain ⟨mid, h1, h2⟩ := LTS.MTr.split hmtr
-    simp only [LTS.MTr.singleton_iff] at h2
-    exact ⟨mid, h2, ih h1⟩
+    constructor
+    · intro hmtr
+      obtain ⟨mid, h1, h2⟩ := hmtr
+      exact LTS.MTr.stepR na.toLTS (ih.mp h2) h1
+    · intro hmtr
+      obtain ⟨mid, h1, h2⟩ := LTS.MTr.split hmtr
+      simp only [LTS.MTr.singleton_iff] at h2
+      exact ⟨mid, h2, ih.mpr h1⟩
 
 /-- `na.reverse` accepts exactly the reversals of the words accepted by `na`. -/
 theorem reverse_language_eq (na : FinAcc State Symbol) :
@@ -52,11 +59,17 @@ theorem reverse_language_eq (na : FinAcc State Symbol) :
   · intro h
     simp only [Accepts] at h ⊢
     obtain ⟨s, hs, s', hs', hmtr⟩ := h
-    rw [← List.reverse_reverse xs] at hmtr
-    exact ⟨s', hs', s, hs, reverse_mtr na.reverse hmtr⟩
+    exact ⟨s', hs', s, hs, (reverse_mtr_iff na).mp hmtr⟩
   · intro h_na
     simp only [Accepts] at h_na ⊢
     obtain ⟨s, hs, s', hs', hmtr⟩ := h_na
-    exact ⟨s', hs', s, hs, reverse_mtr na hmtr⟩
+    exact ⟨s', hs', s, hs, (reverse_mtr_iff na).mpr hmtr⟩
+
+/-- `na.reverse` accepts a word iff `na` accepts its reversal. -/
+theorem reverse_na_accepts (na : FinAcc State Symbol) (xs : List Symbol) :
+    Accepts na.reverse xs ↔ Accepts na xs.reverse := by
+  exact Set.ext_iff.mp (reverse_language_eq na) xs
+
+end FinAcc
 
 end Cslib.Automata.NA
diff --git a/Cslib/Computability/Languages/RegularLanguage.lean b/Cslib/Computability/Languages/RegularLanguage.lean
index e42acadd2..ea939803b 100644
--- a/Cslib/Computability/Languages/RegularLanguage.lean
+++ b/Cslib/Computability/Languages/RegularLanguage.lean
@@ -213,7 +213,15 @@ open NA in
 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, reverse_language_eq nfa
+  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
 
 /-- Languages matching regular expressions are regular. -/
 theorem IsRegular.regex {r : RegularExpression Symbol} :

From 7fd28b39622ffca5cf0261ca3d7e2b8117149322 Mon Sep 17 00:00:00 2001
From: Vignesh Karri <vigneshkarri5@gmail.com>
Date: Wed, 5 Aug 2026 11:15:04 +0530
Subject: [PATCH 03/11] feat(Automata): small changes

---
 Cslib/Computability/Automata/NA/Reverse.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Cslib/Computability/Automata/NA/Reverse.lean b/Cslib/Computability/Automata/NA/Reverse.lean
index 006c13a92..6b5565705 100644
--- a/Cslib/Computability/Automata/NA/Reverse.lean
+++ b/Cslib/Computability/Automata/NA/Reverse.lean
@@ -42,8 +42,7 @@ theorem reverse_mtr_iff (na : FinAcc State Symbol) {xs : List Symbol} {s s' : St
     simp only [List.reverse_cons]
     simp only [LTS.MTr.cons_iff]
     constructor
-    · intro hmtr
-      obtain ⟨mid, h1, h2⟩ := hmtr
+    · rintro ⟨mid, h1, h2⟩
       exact LTS.MTr.stepR na.toLTS (ih.mp h2) h1
     · intro hmtr
       obtain ⟨mid, h1, h2⟩ := LTS.MTr.split hmtr
@@ -52,7 +51,7 @@ theorem reverse_mtr_iff (na : FinAcc State Symbol) {xs : List Symbol} {s s' : St
 
 /-- `na.reverse` accepts exactly the reversals of the words accepted by `na`. -/
 theorem reverse_language_eq (na : FinAcc State Symbol) :
-    language (na.reverse) = (language na).reverse := by
+    language na.reverse = (language na).reverse := by
   ext xs
   simp only [mem_language, mem_reverse]
   constructor
@@ -66,7 +65,8 @@ theorem reverse_language_eq (na : FinAcc State Symbol) :
     exact ⟨s', hs', s, hs, (reverse_mtr_iff na).mpr hmtr⟩
 
 /-- `na.reverse` accepts a word iff `na` accepts its reversal. -/
-theorem reverse_na_accepts (na : FinAcc State Symbol) (xs : List Symbol) :
+@[simp]
+theorem accepts_reverse {na : FinAcc State Symbol} {xs : List Symbol} :
     Accepts na.reverse xs ↔ Accepts na xs.reverse := by
   exact Set.ext_iff.mp (reverse_language_eq na) xs
 

From 76b5448d395e8df5b307f973c28679aab5ceae38 Mon Sep 17 00:00:00 2001
From: Vignesh Karri <vigneshkarri5@gmail.com>
Date: Thu, 6 Aug 2026 00:54:28 +0530
Subject: [PATCH 04/11] feat(Automata): define lts reversal and make NA inherit
 it

---
 Cslib/Computability/Automata/NA/Reverse.lean | 25 +++------
 Cslib/Foundations/Semantics/LTS/Reverse.lean | 53 ++++++++++++++++++++
 2 files changed, 60 insertions(+), 18 deletions(-)
 create mode 100644 Cslib/Foundations/Semantics/LTS/Reverse.lean

diff --git a/Cslib/Computability/Automata/NA/Reverse.lean b/Cslib/Computability/Automata/NA/Reverse.lean
index 6b5565705..17ccc4e5d 100644
--- a/Cslib/Computability/Automata/NA/Reverse.lean
+++ b/Cslib/Computability/Automata/NA/Reverse.lean
@@ -7,6 +7,7 @@ Authors: Vignesh Karri
 module
 
 public import Cslib.Computability.Automata.NA.Basic
+public import Cslib.Foundations.Semantics.LTS.Reverse
 
 /-! # Reversal of nondeterministic automata. -/
 
@@ -23,7 +24,7 @@ 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
-  Tr s x t := na.Tr t x s
+  toLTS := na.toLTS.reverse
   start := na.accept
   accept := na.start
 
@@ -33,21 +34,9 @@ theorem reverse_reverse (na : FinAcc State Symbol) : na.reverse.reverse = na :=
 
 /-- The multistep transitions of `na.reverse` are exactly the reversed multistep transitions
 of `na`. -/
-theorem reverse_mtr_iff (na : FinAcc State Symbol) {xs : List Symbol} {s s' : State} :
-    na.reverse.MTr s' xs s ↔ na.MTr s xs.reverse s' := by
-  induction xs generalizing s s' with
-  | nil =>
-    simp_all [eq_comm]
-  | cons x xs ih =>
-    simp only [List.reverse_cons]
-    simp only [LTS.MTr.cons_iff]
-    constructor
-    · rintro ⟨mid, h1, h2⟩
-      exact LTS.MTr.stepR na.toLTS (ih.mp h2) h1
-    · intro hmtr
-      obtain ⟨mid, h1, h2⟩ := LTS.MTr.split hmtr
-      simp only [LTS.MTr.singleton_iff] at h2
-      exact ⟨mid, h2, ih.mpr h1⟩
+@[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 exactly the reversals of the words accepted by `na`. -/
 theorem reverse_language_eq (na : FinAcc State Symbol) :
@@ -58,11 +47,11 @@ theorem reverse_language_eq (na : FinAcc State Symbol) :
   · intro h
     simp only [Accepts] at h ⊢
     obtain ⟨s, hs, s', hs', hmtr⟩ := h
-    exact ⟨s', hs', s, hs, (reverse_mtr_iff na).mp hmtr⟩
+    exact ⟨s', hs', s, hs, (reverse_mTr na).mp hmtr⟩
   · intro h_na
     simp only [Accepts] at h_na ⊢
     obtain ⟨s, hs, s', hs', hmtr⟩ := h_na
-    exact ⟨s', hs', s, hs, (reverse_mtr_iff na).mpr hmtr⟩
+    exact ⟨s', hs', s, hs, (reverse_mTr na).mpr hmtr⟩
 
 /-- `na.reverse` accepts a word iff `na` accepts its reversal. -/
 @[simp]
diff --git a/Cslib/Foundations/Semantics/LTS/Reverse.lean b/Cslib/Foundations/Semantics/LTS/Reverse.lean
new file mode 100644
index 000000000..e8c3e520e
--- /dev/null
+++ b/Cslib/Foundations/Semantics/LTS/Reverse.lean
@@ -0,0 +1,53 @@
+/-
+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.Basic
+
+/-!
+# Reverse operation for LTS.
+-/
+
+@[expose] public section
+
+namespace Cslib.LTS
+
+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
+
+@[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
+
+/-- 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_all [eq_comm]
+  | cons x xs ih =>
+    simp only [List.reverse_cons, LTS.MTr.cons_iff]
+    constructor
+    · rintro ⟨mid, h1, h2⟩
+      exact LTS.MTr.stepR lts (ih.mp h2) h1
+    · intro hmtr
+      obtain ⟨mid, h1, h2⟩ := LTS.MTr.split hmtr
+      simp only [LTS.MTr.singleton_iff] at h2
+      exact ⟨mid, h2, ih.mpr h1⟩
+
+end Reverse
+
+end Cslib.LTS

From 4ca749d052fba9377c29b23388039d012b4cc2bf Mon Sep 17 00:00:00 2001
From: Vignesh Karri <vigneshkarri5@gmail.com>
Date: Thu, 6 Aug 2026 01:06:11 +0530
Subject: [PATCH 05/11] fix(Automata): register LTS.Reverse in the library root

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.
---
 Cslib.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Cslib.lean b/Cslib.lean
index 8557261bc..47fd79405 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -107,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

From 4af08201337f990baa21e28a9e5bb883d1a54e68 Mon Sep 17 00:00:00 2001
From: Vignesh Karri <vigneshkarri5@gmail.com>
Date: Fri, 7 Aug 2026 01:33:23 +0530
Subject: [PATCH 06/11] feat(LTS): reversal lemmas for defs in LTS/Basic.lean

---
 Cslib/Computability/Automata/NA/Reverse.lean  | 24 ++----
 .../Languages/RegularLanguage.lean            | 31 ++++---
 Cslib/Foundations/Semantics/LTS/Reverse.lean  | 85 ++++++++++++++++---
 3 files changed, 98 insertions(+), 42 deletions(-)

diff --git a/Cslib/Computability/Automata/NA/Reverse.lean b/Cslib/Computability/Automata/NA/Reverse.lean
index 17ccc4e5d..f1eda444c 100644
--- a/Cslib/Computability/Automata/NA/Reverse.lean
+++ b/Cslib/Computability/Automata/NA/Reverse.lean
@@ -38,26 +38,18 @@ of `na`. -/
 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 exactly the reversals of the words accepted by `na`. -/
-theorem reverse_language_eq (na : FinAcc State Symbol) :
-    language na.reverse = (language na).reverse := by
-  ext xs
-  simp only [mem_language, mem_reverse]
-  constructor
-  · intro h
-    simp only [Accepts] at h ⊢
-    obtain ⟨s, hs, s', hs', hmtr⟩ := h
-    exact ⟨s', hs', s, hs, (reverse_mTr na).mp hmtr⟩
-  · intro h_na
-    simp only [Accepts] at h_na ⊢
-    obtain ⟨s, hs, s', hs', hmtr⟩ := h_na
-    exact ⟨s', hs', s, hs, (reverse_mTr na).mpr hmtr⟩
-
 /-- `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
-  exact Set.ext_iff.mp (reverse_language_eq na) xs
+  simp only [Accepts, reverse_mTr]
+  aesop
+
+/-- `na.reverse` accepts exactly the reversals of the words accepted by `na`. -/
+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
 
diff --git a/Cslib/Computability/Languages/RegularLanguage.lean b/Cslib/Computability/Languages/RegularLanguage.lean
index ea939803b..45e897474 100644
--- a/Cslib/Computability/Languages/RegularLanguage.lean
+++ b/Cslib/Computability/Languages/RegularLanguage.lean
@@ -191,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. -/
+@[simp]
+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. -/
+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
@@ -207,22 +222,6 @@ theorem IsRegular.char (a : Symbol) : ({[a]} : Language Symbol).IsRegular := by
     · induction xs using List.reverseRec <;> grind
     · simp_all [flts, List.append_eq_cons_iff]
 
-open NA in
-/-- The reversal of a regular language is regular. -/
-@[simp]
-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
-
 /-- Languages matching regular expressions are regular. -/
 theorem IsRegular.regex {r : RegularExpression Symbol} :
     r.matches'.IsRegular := by
diff --git a/Cslib/Foundations/Semantics/LTS/Reverse.lean b/Cslib/Foundations/Semantics/LTS/Reverse.lean
index e8c3e520e..c049a0ac8 100644
--- a/Cslib/Foundations/Semantics/LTS/Reverse.lean
+++ b/Cslib/Foundations/Semantics/LTS/Reverse.lean
@@ -7,6 +7,7 @@ Authors: Vignesh Karri
 module
 
 public import Cslib.Foundations.Semantics.LTS.Basic
+public import Cslib.Foundations.Semantics.LTS.Execution
 
 /-!
 # Reverse operation for LTS.
@@ -22,6 +23,7 @@ section Reverse
 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
@@ -31,22 +33,85 @@ theorem reverse_tr {lts : LTS State Label} :
 theorem reverse_reverse (lts : LTS State Label) : lts.reverse.reverse = lts := rfl
 
 /-- The multistep transitions of `lts.reverse` are exactly the reversed multistep transitions of
-`lts` -/
+`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_all [eq_comm]
+    simp [eq_comm]
   | cons x xs ih =>
-    simp only [List.reverse_cons, LTS.MTr.cons_iff]
-    constructor
-    · rintro ⟨mid, h1, h2⟩
-      exact LTS.MTr.stepR lts (ih.mp h2) h1
-    · intro hmtr
-      obtain ⟨mid, h1, h2⟩ := LTS.MTr.split hmtr
-      simp only [LTS.MTr.singleton_iff] at h2
-      exact ⟨mid, h2, ih.mpr h1⟩
+    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]
+  constructor
+  · rintro ⟨μs, h⟩
+    exact ⟨_, h⟩
+  · rintro ⟨μs, h⟩
+    exact ⟨μs.reverse, by simpa using h⟩
+
+/-- 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
+  induction μs generalizing s s' ss with
+  | nil => grind
+  | cons μ μs ih =>
+    cases ss with
+    | nil => grind
+    | cons t ts =>
+      obtain rfl : s = t := by grind
+      have htr : lts.Tr s μ (ts[0]'(by grind)) := by grind
+      simpa using Execution.comp (ih (Execution.cons_invert h))
+        (Execution.stepL htr (Execution.refl lts.reverse s))
+
+/-- 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
 

From c402e40fe69f2b11eb4c432dbf0842e55fda5146 Mon Sep 17 00:00:00 2001
From: Vignesh Karri <vigneshkarri5@gmail.com>
Date: Fri, 7 Aug 2026 01:43:34 +0530
Subject: [PATCH 07/11] remove simp tag

---
 Cslib/Computability/Languages/RegularLanguage.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cslib/Computability/Languages/RegularLanguage.lean b/Cslib/Computability/Languages/RegularLanguage.lean
index 45e897474..656c17cfa 100644
--- a/Cslib/Computability/Languages/RegularLanguage.lean
+++ b/Cslib/Computability/Languages/RegularLanguage.lean
@@ -193,13 +193,13 @@ theorem IsRegular.congr_fin_index {Symbol : Type}
 
 open NA in
 /-- The reversal of a regular language is regular. -/
-@[simp]
 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

From 4960db02920a799deb4b063377195919ae1a88a3 Mon Sep 17 00:00:00 2001
From: Vignesh Karri <vigneshkarri5@gmail.com>
Date: Fri, 7 Aug 2026 02:17:56 +0530
Subject: [PATCH 08/11] removed redundant import

---
 Cslib/Foundations/Semantics/LTS/Reverse.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Cslib/Foundations/Semantics/LTS/Reverse.lean b/Cslib/Foundations/Semantics/LTS/Reverse.lean
index c049a0ac8..e0bcd5935 100644
--- a/Cslib/Foundations/Semantics/LTS/Reverse.lean
+++ b/Cslib/Foundations/Semantics/LTS/Reverse.lean
@@ -6,7 +6,6 @@ Authors: Vignesh Karri
 
 module
 
-public import Cslib.Foundations.Semantics.LTS.Basic
 public import Cslib.Foundations.Semantics.LTS.Execution
 
 /-!

From 5312810586987e0a5ecf2daef67b88fb6c7ee040 Mon Sep 17 00:00:00 2001
From: Vignesh Karri <vigneshkarri5@gmail.com>
Date: Fri, 7 Aug 2026 19:06:58 +0530
Subject: [PATCH 09/11] reverse involutive, shorter proof for canReach

---
 Cslib/Computability/Automata/NA/Reverse.lean       |  7 ++++++-
 Cslib/Computability/Languages/RegularLanguage.lean |  4 ++--
 Cslib/Foundations/Semantics/LTS/Reverse.lean       | 12 +++++++-----
 3 files changed, 15 insertions(+), 8 deletions(-)

diff --git a/Cslib/Computability/Automata/NA/Reverse.lean b/Cslib/Computability/Automata/NA/Reverse.lean
index f1eda444c..70156d861 100644
--- a/Cslib/Computability/Automata/NA/Reverse.lean
+++ b/Cslib/Computability/Automata/NA/Reverse.lean
@@ -17,7 +17,7 @@ namespace Cslib.Automata.NA
 
 open Acceptor Language
 
-variable {Symbol State : Type*}
+variable {State Symbol : Type*}
 
 namespace FinAcc
 
@@ -32,6 +32,10 @@ def reverse (na : FinAcc State Symbol) : FinAcc State Symbol where
 @[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]
@@ -46,6 +50,7 @@ theorem accepts_reverse {na : FinAcc State Symbol} {xs : List Symbol} :
   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
diff --git a/Cslib/Computability/Languages/RegularLanguage.lean b/Cslib/Computability/Languages/RegularLanguage.lean
index 656c17cfa..8550d40e8 100644
--- a/Cslib/Computability/Languages/RegularLanguage.lean
+++ b/Cslib/Computability/Languages/RegularLanguage.lean
@@ -193,14 +193,14 @@ theorem IsRegular.congr_fin_index {Symbol : Type}
 
 open NA in
 /-- The reversal of a regular language is regular. -/
-theorem IsRegular.reverse {l : Language Symbol} (h : l.IsRegular) : (l.reverse).IsRegular := by
+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
+theorem IsRegular.reverse_iff {l : Language Symbol} : l.reverse.IsRegular ↔ l.IsRegular := by
   constructor
   · intro h
     simpa using IsRegular.reverse h
diff --git a/Cslib/Foundations/Semantics/LTS/Reverse.lean b/Cslib/Foundations/Semantics/LTS/Reverse.lean
index e0bcd5935..a9a332b83 100644
--- a/Cslib/Foundations/Semantics/LTS/Reverse.lean
+++ b/Cslib/Foundations/Semantics/LTS/Reverse.lean
@@ -16,6 +16,8 @@ public import Cslib.Foundations.Semantics.LTS.Execution
 
 namespace Cslib.LTS
 
+variable {State Label : Type*}
+
 section Reverse
 
 /-- Constructs an LTS by reversing the transitions of an existing LTS. -/
@@ -31,6 +33,10 @@ theorem reverse_tr {lts : LTS State Label} :
 @[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]
@@ -48,11 +54,7 @@ theorem reverse_mTr {lts : LTS State Label} :
 theorem reverse_canReach {lts : LTS State Label} :
     lts.reverse.CanReach s s' ↔ lts.CanReach s' s := by
   simp only [CanReach, reverse_mTr]
-  constructor
-  · rintro ⟨μs, h⟩
-    exact ⟨_, h⟩
-  · rintro ⟨μs, h⟩
-    exact ⟨μs.reverse, by simpa using h⟩
+  conv_rhs => rw [List.reverse_involutive.surjective.exists]
 
 /-- The unlabelled transitions of `lts.reverse` are those of `lts` with the endpoints swapped. -/
 @[simp]

From 8f97c0b0c1584d2eedc411a2f5f0a84eb97cae8b Mon Sep 17 00:00:00 2001
From: Vignesh Karri <vigneshkarri5@gmail.com>
Date: Sat, 8 Aug 2026 23:11:27 +0530
Subject: [PATCH 10/11] grind proof of Execution.reverse

---
 Cslib/Foundations/Semantics/LTS/Reverse.lean | 12 ++----------
 1 file changed, 2 insertions(+), 10 deletions(-)

diff --git a/Cslib/Foundations/Semantics/LTS/Reverse.lean b/Cslib/Foundations/Semantics/LTS/Reverse.lean
index a9a332b83..eeca116cf 100644
--- a/Cslib/Foundations/Semantics/LTS/Reverse.lean
+++ b/Cslib/Foundations/Semantics/LTS/Reverse.lean
@@ -96,16 +96,8 @@ theorem reverse_boundedUpTo {lts : LTS State Label} {n : ℕ} :
 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
-  induction μs generalizing s s' ss with
-  | nil => grind
-  | cons μ μs ih =>
-    cases ss with
-    | nil => grind
-    | cons t ts =>
-      obtain rfl : s = t := by grind
-      have htr : lts.Tr s μ (ts[0]'(by grind)) := by grind
-      simpa using Execution.comp (ih (Execution.cons_invert h))
-        (Execution.stepL htr (Execution.refl lts.reverse s))
+  use by grind
+  grind [reverse_tr]
 
 /-- An execution of `lts.reverse` is an execution of `lts` with the labels, states
 and endpoints reversed. -/

From 45e595945bfd1649feb9dd76af9d5a465c93bdb4 Mon Sep 17 00:00:00 2001
From: Ching-Tsun Chou <chingtsun.chou@gmail.com>
Date: Sat, 8 Aug 2026 13:59:35 -0700
Subject: [PATCH 11/11] improve the proof of Execution.reverse

---
 Cslib/Foundations/Semantics/LTS/Reverse.lean | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/Cslib/Foundations/Semantics/LTS/Reverse.lean b/Cslib/Foundations/Semantics/LTS/Reverse.lean
index eeca116cf..b110d4f8c 100644
--- a/Cslib/Foundations/Semantics/LTS/Reverse.lean
+++ b/Cslib/Foundations/Semantics/LTS/Reverse.lean
@@ -96,8 +96,9 @@ theorem reverse_boundedUpTo {lts : LTS State Label} {n : ℕ} :
 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
-  use by grind
-  grind [reverse_tr]
+  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. -/