Stream: Coq users

Topic: ✔ Equivalent of nat S in Coq.NArith.NArith


view this post on Zulip Julio Di Egidio (Oct 28 2023 at 16:40):

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.

view this post on Zulip Notification Bot (Oct 28 2023 at 16:42):

Julio Di Egidio has marked this topic as resolved.

view this post on Zulip Ana de Almeida Borges (Nov 01 2023 at 17:54):

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.

view this post on Zulip Ana de Almeida Borges (Nov 01 2023 at 17:56):

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.

view this post on Zulip Julio Di Egidio (Nov 02 2023 at 19:33):

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.

view this post on Zulip Notification Bot (Nov 02 2023 at 19:34):

Julio Di Egidio has marked this topic as resolved.


Last updated: Jun 23 2024 at 05:02 UTC