More Ochmanski (i) => (ii)

Author: jefrai

TraceTheory/TraceTheory/Language.lean

@@ -288,7 +288,27 @@ theorem mem_lexNfLanguage_iff_factorCondition (x : List α) :
     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
+  rcases t with ⟨u⟩
+  rw [show Quot.mk (⇑(TraceSetoid I)) u = ⟦u⟧ from rfl]
+  induction u using List.reverseRecOn with
+  | nil =>
+    use []
+    simp
+    apply (mem_lexNfLanguage_iff_factorCondition _ _).mpr
+    apply (isLexNf_iff_factorCondition _ _).mp
+    unfold IsLexNf
+    intro w h_equiv
+    replace h_equiv : w = [] := by
+      simp [List.eq_nil_of_length_eq_zero, length_eq_of_eqv h_equiv.symm]
+    exact ge_of_eq h_equiv
+  | append_singleton u a ih =>
+    rcases ih with ⟨s, hs_equiv, hs_lexNf⟩
+    have h_equiv : TraceEqv I ([a] ++ s) ([a] ++ u) := by
+      apply TraceEqv.compat
+      · exact TraceEqv.refl [a]
+      · --exact hs_equiv
+        sorry
+    sorry
 
 end LexNf
 

TraceTheory/TraceTheory/Ochmanski.lean

@@ -202,6 +202,17 @@ noncomputable def ccDec_aux' (I : Independence α) (w₀ w : List α) : List (Li
           then (a :: b :: v) :: vs
           else [a] :: (b :: v) :: vs
 
