Skip to content

Commit fdb55ca

Browse files
bwbushbwbush
committed
Implemented certificate rule
1 parent 2ce5692 commit fdb55ca

File tree

7 files changed

+210
-0
lines changed

7 files changed

+210
-0
lines changed

‎analysis/markov/.gitignore‎

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

‎analysis/markov/Linleios.lean‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
2+
import Linleios.Evolve

‎analysis/markov/Linleios/Evolve.lean‎

Lines changed: 74 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,74 @@
1+
2+
import Std.Data.HashMap
3+
import Batteries.Lean.HashMap
4+
5+
open Std (HashMap)
6+
7+
8+
abbrev Probability := Float
9+
10+
11+
structure Environment where
12+
activeSlotCoefficient : Probability
13+
Lheader : Nat
14+
Lvote : Nat
15+
Ldiff : Nat
16+
pSpacingOkay : Probability
17+
18+
def makeEnvironment (activeSlotCoefficient : Float) (Lheader Lvote Ldiff : Nat) : Environment :=
19+
{
20+
activeSlotCoefficient := activeSlotCoefficient
21+
Lheader := Lheader
22+
Lvote := Lvote
23+
Ldiff := Ldiff
24+
pSpacingOkay := (1 - activeSlotCoefficient).pow (3 * Lheader + Lvote + Ldiff - 1).toFloat
25+
}
26+
27+
28+
structure State where
29+
rbCount : Nat
30+
ebCount : Nat
31+
deriving Repr, BEq, Hashable, Inhabited
32+
33+
example : (default : State).rbCount = 0 := rfl
34+
35+
example : (default : State).ebCount = 0 := rfl
36+
37+
38+
def Probabilities := HashMap State Probability
39+
deriving Repr, EmptyCollection
40+
41+
instance : Inhabited Probabilities where
42+
default := (∅ : Probabilities).insert Inhabited.default 1
43+
44+
45+
def forge {env : Environment} (state : State) : List (State × Probability) :=
46+
[
47+
⟨
48+
{
49+
state with
50+
rbCount := state.rbCount + 1
51+
}
52+
, env.pSpacingOkay
53+
⟩
54+
, ⟨
55+
{
56+
state with
57+
rbCount := state.rbCount + 1
58+
ebCount := state.ebCount + 1
59+
}
60+
, env.pSpacingOkay
61+
⟩
62+
]
63+
64+
65+
def evolve (transition : State → List (State × Probability)) : Probabilities → Probabilities :=
66+
HashMap.fold
67+
(
68+
fun acc state p =>
69+
HashMap.mergeWith (fun _ => Add.add) acc
70+
∘ HashMap.map (fun _ => Mul.mul p ∘ List.sum ∘ List.map Prod.snd)
71+
∘ List.groupByKey Prod.fst
72+
$ transition state
73+
)
74+
∅

‎analysis/markov/Main.lean‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
2+
import Linleios
3+
4+
5+
def env : Environment := makeEnvironment 0.05 1 4 7
6+
7+
def s0 : Probabilities := default
8+
def s1 := evolve (@forge env) s0
9+
10+
def main : IO Unit :=
11+
IO.println $ (reprPrec s1 0).pretty

‎analysis/markov/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": "c211948581bde9846a99e32d97a03f0d5307c31e",
9+
"name": "mathlib",
10+
"manifestFile": "lake-manifest.json",
11+
"inputRev": "v4.20.0",
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": "2ac43674e92a695e96caac19f4002b25434636da",
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": "6c62474116f525d2814f0157bb468bf3a4f9f120",
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": "a11bcb5238149ae5d8a0aa5e2f8eddf8a3a9b27d",
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": "21e6a0522cd2ae6cf88e9da99a1dd010408ab306",
49+
"name": "proofwidgets",
50+
"manifestFile": "lake-manifest.json",
51+
"inputRev": "v0.0.60",
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": "ddfca7829bf8aa4083cdf9633935dddbb28b7b2a",
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": "2865ea099ab1dd8d6fc93381d77a4ac87a85527a",
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": "7a0d63fbf8fd350e891868a06d9927efa545ac1e",
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": "f9e25dcbed001489c53bceeb1f1d50bbaf7451d4",
89+
"name": "Cli",
90+
"manifestFile": "lake-manifest.json",
91+
"inputRev": "main",
92+
"inherited": true,
93+
"configFile": "lakefile.toml"}],
94+
"name": "linleios",
95+
"lakeDir": ".lake"}

‎analysis/markov/lakefile.toml‎

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
name = "linleios"
2+
version = "0.1.0"
3+
keywords = ["math"]
4+
defaultTargets = ["linleios"]
5+
6+
[[lean_lib]]
7+
name = "Linleios"
8+
9+
[[lean_exe]]
10+
name = "linleios"
11+
root = "Main"
12+
13+
[leanOptions]
14+
pp.unicode.fun = true # pretty-prints `fun a ↦ b`
15+
autoImplicit = false
16+
17+
[[require]]
18+
name = "mathlib"
19+
scope = "leanprover-community"
20+
version = "git#v4.20.0"
21+
22+
[lean]
23+
server-options = [
24+
["checkBinderAnnotations", "false"],
25+
["diagnostics", "true"]
26+
]

‎analysis/markov/lean-toolchain‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
leanprover/lean4:v4.20.0

0 commit comments

Comments
 (0)