module

public import Langlib.Classes.Indexed.Basics.Elementary
public import Langlib.Classes.Indexed.Basics.FiniteSupport
public import Langlib.Classes.Indexed.Closure.Union
public import Langlib.Classes.Indexed.Examples.SingletonWord
public import Langlib.Grammars.Indexed.NormalForm.ParseTree
public import Langlib.Utilities.ClosurePredicates

@[expose]
public section

/-!
# Indexed Languages Intersected with Regular Languages

For an indexed grammar in Aho normal form, annotate each nonterminal with the
entry and exit states of a DFA. Binary rules thread an intermediate state,
push/pop rules preserve both endpoints, and terminal rules realize one DFA
transition. Parse certificates give a compact soundness and completeness proof.
-/

open Classical

noncomputable section

variable {T σ : Type} [Fintype T] [Fintype σ]

/-- An indexed nonterminal annotated with the DFA states immediately before and
after the word generated by that nonterminal. -/
public structure IndexedDFA.nt (N σ : Type) where
  start : σ
  core : N
  stop : σ
deriving DecidableEq

public instance IndexedDFA.nt.fintype {N σ : Type} [Fintype N] [Fintype σ] :
    Fintype (IndexedDFA.nt N σ) :=
  Fintype.ofEquiv (σ × N × σ)
    { toFun := fun x => ⟨x.1, x.2.1, x.2.2⟩
      invFun := fun x => (x.start, x.core, x.stop)
      left_inv := by intro x; cases x; rfl
      right_inv := by intro x; cases x; rfl }

namespace IndexedGrammar

variable (g : IndexedGrammar T) (M : DFA T σ)

public def dfaBinaryRule (r : IRule T g.nt g.flag) (p m q : σ)
    (B C : g.nt) : IRule T (IndexedDFA.nt g.nt σ) g.flag where
  lhs := ⟨p, r.lhs, q⟩
  consume := none
  rhs :=
    [IRhsSymbol.nonterminal ⟨p, B, m⟩ none,
      IRhsSymbol.nonterminal ⟨m, C, q⟩ none]

public def dfaPopRule (r : IRule T g.nt g.flag) (p q : σ)
    (f : g.flag) (B : g.nt) : IRule T (IndexedDFA.nt g.nt σ) g.flag where
  lhs := ⟨p, r.lhs, q⟩
  consume := some f
  rhs := [IRhsSymbol.nonterminal ⟨p, B, q⟩ none]

public def dfaPushRule (r : IRule T g.nt g.flag) (p q : σ)
    (f : g.flag) (B : g.nt) : IRule T (IndexedDFA.nt g.nt σ) g.flag where
  lhs := ⟨p, r.lhs, q⟩
  consume := none
  rhs := [IRhsSymbol.nonterminal ⟨p, B, q⟩ (some f)]

public def dfaTerminalRule (r : IRule T g.nt g.flag) (p : σ)
    (a : T) : IRule T (IndexedDFA.nt g.nt σ) g.flag where
  lhs := ⟨p, r.lhs, M.step p a⟩
  consume := none
  rhs := [IRhsSymbol.terminal a]

/-- All DFA-threaded copies of one indexed-normal-form rule. Malformed rules
contribute no product rules. -/
public def dfaRulesFor (r : IRule T g.nt g.flag) :
    List (IRule T (IndexedDFA.nt g.nt σ) g.flag) :=
  match r.consume, r.rhs with
  | none, [IRhsSymbol.nonterminal B none, IRhsSymbol.nonterminal C none] =>
      Finset.univ.toList.flatMap fun p =>
        Finset.univ.toList.flatMap fun m =>
          Finset.univ.toList.map fun q => g.dfaBinaryRule r p m q B C
  | some f, [IRhsSymbol.nonterminal B none] =>
      Finset.univ.toList.flatMap fun p =>
        Finset.univ.toList.map fun q => g.dfaPopRule r p q f B
  | none, [IRhsSymbol.nonterminal B (some f)] =>
      Finset.univ.toList.flatMap fun p =>
        Finset.univ.toList.map fun q => g.dfaPushRule r p q f B
  | none, [IRhsSymbol.terminal a] =>
      Finset.univ.toList.map fun p => g.dfaTerminalRule M r p a
  | _, _ => []

/-- Product of a normal-form indexed grammar and a DFA, with fixed initial and
final DFA states. -/
public def dfaProduct (p q : σ) : IndexedGrammar T where
  nt := IndexedDFA.nt g.nt σ
  flag := g.flag
  initial := ⟨p, g.initial, q⟩
  rules := g.rules.flatMap (dfaRulesFor g M)

