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

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