feat: List.SatisfiesM_foldlM

leanprover-community / batteries

The "batteries included" extended library for the Lean programming language and theorem prover

Apache License 2.0

253 stars 105 forks source link

In conjunction with #1029, and https://github.com/leanprover/lean4/pull/6023, we can do things like:

def addRandomEvens (n : Nat) (k : Nat) : IO Nat := do
  let mut r := k
  for _ in List.range n do
    r := r + 2 * (← IO.rand 0 37)
  pure r

theorem addRandomEvens_spec (n k) : SatisfiesM (fun r => r % 2 = k % 2) (addRandomEvens n k) := by
  rw [addRandomEvens]
  simp [List.forIn_yield_eq_foldlM]
  apply List.SatisfiesM_foldlM
  · rfl
  · intros b w a m
    apply SatisfiesM.bind_pre
    simp_all [SatisfiesM_EStateM_eq, EStateM.run]

def addRandomEvens' (n : Nat) (k : Nat) : IO { r : Nat // r % 2 = k % 2 } := do
  satisfying (addRandomEvens_spec n k)

leanprover-community / batteries

feat: List.SatisfiesM_foldlM #1034