Work in progress on property-based tests

Author: bwbush

analysis/markov/lake-manifest.json

@@ -21,6 +21,16 @@
    "inputRev": "26d5ce4d60195a869b1fdb100b442794ea63e1ad",
    "inherited": false,
    "configFile": "lakefile.toml"},
+  {"url": "https://github.com/argumentcomputer/LSpec.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "d2bbbfa61a82ac199a5e852aa375acffd9a3b3f1",
+   "name": "LSpec",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": null,
+   "inherited": false,
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,

analysis/markov/lakefile.lean

@@ -1,10 +1,10 @@
-
 import Lake
 
 open Lake DSL
 
 package «linleios» where
   version := StdVer.mk (SemVerCore.mk 0 1 0) ""
+  testDriver := "linleios_test"
   leanOptions := #[
     -- pretty-prints `fun a ↦ b`
     ⟨`pp.unicode.fun, true⟩,
@@ -24,9 +24,16 @@ lean_exe «linleios» where
   srcDir := "src"
   supportInterpreter := false
 
+lean_exe «linleios_test» where
+  root := `LinleiosTest
+  srcDir := "src"
+
 require mathlib from git
   "https://github.com/leanprover-community/mathlib4" @ "v4.20.0"
 
+require LSpec from git
+  "https://github.com/argumentcomputer/LSpec.git"
+
 require Parser from git
   "https://github.com/fgdorais/lean4-parser" @ "26d5ce4d60195a869b1fdb100b442794ea63e1ad"
 

analysis/markov/src/LinleiosTest.lean

@@ -0,0 +1,24 @@
+import Linleios
+import Std.Data.HashMap
+
+open Std.HashMap (singleton_eq_insert)
+
+
+/--
+The genesis state starts with zero counts.
+-/
+theorem genesis : (default : State).clock = 0 ∧ (default : State).rbCount = 0 ∧ (default : State).ebCount = 0 := by
+  constructor
+  rfl
+  constructor
+  rfl
+  rfl
+
+/-
+The initial probability is unity.
+-/
+#guard totalProbability (default : Probabilities) == 1
+
+
+def main : IO Unit :=
+  pure ()