import Langlib.Classes.ContextFree.Basics.Pumping
import Langlib.Classes.ContextFree.Basics.Elementary
import Langlib.Classes.ContextFree.Closure.Concatenation
import Langlib.Classes.ContextFree.Closure.Permutation
import Langlib.Classes.ContextFree.Closure.Bijection
import Langlib.Utilities.ListUtils
import Langlib.Utilities.LanguageOperations
import Langlib.Classes.ContextFree.Definition
import Langlib.Grammars.ContextFree.UnrestrictedCharacterization
import Langlib.Utilities.Tactics
import Langlib.Utilities.ClosurePredicates


/-! # Context-Free Non-Closure Under Intersection

This file proves that context-free languages are not closed under intersection.

It shows that the intersection of the two CF languages `{aⁿbⁿ | n ∈ ℕ}` and `{bⁿcⁿ | n ∈ ℕ}` is `{aⁿbⁿcⁿ | n ∈ ℕ}`, which is not context-free.

## Main declarations

- `notCF_lang_eq_eq` — the language `{aⁿbⁿcⁿ | n ∈ ℕ}` is not context-free
- `nnyCF_of_CF_i_CF` - if L₁ and L₂ are CF, then L₁ ∩ L₂ is not always CF
-/

section defs_over_fin3

def a_ : Fin 3 := 0
def b_ : Fin 3 := 1
def c_ : Fin 3 := 2

private def a : symbol (Fin 3) (Fin 1) := symbol.terminal a_
private def b : symbol (Fin 3) (Fin 1) := symbol.terminal b_
private def c : symbol (Fin 3) (Fin 1) := symbol.terminal c_

private lemma neq_ab : a_ ≠ b_ := by decide
private lemma neq_ba : b_ ≠ a_ := neq_ab.symm
private lemma neq_ac : a_ ≠ c_ := by decide
private lemma neq_ca : c_ ≠ a_ := neq_ac.symm
private lemma neq_bc : b_ ≠ c_ := by decide
private lemma neq_cb : c_ ≠ b_ := neq_bc.symm


def lang_eq_any : Language (Fin 3) :=
fun w => ∃ n m : ℕ, w = List.replicate n a_ ++ List.replicate n b_ ++ List.replicate m c_

def lang_any_eq : Language (Fin 3) :=
fun w => ∃ n m : ℕ, w = List.replicate n a_ ++ List.replicate m b_ ++ List.replicate m c_

def lang_eq_eq : Language (Fin 3) :=
fun w => ∃ n : ℕ, w = List.replicate n a_ ++ List.replicate n b_ ++ List.replicate n c_

end defs_over_fin3


section not_CF

private lemma false_of_uvvxyyz
    {_a _b _c : Fin 3} {n : ℕ} {u v x y z : List (Fin 3)}
    (elimin : ∀ s : Fin 3,  s ≠ _a  →  s ≠ _b  →  s ≠ _c  → False)
    (no_a : _a ∉ v ++ y) (nonempty : (v ++ y).length > 0)
    (counts_ab : ∀ (w : List (Fin 3)), w ∈ lang_eq_eq → List.count_in w _a = List.count_in w _b)
    (counts_ac : ∀ (w : List (Fin 3)), w ∈ lang_eq_eq → List.count_in w _a = List.count_in w _c)
    (counted_a : List.count_in (u ++ v ++ x ++ y ++ z ++ (v ++ y)) _a = n + 1 + List.count_in (v ++ y) _a)
    (counted_b : List.count_in (u ++ v ++ x ++ y ++ z ++ (v ++ y)) _b = n + 1 + List.count_in (v ++ y) _b)
    (counted_c : List.count_in (u ++ v ++ x ++ y ++ z ++ (v ++ y)) _c = n + 1 + List.count_in (v ++ y) _c)
    (pumping : u ++ List.n_times v 2 ++ x ++ List.n_times y 2 ++ z ∈ lang_eq_eq) :
  False :=
by
  have extra_not_a : _b ∈ (v ++ y) ∨ _c ∈ (v ++ y) := by
    let first_letter := (v ++ y).nthLe 0 nonempty
    have first_letter_b_or_c : first_letter = _b ∨ first_letter = _c := by
      have first_letter_not_a : first_letter ≠ _a := by
        by_contra contra
        have yes_a : _a ∈ v ++ y := by
          rw [← contra]
          apply List.nthLe_mem
        exact no_a yes_a
      by_contra contr
      push_neg at contr
      cases contr with
      | intro first_letter_not_b first_letter_not_c =>
          exact elimin ((v ++ y).nthLe 0 nonempty) first_letter_not_a first_letter_not_b
            first_letter_not_c
    cases first_letter_b_or_c with
    | inl first_letter_b =>
        left
        rw [← first_letter_b]
        apply List.nthLe_mem
    | inr first_letter_c =>
        right
        rw [← first_letter_c]
        apply List.nthLe_mem
  have hab := counts_ab (u ++ List.n_times v 2 ++ x ++ List.n_times y 2 ++ z) pumping
  have hac := counts_ac (u ++ List.n_times v 2 ++ x ++ List.n_times y 2 ++ z) pumping
  cases pumping with
  | intro n' pump' =>
      have zero_in_v : List.count_in v _a = 0 := by
        rw [List.mem_append] at no_a; push_neg at no_a
        exact List.count_in_zero_of_notin no_a.left
      have zero_in_y : List.count_in y _a = 0 := by
        rw [List.mem_append] at no_a; push_neg at no_a
        exact List.count_in_zero_of_notin no_a.right
      have count_a : List.count_in (u ++ List.n_times v 2 ++ x ++ List.n_times y 2 ++ z) _a = n + 1 := by
        count_contra
      cases extra_not_a with
      | inl extra_b =>
          have at_least_one_b : List.count_in (v ++ y) _b > 0 :=
            List.count_in_pos_of_in extra_b
          have count_b : List.count_in (u ++ List.n_times v 2 ++ x ++ List.n_times y 2 ++ z) _b > n + 1 := by
            count_contra
          rw [count_a] at hab; rw [hab] at count_b
          exact (lt_irrefl _ count_b)
      | inr extra_c =>
          have at_least_one_c : List.count_in (v ++ y) _c > 0 :=
            List.count_in_pos_of_in extra_c
          have count_c : List.count_in (u ++ List.n_times v 2 ++ x ++ List.n_times y 2 ++ z) _c > n + 1 := by
            count_contra
          rw [count_a] at hac; rw [hac] at count_c
          exact (lt_irrefl _ count_c)

