3

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.

push33n
  • 398
  • 4
  • 12
  • 1
    AFAIR, [extructures](https://github.com/arthuraa/extructures) has its own ordType and an instance for strtings. However, these days there is a number of types with order/lattice structures in Mathcomp: https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/order.v. Although, it does have an instance for strings. – Anton Trunov Aug 14 '20 at 20:22
  • * sorry, I made a typo: does *not* have an instance for strings – Anton Trunov Aug 15 '20 at 11:55

1 Answers1

2

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.
Cyril
  • 367
  • 2
  • 7