Tidied up function definitions

Author: bwbush

analysis/markov/src/Linleios/Evolve.lean

@@ -110,7 +110,7 @@ def simulate (env : Environment) (start : Probabilities) (ε : Float) : Nat →
 Compute the total probabilities of a set of states.
 -/
 def totalProbability (states : Probabilities) : Probability :=
-  states.values.sum
+  states.fold (Function.const State ∘ Add.add) 0
 
 /--
 Compute the distribution of EB counts.
@@ -119,6 +119,7 @@ def ebDistribution : Probabilities → HashMap Nat Probability :=
   HashMap.fold
     (
       fun acc state p =>
+        -- FIXME: Rewrite using `Function.const`.
         HashMap.mergeWith (fun _ => Add.add) acc
           $ singleton ⟨ state.ebCount , p ⟩
     )

analysis/markov/src/Linleios/Types.lean

@@ -74,24 +74,14 @@ structure State where
   canCertify : Bool
 deriving Repr, BEq, Hashable, Inhabited
 
-/--
-The genesis state starts when zero counts.
--/
-theorem genesis : (default : State).clock = 0 ∧ (default : State).rbCount = 0 ∧ (default : State).ebCount = 0 := by
-  constructor
-  rfl
-  constructor
-  rfl
-  rfl
-
-
 /--
 The active states and their probabilities.
 -/
 def Probabilities := HashMap State Probability
 deriving Repr, EmptyCollection
 
 instance : Inhabited Probabilities where
+  -- TODO: Rewrite using `Singleton.singleton`.
   default := (∅ : Probabilities).insert Inhabited.default 1