		Search-engine friendly clone of the ACL2 documentation.

Std/strings/coerce

Lemmas about coerce available in the std/strings library.

We typically do not want to ever reason about coerce. Instead, we rewrite it away into explode or implode.

Definitions and Theorems

Theorem: equal-of-coerce-strings

(defthm equal-of-coerce-strings
  (implies (and (character-listp x)
                (character-listp y))
           (equal (equal (coerce x 'string)
                         (coerce y 'string))
                  (equal x y))))

Theorem: equal-of-coerce-lists

(defthm equal-of-coerce-lists
  (implies (and (stringp x) (stringp y))
           (equal (equal (coerce x 'list)
                         (coerce y 'list))
                  (equal x y))))

Theorem: coerce-list-under-iff

(defthm coerce-list-under-iff
  (iff (coerce string 'list)
       (and (stringp string)
            (not (equal "" string)))))

Theorem: length-of-coerce

(defthm length-of-coerce
  (equal (length (coerce x y))
         (cond ((equal y 'list)
                (if (stringp x) (length x) 0))
               (t (if (stringp x) 0 (len x))))))

Theorem: len-of-coerce-to-string

(defthm len-of-coerce-to-string
  (equal (len (coerce x 'string)) 0))

Theorem: coerce-inverse-1-better

(defthm coerce-inverse-1-better
  (equal (coerce (coerce x 'string) 'list)
         (if (stringp x)
             nil
           (make-character-list x))))

Theorem: coerce-inverse-2-better

(defthm coerce-inverse-2-better
  (equal (coerce (coerce x 'list) 'string)
         (if (stringp x) x "")))

Theorem: coerce-to-list-of-make-character-list

(defthm coerce-to-list-of-make-character-list
  (equal (coerce (make-character-list x) 'string)
         (coerce x 'string)))