lemma notCF_lang_eq_eq : ¬ is_CF lang_eq_eq := by
  intro h

  have pum := CF_pumping h
  obtain ⟨n, pump⟩ := pum
  specialize pump (List.replicate (n+1) a_ ++ List.replicate (n+1) b_ ++ List.replicate (n+1) c_)
  specialize pump (by
    use n + 1) (by
    rw [List.length_append, List.length_replicate]
    calc (List.replicate (n + 1) a_ ++ List.replicate (n + 1) b_).length + (n + 1)
        ≥ n + 1 := le_add_self
    _ ≥ n := Nat.le_succ n)
  rcases pump with ⟨u, v, x, y, z, concatenating, nonempty, vxy_short, pumping⟩
  specialize pumping 2

  have not_all_letters : a_ ∉ (v ++ y) ∨ b_ ∉ (v ++ y) ∨ c_ ∉ (v ++ y) := by
    by_contra contr
    push_neg at contr
    rcases contr with ⟨hva, -, hvc⟩
    have vxy_long : (v ++ x ++ y).length > n := by
      by_contra contr
      push_neg at contr
      have total_length_exactly : u.length + (v ++ x ++ y).length + z.length = 3 * n + 3 := by
        have total_length := congr_arg List.length concatenating
        simp only [List.length_append, List.length_replicate] at total_length
        have vxy_len : (v ++ x ++ y).length = v.length + x.length + y.length := by
          simp only [List.length_append]
        rw [vxy_len]
        omega
      have u_short : u.length ≤ n := by
        -- in contradiction with `hva: a_ ∈ v ++ y`
        by_contra u_too_much
        push_neg at u_too_much
        have relaxed_a : a_ ∈ v ++ x ++ y ++ z := by
          cases (List.mem_append.1 hva) with
          | inl a_in_v =>
              rw [List.append_assoc, List.append_assoc, List.mem_append]
              left
              exact a_in_v
          | inr a_in_y =>
              have a_in_yz : a_ ∈ y ++ z := by
                rw [List.mem_append]
                left
                exact a_in_y
              rw [List.append_assoc, List.mem_append]
              right
              exact a_in_yz
        repeat
          rw [List.append_assoc] at concatenating
        rcases List.nthLe_of_mem relaxed_a with ⟨nₐ, hnₐ, h_nthₐ⟩
        obtain ⟨h_nth_a_pr, h_nth_a⟩ :
            ∃ proofoo, (v ++ x ++ y ++ z).nthLe ((nₐ + u.length) - u.length) proofoo = a_ := by
          rw [Nat.add_sub_cancel nₐ u.length]
          exact ⟨hnₐ, h_nthₐ⟩
        have lt_len : (nₐ + u.length) < (u ++ (v ++ x ++ y ++ z)).length := by
          rw [List.length_append]
          linarith
        rw [← List.nthLe_append_right le_add_self lt_len] at h_nth_a
        have orig_nth_le_eq_a :
            ∃ proofoo,
              (List.replicate (n + 1) a_ ++ (List.replicate (n + 1) b_ ++ List.replicate (n + 1) c_)).nthLe
                  (nₐ + u.length) proofoo =
                a_ := by
          have rebracket : u ++ (v ++ (x ++ (y ++ z))) = u ++ (v ++ x ++ y ++ z) := by
            simp only [List.append_assoc]
          rw [concatenating, rebracket]
          exact ⟨lt_len, h_nth_a⟩
        cases orig_nth_le_eq_a with
        | intro rrr_nth_le_eq_a_pr rrr_nth_le_eq_a =>
            rw [@List.nthLe_append_right (Fin 3)
                (List.replicate (n + 1) a_)
                (List.replicate (n + 1) b_ ++ List.replicate (n + 1) c_)
                (nₐ + u.length)
                (by
                  rw [List.length_replicate]
                  calc n + 1 ≤ u.length := u_too_much
                  _ ≤ nₐ + u.length := le_add_self)
                (by
                  rw [concatenating]
                  rw [← List.append_assoc x, ← List.append_assoc v, ← List.append_assoc v]
                  exact lt_len)] at rrr_nth_le_eq_a
            have a_in_rb_rc : a_ ∈ (List.replicate (n + 1) b_ ++ List.replicate (n + 1) c_) := by
              rw [← rrr_nth_le_eq_a]
              apply List.nthLe_mem
            rw [List.mem_append] at a_in_rb_rc
            cases a_in_rb_rc with
            | inl a_in_rb =>
                rw [List.mem_replicate] at a_in_rb
                exact neq_ab a_in_rb.right
            | inr a_in_rc =>
                rw [List.mem_replicate] at a_in_rc
                exact neq_ac a_in_rc.right
      have z_short : z.length ≤ n := by
        have our_bound : 2 * n + 2 < (u ++ v ++ x ++ y).length := by
          have relaxed_c : c_ ∈ u ++ v ++ x ++ y := by
            cases (List.mem_append.1 hvc) with
            | inl c_in_v =>
                have c_in_uv : c_ ∈ u ++ v := by
                  rw [List.mem_append]
                  right
                  exact c_in_v
                rw [List.append_assoc, List.mem_append]
                left
                exact c_in_uv
            | inr c_in_y =>
                rw [List.mem_append]
                right
                exact c_in_y
          have concat_reassoc : List.replicate (n + 1) a_ ++ List.replicate (n + 1) b_ ++ List.replicate (n + 1) c_ = u ++ v ++ x ++ y ++ z := by
            repeat rw [List.append_assoc] at concatenating
            simp only [List.append_assoc]
            exact concatenating
          rcases List.nthLe_of_mem relaxed_c with ⟨m, hm, mth_is_c⟩
          have m_big : m ≥ 2 * n + 2 := by
            have orig_mth_is_c :
                ∃ proofoo,
                  ((List.replicate (n + 1) a_ ++ List.replicate (n + 1) b_) ++ List.replicate (n + 1) c_).nthLe
                      m proofoo =
                    c_ := by
              rw [concat_reassoc]
              have m_small : m < (u ++ v ++ x ++ y ++ z).length := by
                rw [List.length_append]
                linarith
              use m_small
              -- mth_is_c : (u ++ v ++ x ++ y).nthLe m hm = c_
              -- We need to show: ((List.replicate (n + 1) a_ ++ List.replicate (n + 1) b_) ++ List.replicate (n + 1) c_).nthLe m m_small = c_
              -- After substitution concat_reassoc, we get (u ++ v ++ x ++ y ++ z).nthLe m m_small = c_
              -- We need to relate this to (u ++ v ++ x ++ y).nthLe m hm
              have split_uvxyz : (u ++ v ++ x ++ y ++ z) = (u ++ v ++ x ++ y) ++ z := by
                simp only [List.append_assoc]
              have m_small' : m < ((u ++ v ++ x ++ y) ++ z).length := by
                rw [← split_uvxyz]; exact m_small
              rw [List.nthLe_append]
              exact mth_is_c
            cases orig_mth_is_c with
            | intro proof_m mth_is_c =>
                by_contra mle
                push_neg at mle
                have m_lt_len :
                    m < (List.replicate (n + 1) a_ ++ List.replicate (n + 1) b_).length := by
                  simp only [List.length_append, List.length_replicate]
                  omega
                have regroup_for_mth : ((List.replicate (n + 1) a_ ++ List.replicate (n + 1) b_) ++ List.replicate (n + 1) c_).nthLe m proof_m = (List.replicate (n + 1) a_ ++ List.replicate (n + 1) b_).nthLe m m_lt_len := by
                  rw [List.nthLe_append m_lt_len]
                rw [regroup_for_mth] at mth_is_c
                have c_in_ra_rb :
                    c_ ∈ (List.replicate (n + 1) a_ ++ List.replicate (n + 1) b_) := by
                  rw [← mth_is_c]
                  apply List.nthLe_mem
                rw [List.mem_append] at c_in_ra_rb
                cases c_in_ra_rb with
                | inl c_in_ra =>
                    rw [List.mem_replicate] at c_in_ra
                    exact neq_ca c_in_ra.right
                | inr c_in_rb =>
                    rw [List.mem_replicate] at c_in_rb
                    exact neq_cb c_in_rb.right
          linarith
        rw [← List.length_append] at total_length_exactly
        rw [← List.append_assoc] at total_length_exactly
        rw [← List.append_assoc] at total_length_exactly
        linarith
      linarith
    exact not_le_of_gt vxy_long vxy_short

  have counts_ab : ∀ w ∈ lang_eq_eq, List.count_in w a_ = List.count_in w b_ := by
    intro w w_in
    cases w_in with
    | intro w_n w_prop => rw [w_prop]; count_contra
  have counts_ac : ∀ w ∈ lang_eq_eq, List.count_in w a_ = List.count_in w c_ := by
    intro w w_in
    cases w_in with
    | intro w_n w_prop => rw [w_prop]; count_contra
  have counts_bc : ∀ w ∈ lang_eq_eq, List.count_in w b_ = List.count_in w c_ := by
    intro w w_in
    rw [← counts_ab w w_in]
    exact counts_ac w w_in
  have counts_ba : ∀ w ∈ lang_eq_eq, List.count_in w b_ = List.count_in w a_ := by
    intro w w_in
    symm
    exact counts_ab w w_in
  have counts_ca : ∀ w ∈ lang_eq_eq, List.count_in w c_ = List.count_in w a_ := by
    intro w w_in
    symm
    exact counts_ac w w_in
  have counts_cb : ∀ w ∈ lang_eq_eq, List.count_in w c_ = List.count_in w b_ := by
    intro w w_in
    symm
    exact counts_bc w w_in

  have counted_letter : ∀ s,
      List.count_in (u ++ v ++ x ++ y ++ z ++ (v ++ y)) s =
        List.count_in (List.replicate (n + 1) a_) s + List.count_in (List.replicate (n + 1) b_) s +
          List.count_in (List.replicate (n + 1) c_) s + List.count_in (v ++ y) s := by
    intro s
    rw [← concatenating]
    repeat
      rw [List.count_in_append]
  have counted_a :
      List.count_in (u ++ v ++ x ++ y ++ z ++ (v ++ y)) a_ =
        n + 1 + List.count_in (v ++ y) a_ := by
    rw [counted_letter]; count_contra
  have counted_b :
      List.count_in (u ++ v ++ x ++ y ++ z ++ (v ++ y)) b_ =
        n + 1 + List.count_in (v ++ y) b_ := by
    rw [counted_letter]; count_contra
  have counted_c :
      List.count_in (u ++ v ++ x ++ y ++ z ++ (v ++ y)) c_ =
        n + 1 + List.count_in (v ++ y) c_ := by
    rw [counted_letter]; count_contra

  have elimin_abc : ∀ s : Fin 3, s ≠ a_ → s ≠ b_ → s ≠ c_ → False := by
    intro s hsa hsb hsc
    fin_cases s
    · rw [a_] at hsa
      exact hsa rfl
    · rw [b_] at hsb
      exact hsb rfl
    · rw [c_] at hsc
      exact hsc rfl

  cases not_all_letters with
  | inl no_a =>
      exact false_of_uvvxyyz elimin_abc no_a nonempty counts_ab counts_ac
        counted_a counted_b counted_c pumping
  | inr foo =>
      cases foo with
      | inl no_b =>
          have elimin_bca : ∀ s : Fin 3, s ≠ b_ → s ≠ c_ → s ≠ a_ → False := by
            intro s hsb hsc hsa
            exact elimin_abc s hsa hsb hsc
          exact false_of_uvvxyyz elimin_bca no_b nonempty counts_bc counts_ba
            counted_b counted_c counted_a pumping
      | inr no_c =>
          have elimin_cab : ∀ s : Fin 3, s ≠ c_ → s ≠ a_ → s ≠ b_ → False := by
            intro s hsc hsa hsb
            exact elimin_abc s hsa hsb hsc
          exact false_of_uvvxyyz elimin_cab no_c nonempty counts_ca counts_cb
            counted_c counted_a counted_b pumping

