Skip to content

Commit 828de95

Browse files
jefraijefrai
committed
Initial commit
0 parents  commit 828de95

12 files changed

Lines changed: 333 additions & 0 deletions

‎.github/workflows/create-release.yml‎

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
name: Create Release
2+
3+
on:
4+
push:
5+
branches:
6+
- 'main'
7+
- 'master'
8+
paths:
9+
- 'lean-toolchain'
10+
11+
jobs:
12+
lean-release-tag:
13+
name: Add Lean release tag
14+
runs-on: ubuntu-latest
15+
permissions:
16+
contents: write
17+
steps:
18+
- name: lean-release-tag action
19+
uses: leanprover-community/lean-release-tag@v1
20+
with:
21+
do-release: true
22+
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}

‎.github/workflows/lean_action_ci.yml‎

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
name: Lean Action CI
2+
3+
on:
4+
push:
5+
pull_request:
6+
workflow_dispatch:
7+
8+
# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
9+
permissions:
10+
contents: read # Read access to repository contents
11+
pages: write # Write access to GitHub Pages
12+
id-token: write # Write access to ID tokens
13+
14+
jobs:
15+
build:
16+
runs-on: ubuntu-latest
17+
18+
steps:
19+
- uses: actions/checkout@v4
20+
- uses: leanprover/lean-action@v1
21+
- uses: leanprover-community/docgen-action@v1

‎.github/workflows/update.yml‎

Lines changed: 41 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,41 @@
1+
name: Update Dependencies
2+
3+
on:
4+
# schedule: # Sets a schedule to trigger the workflow
5+
# - cron: "0 8 * * *" # Every day at 08:00 AM UTC (see https://docs.github.com/en/actions/writing-workflows/choosing-when-your-workflow-runs/events-that-trigger-workflows#schedule)
6+
workflow_dispatch: # Allows the workflow to be triggered manually via the GitHub interface
7+
8+
jobs:
9+
check-for-updates: # Determines which updates to apply.
10+
runs-on: ubuntu-latest
11+
outputs:
12+
is-update-available: ${{ steps.check-for-updates.outputs.is-update-available }}
13+
new-tags: ${{ steps.check-for-updates.outputs.new-tags }}
14+
steps:
15+
- name: Run the action
16+
id: check-for-updates
17+
uses: leanprover-community/mathlib-update-action@v1
18+
# START CONFIGURATION BLOCK 1
19+
# END CONFIGURATION BLOCK 1
20+
do-update: # Runs the upgrade, tests it, and makes a PR/issue/commit.
21+
runs-on: ubuntu-latest
22+
permissions:
23+
contents: write # Grants permission to push changes to the repository
24+
issues: write # Grants permission to create or update issues
25+
pull-requests: write # Grants permission to create or update pull requests
26+
needs: check-for-updates
27+
if: ${{ needs.check-for-updates.outputs.is-update-available }}
28+
strategy: # Runs for each update discovered by the `check-for-updates` job.
29+
max-parallel: 1 # Ensures that the PRs/issues are created in order.
30+
matrix:
31+
tag: ${{ fromJSON(needs.check-for-updates.outputs.new-tags) }}
32+
steps:
33+
- name: Run the action
34+
id: update-the-repo
35+
uses: leanprover-community/mathlib-update-action/do-update@v1
36+
with:
37+
tag: ${{ matrix.tag }}
38+
# START CONFIGURATION BLOCK 2
39+
on_update_succeeds: pr # Create a pull request if the update succeeds
40+
on_update_fails: issue # Create an issue if the update fails
41+
# END CONFIGURATION BLOCK 2

‎.gitignore‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
/.lake

‎README.md‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
# trace-theory-lean
2+
3+
## GitHub configuration
4+
5+
To set up your new GitHub repository, follow these steps:
6+
7+
* Under your repository name, click **Settings**.
8+
* In the **Actions** section of the sidebar, click "General".
9+
* Check the box **Allow GitHub Actions to create and approve pull requests**.
10+
* Click the **Pages** section of the settings sidebar.
11+
* In the **Source** dropdown menu, select "GitHub Actions".
12+
13+
After following the steps above, you can remove this section from the README file.

‎TraceTheoryLean.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
import TraceTheoryLean.Main

‎TraceTheoryLean/LangDouble.lean‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
import Mathlib.Data.Fintype.Basic
2+
import Mathlib.Data.Finset.Basic
3+
import Mathlib.Data.List.Basic
4+
import Mathlib.Computability.DFA
5+
import Mathlib.Computability.Language
6+
import Mathlib.Computability.NFA
7+
import Mathlib.Logic.Relation
8+
9+
universe u v
10+
variable {α : Type u} {σ : Type v} {M : NFA α σ}
11+
12+
-- TODO

