Convincing Coq that a function terminates can be frustrating. When modeling programming languages with subtyping, in particular, you might run into situations where the contravariance of function types forces you to swap the arguments of a recursive function. Coq does not know how to handle this recursion pattern and rejects the definition. This post presents a technique for dealing with such cases. Suppose that we want to model a programming language with the following types:

Our language comes with a subtyping relation T <: S that tells when it is safe to use elements of T in a context that expects elements of S. Its definition is given below as an inductive declaration.

Since Top contains arbitrary values, it makes sense for it to be a supertype of every other type in the language. Things get more interesting for functions, as subtyping goes in opposite directions for arguments and results; in common jargon, we say that subtyping treats arguments contravariantly and results covariantly. If arguments worked covariantly, any function f of type (Int → Int) → Int would also have the type Top → Int, since Int → Int <: Top. Thus, it would be possible to apply f to an Int, which has no reason to be safe if f expects a function argument. We would like to show that subtyping is decidable by expressing this relation as a boolean function. Its definition is not difficult in principle, but the naive attempt is rejected:

Recursive definition of subtypeb is ill-formed.
...
Recursive call to subtypeb has principal argument equal to "T2"
instead of one of the following variables: "T1" "S1".

What happened? Recursive functions in Coq are always defined with respect to a principal argument. In this case, the argument was marked as T using the struct keyword, but it can usually be inferred by Coq automatically. For the definition to be valid, all the recursive calls must be performed on principal arguments that are subterms of the original principal argument. However, one of the calls to subtypeb swaps its two arguments, leading to the above error message. Coq provides well-founded recursion to circumvent this rigid check, which allows recursive calls whenever the arguments decrease according to a suitable relation. In the case of subtypeb, for instance, we could show termination by proving that the combined sizes of the two arguments decrease on every call. However, there is a more direct route in this case: it suffices to add a flag to the function to specify if we are computing subtyping in the correct or opposite order. If we flip the flag on the first call, we do not need to swap the arguments.

To relate the two definitions of subtyping, we first show that flipping the flag of subtypeb_gen is equivalent to swapping the other arguments.

This yields a more convenient equation for subtypeb. (We match on S first to ensure that the RHS is definitionally equal to true when S is Top.)

Finally, we can prove that the two definitions are equivalent using the reflect predicate of Ssreflect. Showing that the inductive formulation implies the boolean one is easy: we just proceed by induction on the relation. Proving the converse is a bit more subtle, as it requires generalizing the statement with subtypeb_gen.

Update (August 9, 2019)

Robert Rand and Anton Trunov proposed an alternative approach based on mutual recursion, which I've included here for completeness. Notice how the two recursive functions have different recursive arguments.