Stream: Coq users

Topic: Built in way to convert string to nat (or positive)


view this post on Zulip walker (Feb 12 2023 at 13:03):

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.

view this post on Zulip Karl Palmskog (Feb 12 2023 at 13:06):

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

view this post on Zulip Gaëtan Gilbert (Feb 12 2023 at 13:17):

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

view this post on Zulip walker (Feb 12 2023 at 13:36):

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

view this post on Zulip Gaëtan Gilbert (Feb 12 2023 at 13:37):

the one I linked is nat -> Decimal.uint IIUC
should be pretty easy to go to string from there

view this post on Zulip Pierre Roux (Feb 12 2023 at 16:09):

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

view this post on Zulip walker (Feb 12 2023 at 16:58):

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