lean4 icon indicating copy to clipboard operation
lean4 copied to clipboard
verified publisher icon leanprover

feat: `MonadAttach`

Open datokrat opened this issue 1 month ago • 3 comments

This PR adds the new operation MonadAttach.attach that attaches a proof that a postcondition holds to the return value of a monadic operation. Most non-CPS monads in the standard library support this operation in a nontrivial way. The PR also changes the filterMapM, mapM and flatMapM combinators so that they attach postconditions to the user-provided monadic functions passed to them. This makes it possible to prove termination for some of these for which it wasn't possible before. Additionally, the PR adds many missing lemmas about filterMap(M) and map(M) that were needed in the course of this PR.

datokrat avatar Dec 06 '25 13:12 datokrat

Thanks for taking a look! I believe to have proven this to be a sound and strongest postcondition: https://github.com/leanprover/lean4/pull/11532/files#diff-184d01e2db4041ff3005df8db105c00db20c4f7b16b069cc9d504aafa58a337dR12

Is there a desirable property missing in LawfulMonadAttach or what kind of constraint are you thinking about?

datokrat avatar Dec 09 '25 01:12 datokrat

Mathlib CI status (docs):

  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-12-13 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-13 16:35:26)

leanprover-community-bot avatar Dec 13 '25 16:12 leanprover-community-bot

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-12-13 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-12-13 16:35:27)
  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-12-15 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-12-16 11:46:22)

leanprover-bot avatar Dec 13 '25 16:12 leanprover-bot