## Stream: Coq users

### Topic: Compare two infinite strings lexicographically

#### Huỳnh Trần Khanh (Apr 07 2023 at 03:58):

Here's the next thing I'd like to prove with Coq. I have two strings A and B consisting of characters from a to z. Let extendedA be an infinite string which is composed of the string A repeated infinitely. Let extendedB be an infinite string which is composed of the string B repeated infinitely. I would like to check whether extendedA is lexicographically smaller than extendedB. In order to check, we have a fact: extendedA < extendedB if and only if A + B < B + A. Questions:

• What is the best way to state this fact? I imagine that we could make extendedA and extendedB functions that map from nat to a type that denotes a character from a to z. I need suggestions to state this fact elegantly.
• What is the best strategy to prove this fact? Here is an informal proof, but I doubt this can be formalized elegantly. https://codeforces.com/blog/entry/91381?#comment-808323

#### Huỳnh Trần Khanh (Apr 07 2023 at 17:00):

Hello, is this question too vague? Do you need me to clarify the question?

#### Julin S (Apr 07 2023 at 18:42):

Others might be able to understand the question, but for a noob like me an example would help make things clearer. :-)

#### Julin S (Apr 07 2023 at 18:43):

Does the plus in A+B mean conctenation?

#### Karl Palmskog (Apr 07 2023 at 18:49):

the current recommended way to define and state properties about infinite objects seems to be negative coinductive types, like in the Interaction Trees library: https://github.com/DeepSpec/InteractionTrees

Some discussion here about positive vs. negative coinductive types in Coq: https://proofassistants.stackexchange.com/questions/583/what-is-the-state-of-coinductive-types-and-reasoning-in-coq

#### Laurent Théry (Apr 08 2023 at 08:59):

I am not sure the infiniteness is the problem here. The first line of the proof just tells us that we just need to look at the `(size A) * (size B)` first characters, so the rest of the proof is finite.

#### Paolo Giarrusso (Apr 08 2023 at 09:07):

but infinite strings are needed to formalize that first line

#### Laurent Théry (Apr 08 2023 at 09:10):

yep I guess simply using `nat -> Ascii` would suffice.

Last updated: Jun 20 2024 at 11:02 UTC