end not_CF


section yes_CF

private def lang_aux_ab : Language (Fin 3) :=
fun w => ∃ n : ℕ, w = List.replicate n a_ ++ List.replicate n b_

private lemma CF_lang_aux_ab : is_CF lang_aux_ab := by
  let S_ : Fin 1 := 0
  let S : symbol (Fin 3) (Fin 1) := symbol.nonterminal S_
  let g := CF_grammar.mk
    (Fin 1)
    S_
    [
      (S_, [a, S, b]),
      (S_, ([] : List (symbol (Fin 3) (Fin 1))))
    ]
  apply is_CF_via_cfg_implies_is_CF
  refine ⟨g, ?_⟩
  apply Set.eq_of_subset_of_subset
  · intro w ass
    change CF_derives g [S] (List.map symbol.terminal w) at ass
    have indu :
        ∀ v : List (symbol (Fin 3) (Fin 1)),
          CF_derives g [S] v →
            ∃ n : ℕ,
              v = List.replicate n a ++ List.replicate n b ∨
                v = List.replicate n a ++ [S] ++ List.replicate n b := by
      intro v hyp
      induction hyp with
      | refl =>
          use 0
          right
          rfl
      | tail u' orig hyp_ih =>
          rcases orig with ⟨r, p, q, rin, bef, aft⟩
          cases hyp_ih with
          | intro k ih =>
              cases ih with
              | inl ih =>
                  exfalso
                  rw [ih] at bef
                  have yes_in : symbol.nonterminal r.fst ∈ p ++ [symbol.nonterminal r.fst] ++ q := by
                    apply List.mem_append_left
                    apply List.mem_append_right
                    apply List.mem_cons_self
                  have not_in : symbol.nonterminal r.fst ∉ List.replicate k a ++ List.replicate k b := by
                    rw [List.mem_append]
                    push_neg
                    constructor <;>
                      · rw [List.mem_replicate]
                        push_neg
                        intro trash
                        tauto
                  rw [bef] at not_in
                  exact not_in yes_in
              | inr ih =>
                  have both_rule_rewrite_S : symbol.nonterminal r.fst = S := by
                    cases rin with
                    | head =>
                        rfl
                    | tail _ rin =>
                        cases rin with
                        | head =>
                            rfl
                        | tail _ rin =>
                            cases rin
                  rw [bef] at ih
                  rw [both_rule_rewrite_S] at ih
                  have p_len : p.length = k := by
                    by_contra contra
                    have kth_eq := congr_fun (congr_arg List.nth ih) p.length
                    have plengthth_is_S : (p ++ [S] ++ q).nth p.length = some S := by
                      rw [List.append_assoc]
                      rw [List.nth_append_right (le_of_eq rfl)]
                      · rw [Nat.sub_self]
                        rfl
                    rw [plengthth_is_S] at kth_eq
                    cases lt_or_gt_of_ne contra with
                    | inl h =>
                        have plengthth_is_a :
                            (List.replicate k a ++ [S] ++ List.replicate k b).nth p.length =
                              some a := by
                          rw [List.append_assoc]
                          have plength_small : p.length < (List.replicate k a).length := by
                            rw [List.length_replicate]
                            exact h
                          rw [List.nth_append plength_small]
                          rw [List.nthLe_nth plength_small]
                          apply congr_arg
                          exact List.nthLe_replicate a plength_small
                        rw [plengthth_is_a] at kth_eq
                        have S_neq_a : S ≠ a := by
                          tauto
                        rw [Option.some_inj] at kth_eq
                        exact S_neq_a kth_eq
                    | inr h =>
                        have plengthth_is_b :
                            (List.replicate k a ++ [S] ++ List.replicate k b).nth p.length =
                              some b := by
                          have plength_big : (List.replicate k a ++ [S]).length ≤ p.length := by
                            rw [List.length_append, List.length_replicate]
                            exact Nat.succ_le_iff.mpr h
                          rw [List.nth_append_right plength_big]
                          have len_within_list :
                              p.length - (List.replicate k a ++ [S]).length < (List.replicate k b).length := by
                            have ihlen := congr_arg List.length ih
                            simp only [List.length_replicate, List.length_append, List.length_singleton] at *
                            have ihlen' : p.length + 1 ≤ k + 1 + k := by
                              exact Nat.le.intro ihlen
                            have ihlen'' : p.length < k + 1 + k := by
                              exact Nat.succ_le_iff.mp ihlen'
                            rw [← tsub_lt_iff_left plength_big] at ihlen''
                            exact ihlen''
                          rw [List.nthLe_nth len_within_list]
                          apply congr_arg
                          exact List.nthLe_replicate b len_within_list
                        rw [plengthth_is_b] at kth_eq
                        have S_neq_b : S ≠ b := by
                          tauto
                        rw [Option.some_inj] at kth_eq
                        exact S_neq_b kth_eq
                  have ihl_len : (p ++ [symbol.nonterminal S_]).length = k + 1 := by
                    rw [List.length_append, p_len]
                    rfl
                  have ihr_len : (List.replicate k a ++ [S]).length = k + 1 := by
                    rw [List.length_append, List.length_replicate]
                    rfl
                  have qb : q = List.replicate k b := by
                    apply List.append_inj_right ih
                    rw [ihl_len, ihr_len]
                  have ih_reduced : p ++ [symbol.nonterminal S_] = List.replicate k a ++ [S] := by
                    rw [qb] at ih
                    rw [List.append_left_inj] at ih
                    exact ih
                  have pa : p = List.replicate k a := by
                    rw [List.append_left_inj] at ih_reduced
                    exact ih_reduced
                  cases rin with
                  | head =>
                      use k + 1
                      right
                      rw [aft]
                      -- In head case, r = (S_, [a, S, b])
                      rw [pa, qb]
                      rw [List.replicate_succ_eq_append_singleton]
                      rw [List.replicate_succ_eq_singleton_append]
                      simp
                  | tail _ rin =>
                      cases rin with
                      | head =>
                          use k
                          left
                          rw [aft, List.append_nil, pa, qb]
                      | tail _ rin =>
                          nomatch rin
    cases indu (List.map symbol.terminal w) ass with
    | intro n instantiated =>
        clear indu
        cases instantiated with
        | inl instantiated =>
            use n

            have foo := congr_arg (List.filterMap (
              λ z : symbol (Fin 3) (Fin 1) =>
                match z with
                | symbol.terminal t => some t
                | symbol.nonterminal _ => none
            )) instantiated
            simp only [List.filterMap_append, a, b] at foo

            have filterMap_replicate_terminal : ∀ (n : ℕ) (t : Fin 3),
                List.filterMap (fun z : symbol (Fin 3) (Fin 1) => match z with | symbol.terminal t => some t | symbol.nonterminal _ => none)
                  (List.replicate n (symbol.terminal t)) = List.replicate n t := by
              intro n t
              induction n with
              | zero => rfl
              | succ n ih => simp [List.replicate, ih]

            have filterMap_map_terminal : ∀ (l : List (Fin 3)),
                List.filterMap (fun z : symbol (Fin 3) (Fin 1) => match z with | symbol.terminal t => some t | symbol.nonterminal _ => none)
                  (List.map symbol.terminal l) = l := by
              intro l
              induction l with
              | nil => rfl
              | cons h t ih => simp [List.map, ih]

            rw [filterMap_map_terminal w, filterMap_replicate_terminal n a_, filterMap_replicate_terminal n b_] at foo
            exact foo
        | inr instantiated =>
            exfalso
            have S_in : S ∈ List.map symbol.terminal w := by
              rw [instantiated]
              apply List.mem_append_left
              apply List.mem_append_right
              exact List.mem_cons_self
            simp [S] at S_in
  · intro w ass
    obtain ⟨n, hw⟩ := ass
    change CF_derives g [symbol.nonterminal g.initial] (List.map symbol.terminal w)
    rw [hw, List.map_append, List.map_replicate, List.map_replicate, ←a, ←b]
    clear hw
    induction n with
    | zero =>
      convert_to CF_derives g [symbol.nonterminal g.initial] []
      apply CF_deri_of_tran
      use (S_, ([] : List (symbol (Fin 3) (Fin 1))))
      refine ⟨[], [], ?_, rfl, rfl⟩
      simp [g]
    | succ n ih =>
      convert_to
        CF_derives g
          [symbol.nonterminal g.initial]
          (List.map
            symbol.terminal
            ([a_] ++ (List.replicate n a_ ++ List.replicate n b_) ++ [b_])
          )
      · convert_to
          List.replicate (1 + n) a ++ List.replicate (n + 1) b =
          List.map symbol.terminal ([a_] ++ (List.replicate n a_ ++ List.replicate n b_) ++ [b_])
        · rw [add_comm]
        rw [
          List.map_append_append,
          List.map_singleton,
          List.map_singleton,
          List.replicate_add,
          List.replicate_add,
          a, b
        ]
        simp only [List.replicate, List.append_assoc, List.map_append, List.map_replicate]
      apply CF_deri_of_tran_deri
      · use (S_, [a, S, b])
        refine ⟨[], [], ?_, rfl, rfl⟩
        simp [g]
      rw [List.map_append_append]
      change
        CF_derives g
          ([a] ++ [S] ++ [b])
          ([a] ++ List.map symbol.terminal (List.replicate n a_ ++ List.replicate n b_) ++ [b])
      deri_context
      convert ih
      rw [List.map_append, List.map_replicate, List.map_replicate, a, b]

