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