update-nth

(in-package "ACL2")

(defsection std/lists/update-nth
  :parents (std/lists update-nth)
  :short "Lemmas about @(see update-nth) available in the @(see std/lists)
library."
  (defthm update-nth-when-atom
    (implies (atom x)
      (equal (update-nth n v x) (append (repeat n nil) (list v))))
    :hints (("Goal" :in-theory (enable repeat))))
  (defthm update-nth-when-zp
    (implies (zp a)
      (equal (update-nth a v xs) (cons v (cdr xs)))))
  (defthm update-nth-of-cons
    (equal (update-nth n x (cons a b))
      (if (zp n)
        (cons x b)
        (cons a (update-nth (1- n) x b)))))
  (defthm true-listp-of-update-nth
    (equal (true-listp (update-nth n v x))
      (or (<= (len x) (nfix n)) (true-listp x))))
  (defthm len-of-update-nth
    (equal (len (update-nth n v x))
      (max (len x) (+ 1 (nfix n)))))
  (defthm car-of-update-nth
    (equal (car (update-nth n v x))
      (if (zp n)
        v
        (car x))))
  (defthm cdr-of-update-nth
    (equal (cdr (update-nth n v x))
      (if (zp n)
        (cdr x)
        (update-nth (1- n) v (cdr x)))))
  (defthm nth-update-nth
    (equal (nth m (update-nth n val l))
      (if (equal (nfix m) (nfix n))
        val
        (nth m l))))
  (defthm nth-of-update-nth-same
    (equal (nth n (update-nth n v x)) v))
  (defthm nth-of-update-nth-diff
    (implies (not (equal (nfix n1) (nfix n2)))
      (equal (nth n1 (update-nth n2 v x)) (nth n1 x))))
  (defthm nth-of-update-nth-split-for-constants
    (implies (and (syntaxp (quotep n1)) (syntaxp (quotep n2)))
      (equal (nth n1 (update-nth n2 v x))
        (if (equal (nfix n1) (nfix n2))
          v
          (nth n1 x)))))
  (defthm update-nth-of-nth
    (implies (< (nfix n) (len x))
      (equal (update-nth n (nth n x) x) x)))
  (defthm update-nth-of-nth-free
    (implies (and (equal (nth n x) free) (< (nfix n) (len x)))
      (equal (update-nth n free x) x)))
  (defthm update-nth-of-update-nth-same
    (equal (update-nth n v1 (update-nth n v2 x))
      (update-nth n v1 x)))
  (defthm update-nth-of-update-nth-diff
    (implies (not (equal (nfix n1) (nfix n2)))
      (equal (update-nth n1 v1 (update-nth n2 v2 x))
        (update-nth n2 v2 (update-nth n1 v1 x))))
    :rule-classes ((:rewrite :loop-stopper ((n1 n2 update-nth)))))
  (defthm update-nth-diff-gather-constants
    (implies (and (syntaxp (and (quotep x)
            (quotep n)
            (quotep val1)
            (or (not (quotep m)) (not (quotep val2)))))
        (not (equal (nfix n) (nfix m))))
      (equal (update-nth n val1 (update-nth m val2 x))
        (update-nth m val2 (update-nth n val1 x))))
    :rule-classes ((:rewrite :loop-stopper nil)))
  (defthm final-cdr-of-update-nth
    (equal (final-cdr (update-nth n v x))
      (if (< (nfix n) (len x))
        (final-cdr x)
        nil))
    :hints (("Goal" :induct (update-nth n v x)
       :in-theory (enable final-cdr))))
  (defthm nthcdr-past-update-nth
    (implies (and (< (nfix n2) (len x)) (< (nfix n2) (nfix n1)))
      (equal (nthcdr n1 (update-nth n2 val x)) (nthcdr n1 x))))
  (defthm nthcdr-before-update-nth
    (implies (and (< (nfix n2) (len x)) (<= (nfix n1) (nfix n2)))
      (equal (nthcdr n1 (update-nth n2 val x))
        (update-nth (- (nfix n2) (nfix n1)) val (nthcdr n1 x)))))
  (defthm nthcdr-of-update-nth
    (equal (nthcdr n1 (update-nth n2 val x))
      (if (< (nfix n2) (nfix n1))
        (nthcdr n1 x)
        (update-nth (- (nfix n2) (nfix n1)) val (nthcdr n1 x)))))
  (defthm take-before-update-nth
    (implies (<= (nfix n1) (nfix n2))
      (equal (take n1 (update-nth n2 val x)) (take n1 x))))
  (defthm take-after-update-nth
    (implies (> (nfix n1) (nfix n2))
      (equal (take n1 (update-nth n2 val x))
        (update-nth n2 val (take n1 x)))))
  (defthm take-of-update-nth
    (equal (take n1 (update-nth n2 val x))
      (if (<= (nfix n1) (nfix n2))
        (take n1 x)
        (update-nth n2 val (take n1 x)))))
  (defthm member-equal-update-nth
    (member-equal x (update-nth n x l)))
  (defthm update-nth-append
    (equal (update-nth n v (append a b))
      (if (< (nfix n) (len a))
        (append (update-nth n v a) b)
        (append a (update-nth (- n (len a)) v b)))))
  (def-listp-rule element-list-p-of-update-nth
    (implies (element-list-p (double-rewrite x))
      (iff (element-list-p (update-nth n y x))
        (and (element-p y)
          (or (<= (nfix n) (len x)) (element-p nil)))))
    :hints (("Goal" :in-theory (disable update-nth-when-atom)
       :induct (update-nth n y x))))
  (def-projection-rule elementlist-projection-of-update-nth
    (implies (<= (nfix n) (len x))
      (equal (elementlist-projection (update-nth n v x))
        (update-nth n
          (element-xformer v)
          (elementlist-projection x))))
    :hints (("Goal" :in-theory (disable update-nth-when-atom)))
    :name elementlist-projection-of-update-nth
    :requirement (not nil-preservingp))
  (def-projection-rule elementlist-projection-of-update-nth-nil-preserving
    (implies (equal (element-xformer nil) nil)
      (equal (elementlist-projection (update-nth n v x))
        (update-nth n
          (element-xformer v)
          (elementlist-projection x))))
    :hints (("Goal" :in-theory (disable update-nth-when-atom)))
    :name elementlist-projection-of-update-nth
    :requirement nil-preservingp
    :body (equal (elementlist-projection (update-nth n v x))
      (update-nth n
        (element-xformer v)
        (elementlist-projection x)))))