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