• 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
        • Istrpos
        • Strrpos
          • Strrpos-fast
        • Strpos
        • Collect-syms-with-isubstr
        • Istrprefixp
        • Collect-strs-with-isubstr
        • Iprefixp
        • Strsuffixp
        • Firstn-chars
        • Strprefixp
        • Isubstrp
        • Substrp
      • Strtok
      • Equivalences
      • Url-encoding
      • Lines
      • Explode-implode-equalities
      • Ordering
      • Numbers
      • Pad-trim
      • Coercion
      • 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

• Substrings

Strrpos

Locate the last occurrence of a substring.

(strrpos x y) searches through the string y for the last occurrence of the substring x. If x occurs somewhere in y, it returns the starting index of the last occurrence. Otherwise, it returns nil to indicate that x never occurs in y.

The function is "efficient" in the sense that it does not coerce its arguments into lists, but rather traverses both strings with char. On the other hand, it is a naive string search which operates by repeatedly calling strprefixp, rather than some better algorithm.

Corner case: we say that the empty string is an prefix of any other string. As a consequence, (strrpos "" x) is (length x) for all x.

Definitions and Theorems

Function: strrpos$inline

(defun strrpos$inline (x y)
  (declare (type string x y))
  (let ((x (mbe :logic (str-fix x) :exec x))
        (y (mbe :logic (str-fix y) :exec y))
        (yl (length (the string y))))
    (declare (type string x y)
             (type (integer 0 *) yl))
    (strrpos-fast (the string x)
                  (the string y)
                  (the (integer 0 *) yl)
                  (the (integer 0 *)
                       (length (the string x)))
                  (the (integer 0 *) yl))))

Theorem: strrpos-type

(defthm strrpos-type
  (or (and (integerp (strrpos x y))
           (<= 0 (strrpos x y)))
      (not (strrpos x y)))
  :rule-classes :type-prescription)

Theorem: prefixp-of-strrpos

(defthm prefixp-of-strrpos
  (implies (strrpos x y)
           (prefixp (explode x)
                    (nthcdr (strrpos x y) (explode y)))))

Theorem: completeness-of-strrpos

(defthm completeness-of-strrpos
  (implies (and (prefixp (explode x)
                         (nthcdr m (explode y)))
                (<= m (len y))
                (force (natp m)))
           (and (natp (strrpos x y))
                (>= (strrpos x y) m))))

Theorem: strrpos-upper-bound-weak

(defthm strrpos-upper-bound-weak
  (implies (force (stringp y))
           (<= (strrpos x y) (len (explode y))))
  :rule-classes ((:rewrite) (:linear)))

Theorem: strrpos-upper-bound-strong

(defthm strrpos-upper-bound-strong
  (implies (and (not (equal y ""))
                (not (equal x ""))
                (force (stringp x))
                (force (stringp y)))
           (< (strrpos x y) (len (explode y))))
  :rule-classes ((:rewrite) (:linear)))

Theorem: strrpos-upper-bound-stronger

(defthm strrpos-upper-bound-stronger
  (implies (and (strrpos x y)
                (force (stringp x))
                (force (stringp y)))
           (<= (strrpos x y)
               (- (len (explode y))
                  (len (explode x)))))
  :rule-classes ((:rewrite) (:linear)))

Subtopics

Strrpos-fast

Fast implementation of strrpos.