Annotation for inequalities of sequence lengths

[panacekcz]

The index checker has no way to express that one sequence is at least as long as another sequence. This is useful when indexing a longer sequence by an index for a shorter sequence.

• @LongerThanEq(value, offset) would mean that the annotated sequence is at least as long as value plus offset (if a is @LongerThanEq(value="b", offset="o"), then a.length >= b.length + o)
• if a is @LongerThanEq(value="b", offset="o") and i is @LTLengthOf(value="b", offset="p"), then i can be treated as @LTLengthOf(value="a", offset="o+p")
• a reverse annotation @ShorterThanEq is probably less useful. If it is added, then the glb of @LongerThanEq("a") and @ShorterThanEq("a") should be @SameLen("a")
• @SameLen("a") should be a subtype of @LongerThanEq("a")
• if a is @LongerThanEq(value="b", offset="o") and b is @LongerThanEq(value="b", offset="p"), then a can be treated as @LongerThanEq(value="c", offset="o+p") (transitivity)

This issue was reported before as #43 and panacekcz#11.
The annotations were originally proposed in #158. The difference between these issues is that #158 is about relations of integer variables representing indices, while this is about relations of sequence variables.
Related: #132.

[panacekcz]

• if a is @LongerThanEq(value="b"), then a.length - b.length is @NonNegative
• if a is @LongerThanEq(value="b"), and b is @MinLen(x), then a could be treated as @MinLen(x) (this probably cannot be done because of the order of index subcheckers)