feat: Laws for monads with Alternative instances.

[dtumad]

This PR adds type-classes AlternativeMonad, LawfulAlternative, and LawfulAlternativeLift that enforce laws regarding failure and orElse.

Lemmas about OptionT are also upstreamed from mathlib to use in the LawfulAlternative proof. OptionT.run_bind was changed as part of this move to use Option.elimM rather than explicit pattern matching in the lemma.

Additional instances for Set and List need to be written to mathlib as that is where the main monad instances for those types are.

[leanprover-community-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch batteries-pr-testing-1152 build failed against this PR. (2025-03-05 22:34:17) View Log
• 💥 Mathlib branch batteries-pr-testing-1152 build failed against this PR. (2025-03-07 20:18:56) View Log
• ✅ Mathlib branch batteries-pr-testing-1152 has successfully built against this PR. (2025-03-10 06:32:17) View Log
• ✅ Mathlib branch batteries-pr-testing-1152 has successfully built against this PR. (2025-03-10 10:08:44) View Log
• 🟡 Mathlib branch batteries-pr-testing-1152 build against this PR was cancelled. (2025-03-12 00:34:11) View Log
• 🟡 Mathlib branch batteries-pr-testing-1152 build this PR didn't complete normally. (2025-03-12 00:34:31) View Log
• 💥 Mathlib branch batteries-pr-testing-1152 build failed against this PR. (2025-03-12 02:11:32) View Log
• ✅ Mathlib branch batteries-pr-testing-1152 has successfully built against this PR. (2025-03-12 06:28:46) View Log

[Rob23oba]

I wouldn't immediately go for defining LawfulAlternative on AlternativeMonads, the failure_bind rule can be recovered from map_failure and failure_seq:

class LawfulAlternative (m : Type u → Type v) [Alternative m] extends LawfulApplicative m where
  map_failure {α β : Type u} (f : α → β) : f <$> (failure : m α) = failure
  failure_seq {α β : Type u} (x : m α) : (failure : m (α → β)) <*> x = failure
  -- ...

export LawfulAlternative (map_failure failure_seq)

class AlternativeMonad (m : Type u → Type v) extends Alternative m, Monad m

theorem failure_bind [AlternativeMonad m] [LawfulMonad m] [LawfulAlternative m] (x : α → m β) : failure >>= x = failure := by
  conv => lhs; rw [← map_failure PEmpty.elim]
  conv => rhs; rw [← bind_pure failure]
  conv => rhs; rw [← map_failure PEmpty.elim]
  simp only [bind_map_left]
  congr 1; funext a
  exact a.elim

[dtumad]

@Rob23oba updated to that definition for the class, using PEmpty.elim in the proof like that is a very neat trick.

[dtumad]

What's the procedure for updating mathlib after upstreaming these OptionT lemmas? I'm not sure how to handle coordinating the two changes, should I just open a mathlib PR with the relevant lemmas removed? Or remove the imports from Batteries.lean so that mathlib doesn't see the duplicate lemmas when building mathlib?

[eric-wieser]

LGTM, thanks!

You should get a mathlib adaption PR ready to go before this gets merged, so as not to hold up merging other PRs.

[fgdorais]

This needs a Mathlib adaptation before merging. Ideally, this just involves pushing changes to the Mathlib branch batteries-pr-testing-1152 until it works. Let us know if you have questions of if you run into complications.

[fgdorais]

Thanks! Could you create an actual Mathlib PR out of batteries-pr-testing-1152. I think this needs a review on the Mathlib end. You may have to ping someone to review it. Ask @eric-wieser if they are interested or if they have alternate recommendations for that review. Once that's done, ping back here since Batteries maintainers won't be notified automatically.

[eric-wieser]

I'd be happy to review it

[dtumad]

Sorry about the slow response. This PR has the needed changes. Should I change the mathlib lakefile back to main batteries repo before this gets merged here?

[eric-wieser]

@fgdorais, I'm happy with the adaptation PR, just the stray comment to delete above.

[fgdorais]

I made a few style changes because Batteries prefers to avoid section variables and also makes systematic use of autoimplicits. Please have a quick look at my changes in case there are instances where Lean doesn't automatically make the right choice.