+noncomputable def ccDec_aux_conn (I : Independence α) (w₀ w : List α) : Prop :=
+  match w with
+  | [] => False
+  | a :: w =>
+    match ccDec_aux' I w₀ w with
+    | [] => False
+    | v :: _ =>
+      match v with
+      | [] => False
+      | b :: _ => dependencyTransClosureInL I w₀ a b
+
 lemma ccDec'_aux_nonempty' (w₀ w : List α) : (ccDec_aux' I w₀ w) ≠ [] := by
   induction w with
   | nil => simp [ccDec_aux']
@@ -218,6 +229,48 @@ lemma ccDec'_aux_nonempty' (w₀ w : List α) : (ccDec_aux' I w₀ w) ≠ [] :=
         by_cases hab : dependencyTransClosureInL I w₀ a b
         all_goals simp [hab]
 
+lemma ccDec_aux'_len_C (u w : List α) (a : α) (h : ccDec_aux_conn I u (a :: w)) :
+    (ccDec_aux' I u (a :: w)).length = (ccDec_aux' I u w).length := by
+  simp [ccDec_aux_conn] at h
+  let t := ccDec_aux' I u w
+  have ht : ccDec_aux' I u w = t := rfl
+  rcases t
+  · simp [ht] at h
+  · rename_i c_head c_tail
+    simp [ht] at h
+    cases c_head with
+    | nil => simp at h
+    | cons b c_head =>
+      simp at h
+      simp [ccDec_aux', ht, h]
+
+lemma ccDec_aux'_len_D (u w : List α) (a : α) (h : ¬ ccDec_aux_conn I u (a :: w)) (hw : w ≠ []) :
+    (ccDec_aux' I u (a :: w)).length = (ccDec_aux' I u w).length + 1 := by
+  simp [ccDec_aux_conn] at h
+  let t := ccDec_aux' I u w
+  have ht : ccDec_aux' I u w = t := rfl
+  rcases t
+  · exfalso
+    exact ccDec'_aux_nonempty' _ _ ht
+  · rename_i c_head c_tail
+    simp [ht] at h
+    cases c_head with
+    | nil =>
+      cases w with
+      | nil => simp at hw
+      | cons b w =>
+        simp [ccDec_aux'] at ht
+        let t' := ccDec_aux' I u w
+        have ht' : ccDec_aux' I u w = t' := rfl
+        rcases t'
+        · exfalso
+          exact ccDec'_aux_nonempty' _ _ ht'
+        · rename_i c'_head c'_tail
+          simp [ht'] at ht
+    | cons b c_head =>
+      simp at h
+      simp [ccDec_aux', ht, h]
+
 lemma ccDec'_aux_len (u w : List α) (a : α) :
     (ccDec_aux' I u (a :: w)).length = (ccDec_aux' I u w).length ∨
     (ccDec_aux' I u (a :: w)).length = (ccDec_aux' I u w).length + 1 := by
@@ -233,12 +286,31 @@ lemma ccDec'_aux_len (u w : List α) (a : α) :
       by_cases hab : dependencyTransClosureInL I u a b
       all_goals simp [hab]
 
+lemma ccDec'_aux_offset (u w : List α) (a : α) :
+    (∀ i, ccDec_aux' I u (a :: w)).length = (ccDec_aux' I u w).length ∨
+    (ccDec_aux' I u (a :: w)).length = (ccDec_aux' I u w).length + 1 := by
+  simp [ccDec_aux']
+  cases ccDec_aux' I u w
+  · simp
+  · rename_i c_head c_tail
+    simp
+    cases c_head with
+    | nil => simp
+    | cons b c_head =>
+      simp
+      by_cases hab : dependencyTransClosureInL I u a b
+      all_goals simp [hab]
+
 lemma ccDec'_aux_len_le (u w : List α) (a : α) :
     (ccDec_aux' I u w).length ≤ (ccDec_aux' I u (a :: w)).length := by
   cases ccDec'_aux_len u w a with
   | inl h => rw [h]
   | inr h => simp [h]
 
+lemma ccDec'_aux_sub_idx (u w : List α) (a : α) (i : Fin (ccDec_aux' I u (a :: w)).length) (hiz : i.1 > 0) :
+    ∃ j : Fin (ccDec_aux' I u w).length, (ccDec_aux' I u (a :: w))[i] = (ccDec_aux' I u w)[j] := by
+  sorry
+
 lemma ccDec'_aux_nonempty (u w : List α) (i : ℕ) (hi : i < (ccDec_aux' I u w).length) (hz : w ≠ []) :
     (ccDec_aux' I u w)[i] ≠ [] := by
   induction w generalizing i with
@@ -263,37 +335,39 @@ lemma ccDec'_aux_nonempty (u w : List α) (i : ℕ) (hi : i < (ccDec_aux' I u w)
           simp
           by_cases hab : dependencyTransClosureInL I u a b
           all_goals simp [hab]
-    · -- cases a
-      have : (ccDec_aux' I u (a :: w))[i] = (ccDec_aux' I u w)[i]'sorry ∨ (ccDec_aux' I u (a :: w))[i] = (ccDec_aux' I u w)[i - 1]'sorry := by
-        simp [ccDec_aux']
-        /- cases ccDec_aux' I u w
-        · simp
-        · rename_i c_head c_tail
-          simp
-          cases c_head with
-          | nil => simp
-          | cons b c_head =>
-            simp
-            by_cases hab : dependencyTransClosureInL I u a b
-            all_goals simp [hab] -/
-        sorry
-      cases this with
-      | inl h =>
-        rw [h]
-        apply ih
-        by_contra hz
-        simp [ccDec_aux', hz] at hi
-        exact hiz hi
-      | inr h =>
-        rw [h]
-        have : i - 1 < (ccDec_aux' I u w).length := by sorry
-        apply ih (i - 1) this
-        by_contra hz
-        simp [ccDec_aux', hz] at hi
+    · have hw : w ≠ [] := by
+        by_contra hw
+        simp [hw, ccDec_aux'] at hi
         exact hiz hi
+      have ⟨⟨j, hj⟩, hjw⟩ := ccDec'_aux_sub_idx u w a ⟨i, hi⟩ (Nat.zero_lt_of_ne_zero hiz)
+      simp at hjw
+      rw [hjw]
+      exact ih j hj hw
 
-
-
+lemma ccDec'_subst (u w : List α) (p : α) (i : ℕ) (hi : i + 1 < (ccDec_aux' I u w).length) :
+    List.Sublist ((ccDec_aux' I u w)[i] ++ (ccDec_aux' I u w)[i + 1]) w := by
+  induction w generalizing i with
+  | nil => simp [ccDec_aux'] at hi
+  | cons a w ih =>
+    by_cases hiz : i = 0
+    · simp [hiz]
+      sorry
+    ·
+      have ⟨⟨j, hj⟩, hjw⟩ := ccDec'_aux_sub_idx u w a ⟨i, by omega⟩ (Nat.zero_lt_of_ne_zero hiz)
+      simp at hjw
+      rw [hjw]
+      exact ih j hj
+    cases ccDec_aux' I u w
+    · simp
+    · rename_i c_head c_tail
+      simp
+      cases c_head with
+      | nil => simp
+      | cons b c_head =>
+        simp
+        by_cases hab : dependencyTransClosureInL I w a b
+        all_goals simp [hab]
+        all_goals apply List.Sublist.cons
 
 noncomputable def ccDec_aux (I : Independence α) (w₀ w : List α) (p : α) : List (List α × List α) :=
   match w with