private def lang_aux_c : Language (Fin 3) :=
fun w => ∃ n : ℕ, w = List.replicate n c_

private lemma CF_lang_aux_c : is_CF lang_aux_c := by
  apply is_CF_via_cfg_implies_is_CF
  refine ⟨cfg_symbol_star c_, ?_⟩
  unfold lang_aux_c
  apply language_of_cfg_symbol_star

lemma CF_lang_eq_any : is_CF lang_eq_any := by
  have concatenated : lang_eq_any = lang_aux_ab * lang_aux_c := by
    ext1 w
    constructor
    · rintro ⟨n, m, hnm⟩
      rw [Language.mem_mul]
      exact ⟨_, ⟨n, rfl⟩, _, ⟨m, rfl⟩, hnm.symm⟩
    · intro hmem
      rw [Language.mem_mul] at hmem
      obtain ⟨u, ⟨n, u_eq⟩, v, ⟨m, v_eq⟩, eq_w⟩ := hmem
      use n, m
      rw [← eq_w, ← u_eq, ← v_eq]
  rw [concatenated]
  apply CF_of_CF_c_CF
  exact And.intro CF_lang_aux_ab CF_lang_aux_c


private def lang_aux_a : Language (Fin 3) :=
fun w => ∃ n : ℕ, w = List.replicate n a_

