feat: List.SatisfiesM_foldlM

[kim-em]

No description provided.

[kim-em]

In conjunction with #1029, and leanprover/lean4#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-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch batteries-pr-testing-1034 has successfully built against this PR. (2024-11-11 02:51:09) View Log
• ✅ Mathlib branch batteries-pr-testing-1034 has successfully built against this PR. (2024-11-12 04:13:06) View Log
• 🟡 Mathlib branch batteries-pr-testing-1034 build against this PR was cancelled. (2024-11-12 23:15:22) View Log
• ✅ Mathlib branch batteries-pr-testing-1034 has successfully built against this PR. (2024-11-12 23:54:25) View Log