Fix Ochmanski for refactor

Author: jefrai

TraceTheory/TraceTheory/Basic.lean

@@ -287,8 +287,7 @@ theorem indep_of_comm_singleton {u v w : List α} {a : α} [DecidableEq α]
     (h : TraceEqv I (u ++ [a] ++ v) (w ++ [a])) (h_mem : a ∉ v) :
     Independent I [a] v := by
   induction v using reverseRecOn generalizing w with
-  | nil =>
-    simp
+  | nil => simp
   | append_singleton x b ih =>
     intro a' ha' b' hb'
     simp at ha' hb' h_mem
@@ -308,8 +307,7 @@ theorem indep_of_comm_singleton {u v w : List α} {a : α} [DecidableEq α]
 theorem comm_singleton_of_indep {w : List α} {a : α} (h : Independent I [a] w) :
     TraceEqv I (w ++ [a]) ([a] ++ w) := by
   induction w using reverseRecOn with
-  | nil =>
-    apply TraceEqv.refl
+  | nil => apply TraceEqv.refl
   | append_singleton w' b ih =>
     simp at h
     have haw' : Independent I [a] w' := by

TraceTheory/TraceTheory/Lemmas.lean

@@ -63,25 +63,25 @@ 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 : {a : α // a ∈ s}) := (inducedDependence I).rel a b
 
-def dependencyTransClosureIn' (s : List α) (a b : {a : α // a ∈ s}) := Relation.TransGen (@dependencyIn' α I s) a b
+def dependencyTransClosureIn (s : List α) (a b : {a : α // a ∈ s}) := Relation.TransGen (@dependencyIn α I s) a b
 
-def isConnected' (s : List α) := ∀ a b : {a : α // a ∈ s}, @dependencyTransClosureIn' α I s a b
+def isConnected (s : List α) := ∀ a b : {a : α // a ∈ s}, @dependencyTransClosureIn α I s a b
 
 
-def dependencyIn (t : Trace I) (a b : {a : α // a ∈ t}) := (inducedDependence I).rel a b
+def dependencyInT (t : Trace I) (a b : {a : α // a ∈ t}) := (inducedDependence I).rel a b
 
-def dependencyTransClosureIn (t : Trace I) (a b : {a : α // a ∈ t}) := Relation.TransGen (dependencyIn t) a b
+def dependencyTransClosureInT (t : Trace I) (a b : {a : α // a ∈ t}) := Relation.TransGen (dependencyInT t) a b
 
-def isConnected (t : Trace I) := ∀ a b : {a : α // a ∈ t}, dependencyTransClosureIn t a b
+def isConnectedT (t : Trace I) := ∀ a b : {a : α // a ∈ t}, dependencyTransClosureInT t a b
 
 
-lemma dependencyIn_toTrace (s : List α) : @dependencyIn' α I s = @dependencyIn α I ⟦s⟧ := rfl
+lemma dependencyIn_toTrace (s : List α) : @dependencyIn α I s = @dependencyInT α I ⟦s⟧ := rfl
 
-lemma dependencyTransClosureIn_toTrace (s : List α) : @dependencyTransClosureIn' α I s = @dependencyTransClosureIn α I ⟦s⟧ := rfl
+lemma dependencyTransClosureIn_toTrace (s : List α) : @dependencyTransClosureIn α I s = @dependencyTransClosureInT α I ⟦s⟧ := rfl
 
-lemma isConnected_toTrace (s : List α) : @isConnected' α I s = @isConnected α I ⟦s⟧ := rfl
+lemma isConnected_toTrace (s : List α) : @isConnected α I s = @isConnectedT α I ⟦s⟧ := rfl
 
 
 def isIterativeFactor (X : Language α) (t : List α) :=
@@ -92,9 +92,9 @@ def toTrace (X : Language α) : Set (Trace I) := (fun s => ⟦s⟧) '' X
 
 def kstar (T : Set (Trace I)) := {r | ∃ ts : List (Trace I), (∀ t' ∈ ts, t' ∈ T) ∧ r = traceFlatten ts}
 
-def independent' (u v : Trace I) := ∀ a b, a ∈ u → b ∈ v → I.rel a b
+def IndependentT (u v : Trace I) := ∀ a b, a ∈ u → b ∈ v → I.rel a b
 
-def connectedComponents (X : Set (Trace I)) : Set (Trace I) := {u | isConnected u ∧ u ≠ ⟦[]⟧ ∧ ∃ v, u * v ∈ X ∧ independent' u v}
+def connectedComponents (X : Set (Trace I)) : Set (Trace I) := {u | isConnectedT u ∧ u ≠ ⟦[]⟧ ∧ ∃ v, u * v ∈ X ∧ IndependentT u v}
 
 
 -- open Computability
@@ -105,17 +105,13 @@ lemma kstar_toTrace_commutes (L : Language α) : @toTrace α I (KStar.kstar L) =
   intro t
   apply Iff.intro
   all_goals simp [kstar]
-  · intro ws hws hw
+  · intro ws hL ht
     induction ws generalizing t with
     | nil =>
-      intro hL ht
       use []
-      simp at hw
-      rw [hw] at ht
-      simp [ht, traceFlatten]
+      simp [<- ht, traceFlatten]
     | cons u ws ih =>
       simp at ih
-      intro hL ht
       replace ih := ih (fun y hy => hL y (List.mem_cons_of_mem u hy))
       choose ts hts using ih
       use ⟦u⟧ :: ts
@@ -124,7 +120,7 @@ lemma kstar_toTrace_commutes (L : Language α) : @toTrace α I (KStar.kstar L) =
         cases hs with
         | head => use u; simp [hL]
         | tail s hs => exact hts.left s hs
-      · simp [<- ht, hw]
+      · simp [<- ht]
         -- rw [<- mul_def]
         rw [traceFlatten_append, <- hts.right]
         rfl
@@ -133,30 +129,28 @@ lemma kstar_toTrace_commutes (L : Language α) : @toTrace α I (KStar.kstar L) =
     | nil =>
       use []
       simp [ht, traceFlatten]
-      use []
-      simp
     | cons s ts ih =>
       simp at ih
       replace ih := ih (fun y hy => hts y (List.mem_cons_of_mem s hy))
-      choose w hws hw using ih
+      choose ws hL hws using ih
       rcases s with ⟨u⟩
       rw [show Quot.mk (⇑(TraceSetoid I)) u = ⟦u⟧ from rfl] at ht hts
       replace hts := hts ⟦u⟧
       simp at hts
       choose u' hu' using hts
-      use u' ++ w
+      use u' :: ws
       apply And.intro
-      · rcases hws with ⟨ws, hws⟩
-        use u' :: ws
-        simp [hws.left, hu']
-        exact hws.right
+      · intro y hy
+        cases hy with
+        | head => exact hu'.left
+        | tail y hy => exact hL y hy
       · simp [ht]
-        rw [traceFlatten_append, <- hw, <- hu'.right]
+        rw [traceFlatten_append, <- hws, <- hu'.right]
         rfl
 
-lemma append_indep_is_disconnected_chars (u v : Trace I) (huv : independent' u v)
+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) :
-    ¬ (dependencyTransClosureIn (u * v)) a b := by
+    ¬ (dependencyTransClosureInT (u * v)) a b := by
   intro h
   induction h with
   | single h =>
@@ -170,20 +164,20 @@ lemma append_indep_is_disconnected_chars (u v : Trace I) (huv : independent' u v
       have hb_uv := mem_append.mp b.2
       simp [ih] at hb_uv
       exact hb_uv
-    simp [dependencyIn, inducedDependence] at h_tail
-    unfold independent' at huv
+    simp [dependencyInT, inducedDependence] at h_tail
+    unfold IndependentT at huv
     exact h_tail (huv b c hbu hb)
 
-lemma append_indep_is_disconnected (u v : Trace I) (h : independent' u v) (hu : u ≠ ⟦[]⟧) (hv : v ≠ ⟦[]⟧) :
-    ¬isConnected (u * v) := by
+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
   exact h_ab_dis h_ab_con
 
-lemma connectedComponents_of_connected (T : Set (Trace I)) (h : ∀ t ∈ T, isConnected t) :
+lemma connectedComponents_of_connected (T : Set (Trace I)) (h : ∀ t ∈ T, isConnectedT t) :
     connectedComponents T = T \ {⟦[]⟧} := by
   apply Set.ext
   intro t
@@ -200,7 +194,7 @@ lemma connectedComponents_of_connected (T : Set (Trace I)) (h : ∀ t ∈ T, isC
     use (h t ht), htz, ⟦[]⟧
     rw [right_id]
     use ht
-    unfold independent'
+    unfold IndependentT
     simp [show ⟦[]⟧ = mk' [] from rfl, eps_is_empty]
 
 lemma empty_iff {w : List α} : (⟦w⟧ : Trace I) = ⟦[]⟧ ↔ w = [] := by
@@ -209,7 +203,7 @@ lemma empty_iff {w : List α} : (⟦w⟧ : Trace I) = ⟦[]⟧ ↔ w = [] := by
   | cons a u =>
     apply Iff.intro
     · intro h
-      have h_au := length_eq_of_equiv (Quotient.exact h)
+      have h_au := length_eq_of_eqv (Quotient.exact h)
       simp at h_au
     · simp
 
@@ -223,7 +217,8 @@ def isEmpty : Trace I → Bool := Quotient.lift List.isEmpty (by
     | cons b v => rfl
 )
 
-lemma isEmpty_iff {t : Trace I} : t.isEmpty = true ↔ t = ⟦[]⟧ := by
+--lemma isEmpty_iff {t : Trace I} : t.isEmpty = true ↔ t = ⟦[]⟧ := by
+lemma isEmpty_iff {t : Trace I} : isEmpty t = true ↔ t = ⟦[]⟧ := by
   apply Iff.intro
   · intro h
     rcases t with ⟨s⟩
@@ -234,10 +229,10 @@ lemma isEmpty_iff {t : Trace I} : t.isEmpty = true ↔ t = ⟦[]⟧ := by
     rfl
 
 lemma traceFlatten_filter_not_isEmpty :
-    ∀ {L : List (Trace I)}, traceFlatten (List.filter (!·.isEmpty) L) = traceFlatten L
+    ∀ {L : List (Trace I)}, traceFlatten (List.filter (!isEmpty ·) L) = traceFlatten L
   | [] => rfl
   | t :: L => by
-    by_cases ht : t.isEmpty
+    by_cases ht : isEmpty t
     · apply isEmpty_iff.mp at ht
       simp [ht]
       simp [show isEmpty ⟦[]⟧ = true from rfl]
@@ -271,11 +266,11 @@ lemma kstar_eq_minusEps_trace (T : Set (Trace I)) : kstar (T \ {⟦[]⟧}) = kst
     simp [ht]
     exact fun y hy => Set.diff_subset (hls y hy)
   · intro ⟨ls, hls, ht⟩
-    use ls.filter (!·.isEmpty)
+    use ls.filter (!isEmpty ·)
     simp
     apply And.intro
     · intro y hy hyz
-      exact ⟨hls y hy, Trace.isEmpty_iff.ne.mp (ne_true_of_eq_false hyz)⟩
+      exact ⟨hls y hy, isEmpty_iff.ne.mp (ne_true_of_eq_false hyz)⟩
     · simp [traceFlatten_filter_not_isEmpty, ht]
 
 end TraceTheory

TraceTheory/TraceTheory/MyhillNerode.lean

@@ -1,41 +1,41 @@
-import TraceTheory.Basic
+import TraceTheory.Lemmas
 import Mathlib.Data.Finset.Pi
 
 namespace TraceTheory
 
 variable {α : Type} {I : Independence α}
 
-lemma indep_of_flatten {u : List α} {vs : List (List α)} (i : Fin vs.length) (h : independent I u vs.flatten) :
-    independent I u vs[i] := by
+lemma indep_of_flatten {u : List α} {vs : List (List α)} (i : Fin vs.length) (h : Independent I u vs.flatten) :
+    Independent I u vs[i] := by
   replace ⟨i, hi⟩ := i
   induction vs generalizing i with
   | nil =>
     simp at hi
   | cons v vs' ih =>
-    simp at h ⊢
+    simp [-Independent] at h ⊢
     cases i with
-    | zero => exact (indep_of_concat h).left
+    | zero => exact (indep_of_indep_append_right h).left
     | succ i =>
       simp at hi
-      exact ih (indep_of_concat h).right i hi
+      exact ih (indep_of_indep_append_right h).right i hi
 
 /-- (i) → (ii) of Corollary (2.3) in `Partial Commutation and Traces`.
   Note that t₁, t₂, …, tₙ is expressed as a list [ts], and (t₁ ++ t₂ ++ … ++ tₙ) via [ts.flatten].
   Similarly, p₁, …, pₙ is [ps] and q₁, …, qₙ is [qs]. -/
-theorem levi_lemma_gen (u v : List α) (ts : List (List α)) [DecidableEq α] (h : TraceEquiv I (u ++ v) ts.flatten) :
+theorem levi_lemma_gen (u v : List α) (ts : List (List α)) [DecidableEq α] (h : TraceEqv I (u ++ v) ts.flatten) :
     ∃ (ps qs : List (List α)),
     ps.length = ts.length
     ∧ qs.length = ts.length
-    ∧ TraceEquiv I u ps.flatten
-    ∧ TraceEquiv I v qs.flatten
-    ∧ (∀ i : Fin (min ts.length (min ps.length qs.length)), TraceEquiv I ts[i] (ps[i] ++ qs[i]))
-    ∧ ∀ i : Fin qs.length, ∀ j : Fin ps.length, i.val < j.val → independent I qs[i] ps[j] := by
+    ∧ TraceEqv I u ps.flatten
+    ∧ TraceEqv I v qs.flatten
+    ∧ (∀ i : Fin (min ts.length (min ps.length qs.length)), TraceEqv I ts[i] (ps[i] ++ qs[i]))
+    ∧ ∀ i : Fin qs.length, ∀ j : Fin ps.length, i.val < j.val → Independent I qs[i] ps[j] := by
   induction ts generalizing u v with
   | nil =>
     simp at h ⊢
-    replace h := length_eq_of_equiv h
+    replace h := length_eq_of_eqv h
     simp at h
-    simp [h, TraceEquiv.refl]
+    simp [h, TraceEqv.refl]
     intro ⟨i, hi⟩
     simp at hi
   | cons t tsuf ih =>
@@ -47,12 +47,12 @@ theorem levi_lemma_gen (u v : List α) (ts : List (List α)) [DecidableEq α] (h
     repeat' apply And.intro
     · simp [ih_p_len]
     · simp [ih_q_len]
-    · apply TraceEquiv.trans h_up
+    · apply TraceEqv.trans h_up
       simp
-      exact TraceEquiv.compat (TraceEquiv.refl p) ih_p
-    · apply TraceEquiv.trans h_vq
+      exact TraceEqv.compat (TraceEqv.refl p) ih_p
+    · apply TraceEqv.trans h_vq
       simp
-      exact TraceEquiv.compat (TraceEquiv.refl q) ih_q
+      exact TraceEqv.compat (TraceEqv.refl q) ih_q
     · intro ⟨i, hi⟩
       by_cases hzi : i = 0
       · simp [hzi, h_tpq]
@@ -68,7 +68,7 @@ theorem levi_lemma_gen (u v : List α) (ts : List (List α)) [DecidableEq α] (h
         cases i with
         | zero =>
           simp at hj ⊢
-          have h_ind_ps := indep_of_indep_of_equiv (indep_symm h_ind) ih_p
+          have h_ind_ps := indep_of_indep_of_eqv (independent_symm h_ind) ih_p
           exact indep_of_flatten ⟨j, hj⟩ h_ind_ps
         | succ i =>
           simp at hi hj hij ⊢