coq - ssreflect 中的字符串比较

Question

我正在尝试从涉及字符串的自定义类型中创建一个 ssreflect OrdType 。我假设 ssreflect 中有一些内置的字符串顺序类型，但我在任何地方都找不到。我在 Coq 的标准库中看到了一个，但我不知道定义是否转移到了 ssreflect 库。我宁愿使用 ssreflect 而不是 Coq 标准库。有人可以指点我在哪里看吗？谢谢。

Answer 1

不幸OrdType的是，最终不是集成到mathcomp/ssreflect 包的顺序（Coq-Combi 在此集成之前），但它遵循相同的方案。你要哪个订单？词汇？字首？后缀？

• 如果您想在 mathcomp/ssreflect 中使用具有标准化顺序的字典顺序，我建议您使用 and 之间的同构String和list ascii后者的词法顺序来定义字符串的总顺序（您需要为 提供orderType规范结构ascii）。
• 如果你想要一个前缀顺序，你可以证明Strings.prefix函数是一个偏序。