Progress Ochmanski's Theorem

Author: yisiox

TraceTheory/TraceTheory/Language.lean

@@ -1,4 +1,4 @@
-import Mathlib.Algebra.BigOperators.Group.Finset.Defs
+import Mathlib.Algebra.BigOperators.Group.Finset.Basic
 import Mathlib.Computability.DFA
 import Mathlib.Computability.Language
 import TraceTheory.Basic
@@ -171,6 +171,125 @@ theorem isRegular_lexNf : Language.IsRegular (LexNfLanguage I) := by
   apply Language.IsRegular.compl
   apply isRegular_allForbiddenPatterns
 
+omit [LinearOrder α] [Fintype α] in
+lemma mem_sigma (x : List α) : x ∈ (Sigma : Language α)∗ := by
+  rw [Language.mem_kstar]
+  use [x]
+  simp only [List.flatten_cons, List.flatten_nil, List.append_nil, List.mem_cons,
+    List.not_mem_nil, or_false, Sigma, forall_eq, true_and]
+  apply Set.mem_univ
+
+omit [Fintype α] [LinearOrder α] in
+lemma mem_sum_language
+    {ι : Type*} [DecidableEq ι] {S : Finset ι} {f : ι → Language α} {x : List α} :
+    x ∈ ∑ i ∈ S, f i ↔ ∃ i ∈ S, x ∈ f i := by
+  induction S using Finset.induction_on with
+  | empty => simp
+  | insert i S hi ih =>
+    simp only [Finset.sum_insert hi, Language.mem_add]
+    rw [ih]
+    constructor
+    · rintro (hx | ⟨j, hj, hxj⟩)
+      · exact ⟨i, Finset.mem_insert_self i S, hx⟩
+      · exact ⟨j, Finset.mem_insert_of_mem hj, hxj⟩
+    · rintro ⟨j, hj, hxj⟩
+      simp only [Finset.mem_insert] at hj
+      rcases hj with (rfl | hj)
+      · left
+        exact hxj
+      · right
+        exact ⟨j, hj, hxj⟩
+
+lemma mem_forbiddenPattern_iff {x : List α} {a b : α} :
+    x ∈ ForbiddenPattern I a b ↔
+    ∃ y u z : List α, x = y ++ [b] ++ u ++ [a] ++ z ∧ (∀ c ∈ u, I.rel a c) := by
+  unfold ForbiddenPattern IndependentLetters
+  constructor
+  · intro h
+    simp [Language.mem_mul] at h
+    rcases h with ⟨a1, b1, b2, b3, ⟨⟨ha1, hb1, hb2⟩, hb3⟩, ⟨x, hx, rfl⟩⟩
+    use a1, b2, x
+    constructor
+    · simp only [Letter] at hb3 hb1
+      rw [Set.mem_singleton_iff] at hb3 hb1
+      subst hb3 hb1
+      simp
+    · intro c hc
+      rw [Language.mem_kstar] at hb2
+      rcases hb2 with ⟨L, rfl, hL⟩
+      unfold Letter at hL
+      simp only [List.mem_flatten] at hc
+      rcases hc with ⟨y, hy, hcy⟩
+      have hy_indep := hL y hy
+      rw [mem_sum_language] at hy_indep
+      simp only [Finset.mem_filter, Finset.mem_univ, true_and] at hy_indep
+      rcases hy_indep with ⟨c', hc'_rel, hc'_eq⟩
+      rw [Set.mem_singleton_iff] at hc'_eq
+      subst hc'_eq
+      simp only [List.mem_singleton] at hcy
+      subst hcy
+      exact hc'_rel
+  · intro h
+    rcases h with ⟨y, u, z, rfl, h_indep⟩
+    simp [Language.mem_mul]
+    use y, [b], u, [a]
+    unfold Letter
+    and_intros
+    · apply mem_sigma
+    · rfl
+    · rw [Language.mem_kstar]
+      use u.map (fun c => [c])
+      constructor
+      · induction u with
+        | nil => rfl
+        | cons hd tl ih =>
+          simp only [List.map_cons, List.flatten_cons, List.cons_append, List.nil_append,
+            List.cons.injEq, true_and]
+          simp only [List.mem_cons, forall_eq_or_imp] at h_indep
+          rw [← ih h_indep.right]
+      · intro y hy
+        simp only [List.mem_map] at hy
+        rcases hy with ⟨c, hc, rfl⟩
+        rw [mem_sum_language]
+        simp only [Finset.mem_filter, Finset.mem_univ, true_and]
+        use c, h_indep c hc
+        rfl
+    · rfl
+    · use z
+      constructor
+      · apply mem_sigma
+      · simp
+
+lemma mem_allForbiddenPatterns_iff {x : List α} :
+    x ∈ AllForbiddenPatterns I ↔
+    ∃ a b, a < b ∧ I.rel a b ∧ x ∈ ForbiddenPattern I a b := by
+  unfold AllForbiddenPatterns
+  rw [mem_sum_language]
+  simp only [Finset.mem_filter, Finset.mem_univ, true_and, Prod.exists, and_assoc]
+
+/-- The language LexNfLanguage contains exactly the strings satisfying the factor condition. -/
+theorem mem_lexNfLanguage_iff_factorCondition (x : List α) :
+    x ∈ LexNfLanguage I ↔ SatisfiesFactorCondition I x := by
+  unfold LexNfLanguage SatisfiesFactorCondition
+  rw [Set.mem_compl_iff, mem_allForbiddenPatterns_iff]
+  push_neg
+  constructor
+  · intro h y u z a b hx h_indep hlt
+    by_contra h_all_indep
+    push_neg at h_all_indep
+    have h_in_pattern : x ∈ ForbiddenPattern I a b := by
+      rw [mem_forbiddenPattern_iff]
+      exact ⟨y, u, z, hx, h_all_indep⟩
+    exact h a b hlt h_indep h_in_pattern
+  · intro h a b hlt h_indep h_in_pattern
+    rw [mem_forbiddenPattern_iff] at h_in_pattern
+    rcases h_in_pattern with ⟨y, u, z, hx, h_all_indep⟩
+    rcases h y u z a b hx h_indep hlt with ⟨c, hc_mem, hc_not_indep⟩
+    exact hc_not_indep (h_all_indep c hc_mem)
+
+theorem exists_lexNf_rep (t : Trace I) : ∃ s : List α, ⟦s⟧ = t ∧ s ∈ LexNfLanguage I := by
+  sorry
+
 end LexNf
 
 section rank

