Merge branch 'ys-working' into beta

Author: yisiox

README.md

@@ -0,0 +1,40 @@
+# Trace Theory Lean
+
+This repository contains a formalization of Mazurkiewicz trace theory in the Lean theorem prover.
+
+## Structure
+
+### Core
+- `Defs.lean` contains fundamental definitions for traces.
+- `Basic.lean` contains basic properties of the algebra of traces.
+- `DependenceMorphism.lean` provides a way to show isomorphism to the algebra of traces via dependence morphisms.
+
+### Isomorphic Algebras
+- `DependenceGraph.lean` contains a definition of the algebra of dependence graphs and proof of its isomorphism to traces.
+- `Histories.lean` contains a definition of the algebra of histories and proof of its isomorphism to traces.
+
+### Ochmański's Theorem
+- `Language.lean` contains basic definitions and lemmas for trace languages.
+- `MyhillNerode.lean` supplies a proof of the Myhill-Nerode theorem in the context of monoids.
+- `Hashiguchi.lean` currently contains just the statement of Hashiguchi's theorem on sufficient conditions for a trace language to have finite rank.
+- `RegularExpressions.lean` reinterprets mathlib4's `RegularExpression` on traces.
+- `Ochmanski.lean` contains the proof of Ochmański's theorem on recognizable trace languages and lemmas leading up to it.
+
+### Misc
+- `List.lean` contains misc. definitions and lemmas for `List` (string) manipulation.
+- `Occurences.lean` formalizes ordering of symbol occurrences.
+- `EdgeSubset.lean` is a proof of the negation of a claim in The Book of Traces (Proposition 1.4.2).
+- `Computability.lean` supplies a full proof of Kleene's theorem together with mathlib4.
+
+## Naming Convention
+
+General guideline:
+
+- `a, b, c, d, e` for symbols.
+- `i, j, k` for indices.
+- `n, m` for sizes.
+- `u, v, w, x, y, z` for strings, `x', x''` or `x₁, x₂` or `p, q, r` for factoring.
+- `s, t, u, v` for traces or monoid elements.
+- `S` for (subsets of) alphabets.
+- `X` for word (string) languages.
+- `T` for trace langauges.