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

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

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

Does the plus in A+B mean conctenation?

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

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.

but infinite strings are needed to formalize that first line

yep I guess simply using `nat -> Ascii`

would suffice.

Last updated: Oct 04 2023 at 22:01 UTC