module public import Langlib.Classes.ContextFree.Closure.Homomorphism public import Langlib.Classes.ContextFree.Closure.Intersection public import Langlib.Classes.ContextFree.Closure.Union public import Langlib.Classes.DeterministicContextFree.Closure.Complement public import Langlib.Classes.DeterministicContextFree.Closure.Intersection public import Langlib.Classes.DeterministicContextFree.Closure.IntersectionRegular public import Langlib.Classes.DeterministicContextFree.Closure.Concatenation public import Langlib.Classes.DeterministicContextFree.Closure.Union public import Langlib.Classes.DeterministicContextFree.Closure.UnionRegular public import Langlib.Classes.DeterministicContextFree.Examples.AnBmCm public import Langlib.Classes.DeterministicContextFree.Examples.AnBnCm public import Langlib.Classes.DeterministicContextFree.Inclusion.ContextFree public import Langlib.Classes.Regular.Inclusion.DeterministicContextFree public import Langlib.Classes.Regular.Closure.Concatenation public import Langlib.Classes.Regular.Closure.Homomorphism public import Langlib.Classes.Regular.Closure.Star import Langlib.Examples.AbcPositive import Langlib.Examples.AnBnCnPos import Langlib.Classes.DeterministicContextFree.Examples.AbcPositive /-! # Deterministic Context-Free Languages Are Not Closed Under Kleene Star The proof uses the standard DCFL union witnesses, restricted to strictly positive `a`, `b`, and `c` blocks. The positive restriction prevents a later Kleene-star slice from decomposing one `a+ b+ c+` payload into several witness blocks. -/ namespace DCFStar open PDA private lemma complement_not_pos_union_eq_eq_pos : (lang_not_eq_any_pos + lang_not_any_eq_pos)ᶜ ⊓ abcPositive = lang_eq_eq_pos := by rw [lang_eq_eq_pos_eq_inter] ext w constructor · rintro ⟨hnotUnion, hpos⟩ have hNotLeft : w ∉ lang_not_eq_any_pos := by intro hw exact hnotUnion (Or.inl hw) have hNotRight : w ∉ lang_not_any_eq_pos := by intro hw exact hnotUnion (Or.inr hw) have hEqAny : w ∈ lang_eq_any_pos := by by_contra h exact hNotLeft ⟨h, hpos⟩ have hAnyEq : w ∈ lang_any_eq_pos := by by_contra h exact hNotRight ⟨h, hpos⟩ exact ⟨lang_eq_eq_of_intersection ⟨hEqAny.1, hAnyEq.1⟩, hpos⟩ · intro h constructor · intro hunion rw [Language.add_def] at hunion rcases hunion with hleft | hright · have hi := intersection_of_lang_eq_eq h.1 exact hleft.1 ⟨hi.1, h.2⟩ · have hi := intersection_of_lang_eq_eq h.1 exact hright.1 ⟨hi.2, h.2⟩ · exact h.2 private theorem notDCF_not_pos_union : ¬ is_DCF (lang_not_eq_any_pos + lang_not_any_eq_pos) := by intro hUnion have hComp : is_DCF (lang_not_eq_any_pos + lang_not_any_eq_pos)ᶜ := DCF_closedUnderComplement (lang_not_eq_any_pos + lang_not_any_eq_pos) hUnion have hSlice : is_DCF ((lang_not_eq_any_pos + lang_not_any_eq_pos)ᶜ ⊓ abcPositive) := DCF_inter_regular (lang_not_eq_any_pos + lang_not_any_eq_pos)ᶜ abcPositive hComp abcPositive_regular apply notDCF_lang_eq_eq_pos rwa [complement_not_pos_union_eq_eq_pos] at hSlice private lemma lang_eq_eq_pos_of_intersection {w : List (Fin 3)} (h : w ∈ lang_eq_any_pos ⊓ lang_any_eq_pos) : w ∈ lang_eq_eq_pos := by rw [lang_eq_eq_pos_eq_inter] exact ⟨lang_eq_eq_of_intersection ⟨h.1.1, h.2.1⟩, h.1.2⟩ private lemma intersection_of_lang_eq_eq_pos {w : List (Fin 3)} (h : w ∈ lang_eq_eq_pos) : w ∈ lang_eq_any_pos ⊓ lang_any_eq_pos := by rw [lang_eq_eq_pos_eq_inter] at h have hi := intersection_of_lang_eq_eq h.1 exact ⟨⟨hi.1, h.2⟩, ⟨hi.2, h.2⟩⟩ public theorem DCF_notClosedUnderUnion_pos : ¬ ClosedUnderUnion (α := Fin 3) is_DCF := by intro hclosed have hInter : is_DCF (lang_eq_any_pos ⊓ lang_any_eq_pos) := by rw [show lang_eq_any_pos ⊓ lang_any_eq_pos = (lang_eq_any_posᶜ + lang_any_eq_posᶜ)ᶜ by ext w simp only [Language.add_def] change w ∈ lang_eq_any_pos ∧ w ∈ lang_any_eq_pos ↔ ¬ (w ∈ lang_eq_any_posᶜ ⊔ lang_any_eq_posᶜ) rw [show (lang_eq_any_posᶜ ⊔ lang_any_eq_posᶜ : Set (List (Fin 3))) = Set.union lang_eq_any_posᶜ lang_any_eq_posᶜ by rfl] change w ∈ lang_eq_any_pos ∧ w ∈ lang_any_eq_pos ↔ ¬ (w ∉ lang_eq_any_pos ∨ w ∉ lang_any_eq_pos) tauto] exact DCF_closedUnderComplement (lang_eq_any_posᶜ + lang_any_eq_posᶜ) (hclosed lang_eq_any_posᶜ lang_any_eq_posᶜ (DCF_closedUnderComplement lang_eq_any_pos DCF_lang_eq_any_pos) (DCF_closedUnderComplement lang_any_eq_pos DCF_lang_any_eq_pos)) apply notDCF_lang_eq_eq_pos convert hInter ext w constructor · exact intersection_of_lang_eq_eq_pos · exact lang_eq_eq_pos_of_intersection private lemma abcPositive_pairwise {w : List (Fin 3)} (hw : w ∈ abcPositive) : w.Pairwise (· ≤ ·) := by rcases hw with ⟨n, m, k, rfl⟩ simp +decide [List.pairwise_append, a_, b_, c_] private lemma abcPositive_has_a {w : List (Fin 3)} (hw : w ∈ abcPositive) : a_ ∈ w := by rcases hw with ⟨n, m, k, rfl⟩ simp [List.mem_append, List.mem_replicate, a_] private lemma abcPositive_has_c {w : List (Fin 3)} (hw : w ∈ abcPositive) : c_ ∈ w := by rcases hw with ⟨n, m, k, rfl⟩ simp [List.mem_append, List.mem_replicate, c_] private lemma abcPositive_ne_nil {w : List (Fin 3)} (hw : w ∈ abcPositive) : w ≠ [] := by intro hnil have ha : a_ ∈ w := abcPositive_has_a hw simp [hnil] at ha private lemma abcPositive_no_append_after_positive {u tail w : List (Fin 3)} (hu : u ∈ abcPositive) (ha : a_ ∈ tail) (hwEq : w = u ++ tail) (hw : w ∈ abcPositive) : False := by have hpair := abcPositive_pairwise hw rw [hwEq, List.pairwise_append] at hpair have hc : c_ ∈ u := abcPositive_has_c hu have hle : c_ ≤ a_ := hpair.2.2 c_ hc a_ ha have hnot : ¬ ((c_ : Fin 3) ≤ a_) := by decide exact hnot hle private abbrev marker : Bool ⊕ Fin 3 := Sum.inl false private lemma marker_not_mem_payload (w : List (Fin 3)) : (marker : Bool ⊕ Fin 3) ∉ w.map Sum.inr := by intro h rw [List.mem_map] at h rcases h with ⟨a, _ha, h⟩ cases h private abbrev payloadPositive : Language (Bool ⊕ Fin 3) := Language.map Sum.inr abcPositive private abbrev oneMarkerPositive : Language (Bool ⊕ Fin 3) := ({[marker]} : Language (Bool ⊕ Fin 3)) * payloadPositive private lemma payloadPositive_regular : payloadPositive.IsRegular := abcPositive_regular.map Sum.inr private lemma oneMarkerPositive_regular : oneMarkerPositive.IsRegular := (Language.isRegular_singleton_word ([marker] : List (Bool ⊕ Fin 3))).mul' payloadPositive_regular private lemma mem_oneMarkerPositive_iff {x : List (Bool ⊕ Fin 3)} : x ∈ oneMarkerPositive ↔ ∃ w : List (Fin 3), x = marker :: w.map Sum.inr ∧ w ∈ abcPositive := by rw [oneMarkerPositive, Language.mem_mul] constructor · rintro ⟨u, hu, v, hv, rfl⟩ rw [Set.mem_singleton_iff] at hu subst u rcases hv with ⟨w, hw, rfl⟩ exact ⟨w, rfl, hw⟩ · rintro ⟨w, rfl, hw⟩ exact ⟨[marker], Set.mem_singleton _, w.map Sum.inr, ⟨w, hw, rfl⟩, rfl⟩ private def optionalMarkedLanguage (L₁ L₂ : Language (Fin 3)) : Language (Bool ⊕ Fin 3) := {x | (∃ w, x = marker :: w.map Sum.inr ∧ w ∈ L₁) ∨ (∃ w, x = w.map Sum.inr ∧ w ∈ L₂)} private theorem DCF_optionalMarkedLanguage_pos : is_DCF (optionalMarkedLanguage lang_not_eq_any_pos lang_not_any_eq_pos) := by have hDCF := DCFConcatenation.DCF_optional_marked_union DCF_lang_not_eq_any_pos DCF_lang_not_any_eq_pos simpa [optionalMarkedLanguage, marker] using hDCF private def starSeed : Language (Bool ⊕ Fin 3) := ({[marker]} : Language (Bool ⊕ Fin 3)) + optionalMarkedLanguage lang_not_eq_any_pos lang_not_any_eq_pos private theorem DCF_starSeed : is_DCF starSeed := DCF_regular_union ({[marker]} : Language (Bool ⊕ Fin 3)) (optionalMarkedLanguage lang_not_eq_any_pos lang_not_any_eq_pos) (Language.isRegular_singleton_word [marker]) DCF_optionalMarkedLanguage_pos private lemma starSeed_mem_cases {x : List (Bool ⊕ Fin 3)} (hx : x ∈ starSeed) : x = [marker] ∨ (∃ w, x = marker :: w.map Sum.inr ∧ w ∈ lang_not_eq_any_pos) ∨ (∃ w, x = w.map Sum.inr ∧ w ∈ lang_not_any_eq_pos) := by simpa [starSeed, optionalMarkedLanguage, Language.add_def] using hx private lemma starSeed_marker_free_payload {x : List (Bool ⊕ Fin 3)} (hx : x ∈ starSeed) (hfree : (marker : Bool ⊕ Fin 3) ∉ x) : ∃ w, x = w.map Sum.inr ∧ w ∈ lang_not_any_eq_pos := by rcases starSeed_mem_cases hx with hsingle | hmarked | hunmarked · subst x exact False.elim (hfree (by simp)) · rcases hmarked with ⟨w, rfl, _hw⟩ exact False.elim (hfree (by simp)) · exact hunmarked private lemma map_append_eq_map_split {u w : List (Fin 3)} {z : List (Bool ⊕ Fin 3)} (h : u.map Sum.inr ++ z = w.map Sum.inr) : ∃ v, w = u ++ v ∧ z = v.map Sum.inr := by induction u generalizing w with | nil => exact ⟨w, by simp, by simpa using h⟩ | cons a u ih => cases w with | nil => simp at h | cons b w => simp at h rcases h with ⟨hab, hrest⟩ subst b rcases ih hrest with ⟨v, hv, hz⟩ exact ⟨v, by simp [hv], hz⟩ private lemma payload_decomposition_of_marker_free_starSeed {blocks : List (List (Bool ⊕ Fin 3))} {w : List (Fin 3)} (hflat : blocks.flatten = w.map Sum.inr) (hblocks : ∀ b ∈ blocks, b ∈ starSeed) : ∃ payloads : List (List (Fin 3)), w = payloads.flatten ∧ blocks = payloads.map (fun y => y.map Sum.inr) ∧ ∀ y ∈ payloads, y ∈ lang_not_any_eq_pos := by induction blocks generalizing w with | nil => cases w with | nil => exact ⟨[], by simp, by simp, by simp⟩ | cons a w => simp at hflat | cons block rest ih => have hblock : block ∈ starSeed := hblocks block (by simp) have hfree : (marker : Bool ⊕ Fin 3) ∉ block := by intro hm have hmem : (marker : Bool ⊕ Fin 3) ∈ (block :: rest).flatten := List.mem_flatten.mpr ⟨block, by simp, hm⟩ rw [hflat] at hmem exact marker_not_mem_payload w hmem rcases starSeed_marker_free_payload hblock hfree with ⟨u, hblockEq, hu⟩ subst block have hsplit : ∃ v, w = u ++ v ∧ rest.flatten = v.map Sum.inr := map_append_eq_map_split (by simpa using hflat) rcases hsplit with ⟨v, hw, hrestFlat⟩ have hrestBlocks : ∀ b ∈ rest, b ∈ starSeed := by intro b hb exact hblocks b (by simp [hb]) rcases ih hrestFlat hrestBlocks with ⟨payloads, hv, hrestEq, hpayloads⟩ refine ⟨u :: payloads, ?_, ?_, ?_⟩ · simp [hw, hv] · simp [hrestEq] · intro y hy have hy' : y = u ∨ y ∈ payloads := by simpa using hy rcases hy' with hEq | hy · rw [hEq] exact hu · exact hpayloads _ hy private lemma payloads_singleton_of_abcPositive {payloads : List (List (Fin 3))} {w : List (Fin 3)} (hwEq : w = payloads.flatten) (hw : w ∈ abcPositive) (hpayloads : ∀ y ∈ payloads, y ∈ lang_not_any_eq_pos) : ∃ u, payloads = [u] ∧ w = u ∧ u ∈ lang_not_any_eq_pos := by cases payloads with | nil => have ha : a_ ∈ w := abcPositive_has_a hw simp [hwEq] at ha | cons u rest => have hu : u ∈ lang_not_any_eq_pos := hpayloads u (by simp) cases rest with | nil => exact ⟨u, by simp, by simpa using hwEq, hu⟩ | cons v rest => have hv : v ∈ lang_not_any_eq_pos := hpayloads v (by simp) have haTail : a_ ∈ (v :: rest).flatten := by rw [List.mem_flatten] exact ⟨v, by simp, abcPositive_has_a hv.2⟩ exact False.elim <| abcPositive_no_append_after_positive hu.2 haTail (by simp [hwEq]) hw private lemma marker_payload_mem_starSeed_iff {w : List (Fin 3)} (hw : w ∈ abcPositive) : marker :: w.map Sum.inr ∈ KStar.kstar starSeed ↔ w ∈ lang_not_eq_any_pos ∨ w ∈ lang_not_any_eq_pos := by constructor · intro hstar rw [Language.mem_kstar] at hstar rcases hstar with ⟨blocks, hflat, hblocks⟩ cases blocks with | nil => simp at hflat | cons block rest => have hblock : block ∈ starSeed := hblocks block (by simp) rcases starSeed_mem_cases hblock with hsingle | hmarked | hunmarked · subst block have hrestFlat : rest.flatten = w.map Sum.inr := by simpa using hflat.symm have hrestBlocks : ∀ b ∈ rest, b ∈ starSeed := by intro b hb exact hblocks b (by simp [hb]) rcases payload_decomposition_of_marker_free_starSeed hrestFlat hrestBlocks with ⟨payloads, hwPayloads, _hrestEq, hpayloads⟩ rcases payloads_singleton_of_abcPositive hwPayloads hw hpayloads with ⟨u, hpayloadsEq, hwEq, hu⟩ right rwa [hwEq] · rcases hmarked with ⟨u, hblockEq, hu⟩ subst block have hsplit : ∃ v, w = u ++ v ∧ rest.flatten = v.map Sum.inr := map_append_eq_map_split (by simpa using hflat.symm) rcases hsplit with ⟨v, hwEq, hrestFlat⟩ have hrestBlocks : ∀ b ∈ rest, b ∈ starSeed := by intro b hb exact hblocks b (by simp [hb]) rcases payload_decomposition_of_marker_free_starSeed hrestFlat hrestBlocks with ⟨payloads, hvPayloads, _hrestEq, hpayloads⟩ cases payloads with | nil => left have hvNil : v = [] := by simpa using hvPayloads rwa [hwEq, hvNil, List.append_nil] | cons v₀ restPayloads => have hv₀ : v₀ ∈ lang_not_any_eq_pos := hpayloads v₀ (by simp) have haTail : a_ ∈ (v₀ :: restPayloads).flatten := by rw [List.mem_flatten] exact ⟨v₀, by simp, abcPositive_has_a hv₀.2⟩ have hvEq : v = (v₀ :: restPayloads).flatten := hvPayloads exact False.elim <| abcPositive_no_append_after_positive hu.2 (by simpa [hvEq] using haTail) hwEq hw · rcases hunmarked with ⟨u, hblockEq, hu⟩ subst block cases u with | nil => exact False.elim (abcPositive_ne_nil hu.2 rfl) | cons a u => simp at hflat · intro h rw [Language.mem_kstar] rcases h with h | h · refine ⟨[marker :: w.map Sum.inr], by simp, ?_⟩ intro y hy rw [List.mem_singleton] at hy subst y exact Or.inr (Or.inl ⟨w, rfl, h⟩) · refine ⟨[[marker], w.map Sum.inr], by simp, ?_⟩ intro y hy rw [List.mem_cons] at hy rcases hy with hy | hy · subst y exact Or.inl (Set.mem_singleton [marker]) · rw [List.mem_singleton] at hy subst y exact Or.inr (Or.inr ⟨w, rfl, h⟩) private theorem star_seed_slice_eq_union : [marker] \\ ((KStar.kstar starSeed) ⊓ oneMarkerPositive) = Language.map Sum.inr (lang_not_eq_any_pos + lang_not_any_eq_pos) := by ext x constructor · intro hx change marker :: x ∈ (KStar.kstar starSeed) ⊓ oneMarkerPositive at hx rcases hx with ⟨hstar, hone⟩ rw [mem_oneMarkerPositive_iff] at hone rcases hone with ⟨w, hshape, hwpos⟩ cases hshape rw [marker_payload_mem_starSeed_iff hwpos] at hstar exact ⟨w, by simpa [Language.add_def] using hstar, rfl⟩ · rintro ⟨w, hw, rfl⟩ have hwpos : w ∈ abcPositive := by rw [Language.add_def] at hw rcases hw with hw | hw · exact hw.2 · exact hw.2 change marker :: w.map Sum.inr ∈ (KStar.kstar starSeed) ⊓ oneMarkerPositive constructor · rw [marker_payload_mem_starSeed_iff hwpos] simpa [Language.add_def] using hw · rw [mem_oneMarkerPositive_iff] exact ⟨w, rfl, hwpos⟩ /-- Deterministic context-free languages over `Bool ⊕ Fin 3` are not closed under Kleene star. -/ public theorem DCF_notClosedUnderKleeneStar : ¬ ClosedUnderKleeneStar (α := Bool ⊕ Fin 3) is_DCF := by intro hclosed have hStar : is_DCF (KStar.kstar starSeed) := hclosed starSeed DCF_starSeed have hFiltered : is_DCF ((KStar.kstar starSeed) ⊓ oneMarkerPositive) := DCF_inter_regular (KStar.kstar starSeed) oneMarkerPositive hStar oneMarkerPositive_regular have hQuot : is_DCF ([marker] \\ ((KStar.kstar starSeed) ⊓ oneMarkerPositive)) := DCFHomomorphism.DCF_leftQuotient_singleton marker hFiltered rw [star_seed_slice_eq_union] at hQuot have hUnion : is_DCF (lang_not_eq_any_pos + lang_not_any_eq_pos) := DCF_of_map_injective_DCF_rev (f := Sum.inr) (by intro a b h exact Sum.inr.inj h) (lang_not_eq_any_pos + lang_not_any_eq_pos) hQuot exact notDCF_not_pos_union hUnion end DCFStar