Many programming languages have built-in support for string processing. Coq is no exception. The standard library provides us with its own definition of strings. Unlike other languages, though, strings in Coq are not fundamentally different from other data types: they are defined as an inductive type.

As we can see, strings are much like the list type, but contain ascii elements instead of elements of an arbitrary type. asciis, on the other hand, are just eightuples of bools.

Sure enough, if we had to use constructors explicitly for building strings, using them in Coq wouldn't be very practical. Fortunately, Coq provides a convenient notation for strings and ascii, much like the built-in notation for numbers. They are defined in string_scope and char_scope, respectively.

Let's see what kind of string-processing functions we can write. One could certainly hope that we'd be able to write a function to read numbers. To do this, we will need a function to convert asciis to nats: if the character is a digit, we return the corresponding number. Otherwise, the whole parsing should fail. As in other functional programming languages, we model this by making our function return an option instead ─ in this case, option nat.

We can now use this function to read numbers. To make it more efficient, we can add an acc parameter to store the intermediate results of the computation ─ i.e., the number we've read so far.

We can write some unit tests to make sure our function behaves as expected.

Since we have a function for reading numbers, we should now be able to write one for printing them. Again, as a first step, let's write a function that converts nats to their corresponding digits.

In all rigor, natToDigit should return an option ascii instead of a plain ascii, just like we did in our previous digitToNat function. After all, it doesn't make any sense to associate any digit to, say, 10. However, if we make sure that we only use this function on numbers less than 10, we don't have to do an explicit conversion from option ascii to ascii later on, and our function will still be correct. As a matter of fact, we can now prove a theorem that tells us when it's safe to use natToDigit.

In particular, we get the following consequence, which will be particularly useful later:

Now that we can convert numbers to digits, let's see how we could write our printing function. One idea would be to add a parameter to our function to accumulate the paritially printed number:
    Fixpoint writeNatAux (n : nat) (acc : string) : string :=
      let acc' := String (natToDigit (n mod 10)) acc in
      match n / 10 with
        | 0 => acc'
        | n' => writeNatAux n' acc'
      end.

The algorithm is straightforward. We print the least signigicant digit of the number, adding it to the string we've printed so far (recall that the String constructor adds a character to the front of a string). Then, we divide the number by 10 and print it recursively, until we reach zero. Unfortunately, Coq doesn't accept this definition, since the recursive call is not done on structurally smaller terms. There are lots of ways to make this definition work, such as using the Program command. We will use the somewhat simpler, but standard, trick of adding an explicit "timeout" parameter to our function.

At each step, we do a pattern match on the timeout parameter. If we reach 0, our computation must stop, and we just give back the string we've printed so far. Otherwise, we have a structurally smaller argument we can use to do a recursive call, which will make Coq accept the definition. Now, in order to effectively print a number, we need to find a timeout value that is big enough to perform the entire computation. In this case, as it turns out, we can use the very the number we're printing for the timeout parameter.

Let's test our definition on some simple examples.

It seems clear that readNat is indeed the inverse of writeNat, but can we prove this rigorously in Coq? Formally, we can state the theorem we want as

Since both functions are defined in terms of auxiliary fixpoints, it is better to prove something about them first and then use that fact to get the result we want as a consequence. Here's one such possibility:

Notice the precondition n <= time in the above statement. As mentioned before, we must give enough time to writeNatAux for it to function correctly. This precondition is just stating this fact explicitly. It is easy to prove that this lemma will suffice.

Now, we are ready to prove our intermediate lemma. As usual, since writeNatAux is defined by recursion on time, trying the proof by induction on time seems a good guess. Let's begin with a simple lemma that will be useful later. It states that if the precondition for our lemma is satisfied, then it'll also be satisfied for the recursive call, which will allow us to apply the induction hypothesis.

We can proceed with our proof.

The final result follows easily.