Questions says it all, I am looking for an existing function somewhere that takes string converts it to nat or positive + proofs that it is left and right invertible.

there are really no built-in functions in Coq. And there was no Stdlib function for this last I checked. Here are some "custom" ones that do `string`

to `positive`

: https://github.com/uwplse/verdi/blob/master/lib/FMapVeryWeak.v#L147

there are functions like https://github.com/coq/coq/blob/155688103c43f578a8aef464bf0cb9a76acd269e/theories/Init/Nat.v#L227 used for printing through https://coq.github.io/doc/master/refman/user-extensions/syntax-extensions.html#coq:cmd.Number-Notation

but I don't think we have any proofs about those functions

but those are from nat to positive, right ? or am I missing something ?

the one I linked is `nat -> Decimal.uint`

IIUC

should be pretty easy to go to string from there

Maybe https://github.com/coq/coq/blob/master/theories/Numbers/DecimalString.v can help

actually I thought I would check and see what they are doing in stdpp apparently they had what I was looking for an apparently for the exact same reason:

https://plv.mpi-sws.org/coqdoc/stdpp/stdpp.strings.html#lab102

Last updated: Jun 18 2024 at 09:02 UTC