Search code examples
coqssreflect

string comparison in ssreflect

I'm trying to make an ssreflect OrdType out of a custom type which involves strings. I assume that there is some inbuilt order type for strings in ssreflect, but I can't find it anywhere. I see one in Coq's standard library, but I can't figure out if the definition transfers to the ssreflect library. I'd much rather use ssreflect than the Coq standard library. Could someone point me where to look please? Thanks.

Solution

  • unfortunately OrdType is not the order that has been integrated to mathcomp/ssreflect package in the end (Coq-Combi preceeds this integration), but it follows the same scheme. Which order do you want? Lexicogrphic? Prefix? Suffix?

    • If you want to use lexicographic order with the standardized order in mathcomp/ssreflect, I suggest you use the isomorphism between String and list ascii and the lexical ordering on the latter to define a total order on string (you need to provide a orderType canonical structure for ascii).
    • If you want a prefix order, you can prove Strings.prefix function is a partial order.