‎TraceTheoryLean/Main.lean‎

Lines changed: 68 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,68 @@
1+
import Mathlib.Data.Fintype.Basic
2+
import Mathlib.Data.Finset.Basic
3+
import Mathlib.Data.List.Basic
4+
import Mathlib.Computability.Language
5+
import Mathlib.Logic.Relation
6+
7+
variable {U : Type} [DecidableEq U]
8+
9+
def Alphabet U := Finset U
10+
11+
def proj (S : Finset U) (w : List U) : List U :=
12+
match w with
13+
| [] => []
14+
| b :: u => if b ∈ S then b :: proj S u else proj S u
15+
16+
def cancel (w : List U) (a : U) :=
17+
match w with
18+
| [] => []
19+
| b :: u => if a = b then u else b :: (cancel u a)
20+
21+
lemma cancelling_proj_mem_is_id (S : Finset U) (w : List U) (a : U) :
22+
(a ∉ S) -> (cancel (proj S w) a = proj S w) := by
23+
intro h
24+
induction w with
25+
| nil => rfl
26+
| cons b u IH =>
27+
by_cases h_ab : a = b
28+
· rw [h_ab] at h
29+
simp [proj, h]
30+
exact IH
31+
· by_cases h_bs : b ∈ S
32+
· simp [proj, h_bs]
33+
simp [cancel, h_ab]
34+
exact IH
35+
· simp [proj, h_bs]
36+
exact IH
37+
38+
lemma proj_cancel_comm (S : Finset U) (w : List U) (a : U) : -- (1.3)
39+
proj S (cancel w a) = cancel (proj S w) a := by
40+
induction w with
41+
| nil => rfl
42+
| cons b u IH =>
43+
by_cases h_bs : b ∈ S
44+
· simp [proj, h_bs]
45+
by_cases h_ab : a = b
46+
· simp [cancel, h_ab]
47+
· simp [cancel, h_ab]
48+
simp [proj, h_bs]
49+
exact IH
50+
· by_cases h_ab : a = b
51+
· simp [cancel, h_ab]
52+
simp [proj, h_bs]
53+
symm
54+
apply (cancelling_proj_mem_is_id S u b)
55+
exact h_bs
56+
· simp [cancel, h_ab]
57+
simp [proj, h_bs]
58+
exact IH
59+
60+
def proj_lang (S : Finset U) (A : Language U) : Language U :=
61+
Set.image (proj S) A
62+
63+
def pref (w : List U) : Language U := {u : List U | ∃v, u ++ v = w}
64+
65+
structure Dependency (α) [Fintype α] where
66+
r : α → α → Prop
67+
refl : ∀ x, r x x
68+
symm : ∀ {x y}, r x y → r y x

‎TraceTheoryLean/Scratchpad.lean‎

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
1+
import Mathlib.Data.Fintype.Basic
2+
import Mathlib.Data.Finset.Basic
3+
import Mathlib.Data.List.Basic
4+
import Mathlib.Computability.DFA
5+
import Mathlib.Computability.Language
6+
import Mathlib.Computability.NFA
7+
import Mathlib.Logic.Relation
8+
9+
universe u v
10+
variable {α : Type u} {σ : Type v} {M : NFA α σ}
11+
12+
variable (M) in
13+
def lang_reverse : (NFA α σ) where
14+
step := fun (s : σ) (a : α) => {x | s ∈ M.step x a}
15+
start := M.accept
16+
accept := M.start
17+
18+
variable (M) in
19+
lemma reverse_reverse :
20+
lang_reverse (lang_reverse M) = M := by
21+
simp [lang_reverse]
22+
23+
variable (M) in
24+
lemma forward_subset_reverse_nondisjoint (N : NFA α σ) (S : Set σ) (T : Set σ) (a : α) :
25+
(N = lang_reverse M) -> (T ⊆ M.stepSet S a ∧ T ≠ ∅) -> (S ∩ N.stepSet T a ≠ ∅) := by
26+
intro h1 h2
27+
simp [h1]
28+
simp [NFA.stepSet]
29+
simp [lang_reverse]
30+
obtain ⟨h_sub, h_ne⟩ := h2
31+
obtain ⟨t, ht⟩ := Set.nonempty_iff_ne_empty.mpr h_ne
32+
have ht_mem : t ∈ M.stepSet S a := h_sub ht
33+
simp [NFA.stepSet] at ht_mem
34+
obtain ⟨i, hi, ht_step⟩ := ht_mem
35+
have : i ∈ S ∩ ⋃ s ∈ T, {x | s ∈ M.step x a} :=
36+
⟨hi, by
37+
simp only [Set.mem_iUnion, Set.mem_setOf_eq]
38+
exact ⟨t, ht, ht_step⟩⟩
39+
rw [<- Set.not_nonempty_iff_eq_empty, Set.nonempty_def, Classical.not_not]
40+
use i

