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