feat(Computability): regular languages are closed under reversal (#21573)

This PR proves that regular languages are closed under reversal.

It works by reversing the transitions in the NFA, and proving that the resulting automaton matches the reversed language. The argument proceeds by induction on the input word, ensuring that, at each character, the state sets for the forward and reverse automaton correspond to each other.

I also clean up the existing NFA module, which includes making the `M` argument implicit by default. I can revert that if it's controversial.

Thank you @Rob23oba for their help with the induction proof.

Author: lambda-fairy

Mathlib/Computability/NFA.lean

@@ -23,7 +23,6 @@ open Computability
 
 universe u v
 
-
 /-- An NFA is a set of states (`σ`), a transition function from state to state labelled by the
   alphabet (`step`), a set of starting states (`start`) and a set of acceptance states (`accept`).
   Note the transition function sends a state to a `Set` of states. These are the states that it
@@ -36,64 +35,76 @@ structure NFA (α : Type u) (σ : Type v) where
   /-- Set of accepting states -/
   accept : Set σ
 
-variable {α : Type u} {σ σ' : Type v} (M : NFA α σ)
+variable {α : Type u} {σ : Type v} {M : NFA α σ}
 
 namespace NFA
 
 instance : Inhabited (NFA α σ) :=
   ⟨NFA.mk (fun _ _ => ∅) ∅ ∅⟩
 
+variable (M) in
 /-- `M.stepSet S a` is the union of `M.step s a` for all `s ∈ S`. -/
 def stepSet (S : Set σ) (a : α) : Set σ :=
   ⋃ s ∈ S, M.step s a
 
-theorem mem_stepSet (s : σ) (S : Set σ) (a : α) : s ∈ M.stepSet S a ↔ ∃ t ∈ S, s ∈ M.step t a := by
+theorem mem_stepSet {s : σ} {S : Set σ} {a : α} : s ∈ M.stepSet S a ↔ ∃ t ∈ S, s ∈ M.step t a := by
   simp [stepSet]
 
+variable (M) in
 @[simp]
 theorem stepSet_empty (a : α) : M.stepSet ∅ a = ∅ := by simp [stepSet]
 
+variable (M) in
 /-- `M.evalFrom S x` computes all possible paths through `M` with input `x` starting at an element
   of `S`. -/
-def evalFrom (start : Set σ) : List α → Set σ :=
-  List.foldl M.stepSet start
+def evalFrom (S : Set σ) : List α → Set σ :=
+  List.foldl M.stepSet S
 
+variable (M) in
 @[simp]
 theorem evalFrom_nil (S : Set σ) : M.evalFrom S [] = S :=
   rfl
 
+variable (M) in
 @[simp]
 theorem evalFrom_singleton (S : Set σ) (a : α) : M.evalFrom S [a] = M.stepSet S a :=
   rfl
 
+variable (M) in
 @[simp]
 theorem evalFrom_append_singleton (S : Set σ) (x : List α) (a : α) :
     M.evalFrom S (x ++ [a]) = M.stepSet (M.evalFrom S x) a := by
   simp only [evalFrom, List.foldl_append, List.foldl_cons, List.foldl_nil]
 
+variable (M) in
 /-- `M.eval x` computes all possible paths though `M` with input `x` starting at an element of
   `M.start`. -/
 def eval : List α → Set σ :=
   M.evalFrom M.start
 
+variable (M) in
 @[simp]
 theorem eval_nil : M.eval [] = M.start :=
   rfl
 
+variable (M) in
 @[simp]
 theorem eval_singleton (a : α) : M.eval [a] = M.stepSet M.start a :=
   rfl
 
+variable (M) in
 @[simp]
 theorem eval_append_singleton (x : List α) (a : α) : M.eval (x ++ [a]) = M.stepSet (M.eval x) a :=
-  evalFrom_append_singleton _ _ _ _
+  evalFrom_append_singleton ..
 
+variable (M) in
 /-- `M.accepts` is the language of `x` such that there is an accept state in `M.eval x`. -/
 def accepts : Language α := {x | ∃ S ∈ M.accept, S ∈ M.eval x}
 
 theorem mem_accepts {x : List α} : x ∈ M.accepts ↔ ∃ S ∈ M.accept, S ∈ M.evalFrom M.start x := by
   rfl
 
+variable (M) in
 /-- `M.toDFA` is a `DFA` constructed from an `NFA` `M` using the subset construction. The
   states is the type of `Set`s of `M.state` and the step function is `M.stepSet`. -/
 def toDFA : DFA α (Set σ) where
@@ -121,7 +132,7 @@ namespace DFA
 
 /-- `M.toNFA` is an `NFA` constructed from a `DFA` `M` by using the same start and accept
   states and a transition function which sends `s` with input `a` to the singleton `M.step s a`. -/
-@[simps] def toNFA (M : DFA α σ') : NFA α σ' where
+@[simps] def toNFA (M : DFA α σ) : NFA α σ where
   step s a := {M.step s a}
   start := {M.start}
   accept := M.accept
@@ -146,3 +157,63 @@ theorem toNFA_correct (M : DFA α σ) : M.toNFA.accepts = M.accepts := by
   · exact fun h => ⟨M.eval x, h, rfl⟩
 
 end DFA
+
+namespace NFA
+
+variable (M) in
+/-- `M.reverse` constructs an NFA with the same states as `M`, but all the transitions reversed. The
+resulting automaton accepts a word `x` if and only if `M` accepts `List.reverse x`. -/
+@[simps]
+def reverse : NFA α σ where
+  step s a := { s' | s ∈ M.step s' a }
+  start := M.accept
+  accept := M.start
+
+variable (M) in
+@[simp]
+theorem reverse_reverse : M.reverse.reverse = M := by
+  simp [reverse]
+
+theorem disjoint_stepSet_reverse {a : α} {S S' : Set σ} :
+    Disjoint S (M.reverse.stepSet S' a) ↔ Disjoint S' (M.stepSet S a) := by
+  rw [← not_iff_not]
+  simp only [Set.not_disjoint_iff, mem_stepSet, reverse_step, Set.mem_setOf_eq]
+  tauto
+
+theorem disjoint_evalFrom_reverse {x : List α} {S S' : Set σ}
+    (h : Disjoint S (M.reverse.evalFrom S' x)) : Disjoint S' (M.evalFrom S x.reverse) := by
+  simp only [evalFrom, List.foldl_reverse] at h ⊢
+  induction x generalizing S S' with
+  | nil =>
+    rw [disjoint_comm]
+    exact h
+  | cons x xs ih =>
+    rw [List.foldl_cons] at h
+    rw [List.foldr_cons, ← NFA.disjoint_stepSet_reverse, disjoint_comm]
+    exact ih h
+
+theorem disjoint_evalFrom_reverse_iff {x : List α} {S S' : Set σ} :
+    Disjoint S (M.reverse.evalFrom S' x) ↔ Disjoint S' (M.evalFrom S x.reverse) :=
+  ⟨disjoint_evalFrom_reverse, fun h ↦ List.reverse_reverse x ▸ disjoint_evalFrom_reverse h⟩
+
+@[simp]
+theorem mem_accepts_reverse {x : List α} : x ∈ M.reverse.accepts ↔ x.reverse ∈ M.accepts := by
+  simp [mem_accepts, ← Set.not_disjoint_iff, not_iff_not, disjoint_evalFrom_reverse_iff]
+
+end NFA
+
+namespace Language
+
+protected theorem IsRegular.reverse {L : Language α} (h : L.IsRegular) : L.reverse.IsRegular :=
+  have ⟨σ, _, M, hM⟩ := h
+  ⟨_, inferInstance, M.toNFA.reverse.toDFA, by ext; simp [hM]⟩
+
+protected theorem IsRegular.of_reverse {L : Language α} (h : L.reverse.IsRegular) : L.IsRegular :=
+  L.reverse_reverse ▸ h.reverse
+
+/-- Regular languages are closed under reversal. -/
+@[simp]
+theorem isRegular_reverse_iff {L : Language α} : L.reverse.IsRegular ↔ L.IsRegular :=
+  ⟨.of_reverse, .reverse⟩
+
+end Language