Skip to content

Commit c74911a

Browse files
jefraijefrai
committed
Ochmanski (i) => (ii) fragments 3
1 parent 30b5958 commit c74911a

1 file changed

Lines changed: 175 additions & 38 deletions

File tree

‎TraceTheory/TraceTheory/Ochmanski.lean‎

Lines changed: 175 additions & 38 deletions
Original file line numberDiff line numberDiff line change
@@ -476,6 +476,18 @@ lemma depTrClIn_symm {w : List α} {a b : α} : dependencyTransClosureInL I w a
476476
rw [depIn_symm]
477477
rw [h_symm]
478478

479+
lemma depIn_sub {u w : List α} {a b : α} (huw : u ⊆ w) :
480+
dependencyInL I u a b → dependencyInL I w a b := by
481+
intro ⟨hab, ha, hb⟩
482+
exact ⟨hab, huw ha, huw hb⟩
483+
484+
lemma depTrClIn_sub {u w : List α} {a b : α} (huw : u ⊆ w) :
485+
dependencyTransClosureInL I u a b → dependencyTransClosureInL I w a b := by
486+
intro h
487+
induction h with
488+
| single hab => exact Relation.TransGen.single (depIn_sub huw hab)
489+
| tail hac hcb ih => exact Relation.TransGen.tail ih (depIn_sub huw hcb)
490+
479491
--- variable [DecidableRel I.rel]
480492

