[DO NOT MERGE] REVIEW

.github/workflows/lean_action_ci.yml

@@ -5,17 +5,12 @@ on:
   pull_request:
   workflow_dispatch:
 
-# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
-permissions:
-  contents: read # Read access to repository contents
-  pages: write # Write access to GitHub Pages
-  id-token: write # Write access to ID tokens
-
 jobs:
   build:
     runs-on: ubuntu-latest
 
     steps:
       - uses: actions/checkout@v4
       - uses: leanprover/lean-action@v1
-      - uses: leanprover-community/docgen-action@v1
+        with:
+          lake-package-directory: TraceTheory

.gitignore

@@ -1 +1 @@
-/.lake
+/*.pdf

README.md

@@ -1,13 +1,40 @@
-# trace-theory-lean
+# Trace Theory Lean
 
-## GitHub configuration
+This repository contains a formalization of Mazurkiewicz trace theory in the Lean theorem prover.
 
-To set up your new GitHub repository, follow these steps:
+## Structure
 
-* Under your repository name, click **Settings**.
-* In the **Actions** section of the sidebar, click "General".
-* Check the box **Allow GitHub Actions to create and approve pull requests**.
-* Click the **Pages** section of the settings sidebar.
-* In the **Source** dropdown menu, select "GitHub Actions".
+### 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.
 
-After following the steps above, you can remove this section from the README file.
+### 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` contains a proof of Hashiguchi's theorem on recognizable trace closures.
+- `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.
+- `Occurrence.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.

TraceTheory/.gitignore

@@ -0,0 +1 @@
+/.lake

TraceTheory/TraceTheory.lean

@@ -0,0 +1,4 @@
+import TraceTheory.DependenceGraph
+import TraceTheory.History
+import TraceTheory.Occurrence
+import TraceTheory.Ochmanski