TraceTheory/TraceTheory/Ochmanski.lean

@@ -1,12 +1,16 @@
+import Mathlib.Algebra.Group.PUnit
+import TraceTheory.Language
 import TraceTheory.Lemmas
 import TraceTheory.MyhillNerode
 import TraceTheory.RegularExpressions
 
 namespace TraceTheory
 
+open scoped Pointwise
+
 open RegularExpression
 
-variable {α : Type*} {I : Independence α}
+variable {α : Type} {I : Independence α}
 
 /-- Main component of Theorem 4.1 (ii) => (iii).
 
@@ -120,4 +124,176 @@ theorem cRational_of_isStarConnected (X : RegularExpression α) (h : IsStarConne
     rw [connectedComponents_of_connected _ hP_conn]
     rw [kstar_eq_minusEps_trace]
 
+lemma recognizable_zero : IsRecognizable (∅ : Set (Trace I)) :=
+  ⟨PUnit, inferInstance, inferInstance, inferInstance, 1, by simp⟩
+
+lemma recognizable_epsilon : IsRecognizable ({ 1 } : Set (Trace I)) := by
+  sorry
+
+lemma recognizable_char (a : α) : IsRecognizable ({ ⟦[a]⟧ } : Set (Trace I)) := by
+  sorry
+
+lemma recognizable_union {M : Type} [Monoid M] {P Q : Set M}
+    (hP : IsRecognizable P) (hQ : IsRecognizable Q) : IsRecognizable (P ∪ Q) := by
+  sorry
+
+lemma recognizable_mul {P Q : Set (Trace I)}
+    (hP : IsRecognizable P) (hQ : IsRecognizable Q) : IsRecognizable (P * Q) := by
+  sorry
+
+lemma recognizable_cstar {P : Set (Trace I)}
+    (hP : IsRecognizable P) : IsRecognizable (kstar (connectedComponents P)) := by
+  sorry
+
+/-- Theorem 4.1 (iv) => (i) -/
+theorem recognizable_of_cRational (X : RegularExpression α) :
+    IsRecognizable (matches_cstar_trace I X) := by
+  induction X with
+  | zero => exact recognizable_zero
+  | epsilon => exact recognizable_epsilon
+  | char a => exact recognizable_char a
+  | plus P Q ihP ihQ => exact recognizable_union ihP ihQ
+  | comp P Q ihP ihQ => exact recognizable_mul ihP ihQ
+  | star P ih => exact recognizable_cstar ih
+
+variable [Fintype α] [LinearOrder α] [DecidableRel I.rel]
+
+lemma connected_of_lexNf_sq {w : List α}
+    (hw : w ∈ LexNfLanguage I)
+    (hww : w ++ w ∈ LexNfLanguage I) :
+    IsConnected I ⟦w⟧ := by
+  sorry
+
+omit [Fintype α] [LinearOrder α] in
+lemma mem_sigma (x : List α) : x ∈ KStar.kstar (Sigma : Language α) := by
+  rw [Language.mem_kstar]
+  use [x]
+  simp only [List.flatten_cons, List.flatten_nil, List.append_nil, List.mem_cons,
+    List.not_mem_nil, or_false, Sigma, forall_eq, true_and]
+  apply Set.mem_univ
+
+omit [LinearOrder α] in
+lemma forbidden_of_subword {u w v : List α} {a b : α}
+    (hw : w ∈ ForbiddenPattern I a b) :
+    u ++ w ++ v ∈ ForbiddenPattern I a b := by
+  unfold ForbiddenPattern at *
+  simp [Language.mem_mul] at hw
+  rcases hw with ⟨a1, b1, b2, b3, ⟨⟨ha1, hb1, hb2⟩, hb3⟩, ⟨x, hx, rfl⟩⟩
+  simp [Language.mem_mul]
+  use u ++ a1, b1, b2, b3
+  and_intros
+  · apply mem_sigma
+  · exact hb1
+  · exact hb2
+  · exact hb3
+  · use x ++ v
+    simp [mem_sigma]
+
+lemma sum_forbidden_of_subword {S : Finset (α × α)} {u w v : List α}
+    (hw : w ∈ ∑ p ∈ S, ForbiddenPattern I p.1 p.2) :
+    u ++ w ++ v ∈ ∑ p ∈ S, ForbiddenPattern I p.1 p.2 := by
+  induction S using Finset.induction_on generalizing w with
+  | empty =>
+    simp only [Finset.sum_empty] at hw
+    contradiction
+  | insert p' S' hp ih =>
+    rw [Finset.sum_insert hp] at hw ⊢
+    cases hw with
+    | inl h_left =>
+      left
+      exact forbidden_of_subword h_left
+    | inr h_right =>
+      right
+      exact ih h_right
+
+lemma lexNf_of_subword {u w v : List α} (h : u ++ w ++ v ∈ LexNfLanguage I) :
+    w ∈ LexNfLanguage I := by
+  unfold LexNfLanguage at h ⊢
+  rw [Set.mem_compl_iff] at h ⊢
+  unfold AllForbiddenPatterns at h ⊢
+  contrapose! h
+  exact sum_forbidden_of_subword h
+
+lemma connected_iterativeFactor_of_subset_lexNf {X : Language α}
+    (hX : X ≤ LexNfLanguage I) {w : List α}
+    (hw : IsIterativeFactor X w) :
+    IsConnected I ⟦w⟧ := by
+  rcases hw with ⟨u, v, hw⟩
+  have h_lex1 : u ++ w ++ v ∈ LexNfLanguage I := hX (hw 1)
+  have h_lex2 : u ++ (w ++ w) ++ v ∈ LexNfLanguage I := hX (hw 2)
+  have h_w_lex : w ∈ LexNfLanguage I := lexNf_of_subword h_lex1
+  have h_ww_lex : w ++ w ∈ LexNfLanguage I := lexNf_of_subword h_lex2
+  exact connected_of_lexNf_sq h_w_lex h_ww_lex
+
+omit [Fintype α] [LinearOrder α] in
+lemma isRegular_of_recognizable {L : Language α} (h : IsRecognizable L) :
+    L.IsRegular := by
+  rcases recognizable_is_recognizableDFMA L h with ⟨σ, h_fin, h_decide, M, hM⟩
+  rw [Language.isRegular_iff]
+  let M_DFA : DFA α σ := {
+    step := fun q a => M.step q [a]
+    start := M.start
+    accept := M.accept
+  }
+  use σ, h_fin, M_DFA
+  rw [hM]
+  ext w
+  simp [DFA.accepts, DFA.acceptsFrom, DFA.evalFrom]
+  unfold DFMA.accepts DFMA.eval
+  rw [Set.mem_setOf, Set.mem_setOf]
+  have h_eval : ∀ q, List.foldl M_DFA.step q w = M.step q w := by
+    induction w with
+    | nil =>
+      intro q
+      simp only [List.foldl_nil]
+      exact (M.idempotent q).symm
+    | cons a ws ih =>
+      intro q
+      simp only [List.foldl_cons]
+      rw [ih (M.step q [a])]
+      exact (M.composition q [a] ws)
+  rw [h_eval M_DFA.start]
+
+/-- Theorem 4.1 (i) => (ii) -/
+theorem connectedIterativeFactors_of_recognizable {T : Set (Trace I)}
+    (hT : IsRecognizable T) :
+    ∃ X : RegularExpression α,
+      (∀ s, IsIterativeFactor X.matches' s → IsConnected I ⟦s⟧) ∧
+      toTrace I X.matches' = T := by
+  let L : Language α := (mk' (I := I) ⁻¹' T) ⊓ LexNfLanguage I
+  have hL_reg : L.IsRegular := by
+    apply Language.IsRegular.inf
+    · apply isRegular_of_recognizable
+      apply recognizable_has_recognizablePreImage
+      exact hT
+    · apply isRegular_lexNf
+  have ⟨R, hR_matches⟩ : ∃ R : RegularExpression α, R.matches' = L := by
+    classical
+    have ⟨σ, h_fin, M, hL⟩ : ∃ (σ : Type) (_ : Fintype σ) (M : DFA α σ), M.accepts = L :=
+      Language.isRegular_iff.mp hL_reg
+    haveI : FinEnum σ := FinEnum.ofEquiv (Fin (Fintype.card σ)) (Fintype.equivFin σ)
+    use M.toNFA.toεNFA.toRegex
+    rw [← hL, εNFA.accepts_toRegex, NFA.toεNFA_correct, DFA.toNFA_correct]
+  use R
+  constructor
+  · intro s hs
+    have h_subset : R.matches' ≤ LexNfLanguage I := by
+      simp_all only [inf_le_right, L]
+    exact connected_iterativeFactor_of_subset_lexNf h_subset hs
+  · rw [hR_matches]
+    ext t
+    constructor
+    · rintro ⟨s, hs, rfl⟩
+      exact hs.left
+    · intro ht
+      rcases exists_lexNf_rep I t with ⟨s, hs_eq, hs_lex⟩
+      refine ⟨s, ?_, hs_eq⟩
+      unfold L
+      change s ∈ ⇑mk' ⁻¹' T ∩ LexNfLanguage I
+      constructor
+      · rw [Set.mem_preimage]
+        subst hs_eq
+        exact ht
+      · exact hs_lex
+
 end TraceTheory