• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
      • Pretty-printing
      • Printtree
      • Base64
      • Charset-p
      • Strtok!
      • Cases
      • Concatenation
      • Html-encoding
      • Character-kinds
      • Substrings
      • Strtok
      • Equivalences
      • Url-encoding
      • Lines
      • Explode-implode-equalities
      • Ordering
      • Numbers
      • Pad-trim
      • Coercion
        • Explode
        • Implode
        • Std/strings/make-character-list
        • Std/strings/coerce
      • Std/strings/digit-to-char
      • Substitution
      • Symbols
    • Std/osets
    • Std/io
    • Std/basic
    • Std/system
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Coercion
• Coerce

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)))