Skip to content

Commit e550d82

Browse files
yisioxyisiox
committed
Clean-up up to fact 1.9
1 parent 607adb8 commit e550d82

1 file changed

Lines changed: 332 additions & 32 deletions

File tree

‎TraceTheory/TraceTheory/Trace.lean‎

Lines changed: 332 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -1,63 +1,363 @@
11
import Mathlib.Data.Fintype.Basic
22
import TraceTheory.Basic
33

4-
variable {α : Type*} [DecidableEq α] [Fintype α]
4+
variable {α : Type*} [DecidableEq α]
55

66
namespace Trace
77

8-
/--
9-
A dependence relation is a finite, reflexive, and symmetric relation.
10-
-/
11-
structure Dependence where
8+
/-- A dependence relation is a finite, reflexive, and symmetric relation. -/
9+
structure Dependence (α : Type*) where
1210
rel : α → α → Prop
1311
refl : ∀ a, rel a a
1412
symm: ∀ a b, rel a b → rel b a
1513

16-
/--
17-
An independence relation is a finite, irreflexive, and symmetric relation.
18-
-/
19-
structure Independence where
14+
/-- An independence relation is a finite, irreflexive, and symmetric relation. -/
15+
structure Independence (α : Type*) where
2016
rel : α → α → Prop
2117
irrefl : ∀ a, ¬ rel a a
2218
symm : ∀ a b, rel a b → rel b a
2319

24-
variable {I : Independence}
20+
/-- The Independency relation induced by a Dependency `D`. -/
21+
def inducedIndependency {α : Type*} (D : Dependence α) : Independence α :=
22+
{ rel := fun a b => ¬ D.rel a b,
23+
irrefl := by
24+
intro a h
25+
exact h (D.refl a),
26+
symm := by
27+
intro a b h
28+
exact h ∘ (D.symm b a) }
29+
30+
variable {I : Independence α}
2531

2632
variable (I) in
2733
/--
28-
The trace equivalence relation is the smallest congruence relation induced by the independence relation `I.r`.
29-
Two traces (i.e. lists of symbols) are equivalent if one can be transformed into the other by a finite sequence of swaps of adjacent independent symbols.
30-
31-
The relation is inductively generated by:
32-
- **Swap:** If `I.r a b`, then `[a, b]` is equivalent to `[b, a]` (swapping adjacent independent symbols).
33-
- **Reflexivity:** Every word is equivalent to itself.
34-
- **Symmetry:** If `t₁` is equivalent to `t₂`, then `t₂` is equivalent to `t₁`.
35-
- **Transitivity:** If `t₁` is equivalent to `t₂` and `t₂` is equivalent to `t₃`, then `t₁` is equivalent to `t₃`.
36-
- **Compatibility:** If `t₁` is equivalent to `t₂` and `t₃` is equivalent to `t₄`, then `t₁ ++ t₃` is equivalent to `t₂ ++ t₄`.
34+
The trace equivalence relation is the least congruence $\equiv$ such that for all symbols
35+
$a$ and $b$, $(a,b) \in I \leftrightarrow ab \equiv ba$.
36+
37+
Intuitively, two strings (lists of symbols) are equivalent if one can be transformed into the other
38+
by a finite sequence of swaps of adjacent independent symbols.
39+
40+
The relation is inductively generated by:
41+
- **Swap:** If `I.rel a b`, then `[a, b]` is equivalent to `[b, a]` (swapping adjacent independent
42+
symbols).
43+
- **Reflexivity:** Every word is equivalent to itself.
44+
- **Symmetry:** If `w₁` is equivalent to `w₂`, then `w₂` is equivalent to `w₁`.
45+
- **Transitivity:** If `w₁` is equivalent to `w₂` and `w₂` is equivalent to `w₃`, then `w₁` is
46+
equivalent to `w₃`.
47+
- **Compatibility:** If `w₁` is equivalent to `w₂` and `w₃` is equivalent to `w₄`, then `w₁ ++ w₃`
48+
is equivalent to `w₂ ++ w₄`.
3749
-/
3850
inductive TraceEquiv : List α → List α → Prop
3951
| swap : ∀ a b, I.rel a b → TraceEquiv [a, b] [b, a]
40-
| refl : ∀ t₁, TraceEquiv t₁ t₁
41-
| symm : ∀ {t₁ t₂}, TraceEquiv t₁ t₂ → TraceEquiv t₂ t₁
42-
| trans : ∀ {t₁ t₂ t₃}, TraceEquiv t₁ t₂ → TraceEquiv t₂ t₃ → TraceEquiv t₁ t₃
43-
| compat : ∀ {t₁ t₂ t₃ t₄}, TraceEquiv t₁ t₂ → TraceEquiv t₃ t₄ → TraceEquiv (t₁ ++ t₃) (t₂ ++ t₄)
52+
| refl : ∀ w₁, TraceEquiv w₁ w₁
53+
| symm : ∀ {w₁ w₂}, TraceEquiv w₁ w₂ → TraceEquiv w₂ w₁
54+
| trans : ∀ {w₁ w₂ w₃}, TraceEquiv w₁ w₂ → TraceEquiv w₂ w₃ → TraceEquiv w₁ w₃
55+
| compat : ∀ {w₁ w₂ w₃ w₄}, TraceEquiv w₁ w₂ → TraceEquiv w₃ w₄ → TraceEquiv (w₁ ++ w₃) (w₂ ++ w₄)
4456

45-
omit [DecidableEq α] [Fintype α] in
57+
omit [DecidableEq α] in
4658
variable (I) in
4759
@[simp]
48-
lemma trace_equiv_length_eq {t₁ t₂ : List α} :
49-
TraceEquiv I t₁ t₂ → t₁.length = t₂.length := by
60+
lemma equiv_implies_length_eq {w₁ w₂ : List α} :
61+
TraceEquiv I w₁ w₂ → w₁.length = w₂.length := by
5062
intro h
5163
induction h with
5264
| swap _ _ _ =>
5365
rfl
5466
| refl _ =>
5567
rfl
56-
| symm _ IH =>
57-
exact Eq.symm IH
58-
| trans _ _ IH₁ IH₂ =>
59-
exact Eq.trans IH₁ IH₂
60-
| compat _ _ IH₁ IH₂ =>
61-
simp [IH₁, IH₂]
68+
| symm _ ih =>
69+
exact ih.symm
70+
| trans _ _ ih₁ ih₂ =>
71+
exact ih₁.trans ih₂
72+
| compat _ _ ih₁ ih₂ =>
73+
simp [ih₁, ih₂]
74+
75+
omit [DecidableEq α] in
76+
variable (I) in
77+
@[simp]
78+
lemma equiv_implies_alph_eq {w₁ w₂ : List α} (a : α) :
79+
TraceEquiv I w₁ w₂ → (a ∈ w₁ ↔ a ∈ w₂) := by
80+
intro h
81+
induction h with
82+
| swap _ _ _ =>
83+
simp
84+
exact Or.comm
85+
| refl _ =>
86+
exact Eq.to_iff rfl
87+
| symm _ ih =>
88+
exact Iff.symm ih
89+
| trans _ _ ih₁ ih₂ =>
90+
exact ih₁.trans ih₂
91+
| compat _ _ ih₁ ih₂ =>
92+
simp
93+
exact or_congr ih₁ ih₂
94+
95+
omit [DecidableEq α] in
96+
variable (I) in
97+
@[simp]
98+
lemma mirror_rule {w₁ w₂ : List α} (h : TraceEquiv I w₁ w₂) : -- (1.6)
99+
TraceEquiv I w₁.reverse w₂.reverse := by
100+
induction h with
101+
| swap a b h =>
102+
simp
103+
exact TraceEquiv.swap b a (I.symm a b h)
104+
| refl w₁' =>
105+
exact TraceEquiv.refl w₁'.reverse
106+
| symm _ ih =>
107+
exact ih.symm
108+
| trans _ _ ih₁ ih₂ =>
109+
exact ih₁.trans ih₂
110+
| compat _ _ ih₁ ih₂ =>
111+
simp
112+
exact ih₂.compat ih₁
113+
114+
@[simp]
115+
lemma cancel_right_over_concat {w₁ w₂ : List α} (a : α) :
116+
(w₁ ++ w₂).cancel_right a =
117+
if (a ∈ w₂) then
118+
w₁ ++ w₂.cancel_right a
119+
else
120+
w₁.cancel_right a ++ w₂ := by
121+
induction w₂ using List.induction_right with
122+
| nil =>
123+
simp
124+
| snoc w₂' a' ih =>
125+
nth_rw 1 [← List.append_assoc]
126+
by_cases ha : a ∈ w₂'
127+
all_goals
128+
by_cases heq : a = a'
129+
· rw [List.cancel_right_snoc]
130+
simp [heq]
131+
· rw [List.cancel_right_snoc]
132+
simp [ha, heq, ih]
133+
134+
variable (I) in
135+
lemma cancellation_property {w₁ w₂ : List α} (a : α) (h : TraceEquiv I w₁ w₂) : -- (1.7)
136+
TraceEquiv I (w₁.cancel_right a) (w₂.cancel_right a) := by
137+
induction h with
138+
| swap b c hbc =>
139+
by_cases hab : a = b <;> by_cases hac : a = c
140+
· rw [← hab, ← hac]
141+
exact TraceEquiv.refl _
142+
· rw [← hab]
143+
simp [List.cancel_right, hac]
144+
exact TraceEquiv.refl _
145+
· rw [← hac]
146+
simp [List.cancel_right, hab]
147+
exact TraceEquiv.refl _
148+
· simp [List.cancel_right, hab, hac]
149+
exact TraceEquiv.swap b c hbc
150+
| refl _ =>
151+
exact TraceEquiv.refl _
152+
| symm _ ih =>
153+
exact ih.symm
154+
| trans _ _ ih₁ ih₂ =>
155+
exact ih₁.trans ih₂
156+
| compat t₁ t₂ ih₁ ih₂ =>
157+
rename_i l₃ _
158+
by_cases hal₃ : a ∈ l₃
159+
· have hal₄ := (equiv_implies_alph_eq I a t₂).mp hal₃
160+
simp [hal₃, hal₄]
161+
exact t₁.compat ih₂
162+
· have hal₄ := (equiv_implies_alph_eq I a t₂).mpr.mt hal₃
163+
simp [hal₃, hal₄]
164+
exact ih₁.compat t₂
165+
166+
variable (I) in
167+
@[simp]
168+
lemma projection_rule {w₁ w₂ : List α} (Sigma : Alphabet α) (h : TraceEquiv I w₁ w₂) : -- (1.8)
169+
TraceEquiv I (w₁.proj Sigma) (w₂.proj Sigma) := by
170+
induction h with
171+
| swap a b h =>
172+
by_cases ha : a ∈ Sigma <;> by_cases hb : b ∈ Sigma
173+
all_goals (
174+
simp [List.proj, ha, hb]
175+
try exact TraceEquiv.swap a b h
176+
try exact TraceEquiv.refl _
177+
)
178+
| refl _ =>
179+
exact TraceEquiv.refl _
180+
| symm _ ih =>
181+
exact ih.symm
182+
| trans _ _ ih₁ ih₂ =>
183+
exact ih₁.trans ih₂
184+
| compat _ _ ih₁ ih₂ =>
185+
simp
186+
exact ih₁.compat ih₂
187+
188+
@[simp] -- TODO: move this to basic
189+
lemma singleton_cancel_right {a : α} : [a].cancel_right a = [] := by
190+
rw [← List.nil_append [a], List.cancel_right_snoc]
191+
simp
192+
193+
variable (I) in
194+
lemma equiv_of_length_two {a b : α} {w : List α} (h : TraceEquiv I [a, b] w) :
195+
w = [a, b] ∨ w = [b, a] := by
196+
have h_len := List.length_eq_two.mp (equiv_implies_length_eq I h).symm
197+
rcases h_len with ⟨c, d, hw⟩
198+
rw [hw] at h ⊢
199+
by_cases heq : a = b
200+
· subst heq
201+
have hc : c = a := by
202+
have h' := (equiv_implies_alph_eq I c h.symm).mp
203+
simp at h'
204+
exact h'
205+
have hd : d = a := by
206+
have h' := (equiv_implies_alph_eq I d h.symm).mp
207+
simp at h'
208+
exact h'
209+
simp [hc, hd]
210+
· have ha : a = c ∨ a = d := by
211+
have h' := (equiv_implies_alph_eq I a h).mp
212+
simp at h'
213+
exact h'
214+
have hb : b = c ∨ b = d := by
215+
have h' := (equiv_implies_alph_eq I b h).mp
216+
simp at h'
217+
exact h'
218+
rcases ha with hac | had <;> rcases hb with hbc | hbd
219+
· rw [← hbc] at hac
220+
contradiction
221+
· left
222+
simp [hac, hbd]
223+
· right
224+
simp [had, hbc]
225+
· rw [← hbd] at had
226+
contradiction
227+
228+
omit [DecidableEq α] in
229+
variable (I) in
230+
@[simp]
231+
lemma equiv_of_singletons {a b : α} (h : TraceEquiv I [a] [b]) : a = b := by
232+
generalize hx : ([a] : List α) = x at h
233+
generalize hy : ([b] : List α) = y at h
234+
induction h generalizing a b with
235+
| swap _ _ _ =>
236+
simp at hx
237+
| refl _ =>
238+
simp [← hy] at hx
239+
exact hx
240+
| symm _ ih =>
241+
exact (ih hy hx).symm
242+
| trans t₁ t₂ _ _ =>
243+
have ht₁ := equiv_implies_alph_eq I a t₁
244+
have ht₂ := equiv_implies_alph_eq I a t₂
245+
have h_trans := ht₁.trans ht₂
246+
rw [← hx, ← hy] at h_trans
247+
simp at h_trans
248+
exact h_trans
249+
| compat t₁ t₂ ih₁ ih₂ =>
250+
rcases List.singleton_eq_append_iff.mp hx with ⟨hl₁, hl₃⟩ | ⟨hl₁, hl₃⟩
251+
<;> rcases List.singleton_eq_append_iff.mp hy with ⟨hl₂, hl₄⟩ | ⟨hl₂, hl₄⟩
252+
· exact ih₂ hl₃.symm hl₄.symm
253+
· have h_t₁ := equiv_implies_length_eq I t₁
254+
rw [hl₁, hl₂] at h_t₁
255+
contradiction
256+
· have h_t₁ := equiv_implies_length_eq I t₁
257+
rw [hl₁, hl₂] at h_t₁
258+
contradiction
259+
· exact ih₁ hl₁.symm hl₂.symm
260+
261+
variable (I) in
262+
lemma equiv_and_ne_implies_independence {a b : α} (h : TraceEquiv I [a, b] [b, a]) (hne: a ≠ b):
263+
I.rel a b := by
264+
generalize hx : ([a, b] : List α) = x at h
265+
generalize hy : ([b, a] : List α) = y at h
266+
induction h generalizing a b with
267+
| swap c d r =>
268+
injection hx with ha
269+
injection hy with hb
270+
rw [ha, hb]
271+
exact r
272+
| refl _ =>
273+
injection hx.trans hy.symm with heq
274+
contradiction
275+
| symm _ ih =>
276+
exact I.symm b a (ih (hne.symm) hy hx)
277+
| trans t₁ _ ih₁ ih₂ =>
278+
rename_i t _
279+
rw [← hx] at t₁
280+
have ht := equiv_of_length_two I t₁
281+
rcases ht with h_tab | h_tba
282+
· exact ih₂ hne h_tab.symm hy
283+
· exact ih₁ hne hx h_tba.symm
284+
| compat t₁ t₂ ih₁ ih₂ =>
285+
rename_i l₁ l₂ l₃ l₄
286+
have h_l₁l₃ : l₁.length + l₃.length = 2 := by simp [← List.length_append, ← hx]
287+
have h_l₂l₄ : l₂.length + l₄.length = 2 := by simp [← List.length_append, ← hy]
288+
have h_t₁ := equiv_implies_length_eq I t₁
289+
have h_t₂ := equiv_implies_length_eq I t₂
290+
rcases Nat.add_eq_two_iff.mp h_l₁l₃ with ⟨hl₁, hl₃⟩ | ⟨hl₁, hl₃⟩ | ⟨hl₁, hl₃⟩
291+
<;> rcases Nat.add_eq_two_iff.mp h_l₂l₄ with ⟨hl₂, hl₄⟩ | ⟨hl₂, hl₄⟩ | ⟨hl₂, hl₄⟩
292+
· rw [List.length_eq_zero_iff.mp hl₁, List.nil_append] at hx
293+
rw [List.length_eq_zero_iff.mp hl₂, List.nil_append] at hy
294+
exact ih₂ hne hx hy
295+
· rw [hl₁, hl₂] at h_t₁
296+
contradiction
297+
. rw [hl₁, hl₂] at h_t₁
298+
contradiction
299+
· rw [hl₁, hl₂] at h_t₁
300+
contradiction
301+
· rcases List.length_eq_one_iff.mp hl₁ with ⟨c, hc⟩
302+
rcases List.length_eq_one_iff.mp hl₂ with ⟨d, hd⟩
303+
simp [hc] at hx
304+
simp [hd] at hy
305+
rw [hc, hd] at t₁
306+
have h_cd := equiv_of_singletons I t₁
307+
rw [← hx.left, ← hy.left] at h_cd
308+
contradiction
309+
· rw [hl₁, hl₂] at h_t₁
310+
contradiction
311+
· rw [hl₁, hl₂] at h_t₁
312+
contradiction
313+
· rw [hl₁, hl₂] at h_t₁
314+
contradiction
315+
· rw [List.length_eq_zero_iff.mp hl₃, List.append_nil] at hx
316+
rw [List.length_eq_zero_iff.mp hl₄, List.append_nil] at hy
317+
exact ih₁ hne hx hy
318+
319+
variable (I) in
320+
lemma equiv_of_swapping_tail_implies_tail_is_equiv {w : List α} {a b : α}
321+
(h : TraceEquiv I (w ++ [a, b]) (w ++ [b, a])) :
322+
TraceEquiv I [a, b] [b, a] := by
323+
induction w with
324+
| nil =>
325+
simp at h
326+
exact h
327+
| cons c w' ih =>
328+
simp at h
329+
have h' := mirror_rule I (cancellation_property I c (mirror_rule I h))
330+
simp [List.cancel_right] at h'
331+
exact ih h'
332+
333+
variable (I) in
334+
lemma tail_lemma {u v : List α} {a b : α}
335+
(h_ua_vb : TraceEquiv I (u ++ [a]) (v ++ [b])) (hne : a ≠ b) : -- (1.9)
336+
I.rel a b ∧ ∃ w, TraceEquiv I u (w ++ [b]) ∧ TraceEquiv I v (w ++ [a]) := by
337+
have h_ub_va : TraceEquiv I (u.cancel_right b) (v.cancel_right a) := by
338+
have h_cancel := cancellation_property I b (cancellation_property I a h_ua_vb)
339+
simp [hne] at h_cancel
340+
exact h_cancel
341+
have h_u_wb : TraceEquiv I u (v.cancel_right a ++ [b]) := by
342+
have h_cancel := cancellation_property I a h_ua_vb
343+
simp [hne] at h_cancel
344+
exact h_cancel
345+
have h_v_wa : TraceEquiv I v (u.cancel_right b ++ [a]) := by
346+
have h_cancel := cancellation_property I b h_ua_vb
347+
simp [hne.symm] at h_cancel
348+
exact h_cancel.symm
349+
have hu : TraceEquiv I u (u.cancel_right b ++ [b]) :=
350+
h_u_wb.trans (h_ub_va.compat (TraceEquiv.refl [b])).symm
351+
have h_ua : TraceEquiv I (u ++ [a]) (u.cancel_right b ++ [b] ++ [a]) :=
352+
hu.compat (TraceEquiv.refl [a])
353+
have h_vb : TraceEquiv I (v ++ [b]) (u.cancel_right b ++ [a] ++ [b]) :=
354+
h_v_wa.compat (TraceEquiv.refl [b])
355+
have h_tail : TraceEquiv I (u.cancel_right b ++ [a, b]) (u.cancel_right b ++ [b, a]) := by
356+
have h' := h_vb.symm.trans (h_ua_vb.symm.trans h_ua)
357+
simp at h'
358+
exact h'
359+
have h_ab_ba : TraceEquiv I [a, b] [b, a] :=
360+
equiv_of_swapping_tail_implies_tail_is_equiv I h_tail
361+
exact ⟨equiv_and_ne_implies_independence I h_ab_ba hne, ⟨u.cancel_right b, ⟨hu, h_v_wa⟩⟩⟩
62362

63363
end Trace

0 commit comments

Comments
 (0)