import Mathlib import Langlib.Automata.FiniteState.Equivalence.RegularDFAEquiv import Langlib.Utilities.Tactics import Langlib.Classes.Linear.Definition import Langlib.Classes.Linear.Examples.AnBn import Langlib.Classes.Regular.Inclusion.Linear import Langlib.Classes.Regular.Basics.NonRegular import Langlib.Classes.Regular.Closure.Bijection /-! # RG ⊊ Linear This file uses the example language `{aⁿbⁿ}` to show that regular languages form a strict subclass of linear languages. ## Main results - `exists_Linear_not_regular` — There exists a linear language that is not regular. - `RG_strict_subclass_Linear` — Right-regular languages form a strict subclass of linear languages. -/ open Language List Relation Classical noncomputable section variable {T : Type} /-- There exists a linear language that is not regular. -/ theorem exists_Linear_not_regular : ∃ L : Language Bool, is_Linear L ∧ ¬ L.IsRegular := ⟨anbn, anbn_is_Linear, anbn_not_isRegular⟩ private lemma map_anbn_is_Linear (f : Bool → T) (_hf : Function.Injective f) : is_Linear (Language.map f anbn) := by refine' ⟨ _, _, _ ⟩; exact ⟨ Unit, (), [ ⟨ [ ], (), [ ], [ symbol.terminal ( f false ), symbol.nonterminal (), symbol.terminal ( f true ) ] ⟩, ⟨ [ ], (), [ ], [ ] ⟩ ] ⟩; · simp +decide [ grammar_linear ]; exact ⟨ Or.inr ⟨ [ f false ], (), [ f true ], rfl ⟩, Or.inl fun x hx => by aesop ⟩; · ext w; constructor; · intro hw; have h_deriv : ∀ w, grammar_derives { nt := Unit, initial := (), rules := [{ input_L := [], input_N := (), input_R := [], output_string := [symbol.terminal (f false), symbol.nonterminal (), symbol.terminal (f true)] }, { input_L := [], input_N := (), input_R := [], output_string := [] }] } [symbol.nonterminal ()] w → ∃ n : ℕ, w = List.replicate n (symbol.terminal (f false)) ++ [symbol.nonterminal ()] ++ List.replicate n (symbol.terminal (f true)) ∨ w = List.map symbol.terminal (List.replicate n (f false) ++ List.replicate n (f true)) := by intro w hw induction' hw with w' hw' ih; · exact ⟨ 0, by simp +decide ⟩; · rename_i h₁ h₂ h₃; rcases h₃ with ⟨ n, rfl | rfl ⟩ <;> simp_all +decide [ grammar_transforms ]; · rcases h₂ with ( ⟨ u, v, h₁, rfl ⟩ | ⟨ u, v, h₁, rfl ⟩ ) <;> simp_all +decide [ List.append_eq_append_iff ]; · rcases h₁ with ( ⟨ as, rfl, h₁ ⟩ | ⟨ bs, h₁, h₂ ⟩ ) <;> simp_all +decide [ List.append_eq_append_iff ]; · rcases as with ( _ | ⟨ a, as ⟩ ) <;> simp_all +decide; · use n + 1; simp +decide [ List.replicate_add, h₁.symm ]; exact Or.inl ( by exact Nat.recOn n ( by simp +decide ) fun n ihn => by simp +decide [ List.replicate ] at ihn ⊢; aesop ); · replace h₁ := congr_arg List.toFinset h₁.2; rw [ Finset.ext_iff ] at h₁; specialize h₁ ( symbol.nonterminal () ) ; aesop; · rcases bs with ( _ | ⟨ b, bs ⟩ ) <;> simp_all +decide; · use n + 1; simp +decide [ ← h₁, List.replicate_add ]; exact Or.inl ( by exact Nat.recOn n ( by simp +decide ) fun n ihn => by simp +decide [ List.replicate ] at ihn ⊢; aesop ); · no_nonterminal (b) at h₁ · rcases h₁ with ( ⟨ as, rfl, h₁ ⟩ | ⟨ bs, h₁, h₂ ⟩ ) <;> simp_all +decide [ List.append_eq_append_iff ]; · rcases as with ( _ | ⟨ a, as ⟩ ) <;> simp_all +decide; · exact ⟨ n, Or.inr <| Or.inr <| ⟨ [ ], by aesop ⟩ ⟩; · replace h₁ := congr_arg List.toFinset h₁.2; rw [ Finset.ext_iff ] at h₁; specialize h₁ ( symbol.nonterminal () ) ; aesop; · rcases bs with ( _ | ⟨ b, bs ⟩ ) <;> simp_all +decide [ List.append_eq_append_iff ]; · exact ⟨ n, Or.inr <| Or.inl ⟨ [ ], by aesop ⟩ ⟩; · no_nonterminal (b) at h₁ · rcases h₂ with ( ⟨ u, v, h₁, rfl ⟩ | ⟨ u, v, h₁, rfl ⟩ ) <;> simp_all +decide; · no_nonterminal (symbol.nonterminal ()) · no_nonterminal (symbol.nonterminal ()) obtain ⟨ n, hn ⟩ := h_deriv _ hw; rcases hn with ( hn | hn ); · no_nonterminal (symbol.nonterminal ()) · use List.replicate n false ++ List.replicate n true; exact ⟨ ⟨ n, rfl ⟩, by simpa using List.map_injective_iff.mpr ( show Function.Injective ( fun x : T => symbol.terminal x ) from fun x y hxy => by simpa using hxy ) hn.symm ⟩; · rintro ⟨ v, ⟨ n, rfl ⟩, rfl ⟩; have h_derives : grammar_derives { nt := Unit, initial := (), rules := [{ input_L := [], input_N := (), input_R := [], output_string := [symbol.terminal (f false), symbol.nonterminal (), symbol.terminal (f true)] }, { input_L := [], input_N := (), input_R := [], output_string := [] }] } [symbol.nonterminal ()] (List.replicate n (symbol.terminal (f false)) ++ [symbol.nonterminal ()] ++ List.replicate n (symbol.terminal (f true))) := by induction' n with n ih; · constructor; · have h_step : grammar_transforms { nt := Unit, initial := (), rules := [{ input_L := [], input_N := (), input_R := [], output_string := [symbol.terminal (f false), symbol.nonterminal (), symbol.terminal (f true)] }, { input_L := [], input_N := (), input_R := [], output_string := [] }] } (replicate n (symbol.terminal (f false)) ++ [symbol.nonterminal ()] ++ replicate n (symbol.terminal (f true))) (replicate n (symbol.terminal (f false)) ++ [symbol.terminal (f false), symbol.nonterminal (), symbol.terminal (f true)] ++ replicate n (symbol.terminal (f true))) := by use ⟨ [], (), [], [ symbol.terminal ( f false ), symbol.nonterminal (), symbol.terminal ( f true ) ] ⟩; exact ⟨ by simp +decide, replicate n ( symbol.terminal ( f false ) ), replicate n ( symbol.terminal ( f true ) ), by simp +decide, by simp +decide ⟩; convert ih.tail h_step using 1 ; simp +decide [ List.replicate_add ]; exact Nat.recOn n rfl fun n ih => by rw [ replicate_succ' ] ; aesop; convert h_derives.tail _; use ⟨ [ ], (), [ ], [ ] ⟩ ; aesop /-- Right-regular languages form a strict subclass of linear languages over any nontrivial alphabet. -/ theorem RG_strict_subclass_Linear [Nontrivial T] : (RG : Set (Language T)) ⊂ (Linear : Set (Language T)) := by refine ⟨RG_subclass_Linear, ?_⟩ intro hLinearsubsetRG obtain ⟨a, b, hab⟩ := exists_pair_ne T let f : Bool → T := fun x => if x then b else a have hf : Function.Injective f := by intro x y hxy cases x <;> cases y <;> try rfl · simp [f] at hxy; exact False.elim (hab hxy) · simp [f] at hxy; exact False.elim (hab hxy.symm) have hLinear : Language.map f anbn ∈ (Linear : Set (Language T)) := map_anbn_is_Linear f hf have hRG : Language.map f anbn ∈ (RG : Set (Language T)) := hLinearsubsetRG hLinear have hreg : (Language.map f anbn).IsRegular := isRegular_of_is_RG hRG exact anbn_not_isRegular (Language.IsRegular.of_map_injective hf hreg) end