private lemma CF_lang_aux_a : is_CF lang_aux_a := by
  apply is_CF_via_cfg_implies_is_CF
  refine ⟨cfg_symbol_star a_, ?_⟩
  unfold lang_aux_a
  apply language_of_cfg_symbol_star

private def lang_aux_bc : Language (Fin 3) :=
fun w => ∃ n : ℕ, w = List.replicate n b_ ++ List.replicate n c_

private def permut : Equiv.Perm (Fin 3) := Equiv.mk
  (fun x => ite (x = 2) 0 (x + 1))
  (fun x => ite (x = 0) 2 (x - 1))
  (by
    intro x
    fin_cases x <;> rfl)
  (by
    intro x
    fin_cases x <;> rfl)

private lemma CF_lang_aux_bc : is_CF lang_aux_bc := by
  have permuted : lang_aux_bc = Language.permuteLang lang_aux_ab permut := by
    have psb : permut.symm b_ = a_ := by decide
    have psc : permut.symm c_ = b_ := by decide
    have pa : permut a_ = b_ := by decide
    have pb : permut b_ = c_ := by decide
    ext1 w
    constructor
    · rintro ⟨n, hn⟩
      show List.map permut.symm w ∈ lang_aux_ab
      refine ⟨n, ?_⟩
      rw [hn, List.map_append, List.map_replicate, List.map_replicate, psb, psc]
    · intro h
      show _ ∈ lang_aux_bc
      obtain ⟨n, hn⟩ := h
      refine ⟨n, ?_⟩
      have := congr_arg (List.map permut) hn
      rw [List.map_map, List.map_append, List.map_replicate, List.map_replicate, pa, pb] at this
      simp only [Equiv.self_comp_symm, List.map_id] at this
      exact this
  rw [permuted]
  exact (CF_of_permute_CF permut lang_aux_ab).mpr CF_lang_aux_ab

