/-
Copyright (c) 2025 Harmonic. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
-/
import Mathlib
import Langlib.Grammars.LeftRegular.Definition
import Langlib.Grammars.RightRegular.Definition
import Langlib.Grammars.RightRegular.UnrestrictedCharacterization
import Langlib.Automata.FiniteState.Equivalence.RegularDFAEquiv

/-! # 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