omit [Fintype T] in
private theorem mem_dfaProduct_rules_iff {p₀ q₀ : σ}
    {r' : IRule T (IndexedDFA.nt g.nt σ) g.flag} :
    r' ∈ (dfaProduct g M p₀ q₀).rules ↔
      ∃ r ∈ g.rules, r' ∈ dfaRulesFor g M r := by
  simp [dfaProduct]

private theorem dfaBinaryRule_mem {p₀ q₀ : σ}
    {r : IRule T g.nt g.flag} (hr : r ∈ g.rules)
    {B C : g.nt}
    (hc : r.consume = none)
    (hrhs : r.rhs =
      [IRhsSymbol.nonterminal B none, IRhsSymbol.nonterminal C none])
    (p m q : σ) :
    g.dfaBinaryRule r p m q B C ∈ (g.dfaProduct M p₀ q₀).rules := by
  rw [mem_dfaProduct_rules_iff]
  refine ⟨r, hr, ?_⟩
  simp [dfaRulesFor, hc, hrhs]

private theorem dfaPopRule_mem {p₀ q₀ : σ}
    {r : IRule T g.nt g.flag} (hr : r ∈ g.rules)
    {f : g.flag} {B : g.nt}
    (hc : r.consume = some f)
    (hrhs : r.rhs = [IRhsSymbol.nonterminal B none])
    (p q : σ) :
    g.dfaPopRule r p q f B ∈ (g.dfaProduct M p₀ q₀).rules := by
  rw [mem_dfaProduct_rules_iff]
  refine ⟨r, hr, ?_⟩
  simp [dfaRulesFor, hc, hrhs]

private theorem dfaPushRule_mem {p₀ q₀ : σ}
    {r : IRule T g.nt g.flag} (hr : r ∈ g.rules)
    {f : g.flag} {B : g.nt}
    (hc : r.consume = none)
    (hrhs : r.rhs = [IRhsSymbol.nonterminal B (some f)])
    (p q : σ) :
    g.dfaPushRule r p q f B ∈ (g.dfaProduct M p₀ q₀).rules := by
  rw [mem_dfaProduct_rules_iff]
  refine ⟨r, hr, ?_⟩
  simp [dfaRulesFor, hc, hrhs]

private theorem dfaTerminalRule_mem {p₀ q₀ : σ}
    {r : IRule T g.nt g.flag} (hr : r ∈ g.rules)
    {a : T}
    (hc : r.consume = none)
    (hrhs : r.rhs = [IRhsSymbol.terminal a])
    (p : σ) :
    g.dfaTerminalRule M r p a ∈ (g.dfaProduct M p₀ q₀).rules := by
  rw [mem_dfaProduct_rules_iff]
  refine ⟨r, hr, ?_⟩
  simp [dfaRulesFor, hc, hrhs]

/-- Lift a normal-form parse certificate while threading its DFA endpoints. -/
private theorem NFYield.toDFAProduct {p₀ q₀ : σ}
    {A : g.nt} {stack : List g.flag} {w : List T}
    (hyield : g.NFYield A stack w) (p q : σ)
    (heval : M.evalFrom p w = q) :
    (g.dfaProduct M p₀ q₀).NFYield ⟨p, A, q⟩ stack w := by
  induction hyield generalizing p q with
  | binary hr hlhs hc hrhs hleft hright ihleft ihright =>
      rename_i A B C stack u v r
      let m := M.evalFrom p u
      have hrightEval : M.evalFrom m v = q := by
        rw [← M.evalFrom_of_append]
        exact heval
      let r' := g.dfaBinaryRule r p m q B C
      exact NFYield.binary
        (g := g.dfaProduct M p₀ q₀) (r := r')
        (dfaBinaryRule_mem g M hr hc hrhs p m q)
        (by simp [r', dfaBinaryRule, hlhs]) rfl rfl
        (ihleft p m rfl)
        (ihright m q hrightEval)
  | pop hr hlhs hc hrhs hrest ihrest =>
      rename_i A B f rest w r
      let r' := g.dfaPopRule r p q f B
      exact NFYield.pop
        (g := g.dfaProduct M p₀ q₀) (r := r')
        (dfaPopRule_mem g M hr hc hrhs p q)
        (by simp [r', dfaPopRule, hlhs]) rfl rfl (ihrest p q heval)
  | push hr hlhs hc hrhs hrest ihrest =>
      rename_i A B f stack w r
      let r' := g.dfaPushRule r p q f B
      exact NFYield.push
        (g := g.dfaProduct M p₀ q₀) (r := r')
        (dfaPushRule_mem g M hr hc hrhs p q)
        (by simp [r', dfaPushRule, hlhs]) rfl rfl (ihrest p q heval)
  | terminal hr hlhs hc hrhs =>
      rename_i A stack a r
      simp only [DFA.evalFrom_singleton] at heval
      subst q
      let r' := g.dfaTerminalRule M r p a
      exact NFYield.terminal
        (g := g.dfaProduct M p₀ q₀) (r := r')
        (dfaTerminalRule_mem g M hr hc hrhs p)
        (by simp [r', dfaTerminalRule, hlhs]) rfl rfl

/-- The product of a normal-form indexed grammar and a DFA is again in indexed
normal form. -/
private theorem dfaProduct_isNormalForm {p₀ q₀ : σ}
    [DecidableEq g.nt] (hNF : g.IsNormalForm) :
    (g.dfaProduct M p₀ q₀).IsNormalForm := by
  intro r' hr'
  rw [mem_dfaProduct_rules_iff] at hr'
  obtain ⟨r, hr, hrmem⟩ := hr'
  rcases hNF r hr with hbin | hpop | hpush | hterm
  · rcases hbin with ⟨hc, B, C, hrhs, hB, hC⟩
    simp [dfaRulesFor, hc, hrhs] at hrmem
    rcases hrmem with ⟨p, m, q, rfl⟩
    left
    refine ⟨rfl, ⟨p, B, m⟩, ⟨m, C, q⟩, rfl, ?_, ?_⟩
    · intro heq
      exact hB (congrArg IndexedDFA.nt.core heq)
    · intro heq
      exact hC (congrArg IndexedDFA.nt.core heq)
  · rcases hpop with ⟨f, hc, B, hrhs, hB⟩
    simp [dfaRulesFor, hc, hrhs] at hrmem
    rcases hrmem with ⟨p, q, rfl⟩
    right; left
    refine ⟨f, rfl, ⟨p, B, q⟩, rfl, ?_⟩
    intro heq
    exact hB (congrArg IndexedDFA.nt.core heq)
  · rcases hpush with ⟨hc, B, f, hrhs, hB⟩
    simp [dfaRulesFor, hc, hrhs] at hrmem
    rcases hrmem with ⟨p, q, rfl⟩
    right; right; left
    refine ⟨rfl, ⟨p, B, q⟩, f, rfl, ?_⟩
    intro heq
    exact hB (congrArg IndexedDFA.nt.core heq)
  · rcases hterm with ⟨hc, a, hrhs⟩
    simp [dfaRulesFor, hc, hrhs] at hrmem
    rcases hrmem with ⟨p, rfl⟩
    right; right; right
    exact ⟨rfl, a, rfl⟩

/-- Erase DFA annotations from a product parse certificate and recover the DFA
run described by its endpoints. -/
private theorem NFYield.ofDFAProduct {p₀ q₀ : σ}
    [DecidableEq g.nt] (hNF : g.IsNormalForm)
    {A : IndexedDFA.nt g.nt σ} {stack : List g.flag} {w : List T}
    (hyield : (g.dfaProduct M p₀ q₀).NFYield A stack w) :
    g.NFYield A.core stack w ∧ M.evalFrom A.start w = A.stop := by
  induction hyield using @IndexedGrammar.NFYield.rec T (g.dfaProduct M p₀ q₀) with
  | binary hr' hlhs' hc' hrhs' hleft hright ihleft ihright =>
      rename_i A' B' C' stack u v r'
      rw [mem_dfaProduct_rules_iff] at hr'
      obtain ⟨r, hr, hrmem⟩ := hr'
      rcases hNF r hr with hbin | hpop | hpush | hterm
      · rcases hbin with ⟨hc, B, C, hrhs, hB, hC⟩
        simp [dfaRulesFor, hc, hrhs] at hrmem
        rcases hrmem with ⟨p, m, q, rfl⟩
        simp [dfaBinaryRule] at hlhs' hrhs'
        subst A'
        rcases hrhs' with ⟨rfl, rfl⟩
        constructor
        · exact NFYield.binary hr rfl hc hrhs ihleft.1 ihright.1
        · rw [M.evalFrom_of_append, ihleft.2, ihright.2]
      · rcases hpop with ⟨f, hc, B, hrhs, hB⟩
        simp [dfaRulesFor, hc, hrhs] at hrmem
        rcases hrmem with ⟨p, q, rfl⟩
        simp [dfaPopRule] at hrhs'
      · rcases hpush with ⟨hc, B, f, hrhs, hB⟩
        simp [dfaRulesFor, hc, hrhs] at hrmem
        rcases hrmem with ⟨p, q, rfl⟩
        simp [dfaPushRule] at hrhs'
      · rcases hterm with ⟨hc, a, hrhs⟩
        simp [dfaRulesFor, hc, hrhs] at hrmem
        rcases hrmem with ⟨p, rfl⟩
        simp [dfaTerminalRule] at hrhs'
  | pop hr' hlhs' hc' hrhs' hrest ihrest =>
      rename_i A' B' f rest w r'
      rw [mem_dfaProduct_rules_iff] at hr'
      obtain ⟨r, hr, hrmem⟩ := hr'
      rcases hNF r hr with hbin | hpop | hpush | hterm
      · rcases hbin with ⟨hc, B, C, hrhs, hB, hC⟩
        simp [dfaRulesFor, hc, hrhs] at hrmem
        rcases hrmem with ⟨p, m, q, rfl⟩
        simp [dfaBinaryRule] at hc'
      · rcases hpop with ⟨f₀, hc, B, hrhs, hB⟩
        simp [dfaRulesFor, hc, hrhs] at hrmem
        rcases hrmem with ⟨p, q, rfl⟩
        simp [dfaPopRule] at hlhs' hc' hrhs'
        subst A'
        subst f
        subst B'
        exact ⟨NFYield.pop hr rfl hc hrhs ihrest.1, ihrest.2⟩
      · rcases hpush with ⟨hc, B, f₀, hrhs, hB⟩
        simp [dfaRulesFor, hc, hrhs] at hrmem
        rcases hrmem with ⟨p, q, rfl⟩
        simp [dfaPushRule] at hc'
      · rcases hterm with ⟨hc, a, hrhs⟩
        simp [dfaRulesFor, hc, hrhs] at hrmem
        rcases hrmem with ⟨p, rfl⟩
        simp [dfaTerminalRule] at hc'
  | push hr' hlhs' hc' hrhs' hrest ihrest =>
      rename_i A' B' f stack w r'
      rw [mem_dfaProduct_rules_iff] at hr'
      obtain ⟨r, hr, hrmem⟩ := hr'
      rcases hNF r hr with hbin | hpop | hpush | hterm
      · rcases hbin with ⟨hc, B, C, hrhs, hB, hC⟩
        simp [dfaRulesFor, hc, hrhs] at hrmem
        rcases hrmem with ⟨p, m, q, rfl⟩
        simp [dfaBinaryRule] at hrhs'
      · rcases hpop with ⟨f₀, hc, B, hrhs, hB⟩
        simp [dfaRulesFor, hc, hrhs] at hrmem
        rcases hrmem with ⟨p, q, rfl⟩
        simp [dfaPopRule] at hc'
      · rcases hpush with ⟨hc, B, f₀, hrhs, hB⟩
        simp [dfaRulesFor, hc, hrhs] at hrmem
        rcases hrmem with ⟨p, q, rfl⟩
        simp [dfaPushRule] at hlhs'
        subst A'
        simp only [dfaPushRule, List.cons.injEq, eq_self, and_true,
          IRhsSymbol.nonterminal.injEq, Option.some.injEq] at hrhs'
        rcases hrhs' with ⟨hB', hf⟩
        subst f₀
        rw [← hB'] at ihrest
        subst B'
        exact ⟨NFYield.push hr rfl hc hrhs ihrest.1, ihrest.2⟩
      · rcases hterm with ⟨hc, a, hrhs⟩
        simp [dfaRulesFor, hc, hrhs] at hrmem
        rcases hrmem with ⟨p, rfl⟩
        simp [dfaTerminalRule] at hrhs'
  | terminal hr' hlhs' hc' hrhs' =>
      rename_i A' stack a r'
      rw [mem_dfaProduct_rules_iff] at hr'
      obtain ⟨r, hr, hrmem⟩ := hr'
      rcases hNF r hr with hbin | hpop | hpush | hterm
      · rcases hbin with ⟨hc, B, C, hrhs, hB, hC⟩
        simp [dfaRulesFor, hc, hrhs] at hrmem
        rcases hrmem with ⟨p, m, q, rfl⟩
        simp [dfaBinaryRule] at hrhs'
      · rcases hpop with ⟨f, hc, B, hrhs, hB⟩
        simp [dfaRulesFor, hc, hrhs] at hrmem
        rcases hrmem with ⟨p, q, rfl⟩
        simp [dfaPopRule] at hc'
      · rcases hpush with ⟨hc, B, f, hrhs, hB⟩
        simp [dfaRulesFor, hc, hrhs] at hrmem
        rcases hrmem with ⟨p, q, rfl⟩
        simp [dfaPushRule] at hrhs'
      · rcases hterm with ⟨hc, a₀, hrhs⟩
        simp [dfaRulesFor, hc, hrhs] at hrmem
        rcases hrmem with ⟨p, rfl⟩
        simp [dfaTerminalRule] at hlhs' hrhs'
        subst A'
        subst a
        exact ⟨NFYield.terminal hr rfl hc hrhs, by simp⟩

/-- Exact language characterization of a product grammar with fixed DFA
endpoints. -/
private theorem dfaProduct_generates_iff [DecidableEq g.nt]
    (hNF : g.IsNormalForm) (p q : σ) (w : List T) :
    (g.dfaProduct M p q).Generates w ↔
      g.Generates w ∧ M.evalFrom p w = q := by
  have hProductNF := dfaProduct_isNormalForm g M hNF (p₀ := p) (q₀ := q)
  constructor
  · intro hw
    have hcert : (g.dfaProduct M p q).NFYield ⟨p, g.initial, q⟩ [] w :=
      (NFYield.generates_iff_isNormalForm hProductNF).mp hw
    have hproj := NFYield.ofDFAProduct g M hNF hcert
    exact ⟨(NFYield.generates_iff_isNormalForm hNF).mpr hproj.1, hproj.2⟩
  · rintro ⟨hw, heval⟩
    have hcert : g.NFYield g.initial [] w :=
      (NFYield.generates_iff_isNormalForm hNF).mp hw
    exact (NFYield.generates_iff_isNormalForm hProductNF).mpr
      (NFYield.toDFAProduct g M hcert p q heval)

end IndexedGrammar

/-- Union of a finite family of languages. -/
private def indexedFiniteUnion (s : Finset σ) (L : σ → Language T) : Language T :=
  {w | ∃ q ∈ s, w ∈ L q}

omit [Fintype T] [Fintype σ] in
private theorem is_Indexed_indexedFiniteUnion (s : Finset σ) (L : σ → Language T)
    (hL : ∀ q ∈ s, is_Indexed (L q)) :
    is_Indexed (indexedFiniteUnion s L) := by
  classical
  induction s using Finset.induction with
  | empty =>
      simpa [indexedFiniteUnion] using (is_Indexed_empty : is_Indexed (0 : Language T))
  | @insert q s hq ih =>
      have hqL : is_Indexed (L q) := hL q (by simp)
      have hsL : is_Indexed (indexedFiniteUnion s L) :=
        ih (fun x hx => hL x (by simp [hx]))
      have hunion := Indexed_closedUnderUnion (L q) (indexedFiniteUnion s L) hqL hsL
      simpa [indexedFiniteUnion, Language.mem_add, or_comm, and_assoc] using hunion

/-- The nonempty part of the intersection is generated by the finite union of
the fixed-final-state product grammars. -/
private theorem is_Indexed_inter_dfa_diff_empty [Nonempty T]
    (g₀ : IndexedGrammar T) (M : DFA T σ) :
    is_Indexed ((g₀.Language ⊓ M.accepts) \ ({[]} : Set (List T))) := by
  letI : Inhabited T := ⟨Classical.choice (inferInstance : Nonempty T)⟩
  obtain ⟨g, hnt, hflag, hdec, hNF, hlang⟩ :=
    g₀.exists_finiteSupport_normalForm_nonempty
  let slices : σ → Language T := fun q => (g.dfaProduct M M.start q).Language
  let finals : Finset σ := Finset.univ.filter (fun q => q ∈ M.accept)
  have hslices : ∀ q ∈ finals, is_Indexed (slices q) := by
    intro q hq
    exact ⟨g.dfaProduct M M.start q, rfl⟩
  have hunion : is_Indexed (indexedFiniteUnion finals slices) :=
    is_Indexed_indexedFiniteUnion finals slices hslices
  have heq : indexedFiniteUnion finals slices =
      (g₀.Language ⊓ M.accepts) \ ({[]} : Set (List T)) := by
    ext w
    constructor
    · rintro ⟨q, hq, hwq⟩
      have hqfinal : q ∈ M.accept := by
        simpa [finals] using hq
      have hprod : g.Generates w ∧ M.evalFrom M.start w = q :=
        (IndexedGrammar.dfaProduct_generates_iff g M hNF M.start q w).mp hwq
      have hwne : w ≠ [] := by
        intro hw
        subst w
        exact g.not_generates_nil_of_noEpsilon
          (g.noEpsilon_of_isNormalForm hNF) hprod.1
      refine ⟨⟨?_, ?_⟩, ?_⟩
      · change g₀.Generates w
        exact (hlang w hwne).mp hprod.1
      · change M.evalFrom M.start w ∈ M.accept
        rw [hprod.2]
        exact hqfinal
      · simpa using hwne
    · rintro ⟨⟨hwg₀, hwM⟩, hwne⟩
      have hwne' : w ≠ [] := by simpa using hwne
      let q := M.evalFrom M.start w
      refine ⟨q, ?_, ?_⟩
      · simp [finals, q]
        exact hwM
      · apply (IndexedGrammar.dfaProduct_generates_iff g M hNF M.start q w).mpr
        exact ⟨(hlang w hwne').mpr hwg₀, rfl⟩
  rw [← heq]
  exact hunion

/-- An indexed language intersected with a regular language is indexed. -/
public theorem Indexed_of_Indexed_inter_regular
    (L R : Language T) (hL : is_Indexed L) (hR : R.IsRegular) :
    is_Indexed (L ⊓ R) := by
  obtain ⟨g₀, rfl⟩ := hL
  obtain ⟨τ, _, M, rfl⟩ := hR
  classical
  by_cases hT : Nonempty T
  · letI : Nonempty T := hT
    have hpos : is_Indexed
        ((g₀.Language ⊓ M.accepts) \ ({[]} : Set (List T))) :=
      is_Indexed_inter_dfa_diff_empty g₀ M
    by_cases hnil : [] ∈ (g₀.Language ⊓ M.accepts)
    · have hsingle : is_Indexed ({[]} : Language T) := by
        simpa [singletonWordLanguage] using singletonWordLanguage_is_Indexed (T := T) []
      have hunion := Indexed_closedUnderUnion
        ((g₀.Language ⊓ M.accepts) \ ({[]} : Set (List T)))
        ({[]} : Language T) hpos hsingle
      have heq :
          ((g₀.Language ⊓ M.accepts) \ ({[]} : Set (List T))) +
              ({[]} : Language T) =
            g₀.Language ⊓ M.accepts := by
        ext w
        constructor
        · intro hw
          rw [Language.mem_add] at hw
          rcases hw with hw | hw
          · exact hw.1
          · have hweq : w = [] := by simpa using hw
            subst w
            exact hnil
        · intro hw
          rw [Language.mem_add]
          by_cases hweq : w = []
          · right
            subst w
            exact Set.mem_singleton []
          · left
            exact ⟨hw, by simpa using hweq⟩
      rw [← heq]
      exact hunion
    · have heq :
          (g₀.Language ⊓ M.accepts) \ ({[]} : Set (List T)) =
            g₀.Language ⊓ M.accepts := by
        ext w
        constructor
        · exact fun hw => hw.1
        · intro hw
          refine ⟨hw, ?_⟩
          intro hws
          have : w = [] := by simpa using hws
          subst w
          exact hnil hw
      rw [← heq]
      exact hpos
  · letI : IsEmpty T := not_nonempty_iff.mp hT
    by_cases hnil : [] ∈ (g₀.Language ⊓ M.accepts)
    · have heq : g₀.Language ⊓ M.accepts = ({[]} : Language T) := by
        ext w
        have hw : w = [] := Subsingleton.elim w []
        subst w
        constructor
        · intro _
          rfl
        · intro _
          exact hnil
      rw [heq]
      simpa [singletonWordLanguage] using singletonWordLanguage_is_Indexed (T := T) []
    · have heq : g₀.Language ⊓ M.accepts = (0 : Language T) := by
        ext w
        have hw : w = [] := Subsingleton.elim w []
        subst w
        simp [hnil]
      rw [heq]
      exact is_Indexed_empty

/-- Predicate-form closure theorem used by the closure table. -/
public theorem Indexed_closedUnderIntersectionWithRegular :
    ClosedUnderIntersectionWithRegular (α := T) is_Indexed := by
  intro L hL R hR
  exact Indexed_of_Indexed_inter_regular L R hL hR

end