lemma CF_lang_any_eq : is_CF lang_any_eq := by
  have concatenated : lang_any_eq = lang_aux_a * lang_aux_bc := by
    ext1 w
    constructor
    · rintro ⟨n, m, hnm⟩
      rw [Language.mem_mul]
      exact ⟨_, ⟨n, rfl⟩, _, ⟨m, rfl⟩, by rw [← List.append_assoc]; exact hnm.symm⟩
    · intro hmem
      rw [Language.mem_mul] at hmem
      obtain ⟨u, ⟨n, hu⟩, v, ⟨m, hv⟩, h⟩ := hmem
      use n, m
      rw [List.append_assoc, ← h, ← hu, ← hv]
  rw [concatenated]
  apply CF_of_CF_c_CF
  exact And.intro CF_lang_aux_a CF_lang_aux_bc

end yes_CF


section intersection_inclusions

lemma intersection_of_lang_eq_eq {w : List (Fin 3)} :
  w ∈ lang_eq_eq  →  w ∈ lang_eq_any ⊓ lang_any_eq  :=
by
  intro h
  cases h with
  | intro n hyp =>
      constructor <;> exact ⟨n, n, hyp⟩

/-- Given `rep n₁ a ++ rep n₁ b ++ rep m₁ c = rep n₂ a ++ rep m₂ b ++ rep m₂ c`,
    if `k > 0` and `k ≤ n₁` (or `k ≤ n₂`), the element at position `k-1` in one side
    is `a` but in the other it falls past the `a`-block into `b`/`c`, contradiction. -/
