Scratchwork for 4.1 (i) => (ii)

Author: jefrai

TraceTheory/TraceTheory/Lemmas.lean

@@ -63,16 +63,16 @@ lemma traceFlatten_append {u : Trace I} (L : List (Trace I)) : traceFlatten (u :
   simp
 
 
-def dependencyIn (s : List α) (a b : {a : α // a ∈ s}) := (inducedDependence I).rel a b
+def dependencyIn (s : List α) (a b : α) := (inducedDependence I).rel a b ∧ a ∈ s ∧ b ∈ s
 
-def dependencyTransClosureIn (s : List α) (a b : {a : α // a ∈ s}) := Relation.TransGen (@dependencyIn α I s) a b
+def dependencyTransClosureIn (s : List α) (a b : α) := Relation.TransGen (@dependencyIn α I s) a b
 
 def isConnected (s : List α) := ∀ a b : {a : α // a ∈ s}, @dependencyTransClosureIn α I s a b
 
 
-def dependencyInT (t : Trace I) (a b : {a : α // a ∈ t}) := (inducedDependence I).rel a b
+def dependencyInT (t : Trace I) (a b : α) := (inducedDependence I).rel a b ∧ a ∈ t ∧ b ∈ t
 
-def dependencyTransClosureInT (t : Trace I) (a b : {a : α // a ∈ t}) := Relation.TransGen (dependencyInT t) a b
+def dependencyTransClosureInT (t : Trace I) (a b : α) := Relation.TransGen (dependencyInT t) a b
 
 def isConnectedT (t : Trace I) := ∀ a b : {a : α // a ∈ t}, dependencyTransClosureInT t a b
 
@@ -149,32 +149,31 @@ lemma kstar_toTrace_commutes (L : Language α) : @toTrace α I (KStar.kstar L) =
         rfl
 
 lemma append_indep_is_disconnected_chars (u v : Trace I) (huv : IndependentT u v)
-    (a b : { a // a ∈ u * v }) (ha : a.1 ∈ u) (hb : b.1 ∈ v) :
+    (a b : α) (ha : a ∈ u) (hb : b ∈ v) :
     ¬ (dependencyTransClosureInT (u * v)) a b := by
   intro h
   induction h with
   | single h =>
     rename_i b
-    apply h
-    exact huv a b ha hb
+    have hab := huv a b ha hb
+    exact h.1 hab
   | tail h h_tail ih =>
     rename_i b c
     simp at ih
-    have hbu : b.1 ∈ u :=  by
-      have hb_uv := mem_append.mp b.2
+    have hbu : b ∈ u := by
+      have hb_uv := mem_append.mp h_tail.2.1
       simp [ih] at hb_uv
       exact hb_uv
-    simp [dependencyInT, inducedDependence] at h_tail
-    unfold IndependentT at huv
-    exact h_tail (huv b c hbu hb)
+    have hbc := huv b c hbu hb
+    exact h_tail.1 hbc
 
 lemma append_indep_is_disconnected (u v : Trace I) (h : IndependentT u v) (hu : u ≠ ⟦[]⟧) (hv : v ≠ ⟦[]⟧) :
     ¬isConnectedT (u * v) := by
   by_contra h_con
   have ⟨a, ha⟩ := empty_is_eps u hu
   have ⟨b, hb⟩ := empty_is_eps v hv
   have h_ab_con := h_con ⟨a, mem_append.mpr (Or.inl ha)⟩ ⟨b, mem_append.mpr (Or.inr hb)⟩
-  have h_ab_dis := append_indep_is_disconnected_chars u v h ⟨a, mem_append.mpr (Or.inl ha)⟩ ⟨b, mem_append.mpr (Or.inr hb)⟩ ha hb
+  have h_ab_dis := append_indep_is_disconnected_chars u v h a b ha hb
   exact h_ab_dis h_ab_con
 
 lemma connectedComponents_of_connected (T : Set (Trace I)) (h : ∀ t ∈ T, isConnectedT t) :

TraceTheory/TraceTheory/Ochmanski.lean

@@ -1,3 +1,4 @@
+import TraceTheory.Language
 import TraceTheory.Lemmas
 import TraceTheory.MyhillNerode
 import TraceTheory.RegularExpressions
@@ -173,4 +174,210 @@ theorem starConnected_is_cRational (X : RegularExpression α) (h : RegularExpres
     rw [kstar_eq_minusEps_trace]
 
 
+
+lemma depTrClIn_refl {w : List α} {a : α} (h : a ∈ w) : @dependencyTransClosureIn α I w a a := by
+  unfold dependencyTransClosureIn dependencyIn
+  apply Relation.TransGen.single
+  simp [Dependence.refl, h]
+
+noncomputable instance : ∀ w x y, Decidable (@dependencyTransClosureIn α I w x y) :=
+  fun w x y => Classical.propDecidable (dependencyTransClosureIn w x y)
+
+noncomputable def sep_aux (w₀ w : List α) (p : α) : List (List α × List α) :=
+  match w with
+  | [] => [⟨[], []⟩]
+  | a :: w =>
+    match sep_aux w₀ w p with
+    | [] => [] -- dummy value, unreachable by construction
+    | v :: vs =>
+      if @dependencyTransClosureIn α I w₀ a p
+        then match v.2 with
+        | [] => ⟨a :: v.1, v.2⟩ :: vs
+        | _ :: _ => ⟨[a], []⟩ :: v :: vs
+        else ⟨v.1, a :: v.2⟩ :: vs
+
+noncomputable def sep (w : List α) (p : α) : List (List α × List α) := @sep_aux α I w w p
+
+lemma sep_aux_nonempty (w₀ w : List α) (p : α) : (@sep_aux α I w₀ w p) ≠ [] := by
+  induction w with
+  | nil => simp [sep_aux]
+  | cons a u ih =>
+    simp [sep_aux]
+    cases hs : sep_aux w₀ u p
+    · simp [hs] at ih
+    · simp
+      by_cases ha : @dependencyTransClosureIn α I w₀ a p
+      · rename_i s_head s_tail
+        cases s_head.2
+        all_goals simp [ha]
+      · simp [ha]
+
+lemma sep_aux_zero_idx {w₀ w : List α} {p : α} : 0 < (@sep_aux α I w₀ w p).length := List.length_pos_iff.mpr (sep_aux_nonempty _ _ _)
+
+lemma sep_nonempty (w : List α) (p : α) : (@sep α I w p) ≠ [] := sep_aux_nonempty w w p
+
+lemma sep_invar (u w : List α) (a p : α) (i : Fin (@sep_aux α I (u ++ [p]) (w ++ [p]) p).length) :
+    (@sep_aux α I (u ++ [p]) (a :: w ++ [p]) p)[i] = (@sep_aux α I (u ++ [p]) (w ++ [p]) p)[i] ∨
+    (@sep_aux α I (u ++ [p]) (a :: w ++ [p]) p)[i] = (@sep_aux α I (u ++ [p]) (w ++ [p]) p)[i]
+  := by
+  simp [sep_aux]
+
+lemma sep_aux_1_nonempty_head (u w : List α) (p : α) (h : w ≠ []) :
+    ((@sep_aux α I (u ++ [p]) (w ++ [p]) p)[0]'(sep_aux_zero_idx)).1 ≠ [] := by
+  induction w with
+  | nil => simp at h
+  | cons a w ih =>
+    clear h
+    by_cases hw : w = []
+    · simp [hw, sep_aux, depTrClIn_refl]
+      by_cases hau : @dependencyTransClosureIn α I (u ++ [p]) a p
+      all_goals simp [hau]
+    · simp [hw] at ih
+      let t := @sep_aux α I (u ++ [p]) (w ++ [p]) p
+      have ht : @sep_aux α I (u ++ [p]) (w ++ [p]) p = t := rfl
+      rcases t
+      · exfalso
+        exact sep_aux_nonempty _ _ _ ht
+      · rename_i s_head s_tail
+        by_cases hau : @dependencyTransClosureIn α I (u ++ [p]) a p
+        · suffices hs_dec : ∃ _1 _2 _3 _4, (@sep_aux α I (u ++ [p]) (a :: w ++ [p]) p) = (_1 ::_2, _3) :: _4 from by
+            replace ⟨_1, _2, _3, _4, hs_dec⟩ := hs_dec
+            rw [List.getElem_of_eq hs_dec]
+            simp
+          simp [sep_aux, ht, hau]
+          cases s_head.2
+          · simp
+          · simp
+        · simp [sep_aux, ht, hau]
+          have hs_dec : (@sep_aux α I (u ++ [p]) (w ++ [p]) p)[0]'(sep_aux_zero_idx) = (s_head :: s_tail)[0] := List.getElem_of_eq ht _
+          simp [hs_dec] at ih
+          exact ih
+
+lemma sep_aux_1_nonempty (u w : List α) (p : α) (i : Fin (@sep_aux α I (u ++ [p]) (w ++ [p]) p).length) (h : w ≠ []) :
+    (@sep_aux α I (u ++ [p]) (w ++ [p]) p)[i].1 ≠ [] := by
+  induction w with
+  | nil => simp at h
+  | cons a w ih =>
+    clear h
+    by_cases hw : w = []
+    · rcases i with ⟨i, hi⟩
+      simp [hw, sep_aux, depTrClIn_refl]
+      by_cases hau : @dependencyTransClosureIn α I (u ++ [p]) a p
+      all_goals simp [hau]
+    · simp [hw] at ih
+      rcases i with ⟨i, hi⟩
+      cases i with
+      | zero => exact sep_aux_1_nonempty_head _ _ _ (by simp)
+      | succ i =>
+        by_cases hau : @dependencyTransClosureIn α I (u ++ [p]) a p
+        · let temp := @sep_aux α I (u ++ [p]) (w ++ [p]) p
+          have htemp : @sep_aux α I (u ++ [p]) (w ++ [p]) p = temp := rfl
+          rcases temp
+          · exfalso
+            exact sep_aux_nonempty _ _ _ htemp
+          · rename_i s_head s_tail
+            suffices hs_dec : (∃ _1 _2, (@sep_aux α I (u ++ [p]) (a :: w ++ [p]) p) = _1 :: _2) from by
+              replace ⟨_1, _2, hs_dec⟩ := hs_dec
+              have h_2ne : (_2[i]'(by rw [hs_dec] at hi; exact Nat.succ_lt_succ_iff.mp hi)).1 ≠ [] := by
+                simp [sep_aux, htemp, hau] at hs_dec
+                contrapose hs_dec
+                cases s_head.2
+                · simp
+                  intro _
+                  contrapose hs_dec
+                  rw [<- List.getElem_of_eq hs_dec]
+                · simp
+                  intro _
+                  contrapose hs_dec
+                  rw [<- List.getElem_of_eq hs_dec, <- List.getElem_of_eq htemp]
+                  · exact ih ⟨i, by sorry⟩
+                  · rw [<- htemp]
+                    sorry
+              rw [Fin.getElem_fin]
+              rw [List.getElem_of_eq hs_dec]
+              simp [h_2ne]
+            simp [sep_aux, htemp, hau]
+            cases s_head.2
+            · simp
+            · simp
+        · suffices hs_dec : (∃ _1 _2, (@sep_aux α I (u ++ [p]) (a :: w ++ [p]) p) = _1 :: _2) from by
+            replace ⟨_1, _2, hs_dec⟩ := hs_dec
+            have h_2ne : (_2[i]'(by rw [hs_dec] at hi; exact Nat.succ_lt_succ_iff.mp hi)).1 ≠ [] := by
+              sorry
+            rw [Fin.getElem_fin]
+            rw [List.getElem_of_eq hs_dec]
+            simp [h_2ne]
+          simp [sep_aux, hau]
+          let temp := @sep_aux α I (u ++ [p]) (w ++ [p]) p
+          have htemp : @sep_aux α I (u ++ [p]) (w ++ [p]) p = temp := rfl
+          rcases temp
+          · exfalso
+            exact sep_aux_nonempty _ _ _ htemp
+          · simp [htemp]
+
+lemma sep_aux_2_nonempty (u w : List α) (p : α) (i : Fin (@sep_aux α I (u ++ [p]) (w ++ [p]) p).length) (h : w ≠ []) (hi : i.1 > 0) :
+    (@sep_aux α I (u ++ [p]) (w ++ [p]) p)[i].2 ≠ [] := by sorry
+
+
+
+def proj2 (S : Set α) (hd : ∀ x, Decidable (x ∈ S)) (w : List α) : List α := w.filter (· ∈ S)
+
+lemma proj2_prop {S : Set α} {hd : ∀ x, Decidable (x ∈ S)} {w : List α} {a : α} : a ∈ proj2 S hd w → a ∈ S := by
+  induction w with
+  | nil => simp [proj2]
+  | cons b u ih =>
+    intro h
+    by_cases hab : a = b
+    · simp [proj2, <- hab] at h
+      exact h
+    · simp [proj2] at h
+      exact h.2
+
+variable [LinearOrder α] in
+theorem lexNf_dup_lexNf_isConnected {w : List α} (h : IsLexNf I (w ++ w)) : @isConnected α I w := by
+  have h' : IsLexNf I w := by
+    contrapose h
+    simp [IsLexNf] at h ⊢
+    rcases h with ⟨u, h⟩
+    use w ++ u
+    exact ⟨TraceEqv.compat (TraceEqv.refl w) h.1, List.append_left_lt h.right⟩
+
+  by_contra h_con
+  simp [isConnected] at h_con
+  choose a ha b hb h_con using h_con
+  let A := {x | @dependencyTransClosureIn α I w a x}
+  let B := {x | ¬ @dependencyTransClosureIn α I w a x}
+  have hA_dec : ∀ x, Decidable (x ∈ A) := fun x => Classical.propDecidable (x ∈ A)
+  have hB_dec : ∀ x, Decidable (x ∈ B) := fun x => Classical.propDecidable (x ∈ B)
+  let u := proj2 A hA_dec w
+  let v := proj2 B hB_dec w
+  have : Independent I u v := by
+    intro j hj k hk
+    have hjw : j ∈ w := List.mem_of_mem_filter hj
+    have hkw : k ∈ w := List.mem_of_mem_filter hk
+    unfold u at hj
+    unfold v at hk
+    replace hj := proj2_prop hj
+    replace hk := proj2_prop hk
+    replace hj : @dependencyTransClosureIn α I w a j := hj
+    replace hk : ¬@dependencyTransClosureIn α I w a k := hk
+    by_contra hjk
+
+    have : @dependencyTransClosureInCoe α I w a k := by
+      rcases hj with ⟨ha', hjw', hj⟩
+      have : @dependencyIn α I w ⟨j, hjw'⟩ ⟨k, hkw⟩ := hjk ∘ fun a => a
+      use ha', hkw
+      unfold dependencyTransClosureIn at hj ⊢
+      exact Relation.TransGen.tail hj this
+
+    exact hk this
+
+  have : a ∈ u := by
+    have ha_A : a ∈ A := ⟨ha, ha, Relation.TransGen.single ((inducedDependence I).refl a)⟩
+    exact List.mem_filter_of_mem ha (decide_eq_true ha_A)
+  have : b ∈ v := by
+    have hb_B : b ∈ B := by simp [B, dependencyTransClosureInCoe, h_con]
+    exact List.mem_filter_of_mem hb (decide_eq_true hb_B)
+
+
 end TraceTheory