Relational program logic

This is a formalization of the paper The next 700 relational program logics.

We follow the paper as well as the Coq formalization in SSProve.

class Monad.IsCommutativeAt (m : Type u → Type v) [Monad m] {α β : Type u} (ma : m α) (mb : m β) : Prop

Two monadic actions ma : m α and mb : m β are commutative if the following holds:

(do let a ← ma; let b ← mb; pure (a, b)) = (do let b ← mb; let a ← ma; pure (a, b))

• bind_comm : (do let a ← ma let b ← mb pure (a, b)) = do let b ← mb let a ← ma pure (a, b)

class Monad.IsCommutative (m : Type u → Type v) [Monad m] : Prop

A monad is commutative if any two monadic actions ma : m α and mb : m β can be applied in any order. In other words, the following holds:

(do let a ← ma; let b ← mb; f (a, b)) = (do let b ← mb; let a ← ma; f (a, b))

• bind_comm_comp {α β : Type u} (ma : m α) (mb : m β) : IsCommutativeAt m ma mb