import Langlib.Classes.ContextFree.Closure.Substitution
import Langlib.Classes.ContextFree.Definition
import Langlib.Utilities.ClosurePredicates

/-! # Context-Free Closure Under Concatenation

This file derives closure under concatenation from closure under substitution.

## Main declarations

- `CF_of_CF_c_CF`
-/

variable {T : Type}

/-- The class of context-free languages is closed under concatenation. -/
theorem CF_of_CF_c_CF (L₁ : Language T) (L₂ : Language T) :
    is_CF L₁ ∧ is_CF L₂ → is_CF (L₁ * L₂) := by
  classical
  rintro ⟨h₁, h₂⟩
  let f : Bool → Language T := fun b => if b then L₂ else L₁
  have hsubst : is_CF (({[false, true]} : Language Bool).subst f) := by
    apply CF_of_subst_CF ({[false, true]} : Language Bool) f
    · exact (is_CF_iff_isContextFree).mpr (isContextFree_singleton [false, true])
    · intro b
      cases b with
      | false => simpa [f]
      | true => simpa [f]
  simpa [f] using (Language.subst_pair_eq_mul (f := f) ▸ hsubst)

/-- The class of context-free languages is closed under concatenation. -/
theorem CF_closedUnderConcatenation : ClosedUnderConcatenation (α := T) is_CF :=
  fun L₁ L₂ h₁ h₂ => CF_of_CF_c_CF L₁ L₂ ⟨h₁, h₂⟩