Skip to content

Commit 5c75d8a

Browse files
marcusrosselmarcusrossel
committedFeb 28, 2025
Prove that logical time advances monotonically
1 parent d30394f commit 5c75d8a

File tree

7 files changed

+89
-47
lines changed

7 files changed

+89
-47
lines changed
 

‎ReactorModel/Execution/Theorems/Grouped/Basic.lean

+3
Original file line numberDiff line numberDiff line change
@@ -42,6 +42,9 @@ theorem Grouped.deterministic [Proper α] {s s₁ s₂ : State α}
4242
case refl.step.inst.step.inst e _ f' f => exact e.nonrepeatable f |>.elim
4343
case step.refl.inst.step.inst e _ f' f => exact e.nonrepeatable f |>.elim
4444

45+
theorem Grouped.tag_le [Hierarchical α] {s₁ s₂ : State α} (e : Grouped s₁ s₂) : s₁.tag ≤ s₂.tag :=
46+
e.tail.preserves_tag ▸ e.steps.tag_le
47+
4548
theorem to_grouped [Hierarchical α] {s₁ s₂ : State α} (n : s₁.Nontrivial) (e : s₁ ⇓ s₂) :
4649
Nonempty (Grouped s₁ s₂) := by
4750
induction e <;> try cases ‹_ ↓ _›

‎ReactorModel/Execution/Theorems/Monotonicity.lean

+13
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
import ReactorModel.Execution.Theorems.Step.Basic
2+
3+
open Classical Reactor
4+
5+
namespace Execution
6+
7+
variable [Proper α] {s₁ s₂ : State α}
8+
9+
-- Property (1) on page 10 of https://www.informatik.uni-bremen.de/agbs/jp/papers/trs_script.pdf.
10+
theorem tag_le (e : s₁ ⇓ s₂) : s₁.tag ≤ s₂.tag := by
11+
induction e
12+
case refl => rfl
13+
case trans e₁ e₂ ih => exact e₁.tag_le.trans ih

‎ReactorModel/Execution/Theorems/Step/Basic.lean

+13
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
import ReactorModel.Execution.Theorems.Step.Skip
2+
import ReactorModel.Execution.Theorems.Step.Exec
3+
import ReactorModel.Execution.Theorems.Step.Time
4+
5+
open Classical Reactor Execution State
6+
7+
variable [Hierarchical α] {s₁ s₂ : State α}
8+
9+
namespace Execution.Step
10+
11+
theorem tag_le : (s₁ ↓ s₂) → s₁.tag ≤ s₂.tag
12+
| .skip e | .exec e => le_of_eq e.preserves_tag
13+
| .time e => le_of_lt e.tag_lt

‎ReactorModel/Execution/Theorems/Trivial.lean

+3
Original file line numberDiff line numberDiff line change
@@ -77,4 +77,7 @@ theorem trivial_deterministic
7777
(e₁.to_timeStepRTC <| .of_not_nontrivial triv)
7878
(e₂.to_timeStepRTC <| .of_not_nontrivial triv)
7979

80+
theorem trivial_tag_le (triv : ¬s₁.Nontrivial) (e : s₁ ⇓ s₂) : s₁.tag ≤ s₂.tag :=
81+
e.to_timeStepRTC (.of_not_nontrivial triv) |>.tag_le
82+
8083
end Execution

‎lake-manifest.json