‎lake-manifest.json‎

Lines changed: 95 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,95 @@
1+
{"version": "1.1.0",
2+
"packagesDir": ".lake/packages",
3+
"packages":
4+
[{"url": "https://github.com/leanprover-community/mathlib4",
5+
"type": "git",
6+
"subDir": null,
7+
"scope": "leanprover-community",
8+
"rev": "9411739906304133a323a27ccbbbe22307ab8830",
9+
"name": "mathlib",
10+
"manifestFile": "lake-manifest.json",
11+
"inputRev": "master",
12+
"inherited": false,
13+
"configFile": "lakefile.lean"},
14+
{"url": "https://github.com/leanprover-community/plausible",
15+
"type": "git",
16+
"subDir": null,
17+
"scope": "leanprover-community",
18+
"rev": "240eddc1bb31420fbbc57fe5cc579435c2522493",
19+
"name": "plausible",
20+
"manifestFile": "lake-manifest.json",
21+
"inputRev": "main",
22+
"inherited": true,
23+
"configFile": "lakefile.toml"},
24+
{"url": "https://github.com/leanprover-community/LeanSearchClient",
25+
"type": "git",
26+
"subDir": null,
27+
"scope": "leanprover-community",
28+
"rev": "99657ad92e23804e279f77ea6dbdeebaa1317b98",
29+
"name": "LeanSearchClient",
30+
"manifestFile": "lake-manifest.json",
31+
"inputRev": "main",
32+
"inherited": true,
33+
"configFile": "lakefile.toml"},
34+
{"url": "https://github.com/leanprover-community/import-graph",
35+
"type": "git",
36+
"subDir": null,
37+
"scope": "leanprover-community",
38+
"rev": "dba7fbc707774d1ba830fd44d7f92a717e9bf57f",
39+
"name": "importGraph",
40+
"manifestFile": "lake-manifest.json",
41+
"inputRev": "main",
42+
"inherited": true,
43+
"configFile": "lakefile.toml"},
44+
{"url": "https://github.com/leanprover-community/ProofWidgets4",
45+
"type": "git",
46+
"subDir": null,
47+
"scope": "leanprover-community",
48+
"rev": "6e47cc88cfbf1601ab364e9a4de5f33f13401ff8",
49+
"name": "proofwidgets",
50+
"manifestFile": "lake-manifest.json",
51+
"inputRev": "v0.0.71",
52+
"inherited": true,
53+
"configFile": "lakefile.lean"},
54+
{"url": "https://github.com/leanprover-community/aesop",
55+
"type": "git",
56+
"subDir": null,
57+
"scope": "leanprover-community",
58+
"rev": "523c8ee53f7057447fc62ec14e506fda4cf63dfa",
59+
"name": "aesop",
60+
"manifestFile": "lake-manifest.json",
61+
"inputRev": "master",
62+
"inherited": true,
63+
"configFile": "lakefile.toml"},
64+
{"url": "https://github.com/leanprover-community/quote4",
65+
"type": "git",
66+
"subDir": null,
67+
"scope": "leanprover-community",
68+
"rev": "f85ad59c9b60647ef736719c23edd4578f723806",
69+
"name": "Qq",
70+
"manifestFile": "lake-manifest.json",
71+
"inputRev": "master",
72+
"inherited": true,
73+
"configFile": "lakefile.toml"},
74+
{"url": "https://github.com/leanprover-community/batteries",
75+
"type": "git",
76+
"subDir": null,
77+
"scope": "leanprover-community",
78+
"rev": "6e89c7370ca3a91b7d1f29ef7d727a9d027d7b0d",
79+
"name": "batteries",
80+
"manifestFile": "lake-manifest.json",
81+
"inputRev": "main",
82+
"inherited": true,
83+
"configFile": "lakefile.toml"},
84+
{"url": "https://github.com/leanprover/lean4-cli",
85+
"type": "git",
86+
"subDir": null,
87+
"scope": "leanprover",
88+
"rev": "cacb481a1eaa4d7d4530a27b606c60923da21caf",
89+
"name": "Cli",
90+
"manifestFile": "lake-manifest.json",
91+
"inputRev": "main",
92+
"inherited": true,
93+
"configFile": "lakefile.toml"}],
94+
"name": "«trace-theory-lean»",
95+
"lakeDir": ".lake"}

0 commit comments

Comments
 (0)