The authors provide a Coq formalization of the interplay between nondeterministic choice \(\square\) and probabilistic choice \(\triangleleft p \triangleright\) using a \(\square\)-infinitary version of the axiom \[ x \triangleleft p \triangleright (y \square z) = (x \triangleleft p \triangleright y) \square (x \triangleleft p \triangleright z) \] The composite theory corresponds to the geometrically convex monad on sets, arising from the convex powerset monad on semicomplete semilattices. The paper builds on the work of J. Gibbons and R. Hinze [in: Proceedings of the 16th ACM SIGPLAN international conference on functional programming, ICFP ’11, Tokyo, Japan, September 19–21, 2011. New York, NY: Association for Computing Machinery (ACM). 2–14 (2011; Zbl 1323.68207)] which suffered from a mistake, justifying the need for formalization. This is related to the fact that the dual axiom \[ x \square (y \triangleleft p \triangleright z) = (x \square y) \triangleleft p \triangleright (x \square z) \] is known to yield a degenerate composite theory.
The authors provide a Coq interface for the composite algebraic theory, filling a gap in the MONAE framework for monadic equational reasoning. They build the geometrically convex monad modularly by composing three adjunctions. They provide a formal proof that the composite theory is non-degenerate.
Technical Coq developments mostly rely on packed classes. They include:

●

extending existing formalization of convex spaces with affine functions,

●

formalization of semicomplete semilattices convex spaces,

●

formalization of adjunctions and monads for concrete categories.