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: Oct 13 2024 at 01:02 UTC