nth

(in-package "ACL2")

(in-theory (disable nth))

(defthm nth-of-nil
  (equal (nth n nil) nil)
  :hints (("Goal" :in-theory (enable nth))))

(defthm nth-when-<=-len-cheap
  (implies (and (<= (len x) n) (natp n))
    (equal (nth n x) nil))
  :rule-classes ((:rewrite :backchain-limit-lst (0 nil)))
  :hints (("Goal" :in-theory (enable nth))))

(defthm nth-when-not-consp-cheap
  (implies (not (consp x)) (equal (nth n x) nil))
  :rule-classes ((:rewrite :backchain-limit-lst (0)))
  :hints (("Goal" :in-theory (enable nth))))

(defthm nth-when-zp-cheap
  (implies (and (syntaxp (not (equal n ''0))) (zp n))
    (equal (nth n x) (nth 0 x)))
  :rule-classes ((:rewrite :backchain-limit-lst (nil 0)))
  :hints (("Goal" :in-theory (enable nth))))

(defthmd nth-when-n-is-zp
  (implies (zp n) (equal (nth n lst) (car lst))))

(defthmd nth-when-n-is-not-natp
  (implies (not (natp n)) (equal (nth n lst) (car lst)))
  :rule-classes ((:rewrite :backchain-limit-lst (0)))
  :hints (("Goal" :in-theory (enable nth))))

(defthmd nth-when-<=-len
  (implies (<= (len x) (nfix n)) (equal (nth n x) nil)))

(defthmd nth-of-cons
  (equal (nth n (cons x y))
    (if (zp n)
      x
      (nth (+ -1 n) y)))
  :hints (("Goal" :in-theory (enable nth))))

(defthm nth-of-cons-safe
  (implies (syntaxp (not (and (quotep x) (quotep y))))
    (equal (nth n (cons x y))
      (if (zp n)
        x
        (nth (+ -1 n) y))))
  :hints (("Goal" :in-theory (enable nth))))

(defthm nth-of-cons-constant-version
  (implies (syntaxp (quotep n))
    (equal (nth n (cons x y))
      (if (zp n)
        x
        (nth (+ -1 n) y))))
  :hints (("Goal" :in-theory (enable nth))))

(defthm nth-1-cadr-hack
  (equal (equal (nth 1 x) (car (cdr x))) t)
  :hints (("Goal" :in-theory (enable nth))))

(defthmd car-becomes-nth-of-0
  (equal (car x) (nth 0 x))
  :hints (("Goal" :in-theory (enable nth))))

(defthmd nth-of-0
  (equal (nth 0 lst) (car lst))
  :hints (("Goal" :in-theory (enable nth))))

(theory-invariant (incompatible (:rewrite car-becomes-nth-of-0)
    (:rewrite nth-o-0)))

(defthm nth-of-cdr
  (equal (nth n (cdr x)) (nth (+ 1 (nfix n)) x))
  :hints (("Goal" :in-theory (enable nth))))

(theory-invariant (incompatible (:definition nth) (:rewrite nth-of-cdr)))

(defthm equal-of-nth-forward-to-consp
  (implies (and (equal free (nth n x)) (syntaxp (quotep free)) free)
    (consp x))
  :rule-classes :forward-chaining)

(defthmd cadr-becomes-nth-of-1 (equal (cadr x) (nth 1 x)))

(defthm nth-of-append
  (equal (nth n (append x y))
    (if (< (nfix n) (len x))
      (nth n x)
      (nth (- n (len x)) y)))
  :hints (("Goal" :in-theory (e/d (nth) (nth-of-cdr)))))

(defthm nth-of-true-list-fix
  (equal (nth n (true-list-fix x)) (nth n x))
  :hints (("Goal" :in-theory (e/d (nth) (nth-of-cdr)))))

(defthm equal-of-car-and-nth-of-0
  (equal (equal (car x) (nth 0 x)) t))

(defthm equal-of-cadr-and-nth-of-1
  (equal (equal (cadr x) (nth 1 x)) t))

(defthm equal-of-nth-2-and-caddr
  (equal (equal (nth 2 x) (caddr x)) t))

(defthm not-<-of-car-and-nth-of-0
  (not (< (car x) (nth 0 x))))

(defthm not-<-of-nth-of-0-and-car
  (not (< (nth 0 x) (car x))))

(defthm nth-of-plus-of-cons-when-constant
  (implies (and (syntaxp (quotep k)) (posp k) (natp n))
    (equal (nth (+ k n) (cons a rst)) (nth (+ (+ -1 k) n) rst)))
  :hints (("Goal" :in-theory (e/d (nth) (nth-of-cdr)))))

(defthm <=-of-acl2-count-of-nth-linear
  (<= (acl2-count (nth n l)) (acl2-count l))
  :rule-classes :linear :hints (("Goal" :in-theory (enable (:i nth)))))

(defthm <-of-acl2-count-of-nth-linear
  (implies (consp l)
    (< (acl2-count (nth n l)) (acl2-count l)))
  :rule-classes :linear :hints (("Goal" :in-theory (enable (:i nth)))))