private lemma replicate_abc_nthLe_contradiction
    {k₁ k₂ : ℕ} {a_ : Fin 3}
    (k₁pos : k₁ > 0) (hlt : k₁ > k₂)
    (l₁ l₂ : List (Fin 3))
    (equ : List.replicate k₁ a_ ++ l₁ = List.replicate k₂ a_ ++ l₂)
    (h_l₂ : ∀ x ∈ l₂, x ≠ a_) :
    False := by
  have idx_in_k₁ : k₁ - 1 < (List.replicate k₁ a_).length := by
    rw [List.length_replicate]; exact Nat.sub_lt k₁pos (Nat.succ_pos 0)
  have idx_past_k₂ : (List.replicate k₂ a_).length ≤ k₁ - 1 := by
    rw [List.length_replicate]; exact Nat.le_pred_of_lt hlt
  have idx_in_rhs : k₁ - 1 < (List.replicate k₂ a_ ++ l₂).length := by
    rw [← equ, List.length_append]; linarith [idx_in_k₁]
  have lhs_val : (List.replicate k₁ a_ ++ l₁).nthLe (k₁ - 1)
      (by rw [List.length_append]; linarith [idx_in_k₁]) = a_ := by
    rw [List.nthLe_append idx_in_k₁]
    exact List.nthLe_replicate a_ idx_in_k₁
  have rhs_val := List.nthLe_of_eq equ
    (n := k₁ - 1) (hn := by rw [List.length_append]; linarith [idx_in_k₁])
  rw [lhs_val] at rhs_val
  rw [List.nthLe_append_right idx_past_k₂ idx_in_rhs] at rhs_val
  exact h_l₂ _ (List.nthLe_mem _) rhs_val.symm

/-- In `rep n₁ a ++ rep n₁ b ++ rep m₁ c = rep n₂ a ++ rep m₂ b ++ rep m₂ c`, the
    nthLe-based argument gives `a` on one side and a non-`a` element on the other. -/
private lemma not_mem_bc_of_ne (a_ b_ c_ : Fin 3) (a_neq_b : a_ ≠ b_) (a_neq_c : a_ ≠ c_)
    {m₁ m₂ : ℕ} : ∀ x ∈ List.replicate m₁ b_ ++ List.replicate m₂ c_, x ≠ a_ := by
  intro x hx hxa
  rw [List.mem_append] at hx
  cases hx with
  | inl h => exact a_neq_b (hxa ▸ (List.mem_replicate.mp h).right)
  | inr h => exact a_neq_c (hxa ▸ (List.mem_replicate.mp h).right)

private lemma doubled_le_singled
    (n₁ m₁ n₂ m₂ : ℕ) (n₁pos : n₁ > 0)
    (a_ b_ c_ : Fin 3) (a_neq_b : a_ ≠ b_) (a_neq_c : a_ ≠ c_)
    (equ :
      List.replicate n₁ a_ ++ List.replicate n₁ b_ ++ List.replicate m₁ c_ =
      List.replicate n₂ a_ ++ List.replicate m₂ b_ ++ List.replicate m₂ c_
    ) :
  n₁ ≤ n₂ := by
  by_contra contr
  push_neg at contr
  rw [List.append_assoc, List.append_assoc] at equ
  exact replicate_abc_nthLe_contradiction n₁pos contr _ _ equ
    (not_mem_bc_of_ne a_ b_ c_ a_neq_b a_neq_c)

private lemma doubled_ge_singled
    (n₁ m₁ n₂ m₂ : ℕ) (n₂pos : n₂ > 0)
    (a_ b_ c_ : Fin 3) (a_neq_b : a_ ≠ b_) (a_neq_c : a_ ≠ c_)
    (equ :
      List.replicate n₁ a_ ++ List.replicate n₁ b_ ++ List.replicate m₁ c_ =
      List.replicate n₂ a_ ++ List.replicate m₂ b_ ++ List.replicate m₂ c_
    ) :
  n₁ ≥ n₂ := by
  by_contra contr
  push_neg at contr
  rw [List.append_assoc, List.append_assoc] at equ
  exact replicate_abc_nthLe_contradiction n₂pos contr _ _ equ.symm
    (not_mem_bc_of_ne a_ b_ c_ a_neq_b a_neq_c)



lemma lang_eq_eq_of_intersection {w : List (Fin 3)} :
  w ∈ lang_eq_any ⊓ lang_any_eq  →  w ∈ lang_eq_eq  :=
