module /- Copyright (c) 2025 Harmonic. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -/ public import Langlib.Grammars.LeftRegular.Definition public import Langlib.Classes.Regular.Definition import Langlib.Automata.FiniteState.Equivalence.Regular import Langlib.Grammars.RightRegular.UnrestrictedCharacterization import Mathlib.Algebra.Order.Floor.Extended import Mathlib.Algebra.Order.Floor.Semifield import Mathlib.Algebra.Order.Interval.Basic import Mathlib.Analysis.Complex.UpperHalfPlane.Basic import Mathlib.Analysis.SpecialFunctions.Bernstein import Mathlib.Analysis.SpecialFunctions.Gamma.Basic import Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp import Mathlib.CategoryTheory.Category.Init import Mathlib.Combinatorics.Enumerative.DyckWord import Mathlib.Combinatorics.SimpleGraph.Triangle.Removal import Mathlib.Data.NNRat.Floor import Mathlib.Data.Nat.Factorial.DoubleFactorial import Mathlib.Geometry.Euclidean.Altitude import Mathlib.NumberTheory.Height.Basic import Mathlib.NumberTheory.LucasLehmer import Mathlib.NumberTheory.SelbergSieve import Mathlib.Tactic.NormNum.BigOperators import Mathlib.Tactic.NormNum.Irrational import Mathlib.Tactic.NormNum.IsCoprime import Mathlib.Tactic.NormNum.IsSquare import Mathlib.Tactic.NormNum.LegendreSymbol import Mathlib.Tactic.NormNum.ModEq import Mathlib.Tactic.NormNum.NatFactorial import Mathlib.Tactic.NormNum.NatFib import Mathlib.Tactic.NormNum.NatLog import Mathlib.Tactic.NormNum.NatSqrt import Mathlib.Tactic.NormNum.Ordinal import Mathlib.Tactic.NormNum.Parity import Mathlib.Tactic.NormNum.Prime import Mathlib.Tactic.NormNum.RealSqrt import Mathlib.Topology.Sheaves.Init @[expose] public section /-! # Equivalence of Left-Regular and Right-Regular Grammars This file proves that the class of languages generated by left-regular grammars coincides with the class of languages generated by right-regular grammars, i.e., both define exactly the regular languages. ## Proof strategy The key observation is that reversing the output of each rule converts a left-regular grammar into a right-regular grammar (and vice versa), and a derivation step in one corresponds to a derivation step on the reversed sentential form in the other. Concretely, if `g` is a left-regular grammar, we construct a right-regular grammar `RG_of_LG g` such that `LG_language g = (RG_language (RG_of_LG g)).reverse`. Since the class of right-regular languages is closed under reversal (via Mathlib's `Language.isRegular_reverse_iff` and `is_RG_iff_isRegular`), this gives `is_LG L → is_RG L`. The converse direction is symmetric. ## Main results - `is_LG_iff_is_RG` — A language is left-regular iff it is right-regular. - `LG_eq_RG` — The class of left-regular languages equals the class of right-regular languages. ## References * Hopcroft, Motwani, Ullman. *Introduction to Automata Theory, Languages, and Computation*, 3rd ed. Section 3.3. -/ open Relation Classical noncomputable section variable {T : Type} -- ============================================================================ -- Part 1: Conversions between LG and RG rules/grammars -- ============================================================================ /-- Convert a left-regular rule to a right-regular rule by reversing the output. - `A → Ba` becomes `A → aB` - `A → a` stays `A → a` - `A → ε` stays `A → ε` -/ def RG_rule_of_LG_rule {N : Type} : LG_rule T N → RG_rule T N | .cons A a B => .cons A a B | .single A a => .single A a | .epsilon A => .epsilon A /-- Convert a right-regular rule to a left-regular rule by reversing the output. - `A → aB` becomes `A → Ba` - `A → a` stays `A → a` - `A → ε` stays `A → ε` -/ def LG_rule_of_RG_rule {N : Type} : RG_rule T N → LG_rule T N | .cons A a B => .cons A a B | .single A a => .single A a | .epsilon A => .epsilon A /-- Convert a left-regular grammar to a right-regular grammar. -/ def RG_of_LG (g : LG_grammar T) : RG_grammar T where nt := g.nt initial := g.initial rules := g.rules.map RG_rule_of_LG_rule /-- Convert a right-regular grammar to a left-regular grammar. -/ def LG_of_RG (g : RG_grammar T) : LG_grammar T where nt := g.nt initial := g.initial rules := g.rules.map LG_rule_of_RG_rule -- ============================================================================ -- Part 2: Correspondence between rule properties -- ============================================================================ lemma RG_rule_of_LG_rule_lhs {N : Type} (r : LG_rule T N) : (RG_rule_of_LG_rule r).lhs = r.lhs := by cases r <;> rfl lemma LG_rule_of_RG_rule_lhs {N : Type} (r : RG_rule T N) : (LG_rule_of_RG_rule r).lhs = r.lhs := by cases r <;> rfl lemma RG_rule_of_LG_rule_output {N : Type} (r : LG_rule T N) : (RG_rule_of_LG_rule r).output = r.output.reverse := by cases r <;> simp [RG_rule_of_LG_rule, RG_rule.output, LG_rule.output] lemma LG_rule_of_RG_rule_output {N : Type} (r : RG_rule T N) : (LG_rule_of_RG_rule r).output = r.output.reverse := by cases r <;> simp [LG_rule_of_RG_rule, LG_rule.output, RG_rule.output] -- ============================================================================ -- Part 3: Step correspondence via list reversal -- ============================================================================ /-- An LG transformation step corresponds to an RG transformation step on the reversed sentential form. -/ lemma RG_transforms_reverse_of_LG_transforms {g : LG_grammar T} {w₁ w₂ : List (symbol T g.nt)} (h : LG_transforms g w₁ w₂) : RG_transforms (RG_of_LG g) w₁.reverse w₂.reverse := by obtain ⟨r, hr, u, v, hw1, hw2⟩ := h refine ⟨RG_rule_of_LG_rule r, List.mem_map.mpr ⟨r, hr, rfl⟩, v.reverse, u.reverse, ?_, ?_⟩ · rw [hw1, RG_rule_of_LG_rule_lhs] simp [List.reverse_append] · rw [hw2, RG_rule_of_LG_rule_output] simp [List.reverse_append] /-- An RG transformation step on `RG_of_LG g` corresponds to an LG transformation step on the reversed sentential form. -/ lemma LG_transforms_of_RG_transforms_reverse {g : LG_grammar T} {w₁ w₂ : List (symbol T g.nt)} (h : RG_transforms (RG_of_LG g) w₁ w₂) : LG_transforms g w₁.reverse w₂.reverse := by obtain ⟨r, hr, u, v, hw1, hw2⟩ := h simp [RG_of_LG] at hr obtain ⟨r', hr', rfl⟩ := hr refine ⟨r', hr', v.reverse, u.reverse, ?_, ?_⟩ · rw [hw1, RG_rule_of_LG_rule_lhs] simp [List.reverse_append] · rw [hw2, RG_rule_of_LG_rule_output] simp [List.reverse_append] /-- LG derivation corresponds to RG derivation on reversed sentential forms. -/ lemma RG_derives_reverse_of_LG_derives {g : LG_grammar T} {w₁ w₂ : List (symbol T g.nt)} (h : LG_derives g w₁ w₂) : RG_derives (RG_of_LG g) w₁.reverse w₂.reverse := by induction h with | refl => exact RG_deri_self _ | tail _ hs ih => exact RG_deri_of_deri_tran ih (RG_transforms_reverse_of_LG_transforms hs) /-- RG derivation on `RG_of_LG g` corresponds to LG derivation on reversed sentential forms. -/ lemma LG_derives_of_RG_derives_reverse {g : LG_grammar T} {w₁ w₂ : List (symbol T g.nt)} (h : RG_derives (RG_of_LG g) w₁ w₂) : LG_derives g w₁.reverse w₂.reverse := by induction h with | refl => exact LG_deri_self _ | tail _ hs ih => exact LG_deri_of_deri_tran ih (LG_transforms_of_RG_transforms_reverse hs) -- ============================================================================ -- Part 4: Language relationship -- ============================================================================ lemma LG_generates_iff_RG_generates_reverse (g : LG_grammar T) (w : List T) : LG_generates g w ↔ RG_generates (RG_of_LG g) w.reverse := by constructor · intro h unfold LG_generates at h unfold RG_generates have := RG_derives_reverse_of_LG_derives h simp [List.map_reverse] at this ⊢ convert this using 1 · intro h unfold RG_generates at h unfold LG_generates have := LG_derives_of_RG_derives_reverse h simp [List.map_reverse] at this ⊢ convert this using 1 lemma LG_language_eq_RG_language_reverse (g : LG_grammar T) : LG_language g = (RG_language (RG_of_LG g)).reverse := by ext w simp only [LG_language, RG_language, Language.reverse] exact LG_generates_iff_RG_generates_reverse g w -- ============================================================================ -- Symmetric results: RG → LG via LG_of_RG -- ============================================================================ /-- An RG transformation step corresponds to an LG transformation step on the reversed sentential form. -/ lemma LG_transforms_reverse_of_RG_transforms {g : RG_grammar T} {w₁ w₂ : List (symbol T g.nt)} (h : RG_transforms g w₁ w₂) : LG_transforms (LG_of_RG g) w₁.reverse w₂.reverse := by obtain ⟨r, hr, u, v, hw1, hw2⟩ := h refine ⟨LG_rule_of_RG_rule r, List.mem_map.mpr ⟨r, hr, rfl⟩, v.reverse, u.reverse, ?_, ?_⟩ · rw [hw1, LG_rule_of_RG_rule_lhs] simp [List.reverse_append] · rw [hw2, LG_rule_of_RG_rule_output] simp [List.reverse_append] lemma RG_transforms_of_LG_transforms_reverse {g : RG_grammar T} {w₁ w₂ : List (symbol T g.nt)} (h : LG_transforms (LG_of_RG g) w₁ w₂) : RG_transforms g w₁.reverse w₂.reverse := by obtain ⟨r, hr, u, v, hw1, hw2⟩ := h simp [LG_of_RG] at hr obtain ⟨r', hr', rfl⟩ := hr refine ⟨r', hr', v.reverse, u.reverse, ?_, ?_⟩ · rw [hw1, LG_rule_of_RG_rule_lhs] simp [List.reverse_append] · rw [hw2, LG_rule_of_RG_rule_output] simp [List.reverse_append] lemma LG_derives_reverse_of_RG_derives {g : RG_grammar T} {w₁ w₂ : List (symbol T g.nt)} (h : RG_derives g w₁ w₂) : LG_derives (LG_of_RG g) w₁.reverse w₂.reverse := by induction h with | refl => exact LG_deri_self _ | tail _ hs ih => exact LG_deri_of_deri_tran ih (LG_transforms_reverse_of_RG_transforms hs) lemma RG_derives_of_LG_derives_reverse {g : RG_grammar T} {w₁ w₂ : List (symbol T g.nt)} (h : LG_derives (LG_of_RG g) w₁ w₂) : RG_derives g w₁.reverse w₂.reverse := by induction h with | refl => exact RG_deri_self _ | tail _ hs ih => exact RG_deri_of_deri_tran ih (RG_transforms_of_LG_transforms_reverse hs) lemma RG_generates_iff_LG_generates_reverse (g : RG_grammar T) (w : List T) : RG_generates g w ↔ LG_generates (LG_of_RG g) w.reverse := by constructor · intro h unfold RG_generates at h unfold LG_generates have := LG_derives_reverse_of_RG_derives h simp [List.map_reverse] at this ⊢ convert this using 1 · intro h unfold LG_generates at h unfold RG_generates have := RG_derives_of_LG_derives_reverse h simp [List.map_reverse] at this ⊢ convert this using 1 lemma RG_language_eq_LG_language_reverse (g : RG_grammar T) : RG_language g = (LG_language (LG_of_RG g)).reverse := by ext w simp only [RG_language, LG_language, Language.reverse] exact RG_generates_iff_LG_generates_reverse g w -- ============================================================================ -- Part 5: Main equivalence theorems -- ============================================================================ variable [Fintype T] /-- Every left-regular language is right-regular. -/ theorem is_RG_of_is_LG {L : Language T} (h : is_LG L) : is_RG L := by obtain ⟨g, rfl⟩ := h rw [LG_language_eq_RG_language_reverse] have hRG : is_RG (RG_language (RG_of_LG g)) := is_RG_via_rg_implies_is_RG ⟨RG_of_LG g, rfl⟩ have hIR := isRegular_of_is_RG hRG have hIR_rev : (RG_language (RG_of_LG g)).reverse.IsRegular := Language.isRegular_reverse_iff.mpr hIR exact is_RG_of_isRegular hIR_rev /-- Every right-regular language is left-regular. -/ theorem is_LG_of_is_RG {L : Language T} (h : is_RG L) : is_LG L := by obtain ⟨g, rfl⟩ := is_RG_implies_is_RG_via_rg h have hIR := isRegular_of_is_RG (is_RG_via_rg_implies_is_RG ⟨g, rfl⟩) have hIR_rev : (RG_language g).reverse.IsRegular := Language.isRegular_reverse_iff.mpr hIR obtain ⟨g', hg'⟩ := is_RG_implies_is_RG_via_rg (is_RG_of_isRegular hIR_rev) refine ⟨LG_of_RG g', ?_⟩ rw [RG_language_eq_LG_language_reverse] at hg' have : (LG_language (LG_of_RG g')).reverse = (RG_language g).reverse := hg' have := congr_arg Language.reverse this simp [Language.reverse_reverse] at this exact this /-- A language is left-regular if and only if it is right-regular. -/ theorem is_LG_iff_is_RG {L : Language T} : is_LG L ↔ is_RG L := ⟨is_RG_of_is_LG, is_LG_of_is_RG⟩ /-- The class of left-regular languages equals the class of right-regular languages. -/ theorem LG_eq_RG : (LG : Set (Language T)) = RG := by ext L exact is_LG_iff_is_RG end