Skip to content

Commit 89e5412

Browse files
yisioxyisiox
committed
Merge branch 'ys-working' into beta
2 parents 1c20e07 + ab9fd7a commit 89e5412

2 files changed

Lines changed: 182 additions & 101 deletions

File tree

‎TraceTheory/TraceTheory/Language.lean‎

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -365,7 +365,7 @@ theorem kstar_diff_one (X : Language α) : (X \ {[]})∗ = X∗ := by
365365
def IsValidFactorization
366366
(I : Independence α) (X : Language α) (x y : List α) (xs ys : List (List α)) : Prop :=
367367
xs.length = ys.length ∧
368-
(zipWith (· ++ ·) xs ys).flatten ∈ traceClosure I X ∧
368+
(zipWith (· ++ ·) xs ys).flatten ∈ X ∧
369369
TraceEqv I x xs.flatten ∧
370370
TraceEqv I y ys.flatten ∧
371371
∀ i j (hi : i < ys.length) (hj : j < xs.length), i < j →
@@ -402,11 +402,12 @@ theorem concat_closed_rank [DecidableEq α]
402402
replace h₁ := h₁ (z₁ ++ z₃)
403403
replace h₂ := h₂ (z₂ ++ z₄)
404404
rw [Set.mem_setOf] at h₁ h₂
405-
use z₁ ++ z₃ ++ (z₂ ++ z₄)
405+
use z₁ ++ z₃
406406
constructor
407-
· rw [Language.mem_mul]
408-
exact ⟨z₁ ++ z₃, h₁.mp ⟨x₁, hx₁, hx₁_eqv⟩, z₂ ++ z₄, h₂.mp ⟨x₂, hx₂, hx₂_eqv⟩, rfl⟩
409-
· apply TraceEqv.refl
407+
· exact h₁.mp ⟨x₁, hx₁, hx₁_eqv⟩
408+
· use z₂ ++ z₄
409+
simp only [append_assoc, and_true]
410+
exact h₂.mp ⟨x₂, hx₂, hx₂_eqv⟩
410411
· simpa
411412
· simpa
412413
· intro i j

‎TraceTheory/TraceTheory/Ochmanski.lean‎

