First a note: you are using the syntax for so-called "positive" coinductive types, which makes them look like inductive types, defined by "constructors". This has various problems: it's not well-justified semantically, and syntactically it breaks "subject reduction". Modern versions of Coq also support "negative" coinductive types, which look like record types rather than inductive types, defined by "fields", and are much better-behaved, so it is suggested to use those instead. See the reference manual.
As for the actual question, I believe one place that coinduction is valuable is when computational behavior matters. An infinite list represented by a function nat -> A is "random access": you can ask it for f n whenever you wish, and it doesn't in principle need to know anything about f k for k < n to compute f n. Whereas the elements of a coinductive stream must be computed in order. This certainly makes the function-representation easier to reason about.
However, if your "infinite list" has the property that in practice we have to compute all the f k for k < n in order to find f n, then working with the coinductive version respects this, and encourages the user to take account of it. Given a stream we can turn it into a function where f n is computed by pulling off n elements of the stream and returning the last one, but this performs a lot of computation if n is large, and if we call f a lot of times it could be very inefficient. A coinductive data representation encourages the writing of corecursive functions, which force us to deal with this kind of stepwise-computed list more efficiently.
Streams are arguably a bit too simple for this behavior to be clearly visible. I like to think of a general coinductive type as a "server", in line with Conor McBride's comment in Let's see how things unfold:
As a total programmer, I am often asked 'how do I implement a server as a program in your terminating language?', and I reply that I do not: a server is a coprogram in a language guaranteeing liveness.
An element of a coinductive "server type" represents the server in a particular state. When we call its destructor, we pass it some request from a client, and it returns a response to the client and also the new state of the server. By contrast, using the corresponding "functional" representation, in order to compute the response of the server to any query we would have to replay the entire history of interaction of all clients with the server up to that point. Clearly this is inefficient, and also a bad representation of how a real-world server actually works.
Coinductive types can also be valuable in situations where type dependency makes it tricky to even come up with a functional representation, and if you do come up with one it's more awkward. I'm most familiar with this in the case of homotopy theory and higher category theory. For instance, a "globular set" can be defined coinductively as a set $A$ together with a family of globular sets indexed by $A\times A$:
CoInductive GSet : Type := {
carr : Type;
hom : carr -> carr -> GSet;
}.
The corresponding functional representation is much less clear. This can be enhanced to deal with infinite-dimensional categories in a surprisingly clean way.
