		Search-engine friendly clone of the ACL2 documentation.

Ordering

Charlistnat<

Mixed alphanumeric character-list less-than test.

(charlistnat< x y) determines if the character list x is "smaller" than the character list y, using an ordering that is nice for humans.

This is almost an ordinary case-sensitive lexicographic ordering. But, unlike a simple lexicographic order, we identify sequences of natural number digits and group them together so that they can be sorted numerically.

Even though this function operates on character lists, let's just talk about strings instead since they are easier to write down. If you give most string sorts a list of inputs like "x0" through "x11", they will end up in a peculiar order:

"x0", "x1", "x10", "x11", "x2", "x3", ... "x9"

But in charlistnat<, we see the adjacent digits as bundles and sort them as numbers. This leads to a nicer ordering:

"x0", "x1", "x2", ..., "x9", "x10", "x11"

This is almost entirely straightforward. One twist is how to accommodate leading zeroes. Our approach is: instead of grouping adjacent digits and treating them as a natural number, treat them as a pair with a value and a length. We then sort these pairs first by value, and then by length. Hence, a string such as "x0" is considered to be less than "x00", etc.

Definitions and Theorems

Function: charlistnat<

(defun charlistnat< (x y)
  (declare (xargs :guard (and (character-listp x)
                              (character-listp y))))
  (cond ((atom y) nil)
        ((atom x) t)
        ((and (dec-digit-char-p (car x))
              (dec-digit-char-p (car y)))
         (b* (((mv v1 l1 rest-x)
               (parse-nat-from-charlist x 0 0))
              ((mv v2 l2 rest-y)
               (parse-nat-from-charlist y 0 0)))
           (cond ((or (< v1 v2)
                      (and (int= v1 v2) (< l1 l2)))
                  t)
                 ((or (< v2 v1)
                      (and (int= v1 v2) (< l2 l1)))
                  nil)
                 (t (charlistnat< rest-x rest-y)))))
        ((char< (car x) (car y)) t)
        ((char< (car y) (car x)) nil)
        (t (charlistnat< (cdr x) (cdr y)))))

Theorem: charlisteqv-implies-equal-charlistnat<-1

(defthm charlisteqv-implies-equal-charlistnat<-1
  (implies (charlisteqv x x-equiv)
           (equal (charlistnat< x y)
                  (charlistnat< x-equiv y)))
  :rule-classes (:congruence))

Theorem: charlisteqv-implies-equal-charlistnat<-2

(defthm charlisteqv-implies-equal-charlistnat<-2
  (implies (charlisteqv y y-equiv)
           (equal (charlistnat< x y)
                  (charlistnat< x y-equiv)))
  :rule-classes (:congruence))

Theorem: charlistnat<-irreflexive

(defthm charlistnat<-irreflexive
  (not (charlistnat< x x)))

Theorem: charlistnat<-antisymmetric

(defthm charlistnat<-antisymmetric
  (implies (charlistnat< x y)
           (not (charlistnat< y x))))

Theorem: charlistnat<-transitive

(defthm charlistnat<-transitive
  (implies (and (charlistnat< x y)
                (charlistnat< y z))
           (charlistnat< x z)))

Theorem: charlistnat<-trichotomy-weak

(defthm charlistnat<-trichotomy-weak
  (implies (and (not (charlistnat< x y))
                (not (charlistnat< y x)))
           (equal (charlisteqv x y) t)))

Theorem: charlistnat<-trichotomy-strong

(defthm charlistnat<-trichotomy-strong
  (equal (charlistnat< x y)
         (and (not (charlisteqv x y))
              (not (charlistnat< y x))))
  :rule-classes ((:rewrite :loop-stopper ((x y)))))