suffixp

(in-package "STR")

(include-book "strprefixp")

(local (include-book "std/lists/nthcdr" :dir :system))

(local (include-book "arithmetic/top" :dir :system))

(local (in-theory (disable prefixp-when-equal-lengths)))

(local (defthm crock
    (implies (and (equal (len x) (len y))
        (true-listp x)
        (true-listp y))
      (equal (prefixp x y) (equal x y)))
    :hints (("Goal" :in-theory (enable prefixp)))))

(defsection strsuffixp
  :parents (substrings)
  :short "Case-sensitive string suffix test."
  :long "<p>@(call strsuffixp) determines if the string @('x') is a suffix of
the string @('y'), in a case-sensitive manner.</p>

<p>Logically, we ask whether @('|x| < |y|'), and whether</p>

@({
  (equal (nthcdr (- |y| |x|) (explode x))
         (explode y))
})

<p>But we use a more efficient implementation that avoids coercing the strings
into lists; basically we ask if the last @('|x|') characters of @('y') are
equal to @('x').</p>

<p>Corner case: we regard the empty string as a suffix of every other string.
That is, @('(strsuffixp "" x)') is always true.</p>"
  (definlined strsuffixp
    (x y)
    (declare (type string x y))
    (mbe :logic (let* ((xchars (explode x)) (ychars (explode y))
          (xlen (len xchars))
          (ylen (len ychars)))
        (and (<= xlen ylen)
          (equal (nthcdr (- ylen xlen) (explode y))
            (explode x))))
      :exec (let* ((xlen (length x)) (ylen (length y)))
        (and (<= xlen ylen)
          (strprefixp-impl x
            y
            0
            (- ylen xlen)
            xlen
            ylen)))))
  (local (in-theory (enable strsuffixp)))
  (local (defthm c0
      (implies (and (natp n)
          (<= (len x) n)
          (true-listp x))
        (equal (nthcdr n x) nil))))
  (local (defthm c1
      (implies (true-listp x)
        (not (nthcdr (len x) x)))))
  (defthm strsuffixp-of-empty
    (strsuffixp "" y))
  (defcong streqv
    equal
    (strsuffixp x y)
    1)
  (defcong streqv
    equal
    (strsuffixp x y)
    2))