The notion of monotonic, or order-preserving, functions is a key notion in programming languages semantics, being used in both logical relations and denotational semantics. In Coq, monotonic functions are also known as Proper functions, because they are usually defined with the Proper typeclass, and they are used for setoid rewriting. Although it is straightforward to define a Coq type for Proper functions, it is onerous and time-consuming to build any non-trivial Proper functions in this type, as the user has to manually write the proofs of monotonicity at every Proper abstraction. Further, rewriting these Proper functions requires rewriting their proofs as well, which can increase the size of expressions dramatically with each rewrite step.

In this talk, ongoing work will be presented that addresses both of these problems. To build Proper functions, a collection of Coq typeclass instances and notations are used to automatically build monotonicity proofs, effectively creating an embedded domain-specific language (EDSL) of Proper functions inside Coq. To rewrite Proper functions, they are first reflected into a Coq inductive datatype that represents Proper functions without requiring monotonicity proofs. This reflection is performed using a second collection of Coq typeclass instances. Because this inductive datatype does not require monotonicity proofs, rewriting becomes orders of magnitude more efficient.