Stream: Coq users

Topic: Associativity of monadic bind

Huỳnh Trần Khanh (Sep 29 2023 at 06:53):

This is a very basic question. I have a monad. I wrote the bind function. As the monad is a unit monad I don't have to prove identity rules, but I still have associativity. I have 10 cases now, am I supposed to plow through them? I remember that I've seen a trick to prove these cases quickly. https://github.com/huynhtrankhanh/CoqCP/blob/d478e0cb195e18f3a6fedb5788a1871ad434d1cd/theories/Imperative.v#L36

Karl Palmskog (Sep 29 2023 at 07:02):

I think you're asking several questions here. There is the domain-specific question of expressing the monad (you might want to look at ExtLib and in particular its Monad typeclass). There is also the proof engineering question of easy/maintainable proof scripts, where you have many options from custom Ltac tactics to reflection machinery. It's usually good to use simple machinery such as hand-written low-level tactics to get to Qed first and then make it better afterwards. I wrote something about the "hierarchy" of automation tactics here.

Last updated: Oct 08 2024 at 16:02 UTC