Stream: Coq users

Topic: Compare two infinite strings lexicographically


view this post on Zulip 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:

view this post on Zulip 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?

view this post on Zulip 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. :-)

view this post on Zulip Julin S (Apr 07 2023 at 18:43):

Does the plus in A+B mean conctenation?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Apr 08 2023 at 09:07):

but infinite strings are needed to formalize that first line

view this post on Zulip 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