decreases_to! #

The expression decreases_to!(e1, e2, ..., en => f1, f2, ..., fn) is a bool indicating if the left-hand sequence e1, e2, ..., en lexicographically-decreases-to the right-hand sequence f1, f2, ..., fn

The lexicographic-decreases-to is used to check the decreases measure for spec functions.

See this tutorial chapter for an introductory discussion of lexicographic-decreases.

Syntax #

V@[decreases_to_expr] ::= decreases_to!( V@[spec_expr] (, V@[spec_expr])* => V@[spec_expr] (, V@[spec_expr])* )

Typing #

The two expression lists on either side of => must have the same number of items. There are no other typing requirements.

Semantics #

We say that e1, e2, ..., en lexicographically-decreases-to f1, f2, ..., fn if there exists a k where 1 <= k <= n such that:

• ek decreases-to fk.
• For each i where 1 <= i < k, ei == fi.

The decreases-to relation is a partial order on all values; values of different types are comparable. The relation permits, but is not necessarily limited to:

• If x and y are integers, where x > y >= 0, then x decreases-to y.
• If a is a datatype (struct, tuple, or enum) and f is one of its "potentially recursive" fields, then a decreases-to a.f.
  • For a datatype X, a field is considered "potentially recursive" if it either mentions X or a generic type parameter of X.
• If f is a spec_fn, then f decreases-to f(i).
• If s is a Seq, then s decreases-to s[i].
• If s is a Seq, then s decreases-to s.subrange(i, j) if the given range is strictly smaller than 0 .. s.len().
  • axiom_seq_len_decreases provides a more general axiom; it must be invoked explicitly.
• If v is a Vec, then v decreases-to v@.

These axioms are triggered when the relevant expression (e.g., x.f, x->f, s[i], v@) is used as part of a decreases-to expression.

Notes #

1. Tuples are not compared lexicographically; tuples are datatypes, which are compared as explained above, e.g., a decreases-to a.0. Only the "top level" sequences in a decreases_to! expression are compared lexicographically.

2. Sequences are not compared on len() alone. However, you can always use s.len() as a decreases-measure instead of s.

Examples #

{{#include ../../../../examples/guide/recursion.rs:example_decreases_to}}