Summary

Make it possible to write explicit expressions, especially in assertions, that describe the proposition that a termination metric decreases.

Background and Motivation

As part of #2987, we want to be able to create an explicit assert statement for any proof goal that fails. Currently, stating that a termination metric decreases is awkward or impossible, for several reasons:

• The direct statement that a set of metrics a, b, c decreases to a', b', c' is something roughly like a > a' || (a == a' && b > b') || (a == a' && b == b' && c > c'), which is large and hard to read.
• Writing a > a’ doesn’t currently mean the right thing for sequences or datatypes.
• Equality isn’t well-typed for all instances involving datatypes (since the two sides may have different types).

Proposed Feature

I propose we introduce a custom expression form, a, b, c decreases to a', b', c' that is shorthand for roughly the larger expression shown above but with the correct semantics for == and > when considering sequences and datatypes.

The parser will eagerly parse all commas when parsing this form, so parentheses may be required to disambiguate some instances, but frequently should be unnecessary.

Alternatives

Several alternatives are possible:

• We could introduce a new operator that describes the appropriate ordering for sequences or datatypes and use an expanded form of the termination predicate roughly like shown above but with the new operator. This would be verbose, however.
• We could update > ordering for sequences or datatypes and use a termination predicate exactly of the form shown above. This could perhaps break existing code and would be verbose.