Redefine trace equivalence without using ConGen.Rel

Author: richwill28

TraceTheory/TraceTheory/Trace.lean

@@ -1,5 +1,4 @@
 import Mathlib.Data.Fintype.Basic
-import Mathlib.GroupTheory.Congruence.Defs
 import TraceTheory.Basic
 
 variable {α : Type*} [DecidableEq α] [Fintype α]
@@ -10,39 +9,55 @@ namespace Trace
   A dependence relation is a finite, reflexive, and symmetric relation.
 -/
 structure Dependence where
-  r : α → α → Prop
-  refl : ∀ a, r a a
-  symm: ∀ a b, r a b → r b a
+  rel : α → α → Prop
+  refl : ∀ a, rel a a
+  symm: ∀ a b, rel a b → rel b a
 
 /--
   An independence relation is a finite, irreflexive, and symmetric relation.
 -/
 structure Independence where
-  r : α → α → Prop
-  irrefl : ∀ a, ¬ r a a
-  symm : ∀ a b, r a b → r b a
+  rel : α → α → Prop
+  irrefl : ∀ a, ¬ rel a a
+  symm : ∀ a b, rel a b → rel b a
 
 variable {I : Independence}
 
+variable (I) in
 /--
-  The product of two traces (i.e. list of symbols) is the concatenation of the two traces.
--/
-instance : Mul (List α) := ⟨List.append⟩
-
-/--
-  The trace equivalence relation is defined as the smallest multiplicative (i.e. concatenation) congruence relation induced by the independence relation `I.r`.
-  That is, 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.
+  The trace equivalence relation is the smallest congruence relation induced by the independence relation `I.r`.
+  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.
 
-  More precisely, `ConGen.Rel I.r` is the inductive closure of the following axioms:
-  - **Base:** If `I.r a b`, then `[a, b]` is equivalent to `[b, a]` (i.e., swapping adjacent independent symbols).
+  The relation is inductively generated by:
+  - **Swap:** If `I.r a b`, then `[a, b]` is equivalent to `[b, a]` (swapping adjacent independent symbols).
   - **Reflexivity:** Every word is equivalent to itself.
-  - **Symmetry:** If `u` is equivalent to `v`, then `v` is equivalent to `u`.
-  - **Transitivity:** If `u` is equivalent to `v` and `v` is equivalent to `w`, then `u` is equivalent to `w`.
-  - **Compatibility:** If `u₁` is equivalent to `v₁` and `u₂` is equivalent to `v₂`, then `u₁ ++ u₂` is equivalent to `v₁ ++ v₂`.
-
-  Thus, two traces are equivalent if and only if one can be obtained from the other by a finite sequence of these operations (or their inverses).
+  - **Symmetry:** If `t₁` is equivalent to `t₂`, then `t₂` is equivalent to `t₁`.
+  - **Transitivity:** If `t₁` is equivalent to `t₂` and `t₂` is equivalent to `t₃`, then `t₁` is equivalent to `t₃`.
+  - **Compatibility:** If `t₁` is equivalent to `t₂` and `t₃` is equivalent to `t₄`, then `t₁ ++ t₃` is equivalent to `t₂ ++ t₄`.
 -/
-def trace_equiv : List α → List α → Prop :=
-  ConGen.Rel I.r
+inductive TraceEquiv : List α → List α → Prop
+  | swap : ∀ a b, I.rel a b → TraceEquiv [a, b] [b, a]
+  | refl : ∀ t₁, TraceEquiv t₁ t₁
+  | symm : ∀ t₁ t₂, TraceEquiv t₁ t₂ → TraceEquiv t₂ t₁
+  | trans : ∀ t₁ t₂ t₃, TraceEquiv t₁ t₂ → TraceEquiv t₂ t₃ → TraceEquiv t₁ t₃
+  | compat : ∀ t₁ t₂ t₃ t₄, TraceEquiv t₁ t₂ → TraceEquiv t₃ t₄ → TraceEquiv (t₁ ++ t₃) (t₂ ++ t₄)
+
+omit [DecidableEq α] [Fintype α] in
+variable (I) in
+@[simp]
+lemma trace_equiv_length_eq {t₁ t₂ : List α} :
+    TraceEquiv I t₁ t₂ → t₁.length = t₂.length := by
+  intro h
+  induction h with
+  | swap _ _ _ =>
+    rfl
+  | refl _ =>
+    rfl
+  | symm _ _ _ IH =>
+    exact Eq.symm IH
+  | trans _ _ _ _ _ IH₁ IH₂ =>
+    exact Eq.trans IH₁ IH₂
+  | compat _ _ _ _ _ _ IH₁ IH₂ =>
+    simp [IH₁, IH₂]
 
 end Trace