string comparison in ssreflect

user_9910692 0
Viewed 86

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.

ssreflect coq
1 Answers

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.
user_150298030
Related