Lines changed: 176 additions & 96 deletions
Original file line numberDiff line numberDiff line change
@@ -499,16 +499,36 @@ lemma split_indices_bound [Fintype α] [DecidableEq α] {n : ℕ} {ps qs : List
499499
rw [← Fintype.card_coe S]
500500
exact h_card
501501

502+
/-- Helper for `group_split_factors`. -/
503+
def IsValidBlock (X : Language α) (p q : List α) : Prop :=
504+
(p ∈ X∗ ∧ q ∈ X∗) ∨ (p ++ q ∈ X)
505+
506+
lemma block_concat_in_kstar {X : Language α} {p q : List α} (h : IsValidBlock X p q) :
507+
p ++ q ∈ X∗ := by
508+
cases h with
509+
| inl h_non_split =>
510+
simp only [Language.mem_kstar] at *
511+
rcases h_non_split with ⟨⟨L₁, rfl, hL₁⟩, ⟨L₂, rfl, hL₂⟩⟩
512+
use L₁ ++ L₂
513+
simp only [List.flatten_append, List.mem_append, true_and]
514+
rintro y (hy₁ | hy₂)
515+
· exact hL₁ y hy₁
516+
· exact hL₂ y hy₂
517+
| inr h_split =>
518+
simp only [Language.mem_kstar]
519+
use [p ++ q]
520+
simpa
521+
502522
lemma group_split_factors_aux {n : ℕ} {X : Language α} [DecidableEq α]
503523
(ps qs : List (List α))
504524
(hps_len : ps.length = n) (hqs_len : qs.length = n)
505525
(hpq_in_X : ∀ i (hi : i < n), ps[i] ++ qs[i] ∈ X)
506526
(h_indep : ∀ i j (hi : i < n) (hj : j < n), i < j → I.Independent qs[i] ps[j]) :
507527
∃ xs ys : List (List α),
508528
xs.length = ys.length ∧
509-
xs.length ≤
510-
2 * (Finset.univ.filter (fun (i : Fin n) => ps[i.val] ≠ [] ∧ qs[i.val] ≠ [])).card + 1 ∧
511-
(List.zipWith (· ++ ·) xs ys).flatten ∈ traceClosure I X∗ ∧
529+
xs.length ≤ 2 * (Finset.univ.filter (fun (i : Fin n) => ps[i.val] ≠ [] ∧ qs[i.val] ≠ [])).card + 1 ∧
530+
(∀ i (hi : i < xs.length) (hi' : i < ys.length), IsValidBlock X xs[i] ys[i] ∧
531+
(i = 0 → xs[i] ∈ X∗ ∧ ys[i] ∈ X∗)) ∧
512532
TraceEqv I ps.flatten xs.flatten ∧
513533
TraceEqv I qs.flatten ys.flatten ∧
514534
∀ (i j : ℕ) (hi : i < ys.length) (hj : j < xs.length), i < j →
@@ -519,10 +539,7 @@ lemma group_split_factors_aux {n : ℕ} {X : Language α} [DecidableEq α]
519539
have hqs : qs = [] := List.length_eq_zero_iff.mp hqs_len
520540
subst hps hqs
521541
use [[]], [[]]
522-
simp [TraceEqv.refl]
523-
unfold traceClosure
524-
use []
525-
simp [TraceEqv.refl, Language.nil_mem_kstar]
542+
simp [TraceEqv.refl, IsValidBlock, Language.nil_mem_kstar]
526543
| succ n' ih =>
527544
cases ps with | nil => contradiction | cons p ps' =>
528545
cases qs with | nil => contradiction | cons q qs' =>
@@ -534,10 +551,10 @@ lemma group_split_factors_aux {n : ℕ} {X : Language α} [DecidableEq α]
534551
have h_indep' : ∀ i j (hi : i < n') (hj : j < n'), i < j → I.Independent qs'[i] ps'[j] := by
535552
intro i j hi hj hlt
536553
simpa using h_indep (i + 1) (j + 1) (by omega) (by omega) (by omega)
537-
have ⟨xs', ys', h_len_eq, h_bound, h_zip_in, h_ps_eqv, h_qs_eqv, h_xs_indep⟩ :=
554+
have ⟨xs', ys', h_len_eq, h_bound, h_blocks, h_ps_eqv, h_qs_eqv, h_xs_indep⟩ :=
538555
ih ps' qs' hps'_len hqs'_len hpq_in_X' h_indep'
539556
by_cases h_split : p ≠ [] ∧ q ≠ []
540-
· use (p :: xs'), (q :: ys')
557+
· use ([] :: p :: xs'), ([] :: q :: ys')
541558
and_intros
542559
· simp [h_len_eq]
543560
· simp only [List.length_cons]
@@ -573,46 +590,66 @@ lemma group_split_factors_aux {n : ℕ} {X : Language α} [DecidableEq α]
573590
exact Fin.succ_ne_zero y hy_eq
574591
rw [h_card]
575592
omega
576-
· simp only [List.zipWith_cons_cons, List.flatten_cons]
577-
unfold traceClosure at h_zip_in ⊢
578-
rw [Set.mem_setOf] at h_zip_in ⊢
579-
rcases h_zip_in with ⟨x, hx, hx_eqv⟩
580-
rw [Language.mem_kstar] at hx
581-
rcases hx with ⟨L, hL, hLX⟩
582-
have hpq_append_in_X := by simpa using hpq_in_X 0 (by omega)
583-
use p ++ q ++ x
584-
constructor
585-
· rw [Language.mem_kstar]
586-
use [p ++ q] ++ L
587-
simp [hL, hpq_append_in_X]
588-
exact hLX
589-
· exact TraceEqv.compat (TraceEqv.refl _) hx_eqv
590-
· simp only [List.flatten_cons]
593+
· intro i hi hi'
594+
cases i with
595+
| zero =>
596+
simp only [List.getElem_cons_zero]
597+
simp only [Language.nil_mem_kstar, and_self, imp_self, and_true]
598+
left
599+
simp [Language.nil_mem_kstar]
600+
| succ i' =>
601+
cases i' with
602+
| zero =>
603+
simp only [List.getElem_cons_succ]
604+
constructor
605+
· right
606+
exact hpq_in_X 0 (by omega)
607+
· intro h_absurd
608+
contradiction
609+
| succ i'' =>
610+
simp only [List.getElem_cons_succ]
611+
constructor
612+
· exact (h_blocks i'' (by simpa using hi) (by simpa using hi')).left
613+
· intro h_absurd
614+
contradiction
615+
· simp only [List.flatten_cons, List.nil_append]
591616
exact TraceEqv.compat (TraceEqv.refl _) h_ps_eqv
592-
· simp only [List.flatten_cons]
617+
· simp only [List.flatten_cons, List.nil_append]
593618
exact TraceEqv.compat (TraceEqv.refl _) h_qs_eqv
594619
· intro i j hi hj hlt
595620
cases i with
596621
| zero =>
597-
cases j with
598-
| zero => contradiction
599-
| succ j' =>
600-
simp only [List.getElem_cons_zero, List.getElem_cons_succ]
601-
have hq_ps_flat : I.Independent q ps'.flatten := by
602-
intro a ha b hb
603-
simp only [List.mem_flatten] at hb
604-
rcases hb with ⟨p_k, hp_k_in, hb_in⟩
605-
rcases List.mem_iff_getElem.mp hp_k_in with ⟨k, hk_lt, rfl⟩
606-
exact h_indep 0 (k + 1) (by omega) (by omega) (by omega) a ha b hb_in
607-
have hq_xs_flat : I.Independent q xs'.flatten :=
608-
indep_of_indep_of_eqv hq_ps_flat h_ps_eqv
609-
exact indep_of_indep_flatten_right j' (by simpa using hj) hq_xs_flat
622+
simp only [List.getElem_cons_zero]
623+
intro a ha b hb
624+
cases ha
610625
| succ i' =>
611-
cases j with
612-
| zero => contradiction
613-
| succ j' =>
614-
simp only [List.getElem_cons_succ]
615-
exact h_xs_indep i' j' (by simpa using hi) (by simpa using hj) (by omega)
626+
cases i' with
627+
| zero =>
628+
cases j with
629+
| zero => contradiction
630+
| succ j' =>
631+
cases j' with
632+
| zero => contradiction
633+
| succ j'' =>
634+
simp only [List.getElem_cons_succ, List.getElem_cons_zero]
635+
have hq_ps_flat : I.Independent q ps'.flatten := by
636+
intro a ha b hb
637+
simp only [List.mem_flatten] at hb
638+
rcases hb with ⟨p_k, hp_k_in, hb_in⟩
639+
rcases List.mem_iff_getElem.mp hp_k_in with ⟨k, hk_lt, rfl⟩
640+
exact h_indep 0 (k + 1) (by omega) (by omega) (by omega) a ha b hb_in
641+
have hq_xs_flat : I.Independent q xs'.flatten :=
642+
indep_of_indep_of_eqv hq_ps_flat h_ps_eqv
643+
exact indep_of_indep_flatten_right j'' (by simpa using hj) hq_xs_flat
644+
| succ i'' =>
645+
cases j with
646+
| zero => contradiction
647+
| succ j' =>
648+
cases j' with
649+
| zero => contradiction
650+
| succ j'' =>
651+
simp only [List.getElem_cons_succ]
652+
exact h_xs_indep i'' j'' (by simpa using hi) (by simpa using hj) (by omega)
616653
· rcases xs' with _ | ⟨x_head, xs_tail⟩
617654
· have h_ys_nil : ys' = [] := by
618655
cases ys'
@@ -623,17 +660,26 @@ lemma group_split_factors_aux {n : ℕ} {X : Language α} [DecidableEq α]
623660
and_intros
624661
· rfl
625662
· simp only [List.length_singleton]; omega
626-
· simp only [List.zipWith_cons_cons, List.zipWith_self, List.map_nil, List.flatten_cons,
627-
List.flatten_nil, List.append_nil]
628-
unfold traceClosure
629-
rw [Set.mem_setOf]
630-
have hpq_append_in_X := by simpa using hpq_in_X 0 (by omega)
631-
use p ++ q
632-
constructor
633-
· rw [Language.mem_kstar]
634-
use [p ++ q]
635-
simp [hpq_append_in_X]
636-
· exact TraceEqv.refl _
663+
· intro i hi hi'
664+
cases i with
665+
| zero =>
666+
simp only [List.getElem_cons_zero]
667+
constructor
668+
· right
669+
exact hpq_in_X 0 (by omega)
670+
· simp only [forall_const]
671+
rcases (by simpa using not_and_or.mp h_split) with rfl | rfl
672+
· have hq := by simpa using hpq_in_X 0 (by omega)
673+
constructor
674+
· apply Language.nil_mem_kstar
675+
· rw [Language.mem_kstar]
676+
exact ⟨[q], by simp [hq]⟩
677+
· have hp := by simpa using hpq_in_X 0 (by omega)
678+
constructor
679+
· rw [Language.mem_kstar]
680+
exact ⟨[p], by simp [hp]⟩
681+
· apply Language.nil_mem_kstar
682+
| succ i' => contradiction
637683
· simp only [List.flatten_cons, List.flatten_nil, List.append_nil]
638684
have h1 : TraceEqv I (p ++ ps'.flatten) (p ++ []) := TraceEqv.compat (TraceEqv.refl _) h_ps_eqv
639685
rw [List.append_nil] at h1
@@ -677,46 +723,49 @@ lemma group_split_factors_aux {n : ℕ} {X : Language α} [DecidableEq α]
677723
rw [h_S_eq, Finset.card_image_of_injective _ (Fin.succ_injective _)]
678724
rw [h_card]
679725
exact h_bound
680-
· simp only [List.zipWith_cons_cons, List.flatten_cons]
681-
unfold traceClosure at h_zip_in ⊢
682-
rw [Set.mem_setOf] at h_zip_in ⊢
683-
rcases h_zip_in with ⟨x, hx, hx_eqv⟩
684-
have hpq_append_in_X := by simpa using hpq_in_X 0 (by omega)
685-
use p ++ q ++ x
686-
constructor
687-
· rw [Language.mem_kstar] at hx ⊢
688-
rcases hx with ⟨L, hL, hLX⟩
689-
use [p ++ q] ++ L
690-
simp [hL, hpq_append_in_X]
691-
exact hLX
692-
· have hq_ps_flat : I.Independent q ps'.flatten := by
693-
intro a ha b hb
694-
simp only [List.mem_flatten] at hb
695-
rcases hb with ⟨p_k, hp_k_in, hb_in⟩
696-
rcases List.mem_iff_getElem.mp hp_k_in with ⟨k, hk_lt, rfl⟩
697-
exact h_indep 0 (k + 1) (by omega) (by omega) (by omega) a ha b hb_in
698-
have hq_xs_flat := indep_of_indep_of_eqv hq_ps_flat h_ps_eqv
699-
have hq_xhead : I.Independent q x_head := by
700-
intro a ha b hb
701-
have hb_flat : b ∈ (x_head :: xs_tail).flatten := by
702-
simp only [List.flatten_cons, List.mem_append]
703-
exact Or.inl hb
704-
exact hq_xs_flat a ha b hb_flat
705-
have h_list_eq1 : (((p ++ x_head) ++ (q ++ y_head)) ++ (List.zipWith (fun x1 x2 => x1 ++ x2) xs_tail ys_tail).flatten) =
706-
(p ++ ((x_head ++ q) ++ y_head) ++ (List.zipWith (fun x1 x2 => x1 ++ x2) xs_tail ys_tail).flatten) := by simp
707-
rw [h_list_eq1]
708-
have h_swap : TraceEqv I (x_head ++ q) (q ++ x_head) := (comm_append_of_indep hq_xhead).symm
709-
have h_swap2 : TraceEqv I ((x_head ++ q) ++ y_head) ((q ++ x_head) ++ y_head) := TraceEqv.compat h_swap (TraceEqv.refl _)
710-
have h_swap3 : TraceEqv I (p ++ ((x_head ++ q) ++ y_head)) (p ++ ((q ++ x_head) ++ y_head)) := TraceEqv.compat (TraceEqv.refl _) h_swap2
711-
have h_swap4 : TraceEqv I ((p ++ ((x_head ++ q) ++ y_head)) ++ (List.zipWith (fun x1 x2 => x1 ++ x2) xs_tail ys_tail).flatten)
712-
((p ++ ((q ++ x_head) ++ y_head)) ++ (List.zipWith (fun x1 x2 => x1 ++ x2) xs_tail ys_tail).flatten) :=
713-
TraceEqv.compat h_swap3 (TraceEqv.refl _)
714-
have h_list_eq2 : (p ++ ((q ++ x_head) ++ y_head) ++ (List.zipWith (fun x1 x2 => x1 ++ x2) xs_tail ys_tail).flatten) =
715-
((p ++ q) ++ ((x_head ++ y_head) ++ (List.zipWith (fun x1 x2 => x1 ++ x2) xs_tail ys_tail).flatten)) := by simp
716-
have h_final : TraceEqv I ((p ++ q) ++ ((x_head ++ y_head) ++ (List.zipWith (fun x1 x2 => x1 ++ x2) xs_tail ys_tail).flatten))
717-
((p ++ q) ++ x) := TraceEqv.compat (TraceEqv.refl _) hx_eqv.symm
718-
rw [h_list_eq2] at h_swap4
719-
exact h_final.symm.trans h_swap4.symm
726+
· intro i hi hi'
727+
cases i with
728+
| zero =>
729+
simp only [List.getElem_cons_zero]
730+
rcases (by simpa using not_and_or.mp h_split) with rfl | rfl
731+
· have hq := by simpa using hpq_in_X 0 (by simp)
732+
have h_head := (h_blocks 0 (by simp) (by simp)).right rfl
733+
rcases h_head with ⟨hx_head, hy_head⟩
734+
simp only [List.getElem_cons_zero] at hx_head hy_head
735+
rcases hy_head with ⟨L, rfl, hL⟩
736+
constructor
737+
· left
738+
use hx_head
739+
use [q] ++ L
740+
simp only [List.cons_append, List.nil_append, List.flatten_cons, List.mem_cons,
741+
forall_eq_or_imp, hq, true_and]
742+
exact hL
743+
· simp only [List.nil_append, hx_head, true_and, forall_const]
744+
use [q] ++ L
745+
simp only [List.cons_append, List.nil_append, List.flatten_cons, List.mem_cons,
746+
forall_eq_or_imp, hq, true_and]
747+
exact hL
748+
· have hp := by simpa using hpq_in_X 0 (by simp)
749+
have h_head := (h_blocks 0 (by simp) (by simp)).right rfl
750+
rcases h_head with ⟨hx_head, hy_head⟩
751+
simp only [List.getElem_cons_zero] at hx_head hy_head
752+
rcases hx_head with ⟨L, rfl, hL⟩
753+
constructor
754+
· left
755+
constructor
756+
· use [p] ++ L
757+
simp only [List.cons_append, List.nil_append, List.flatten_cons, List.mem_cons,
758+
forall_eq_or_imp, hp, true_and]
759+
exact hL
760+
· simp [hy_head]
761+
· simp only [List.nil_append, hy_head, and_true, forall_const]
762+
use [p] ++ L
763+
simp only [List.cons_append, List.nil_append, List.flatten_cons, List.mem_cons,
764+
forall_eq_or_imp, hp, true_and]
765+
exact hL
766+
| succ i' =>
767+
simp only [List.getElem_cons_succ]
768+
simpa using h_blocks (i' + 1) (by simpa using hi) (by simpa using hi')
720769
· simp only [List.flatten_cons]
721770
rw [List.append_assoc]
722771
exact TraceEqv.compat (TraceEqv.refl _) h_ps_eqv
@@ -752,6 +801,36 @@ lemma group_split_factors_aux {n : ℕ} {X : Language α} [DecidableEq α]
752801
simp only [List.getElem_cons_succ]
753802
exact h_xs_indep (i' + 1) (j' + 1) (by simpa using hi) (by simpa using hj) (by omega)
754803

804+
lemma flatten_mem_kstar {X : Language α} (L : List (List α)) (h : ∀ w ∈ L, w ∈ X∗) :
805+
L.flatten ∈ X∗ := by
806+
induction L with
807+
| nil => simp [Language.nil_mem_kstar]
808+
| cons w L' ih =>
809+
simp only [Language.mem_kstar, List.flatten_cons]
810+
simp only [List.mem_cons, forall_eq_or_imp] at h
811+
rcases h.left with ⟨L₁, rfl, hL₁⟩
812+
rcases ih h.right with ⟨L₂, heq, hL₂⟩
813+
use L₁ ++ L₂
814+
rw [heq]
815+
simp only [List.flatten_append, List.mem_append, true_and]
816+
rintro y (hy₁ | hy₂)
817+
· exact hL₁ y hy₁
818+
· exact hL₂ y hy₂
819+
820+
lemma zipWith_append_mem_kstar {X : Language α} {xs ys : List (List α)}
821+
(h_len : xs.length = ys.length)
822+
(h_blocks : ∀ i (hi : i < xs.length) (hi' : i < ys.length), IsValidBlock X xs[i] ys[i] ∧
823+
(i = 0 → xs[i] ∈ X∗ ∧ ys[i] ∈ X∗)) :
824+
(List.zipWith (· ++ ·) xs ys).flatten ∈ X∗ := by
825+
apply flatten_mem_kstar
826+
intro w hw
827+
rcases List.mem_iff_getElem.mp hw with ⟨i, hi_zip, rfl⟩
828+
have hi_xs : i < xs.length := by
829+
rw [List.length_zipWith, h_len, min_self, ← h_len] at hi_zip
830+
exact hi_zip
831+
rw [List.getElem_zipWith]
832+
exact block_concat_in_kstar (h_blocks i hi_xs (by simp_all)).left
833+
755834
lemma group_split_factors
756835
{x y : List α} {X : Language α} {n : ℕ} {ps qs : List (List α)} [Fintype α] [DecidableEq α]
757836
(hps_len : ps.length = n) (hqs_len : qs.length = n)
@@ -764,13 +843,14 @@ lemma group_split_factors
764843
∃ xs ys : List (List α),
765844
xs.length ≤ 2 * Fintype.card α + 1 ∧
766845
IsValidFactorization I X∗ x y xs ys := by
767-
have ⟨xs, ys, h_len_eq, h_len_bound, h_zip_in, h_ps_eqv, h_qs_eqv, h_xs_indep⟩ :=
846+
have ⟨xs, ys, h_len_eq, h_len_bound, h_blocks, h_ps_eqv, h_qs_eqv, h_xs_indep⟩ :=
768847
group_split_factors_aux ps qs hps_len hqs_len hpq_in_X h_indep
769848
use xs, ys
770849
constructor
771850
· omega
772851
· unfold IsValidFactorization
773-
refine ⟨h_len_eq, h_zip_in, ?_, ?_, h_xs_indep⟩
852+
refine ⟨h_len_eq, ?_, ?_, ?_, h_xs_indep⟩
853+
· exact zipWith_append_mem_kstar h_len_eq h_blocks
774854
· exact TraceEqv.trans hx_eqv h_ps_eqv
775855
· exact TraceEqv.trans hy_eqv h_qs_eqv
776856

0 commit comments

Comments
 (0)