by
  rintro ⟨⟨n₁, m₁, w_eq₁⟩, ⟨n₂, m₂, w_eq₂⟩⟩
  have equ := Eq.trans w_eq₁.symm w_eq₂
  by_cases hn₁ : n₁ = 0
  · have hn₂ : n₂ = 0 := by
      by_contra h
      have a_yes : a_ ∈ List.replicate n₂ a_ := List.mem_replicate.mpr ⟨h, rfl⟩
      have a_in_equ := congr_arg (fun lis => a_ ∈ lis) equ
      rw [hn₁] at a_in_equ
      simp [a_yes, List.mem_replicate, List.mem_append, neq_ab, neq_ac] at a_in_equ
    have hm₂ : m₂ = 0 := by
      by_contra h
      have b_yes : b_ ∈ List.replicate m₂ b_ := List.mem_replicate.mpr ⟨h, rfl⟩
      have b_in_equ := congr_arg (fun lis => b_ ∈ lis) equ
      rw [hn₁, hn₂] at b_in_equ
      simp [b_yes, List.mem_replicate, List.mem_append, neq_bc] at b_in_equ
    exact ⟨0, by rw [hn₂, hm₂] at w_eq₂; exact w_eq₂⟩
  have n₁pos : n₁ > 0 := Nat.pos_of_ne_zero hn₁
  have n₂pos : n₂ > 0 := by
    by_contra h; push_neg at h
    rw [Nat.eq_zero_of_le_zero h, List.replicate_zero, List.nil_append] at equ
    have a_in_equ := congr_arg (fun lis => a_ ∈ lis) equ
    simp [List.mem_append, List.mem_replicate, hn₁, neq_ab, neq_ac] at a_in_equ
  have m₂pos : m₂ > 0 := by
    by_contra h; push_neg at h
    rw [Nat.eq_zero_of_le_zero h, List.replicate_zero, List.append_nil] at equ
    have b_in_equ := congr_arg (fun lis => b_ ∈ lis) equ
    simp [List.mem_append, List.mem_replicate, hn₁, neq_ba] at b_in_equ
  have m₁pos : m₁ > 0 := by
    by_contra h; push_neg at h
    rw [Nat.eq_zero_of_le_zero h, List.replicate_zero, List.append_nil] at equ
    have c_in_equ := congr_arg (fun lis => c_ ∈ lis) equ
    simp [List.mem_append, List.mem_replicate, neq_ca, neq_cb, (show m₂ ≠ 0 by omega)] at c_in_equ

  have n_ge := doubled_ge_singled n₁ m₁ n₂ m₂ n₂pos a_ b_ c_ neq_ab neq_ac equ
  have n_le := doubled_le_singled n₁ m₁ n₂ m₂ n₁pos a_ b_ c_ neq_ab neq_ac equ
  have eqn : n₁ = n₂ := le_antisymm n_le n_ge
  -- For the m₁/m₂ comparison, reverse both sides
  have rev : List.replicate m₂ c_ ++ List.replicate m₂ b_ ++ List.replicate n₂ a_ =
             List.replicate m₁ c_ ++ List.replicate n₁ b_ ++ List.replicate n₁ a_ := by
    have := congr_arg List.reverse equ
    repeat rw [List.reverse_append] at this
    simp only [List.reverse_replicate, ← List.append_assoc] at this
    exact this.symm
  have m_ge : m₁ ≥ m₂ :=
    doubled_le_singled m₂ n₂ m₁ n₁ m₂pos c_ b_ a_ neq_cb neq_ca rev
  have m_le : m₁ ≤ m₂ :=
    doubled_ge_singled m₂ n₂ m₁ n₁ m₁pos c_ b_ a_ neq_cb neq_ca rev
  have eqm : m₁ = m₂ := le_antisymm m_le m_ge
  have eq₂ : n₂ = m₂ := by
    have lengs := congr_arg List.length equ
    simp only [List.length_append, List.length_replicate] at lengs
    omega
  rw [eq₂] at w_eq₂
  exact ⟨m₂, w_eq₂⟩

end intersection_inclusions


/-- The class of context-free languages isn't closed under intersection. -/
theorem nnyCF_of_CF_i_CF : ¬ (∀ L₁ L₂ : Language (Fin 3),
    is_CF L₁  ∧  is_CF L₂   →   is_CF (L₁ ⊓ L₂)
) :=
by
  by_contra contra
  specialize contra lang_eq_any lang_any_eq ⟨CF_lang_eq_any, CF_lang_any_eq⟩
  apply notCF_lang_eq_eq
  convert contra
  ext w
  constructor
  · apply intersection_of_lang_eq_eq
  · apply lang_eq_eq_of_intersection

/-- Context-free languages over `Fin 3` are not closed under intersection. -/
theorem CF_notClosedUnderIntersection :
    ¬ ClosedUnderIntersection (α := Fin 3) is_CF := by
  rw [ClosedUnderIntersection]
  have contra := nnyCF_of_CF_i_CF
  grind

private lemma Language.map_inf_injective {α β : Type} {f : α → β} (hf : Function.Injective f)
    (L₁ L₂ : Language α) :
    Language.map f (L₁ ⊓ L₂) = Language.map f L₁ ⊓ Language.map f L₂ := by
  ext w
  constructor
  · rintro ⟨v, ⟨hv1, hv2⟩, rfl⟩
    exact ⟨⟨v, hv1, rfl⟩, ⟨v, hv2, rfl⟩⟩
  · rintro ⟨⟨v1, hv1, hmap1⟩, ⟨v2, hv2, hmap2⟩⟩
    have heq : v1 = v2 := by
      apply List.map_injective_iff.mpr hf
      rw [hmap1, hmap2]
    subst heq
    exact ⟨v1, ⟨hv1, hv2⟩, hmap1⟩

/-- Context-free languages are not closed under intersection for any type with at least
    3 elements. That is, as long as `α` has at least 3 distinct elements, not all
    intersections of context-free languages over `α` are context-free. -/
theorem CF_notClosedUnderIntersection_of_three {α : Type}
    (a b c : α) (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) :
    ¬ ClosedUnderIntersection (α := α) is_CF := by
  intro hclosed
  -- Build an injection Fin 3 → α
  have hf : Function.Injective (fun i : Fin 3 => (![a, b, c] : Fin 3 → α) i) := by
    intro i j h
    fin_cases i <;> fin_cases j <;> simp_all [Matrix.cons_val_zero, Matrix.cons_val_one]
  set f : Fin 3 → α := fun i => ![a, b, c] i
  -- Transfer the Fin 3 non-closure result
  apply nnyCF_of_CF_i_CF
  intro L₁ L₂ ⟨hL₁, hL₂⟩
  have hfL₁ : is_CF (Language.map f L₁) := CF_of_map_CF f L₁ hL₁
  have hfL₂ : is_CF (Language.map f L₂) := CF_of_map_CF f L₂ hL₂
  have hinter : is_CF (Language.map f L₁ ⊓ Language.map f L₂) :=
    hclosed _ _ hfL₁ hfL₂
  rw [← Language.map_inf_injective hf] at hinter
  exact CF_of_map_injective_CF_rev hf _ hinter
