coq - ssreflect 中的字符串比较

Question

我正在尝试制作 ssreflect OrdType来自涉及字符串的自定义类型。我假设 ssreflect 中有一些内置的字符串订单类型，但我无法在任何地方找到它。我在 Coq 的标准库中看到一个，但我无法弄清楚定义是否转移到 ssreflect 库。我宁愿使用 ssreflect 而不是 Coq 标准库。有人可以指点我在哪里看吗？谢谢。

Answer 1

很遗憾，OrdType 不是已集成到 mathcomp/ssreflect package 的订单最后(Coq-Combi 在此集成之前)，但它遵循相同的方案。你要哪个顺序？辞典？字首？后缀？

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