+54-44
Original file line numberDiff line numberDiff line change
@@ -1,95 +1,105 @@
11
{"version": "1.1.0",
22
"packagesDir": ".lake/packages",
33
"packages":
4-
[{"url": "https://github.com/leanprover-community/batteries",
4+
[{"url": "https://github.com/leanprover-community/mathlib4",
55
"type": "git",
66
"subDir": null,
77
"scope": "leanprover-community",
8-
"rev": "33d7f346440869364a2cd077bde8cebf73243aaa",
9-
"name": "batteries",
8+
"rev": "9837ca9d65d9de6fad1ef4381750ca688774e608",
9+
"name": "mathlib",
1010
"manifestFile": "lake-manifest.json",
11-
"inputRev": "main",
11+
"inputRev": "v4.15.0",
12+
"inherited": false,
13+
"configFile": "lakefile.lean"},
14+
{"url": "https://github.com/nomeata/lean-calcify",
15+
"type": "git",
16+
"subDir": null,
17+
"scope": "nomeata",
18+
"rev": "ec3743a033ccbcf54cc5fd0157c87342099d9120",
19+
"name": "calcify",
20+
"manifestFile": "lake-manifest.json",
21+
"inputRev": "master",
1222
"inherited": true,
1323
"configFile": "lakefile.toml"},
14-
{"url": "https://github.com/leanprover-community/quote4",
24+
{"url": "https://github.com/leanprover-community/plausible",
1525
"type": "git",
1626
"subDir": null,
1727
"scope": "leanprover-community",
18-
"rev": "303b23fbcea94ac4f96e590c1cad6618fd4f5f41",
19-
"name": "Qq",
28+
"rev": "2c57364ef83406ea86d0f78ce3e342079a2fece5",
29+
"name": "plausible",
2030
"manifestFile": "lake-manifest.json",
21-
"inputRev": "master",
31+
"inputRev": "v4.15.0",
2232
"inherited": true,
23-
"configFile": "lakefile.lean"},
24-
{"url": "https://github.com/leanprover-community/aesop",
33+
"configFile": "lakefile.toml"},
34+
{"url": "https://github.com/leanprover-community/LeanSearchClient",
2535
"type": "git",
2636
"subDir": null,
2737
"scope": "leanprover-community",
28-
"rev": "de91b59101763419997026c35a41432ac8691f15",
29-
"name": "aesop",
38+
"rev": "003ff459cdd85de551f4dcf95cdfeefe10f20531",
39+
"name": "LeanSearchClient",
3040
"manifestFile": "lake-manifest.json",
31-
"inputRev": "master",
41+
"inputRev": "main",
3242
"inherited": true,
3343
"configFile": "lakefile.toml"},
34-
{"url": "https://github.com/leanprover-community/ProofWidgets4",
44+
{"url": "https://github.com/leanprover-community/import-graph",
3545
"type": "git",
3646
"subDir": null,
3747
"scope": "leanprover-community",
38-
"rev": "1383e72b40dd62a566896a6e348ffe868801b172",
39-
"name": "proofwidgets",
48+
"rev": "9a0b533c2fbd6195df067630be18e11e4349051c",
49+
"name": "importGraph",
4050
"manifestFile": "lake-manifest.json",
41-
"inputRev": "v0.0.46",
51+
"inputRev": "v4.15.0",
4252
"inherited": true,
43-
"configFile": "lakefile.lean"},
44-
{"url": "https://github.com/leanprover/lean4-cli",
53+
"configFile": "lakefile.toml"},
54+
{"url": "https://github.com/leanprover-community/ProofWidgets4",
4555
"type": "git",
4656
"subDir": null,
47-
"scope": "leanprover",
48-
"rev": "726b3c9ad13acca724d4651f14afc4804a7b0e4d",
49-
"name": "Cli",
57+
"scope": "leanprover-community",
58+
"rev": "2b000e02d50394af68cfb4770a291113d94801b5",
59+
"name": "proofwidgets",
5060
"manifestFile": "lake-manifest.json",
51-
"inputRev": "main",
61+
"inputRev": "v0.0.48",
5262
"inherited": true,
53-
"configFile": "lakefile.toml"},
54-
{"url": "https://github.com/leanprover-community/import-graph",
63+
"configFile": "lakefile.lean"},
64+
{"url": "https://github.com/leanprover-community/aesop",
5565
"type": "git",
5666
"subDir": null,
5767
"scope": "leanprover-community",
58-
"rev": "119b022b3ea88ec810a677888528e50f8144a26e",
59-
"name": "importGraph",
68+
"rev": "2689851f387bb2cef351e6825fe94a56a304ca13",
69+
"name": "aesop",
6070
"manifestFile": "lake-manifest.json",
61-
"inputRev": "main",
71+
"inputRev": "v4.15.0",
6272
"inherited": true,
6373
"configFile": "lakefile.toml"},
64-
{"url": "https://github.com/leanprover-community/LeanSearchClient",
74+
{"url": "https://github.com/leanprover-community/quote4",
6575
"type": "git",
6676
"subDir": null,
6777
"scope": "leanprover-community",
68-
"rev": "d7caecce0d0f003fd5e9cce9a61f1dd6ba83142b",
69-
"name": "LeanSearchClient",
78+
"rev": "f0c584bcb14c5adfb53079781eeea75b26ebbd32",
79+
"name": "Qq",
7080
"manifestFile": "lake-manifest.json",
71-
"inputRev": "main",
81+
"inputRev": "v4.15.0",
7282
"inherited": true,
7383
"configFile": "lakefile.toml"},
74-
{"url": "https://github.com/leanprover-community/plausible",
84+
{"url": "https://github.com/leanprover-community/batteries",
7585
"type": "git",
7686
"subDir": null,
7787
"scope": "leanprover-community",
78-
"rev": "42dc02bdbc5d0c2f395718462a76c3d87318f7fa",
79-
"name": "plausible",
88+
"rev": "e8dc5fc16c625fc4fe08f42d625523275ddbbb4b",
89+
"name": "batteries",
8090
"manifestFile": "lake-manifest.json",
81-
"inputRev": "main",
91+
"inputRev": "v4.15.0",
8292
"inherited": true,
8393
"configFile": "lakefile.toml"},
84-
{"url": "https://github.com/leanprover-community/mathlib4",
94+
{"url": "https://github.com/leanprover/lean4-cli",
8595
"type": "git",
8696
"subDir": null,
87-
"scope": "",
88-
"rev": "af1911940422ded96480cde9daed0a5de7a435d3",
89-
"name": "mathlib",
97+
"scope": "leanprover",
98+
"rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd",
99+
"name": "Cli",
90100
"manifestFile": "lake-manifest.json",
91-
"inputRev": "master",
92-
"inherited": false,
93-
"configFile": "lakefile.lean"}],
94-
"name": "«reactor-model»",
101+
"inputRev": "main",
102+
"inherited": true,
103+
"configFile": "lakefile.toml"}],
104+
"name": "ReactorModel",
95105
"lakeDir": ".lake"}

‎lakefile.toml

+2-2
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,8 @@ defaultTargets = ["ReactorModel"]
33

44
[[require]]
55
name = "mathlib"
6-
git = "https://github.com/leanprover-community/mathlib4"
7-
rev = "master"
6+
git = "https://github.com/leanprover-community/mathlib4"
7+
rev = "9837ca9d65d9de6fad1ef4381750ca688774e608"
88

99
[[lean_lib]]
1010
name = "ReactorModel"

‎lean-toolchain

+1-1
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
leanprover/lean4:v4.14.0-rc2
1+
leanprover/lean4:v4.15.0

0 commit comments

Comments
 (0)
Please sign in to comment.