-
Notifications
You must be signed in to change notification settings - Fork 26
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Express range constraints where an expression is bounded #1801
Comments
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!). |
@JacquesCarette I may have recklessly used the term "list" instead of "vector". From Drasil's perspective, the |
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 In general, there are really 2 kinds of constraints:
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] |
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 anExpr
with thedim
function in Drasil. So we want to constrain the expressiondim x
. But in Drasil, the thing we are constraining must itself be a quantity in Drasil. So we would first need to create aQuantityDict
for the size of x, aQDefinition
to give it the definingExpr
, and aConstrainedChunk
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?
The text was updated successfully, but these errors were encountered: