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:
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