; (certify-book "utilities")

(in-package "ACL2")

(include-book "arithmetic/top-with-meta" :dir :system)
(include-book "ordinals/lexicographic-ordering" :dir :system)
(in-theory (enable posp))

; A little digression... Here is a little fact ACL2 ought to know but can't
; puzzle out from its axioms, without help.
(defthm coerce-lemma
  (implies (and (stringp pat)
                (not (equal pat "")))
           (consp (coerce pat 'list)))
  :hints (("Goal" :use (:instance coerce-inverse-2
                                  (x pat))
           :in-theory (disable coerce-inverse-2))))

(defthm coerce-lemma-corrollary
  (implies (and (stringp pat)
                (not (equal pat "")))
           (coerce pat 'list))
  :hints (("Goal" :use coerce-lemma :in-theory (disable coerce-lemma))))

(defthm nthcdr-len
  (implies (true-listp x) (equal (nthcdr (len x) x) nil)))


; This lemma is ugly but is the way it is to avoid folding len via the more
; natural (len (cdr x)) = (- (len x) 1).
(defthm nthcdr-firstn
  (implies (and (natp i)
                (natp d)
                (<= i d))
           (equal (nthcdr i (firstn d x))
                  (firstn (- d i) (nthcdr i x)))))

(defthm len-firstn
  (equal (len (firstn n x)) (min (len x) (nfix n))))

(defthm car-firstn
  (equal (car (firstn n x)) (if (zp n) nil (car x))))

(defthm true-listp-nthcdr
  (implies (true-listp x)
           (true-listp (nthcdr n x))))

(defthm true-listp-cdr
  (implies (true-listp x)
           (true-listp (cdr x))))

(defthm nthcdr-nil-2
  (equal (nthcdr i nil) nil))

(defthm nth-nthcdr
  (equal (nth n (nthcdr m x))
	 (nth (+ (nfix n) (nfix m)) x)))

(defthm len-nthcdr
  (equal (len (nthcdr n x))
	 (nfix (- (len x) (nfix n)))))

; This lemma is ugly but is the way it is to avoid folding len via the more
; natural (len (cdr x)) = (- (len x) 1).

(defthm len-cdr
  (implies (natp j)
           (equal (len (cdr (nthcdr j pat)))
                  (nfix (- (len pat) (+ j 1))))))


(defthm nthcdr-cdr
  (equal (nthcdr i (cdr x)) (cdr (nthcdr i x))))

(defthm consp-nthcdr-2
  (iff (consp (nthcdr i x))
       (< (nfix i) (len x))))

(defthm nth-is-car-nthcdr-2
  (equal (nth i x) (car (nthcdr i x))))


(defthm dumb-lemma
  (implies (and (integerp i)
		(integerp j))
	   (equal (equal (+ i j) 0)
		  (equal i (- j)))))

(defthm nth-is-car-nthcdr
  (equal (nth i x) (car (nthcdr i x))))

(defthm nthcdr-nil
  (equal (nthcdr i nil) nil))

(defthm consp-nthcdr
  (implies (natp i)
	   (iff (consp (nthcdr i x))
		(< i (len x)))))

(defthm nthcdr-firstn-nthcdr
  (implies (and (natp n)
                (natp i)
                (natp d))
           (equal (nthcdr n (firstn d (nthcdr i txt)))
                  (firstn (+ d (- n))
                          (nthcdr (+ i n) txt)))))

(defun up-down-hint (i d)
  (cond ((zp d) (list i d))
        (t (up-down-hint (+ 1 i) (- d 1)))))

(defthm firstn-nthcdr-firstn
  (implies (and (natp i)
                (natp n)
                (<= (+ d i) n))
         (equal (firstn d (nthcdr i (firstn n txt)))
                (firstn d (nthcdr i txt))))
  :hints (("goal" :induct (up-down-hint i d))))

(defthm nthcdr-non-nil
  (iff (nthcdr j pat)
       (if (natp j)
           (or (< j (len pat))
               (and (not (true-listp pat))
                    (equal j (len pat))))
         pat)))

; !!!

; We are going to explore using the elim rule to replace txt by (append a b),
; where a and b are new variables representing the firstn and nthcdr of txt.
; If we get through this proof we should move this work into utilities and
; start over, using this technique widely.

; These lemmas were typed in ahead of time, anticipating what would happen.

(defthm firstn-nthcdr-elim
  (implies (and (natp n)
                (< n (len x)))
           (equal (append (firstn n x) (nthcdr n x)) x))
  :rule-classes :elim)

(defthm len-firstn-gen
  (equal (len (firstn n x))
         (min (len x) (nfix n)))
  :rule-classes :generalize)

(defthm len-append
  (equal (len (append x y))
         (+ (len x) (len y))))

(defthm len-nthcdr-gen
  (equal (len (nthcdr n x))
         (nfix (- (len x) (nfix n))))
  :rule-classes :generalize)

; Then we discovered the need for these lemmas using The Method as
; we banged away on matchpx-pmatchp below.

(defthm firstn-firstn
  (equal (firstn n (firstn k x))
         (if (<= (nfix n) (nfix k))
             (firstn n x)
           (firstn k x))))
  
(defthm true-listp-nthcdr-gen
  (implies (true-listp x)
           (true-listp (nthcdr n x)))
  :rule-classes :generalize)


(defthm firstn-len
  (implies (true-listp x)
           (equal (firstn (len x) x) x)))

(defthm true-listp-append
  (equal (true-listp (append x y))
         (true-listp y)))

(defthm firstn-too-big
  (implies (and (natp n)
                (<= (len x) n)
                (true-listp x))
           (equal (firstn n x) x)))

(defthm firstn-append
  (equal (firstn n (append a b))
         (if (<= (nfix n) (len a))
             (firstn n a)
           (append a (firstn (- (nfix n) (len a)) b)))))

(defun hint2 (a b)
  (if (consp a)
      (if (consp b)
          (hint2 (cdr a) (cdr b))
        (list a b))
    (list a b)))

(defthm equal-append
  (implies (and (true-listp a)
                (true-listp b)
                (equal (len a) (len b)))
           (equal (equal (append a c)
                         (append b d))
                  (and (equal a b)
                       (equal c d))))
  :hints (("Goal" :induct (hint2 a b))))

(defthm nthcdr-append
  (equal (nthcdr n (append a b))
         (if (<= (nfix n) (len a))
             (append (nthcdr n a) b)
           (nthcdr (- (nfix n) (len a)) b))))

(defthm characterp-car-nthcdr-coerce
  (implies (character-listp x)
           (equal (characterp (car (nthcdr i x)))
                  (< (nfix i) (len x)))))

(defthm lens-differ
  (implies (not (equal (len x) (len y)))
           (not (equal x y))))

; These two lemmas are needed for reasoning about M1 code.

(defthm equal-char-codes
  (implies (and (characterp x)
                (characterp y))
           (equal (equal (char-code x) (char-code y))
                  (equal x y)))
  :hints (("Goal"
           :use ((:instance CODE-CHAR-CHAR-CODE-IS-IDENTITY (c x))
                 (:instance CODE-CHAR-CHAR-CODE-IS-IDENTITY (c y)))
           :in-theory (disable CODE-CHAR-CHAR-CODE-IS-IDENTITY))))

(defthm equal-length-0
  (equal (equal (length x) 0)
         (if (stringp x) (equal x "") (atom x))))