481493
---
@@ -723,6 +735,10 @@ lemma ccDec_aux_elem_nonempty (u w : List α) (i : ℕ) (hi : i < (ccDec_aux I u
723735
apply ih
724736
exact hw
725737

738+
lemma ccDec_aux_elem_nonempty_len (u w : List α) (i : ℕ) (hi : i < (ccDec_aux I u w).length) (hz : w ≠ []) :
739+
0 < (ccDec_aux I u w)[i].length :=
740+
List.length_pos_iff.mpr (@ccDec_aux_elem_nonempty α I _ _ _ hi hz)
741+
726742
lemma ccDec_aux_flatten (I : Independence α) (u w : List α) :
727743
(ccDec_aux I u w).flatten = w := by
728744
induction w with
@@ -757,6 +773,17 @@ lemma ccDec_flatten_prefix2 (L : List (List α)) (h : 1 < L.length) :
757773
| nil => simp at h
758774
| cons v L => simp
759775

776+
lemma List.flatten_infix (L : List (List α)) (i : ℕ) (hi : i < L.length) :
777+
List.IsInfix L[i] L.flatten := by
778+
induction L generalizing i with
779+
| nil => simp at hi
780+
| cons w L ih =>
781+
cases i with
782+
| zero => exact List.infix_append_left
783+
| succ i =>
784+
simp
785+
exact List.infix_append_of_infix_right (ih i (Nat.succ_lt_succ_iff.mp hi))
786+
760787
lemma List.flatten_adj_infix (L : List (List α)) (i : ℕ) (hi : i + 1 < L.length) :
761788
List.IsInfix (L[i] ++ L[i + 1]) L.flatten := by
762789
induction L generalizing i with
@@ -790,7 +817,12 @@ lemma ccDec_aux_prefix (I : Independence α) (u w : List α) :
790817
nth_rw 3 [<- ccDec_aux_flatten I u w]
791818
exact List.flatten_prefix _ (ccDec_aux_nonempty u w)
792819

793-
lemma ccDec_aux_infix (I : Independence α) (u w : List α) (i : ℕ) (hi : i + 1 < (ccDec_aux I u w).length) :
820+
lemma ccDec_aux_infix (I : Independence α) (u w : List α) (i : ℕ) (hi : i < (ccDec_aux I u w).length) :
821+
List.IsInfix (ccDec_aux I u w)[i] w := by
822+
nth_rw 2 [<- ccDec_aux_flatten I u w]
823+
exact List.flatten_infix (ccDec_aux I u w) i hi
824+
825+
lemma ccDec_aux_adj_infix (I : Independence α) (u w : List α) (i : ℕ) (hi : i + 1 < (ccDec_aux I u w).length) :
794826
List.IsInfix ((ccDec_aux I u w)[i] ++ (ccDec_aux I u w)[i + 1]) w := by
795827
nth_rw 7 [<- ccDec_aux_flatten I u w]
796828
exact List.flatten_adj_infix (ccDec_aux I u w) i hi
@@ -924,31 +956,42 @@ lemma ccDec_aux_adj_char_indep (u w : List α) (i : ℕ) (hi : i + 1 < (ccDec_au
924956
¬dependencyTransClosureInL I u
925957
((ccDec_aux I u w)[i].getLast (ccDec_aux_elem_nonempty u w i (Nat.lt_of_succ_lt hi) hw))
926958
((ccDec_aux I u w)[i + 1][0]'(List.length_pos_iff.mpr (ccDec_aux_elem_nonempty u w (i + 1) hi hw))) := by
927-
by_cases hiz : i = 0
928-
· simp [hiz] at hi ⊢
929-
exact ccDec_aux_adj_head_char_indep u w hi hw
930-
· induction w generalizing i with
931-
| nil => simp at hw
932-
| cons a w ih =>
933-
sorry
934-
/- by_cases hab : ccDec_aux_conn I u (a :: w)
935-
· rw [ccDec_aux_tail_C hab]
936-
apply ih (List.subset_of_cons_subset hwu)
937-
exact Nat.zero_lt_of_ne_zero hiz
938-
· rw [ccDec_aux_tail_D' hab]
939-
apply ih (List.subset_of_cons_subset hwu)
940-
rw [ccDec_aux_len_D hab] at hi
941-
cases i with
942-
| zero => simp at hiz
943-
| succ i => exact Nat.succ_lt_succ_iff.mp hi -/
944-
945-
lemma ccDec_aux_adj_indep (u w : List α) (i : ℕ) (hi : i + 1 < (ccDec_aux I u w).length) :
946-
Independent I (ccDec_aux I u w)[i] (ccDec_aux I u w)[i + 1] := by
947959
induction w generalizing i with
948-
| nil => simp [ccDec_aux]
960+
| nil => simp at hw
949961
| cons a w ih =>
950-
intro p hp q hq
951-
sorry
962+
by_cases hw : w = []
963+
· simp [hw, ccDec_aux] at hi
964+
cases i with
965+
| zero => exact ccDec_aux_adj_head_char_indep u (a :: w) (Nat.lt_of_succ_le hi) (List.cons_ne_nil a w)
966+
| succ i =>
967+
by_cases hab : ccDec_aux_conn I u (a :: w)
968+
· rw [List.getLast.congr_simp _ _ (ccDec_aux_tail_C hab (i + 1) (Nat.lt_of_succ_lt hi) (Nat.zero_lt_succ i))]
969+
rw [List.getElem_of_eq (ccDec_aux_tail_C hab (i + 2) hi (Nat.zero_lt_succ (i + 1)))]
970+
exact ih _ _ hw
971+
· rw [List.getLast.congr_simp _ _ (ccDec_aux_tail_D hab i (Nat.lt_of_succ_lt hi))]
972+
rw [List.getElem_of_eq (ccDec_aux_tail_D hab (i + 1) hi)]
973+
exact ih _ _ hw
974+
975+
lemma ccDec_aux_adj_indep (u w : List α) (i : ℕ) (hi : i + 1 < (ccDec_aux I u w).length) (hwu : w ⊆ u) :
976+
Independent I (ccDec_aux I u w)[i] (ccDec_aux I u w)[i + 1] := by
977+
by_cases hw : w = []
978+
· simp [hw, ccDec_aux] at hi
979+
intro p hp q hq
980+
by_contra hpq
981+
apply ccDec_aux_adj_char_indep u w i hi hw
982+
rw [List.getLast_eq_getElem]
983+
have hqR : dependencyTransClosureInL I u q (((ccDec_aux I u w)[i + 1]'hi)[0]'(List.length_pos_of_mem hq)) :=
984+
ccDec_aux_elem_conn u w hwu (i + 1) hi _ _ hq (List.getElem_mem (List.length_pos_of_mem hq))
985+
refine Relation.TransGen.trans ?_ hqR
986+
replace hpq : dependencyTransClosureInL I u p q := by
987+
unfold dependencyTransClosureInL dependencyInL inducedDependence
988+
simp
989+
apply Relation.TransGen.single
990+
use hpq
991+
use hwu (List.IsInfix.mem hp (ccDec_aux_infix I u w i (Nat.lt_of_succ_lt hi)))
992+
exact hwu (List.IsInfix.mem hq (ccDec_aux_infix I u w (i + 1) hi))
993+
refine Relation.TransGen.trans ?_ hpq
994+
exact ccDec_aux_elem_conn u w hwu i (Nat.lt_of_succ_lt hi) _ _ (by simp) hp
952995

953996
lemma ccDec_disconnected_len (w : List α) (h : ¬ IsConnectedL I w) :
954997
(ccDec I w).length ≥ 2 := by
@@ -989,6 +1032,56 @@ lemma lexNf_infix_is_lexNf {s t : List α} (hst : List.IsInfix s t) (ht : IsLexN
9891032
simp [<- hst, hs] at ht
9901033
exact ht
9911034

1035+
omit [Fintype α] [LinearOrder α] [DecidableRel I.rel] in
1036+
lemma connected_dep_concat {u v : List α} (hu : IsConnectedL I u) (hv : IsConnectedL I v) (huv : ¬Independent I u v) :
1037+
IsConnectedL I (u ++ v) := by
1038+
intro ⟨a, ha⟩ ⟨b, hb⟩
1039+
simp at ha hb
1040+
cases ha with
1041+
| inl ha =>
1042+
cases hb with
1043+
| inl hb => exact depTrClIn_sub (List.subset_append_of_subset_left v (by simp)) (hu ⟨a, ha⟩ ⟨b, hb⟩)
1044+
| inr hb =>
1045+
simp at huv
1046+
have ⟨a', ha', b', hb', hab⟩ := huv
1047+
have haa' : dependencyTransClosureInL I (u ++ v) a a' :=
1048+
depTrClIn_sub (List.subset_append_of_subset_left v (by simp)) (hu ⟨a, ha⟩ ⟨a', ha'⟩)
1049+
have hb'b : dependencyTransClosureInL I (u ++ v) b' b :=
1050+
depTrClIn_sub (List.subset_append_of_subset_right u (by simp)) (hv ⟨b', hb'⟩ ⟨b, hb⟩)
1051+
have ha'b' : dependencyTransClosureInL I (u ++ v) a' b' := by
1052+
apply Relation.TransGen.single
1053+
simp [dependencyInL, inducedDependence]
1054+
exact ⟨hab, Or.inl ha', Or.inr hb'⟩
1055+
exact Relation.TransGen.trans haa' (Relation.TransGen.trans ha'b' hb'b)
1056+
| inr ha =>
1057+
cases hb with
1058+
| inl hb =>
1059+
simp at huv
1060+
have ⟨b', hb', a', ha', hab⟩ := huv
1061+
have haa' : dependencyTransClosureInL I (u ++ v) a a' :=
1062+
depTrClIn_sub (List.subset_append_of_subset_right u (by simp)) (hv ⟨a, ha⟩ ⟨a', ha'⟩)
1063+
have hb'b : dependencyTransClosureInL I (u ++ v) b' b :=
1064+
depTrClIn_sub (List.subset_append_of_subset_left v (by simp)) (hu ⟨b', hb'⟩ ⟨b, hb⟩)
1065+
have ha'b' : dependencyTransClosureInL I (u ++ v) a' b' := by
1066+
apply Relation.TransGen.single
1067+
simp [dependencyInL, inducedDependence]
1068+
exact ⟨fun h => hab (I.symm _ _ h), Or.inr ha', Or.inl hb'⟩
1069+
exact Relation.TransGen.trans haa' (Relation.TransGen.trans ha'b' hb'b)
1070+
| inr hb => exact depTrClIn_sub (List.subset_append_of_subset_right u (by simp)) (hv ⟨a, ha⟩ ⟨b, hb⟩)
1071+
1072+
omit [Fintype α] [LinearOrder α] [DecidableRel I.rel] in
1073+
lemma connected_dup_is_connected {w : List α} (hw : IsConnectedL I w) :
1074+
IsConnectedL I (w ++ w) := by
1075+
cases w with
1076+
| nil => simp [hw]
1077+
| cons a w =>
1078+
have h_dep : ¬Independent I (a :: w) (a :: w) := by
1079+
simp
1080+
intro ha
1081+
exfalso
1082+
exact I.irrefl a ha
1083+
exact connected_dep_concat hw hw h_dep
1084+
9921085
lemma lexNf_sq_is_lexNf {w : List α} (h : w ++ w ∈ LexNfLanguage I) :
9931086
w ∈ LexNfLanguage I := by
9941087
apply (mem_lexNfLanguage_iff_factorCondition _ _).mp at h
@@ -1001,11 +1094,65 @@ lemma lexNf_sq_is_lexNf {w : List α} (h : w ++ w ∈ LexNfLanguage I) :
10011094
use w ++ u
10021095
exact ⟨TraceEqv.compat (TraceEqv.refl w) h.1, List.append_left_lt h.right⟩
10031096

1097+
omit [Fintype α] [DecidableRel I.rel] in
1098+
lemma lexNf_concat_of_indep {u v : List α} (h_indep : Independent I u v) (huv : IsLexNf I (u ++ v))
1099+
(hu : u ≠ []) (hv : v ≠ []) :
1100+
(u[0]'(List.length_pos_iff.mpr hu) < v[0]'(List.length_pos_iff.mpr hv)) := by
1101+
apply (isLexNf_iff_factorCondition _ _).mp at huv
1102+
1103+
rcases u
1104+
· simp at hu
1105+
rename_i a u
1106+
1107+
rcases v
1108+
· simp at hv
1109+
rename_i b v
1110+
1111+
replace huv := huv [] u v b a
1112+
simp at huv h_indep ⊢
1113+
1114+
by_contra h_ge
1115+
have h_ne : a ≠ b := by
1116+
by_contra h_eq
1117+
rw [h_eq] at h_indep
1118+
exact (I.irrefl _) h_indep.1.1
1119+
have h_gt : b < a := by
1120+
simp at h_ge
1121+
exact lt_of_le_of_ne h_ge (Ne.symm h_ne)
1122+
1123+
have ⟨c, hcs, hac⟩ := huv (I.symm _ _ h_indep.1.1) h_gt
1124+
exact hac (I.symm _ _ (h_indep.2 c hcs).1)
1125+
1126+
lemma lexNf_ccDec_adj_order {w : List α} (hw : w ∈ LexNfLanguage I) (hz : w ≠ []) (i : ℕ)
1127+
(hi : i + 1 < (ccDec_aux I w w).length) :
1128+
(ccDec_aux I w w)[i][0]'(ccDec_aux_elem_nonempty_len _ _ _ _ hz) <
1129+
(ccDec_aux I w w)[i + 1][0]'(ccDec_aux_elem_nonempty_len _ _ _ _ hz) := by
1130+
apply (mem_lexNfLanguage_iff_factorCondition _ _).mp at hw
1131+
apply (isLexNf_iff_factorCondition _ _).mpr at hw
1132+
have h_infix := lexNf_infix_is_lexNf (ccDec_aux_adj_infix I w w i hi) hw
1133+
1134+
apply lexNf_concat_of_indep (ccDec_aux_adj_indep w w i hi (by simp)) h_infix
1135+
use (ccDec_aux_elem_nonempty w w i (Nat.lt_of_succ_lt hi) hz)
1136+
exact ccDec_aux_elem_nonempty w w (i + 1) hi hz
1137+
1138+
lemma lexNf_ccDec_order {w : List α} (hw : w ∈ LexNfLanguage I) (hz : w ≠ []) (i j : ℕ)
1139+
(hij : i < j) (hj : j < (ccDec_aux I w w).length) :
1140+
(ccDec_aux I w w)[i][0]'(ccDec_aux_elem_nonempty_len _ _ _ _ hz) <
1141+
(ccDec_aux I w w)[j][0]'(ccDec_aux_elem_nonempty_len _ _ _ _ hz) := by
1142+
induction hij with
1143+
| refl => exact lexNf_ccDec_adj_order hw hz i hj
1144+
| step hij ih =>
1145+
clear j
1146+
rename_i j
1147+
exact lt_trans (ih (Nat.lt_of_succ_lt hj)) (lexNf_ccDec_adj_order hw hz j hj)
1148+
10041149
lemma connected_of_lexNf_sq {w : List α}
10051150
(hw : w ∈ LexNfLanguage I)
10061151
(hww : w ++ w ∈ LexNfLanguage I) :
10071152
IsConnected I ⟦w⟧ := by
10081153
rw [<- IsConnected_eq]
1154+
-- by_contra h_con
1155+
-- have h_dec_len := @ccDec_disconnected_len α I (w ++ w) (by)
10091156
cases w with
10101157
| nil => simp [IsConnectedL]
10111158
| cons a w' =>
@@ -1019,13 +1166,13 @@ lemma connected_of_lexNf_sq {w : List α}
10191166
(ccDec_aux I w w)[i][0]'(List.length_pos_iff.mpr (ccDec_aux_elem_nonempty w w i (Nat.lt_of_succ_lt hi) hz)) <
10201167
((ccDec_aux I w w)[i + 1][0]'(List.length_pos_iff.mpr (ccDec_aux_elem_nonempty w w (i + 1) hi hz))) := by
10211168
intro i hi
1022-
have h_infix := ccDec_aux_infix I w w i hi
1169+
have h_infix := ccDec_aux_adj_infix I w w i hi
10231170
apply (mem_lexNfLanguage_iff_factorCondition _ _).mp at hw
10241171
apply (isLexNf_iff_factorCondition _ _).mpr at hw
10251172
replace h_infix := lexNf_infix_is_lexNf h_infix hw
10261173
apply (isLexNf_iff_factorCondition _ _).mp at h_infix
10271174

1028-
have h_indep : Independent I (ccDec_aux I w w)[i] (ccDec_aux I w w)[i + 1] := ccDec_aux_adj_indep w w i hi
1175+
have h_indep : Independent I (ccDec_aux I w w)[i] (ccDec_aux I w w)[i + 1] := ccDec_aux_adj_indep w w i hi (by simp)
10291176

10301177
let t₁ := (ccDec_aux I w w)[i]
10311178
have ht₁ : (ccDec_aux I w w)[i] = t₁ := rfl
@@ -1062,18 +1209,8 @@ lemma connected_of_lexNf_sq {w : List α}
10621209
(ccDec_aux I w w)[i][0]'(List.length_pos_iff.mpr (ccDec_aux_elem_nonempty w w i (Nat.lt_of_succ_lt hi) hz)) <
10631210
((ccDec_aux I w w)[(ccDec_aux I w w).length - 1][0]'(List.length_pos_iff.mpr (ccDec_aux_elem_nonempty w w ((ccDec_aux I w w).length - 1) (Nat.sub_one_lt_of_lt h_con) hz))) := by
10641211
intro i hi
1065-
replace hi : i < (ccDec_aux I w w).length - 1 := Nat.lt_sub_of_add_lt hi
1066-
replace hi : i ≤ (ccDec_aux I w w).length - 1 := Nat.le_of_succ_le hi
1067-
induction hi using Nat.decreasingInduction with
1068-
| self =>
1069-
replace hi : (ccDec_aux I w w).length = 0 := by
1070-
contrapose hi
1071-
simp
1072-
exact le_tsub_add
1073-
exfalso
1074-
exact (ccDec_aux_nonempty _ _) (List.eq_nil_iff_length_eq_zero.mpr hi)
1075-
| of_succ k h ih =>
1076-
sorry
1212+
-- exact @lexNf_ccDec_order α I _ _ _ _ _ _ i (i + 1) _ _
1213+
sorry
10771214

10781215
sorry
10791216

0 commit comments

Comments
 (0)