Express range constraints where an expression is bounded

[bmaclach]

A Range constraint can be used to express bounds on a quantity, but that means that the thing you are bounding must be a quantity. Consider the constraint that the size of a list x must be greater than some number. The size of a list can be represented as an Expr with the dim function in Drasil. So we want to constrain the expression dim x. But in Drasil, the thing we are constraining must itself be a quantity in Drasil. So we would first need to create a QuantityDict for the size of x, a QDefinition to give it the defining Expr, and a ConstrainedChunk to add the constraint.

I wonder if we should be able to instead define constraints on an expression. So this would be a constraint on x, but in the constraint we would be able to include x in an expression.

Or is this a case where what we have currently is good, but in the future we would want to be able to inline the expression for that quantity for the size of x, so that it looks (when reading the SRS) that the constraint is on an expression?

[JacquesCarette]

This is another encoding issue. If you were using a sized vector instead of a list, then the vector's size is a known quantity that you can access directly. 'lists' are sized vectors that have forgotten their size (this is actually something that can be proved formally!).

[bmaclach]

@JacquesCarette I may have recklessly used the term "list" instead of "vector". From Drasil's perspective, the Space of the quantity x is a Vector. I may be misunderstanding your comment, but I don't think being able to directly access the size solves this issue (accessing the size is still an Expr, isn't it?). Regardless, accessing the size is the example I happened to choose to demonstrate the issue, but this issue exists for any constraint where the value being bounded is an Expr. There are other places where this arises in SSP. Another example is the constraint that the angle between adjacent slice bases must exceed 110 degrees, which is a constraint on the expression for the angle between two slice bases.

[JacquesCarette]

In a properly dependently-typed system, the size of a vector would have to be an independent quantity that pre-exists. So in that case, there is no need for a range constraint on an Expr.

In general, there are really 2 kinds of constraints:

1. those we can 'invert', i.e. those where we can immediately compute lots of consequences of the constraint holding immediately
2. the others, which are general relations between things, and with which the system can't do much.

We want to maximize our use of constraints of type 1. And this is a bit tricky at times, because often mathematically equivalent formulations will computationally shift between 1 & 2. [This usually happens when the 'equivalence' of the formulations requires a not-entirely-trivial proof]