1

How to define list of natural numbers without gaps in Coq? For example [2, 1, 3] is valid list, but [5, 1, 3] is not because it have two gaps: between 1 and 3, 3 and 5.

I have try to ask Google, but nothing similar was found

1 Answer 1

1

You could say that a list of length n is without gaps iff its sorted version is equal to the list of naturals from 1 to n. If need be, this could be packaged in a dependent record, with the list and its no-gap property as fields.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.