@@ -2,6 +2,8 @@ import Mathlib.Algebra.FreeMonoid.Basic
22import Mathlib.GroupTheory.Congruence.Basic
33import TraceTheory.List
44
5+ open FreeMonoid
6+
57namespace TraceTheory
68
79variable {α : Type *}
@@ -32,22 +34,123 @@ def inducedIndependence {α : Type*} (D : Dependence α) : Independence α where
3234
3335instance : Coe α (FreeMonoid α) := ⟨FreeMonoid.of⟩
3436
37+ attribute [coe] FreeMonoid.of
38+
3539/-- The binary relation $~$ such that $u~v$ if and only if there exists strings $x,y$ and symbols
36- $a,b$ such that $u=xaby$ and $v=xbay$. -/
40+ $a,b$ such that $aIb$, $ u=xaby$ and $v=xbay$. -/
3741inductive SwapOnce (I : Independence α) : FreeMonoid α → FreeMonoid α → Prop
3842 | swap (a b : α) : I.rel a b → SwapOnce I (↑a * ↑b) (↑b * ↑a)
3943
40- /-- Trace equivalence as the least congruence containing $~$. -/
41- def traceCon (I : Independence α) : Con (FreeMonoid α) := conGen (SwapOnce I)
44+ /-- Trace equivalence defined as the least congruence containing $~$. -/
45+ def TraceEqv (I : Independence α) : Con (FreeMonoid α) := conGen (SwapOnce I)
4246
43- /-- The trace monoid. -/
44- def TraceMonoid (I : Independence α) := (traceCon I).Quotient
47+ /-- The trace monoid defined as the quotient of the free monoid by the trace equivalence relation
48+ induced by `I`. -/
49+ def TraceMonoid (I : Independence α) := (TraceEqv I).Quotient
4550
4651variable {I : Independence α}
4752
48- instance : Monoid (TraceMonoid I) := (traceCon I).monoid
53+ instance : Monoid (TraceMonoid I) := (TraceEqv I).monoid
54+
55+ theorem length_eq_of_eqv {u v : FreeMonoid α} (h : TraceEqv I u v) : u.length = v.length := by
56+ induction h with
57+ | of _ _ h_swap => cases h_swap; simp
58+ | refl w => rfl
59+ | symm _ ih => simp [ih]
60+ | trans _ _ ih₁ ih₂ => simp [ih₁, ih₂]
61+ | mul _ _ ih₁ ih₂ => simp [ih₁, ih₂]
62+
63+ theorem mem_iff_mem {u v : FreeMonoid α} (a : α) (h : TraceEqv I u v) : a ∈ u ↔ a ∈ v := by
64+ induction h with
65+ | of _ _ h_swap => cases h_swap; simp [mem_mul, mem_of, Or.comm]
66+ | refl w => rfl
67+ | symm _ ih => simp [ih]
68+ | trans _ _ ih₁ ih₂ => simp [ih₁, ih₂]
69+ | mul _ _ ih₁ ih₂ => simp [ih₁, ih₂]
70+
71+ theorem rev_eqv_of_eqv {u v : FreeMonoid α} (h : TraceEqv I u v) :
72+ TraceEqv I u.reverse v.reverse := by
73+ induction h with
74+ | of _ _ h_swap =>
75+ cases h_swap with
76+ | swap a b h_indep =>
77+ simp only [reverse_mul]
78+ apply ConGen.Rel.of
79+ exact SwapOnce.swap b a (I.symm _ _ h_indep)
80+ | refl _ => apply (TraceEqv I).refl
81+ | symm _ ih => exact ih.symm
82+ | trans _ _ ih₁ ih₂ => exact ih₁.trans ih₂
83+ | mul _ _ ih₁ ih₂ =>
84+ simp only [reverse_mul]
85+ exact ih₂.mul ih₁
86+
87+ theorem proj_eqv_of_eqv {u v : FreeMonoid α} {S : Finset α} [DecidableEq α] (h : TraceEqv I u v) :
88+ TraceEqv I (proj S u) (proj S v) := by
89+ sorry
90+
91+ theorem of_mul_cancel_left {a : α} {u v : FreeMonoid α} [DecidableEq α]
92+ (h : TraceEqv I (↑a * u) (↑a * v)) :
93+ TraceEqv I u v := by
94+ sorry
4995
50- theorem length_eq_of_con {u v : FreeMonoid α} (h : traceCon I u v) : u.length = v.length := by
96+ theorem of_mul_cancel_right {a : α} {u v : FreeMonoid α} [DecidableEq α]
97+ (h : TraceEqv I (u * ↑a) (v * ↑a)) :
98+ TraceEqv I u v := by
5199 sorry
52100
101+ theorem mul_cancel_left {w u v : FreeMonoid α} [DecidableEq α] (h : TraceEqv I (w * u) (w * v)) :
102+ TraceEqv I u v := by
103+ induction w using recOn with
104+ | h0 => exact h
105+ | ih _ _ ih =>
106+ rw [mul_assoc, mul_assoc] at h
107+ exact ih (of_mul_cancel_left h)
108+
109+ theorem mul_cancel_right {w u v : FreeMonoid α} [DecidableEq α] (h : TraceEqv I (u * w) (v * w)) :
110+ TraceEqv I u v := by
111+ induction w using List.reverseRecOn with
112+ | nil =>
113+ change TraceEqv I (u * 1 ) (v * 1 ) at h
114+ simp_all [mul_one]
115+ | append_singleton w' a ih =>
116+ change (TraceEqv I) (u * (↑w' * ↑a)) (v * (↑w' * ↑a)) at h
117+ rw [← mul_assoc, ← mul_assoc] at h
118+ exact ih (of_mul_cancel_right h)
119+
120+ instance [DecidableEq α] : CancelMonoid (TraceMonoid I) where
121+ mul_left_cancel := by
122+ intro a b c heq
123+ induction a using Quotient.inductionOn with | h a =>
124+ induction b using Quotient.inductionOn with | h b =>
125+ induction c using Quotient.inductionOn with | h c =>
126+ apply Quotient.sound
127+ simp only at heq
128+ have heqv := by simpa using Quotient.exact heq
129+ exact mul_cancel_left heqv
130+ mul_right_cancel := by
131+ intro a b c heq
132+ induction a using Quotient.inductionOn with | h a =>
133+ induction b using Quotient.inductionOn with | h b =>
134+ induction c using Quotient.inductionOn with | h c =>
135+ apply Quotient.sound
136+ simp only at heq
137+ have heqv := by simpa using Quotient.exact heq
138+ exact mul_cancel_right heqv
139+
140+ inductive SwapOnce' (I : Independence α) : List α → List α → Prop
141+ | swap (a b : α) : I.rel a b → SwapOnce' I [a, b] [b, a]
142+
143+ instance : Monoid (List α) where
144+ one := []
145+ mul := List.append
146+ mul_assoc := List.append_assoc
147+ mul_one := List.append_nil
148+ one_mul := List.nil_append
149+
150+ def TraceEqv' (I : Independence α) : Con (List α) := conGen (SwapOnce' I)
151+
152+ def TraceMonoid' (I : Independence α) := (TraceEqv' I).Quotient
153+
154+ instance : Monoid (TraceMonoid' I) := (TraceEqv' I).monoid
155+
53156end TraceTheory
0 commit comments