Thanks @Pierre Castéran, that works, though writing recursive functions gets quite tricky due to 'positive' being low-endian, to the point that I am not sure how actually usable it is (for my purposes). Anyway I am quite new to the ecosystem, still lots to learn.

Thanks very much everybody for the help. I am closing this question.

Julio Di Egidio has marked this topic as resolved.

Working with `N`

is annoying precisely because of this. If your definitions happen to depend only on arithmetic such as addition, multiplication, and so on, you might consider using only the already existing definitions to build your own, without going down to fixpoints. Then `lia`

ought to help with proofs. If you do need to define recursive functions decreasing on an `N`

argument and later prove theorems about them by induction, it might be easier to do everything with `nat`

and then refine it to `N`

.

By refinement I mean having two versions of every definition, one with `nat`

and one with `N`

. You then prove whatever you want about the `nat`

version and use a lemma to the effect that `nat`

and `N`

behave the same to transport the results on the `nat`

version to the `N`

version, thus avoiding inductive arguments for proofs about the `N`

version.

Thanks @Ana de Almeida Borges, that was very helpful.

I will mark this question again as resolved: though I will probably post what I eventually come up with, for more feedback.

Julio Di Egidio has marked this topic as resolved.

Last updated: Jun 23 2024 at 05:02 UTC