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

(defun insert (x y)
  (if (endp y)
      (list x)
      (cons (append x y)
            (insert (cons (car y) x)
                    (cdr y)))))

(defun mappend-insert (x y)
  (if (endp y)
      nil
      (append (insert x (car y))
              (mappend-insert x (cdr y)))))

(defun permutations (x)
  (if (endp x)
      (list nil)
      (mappend-insert (list (car x))
                      (permutations (cdr x)))))

(defun nat-expt (m n)
  (cond
    ((zp n) 1)
    ((zp (1- n)) m)
    (t (* m (nat-expt m (1- n))))))

(defun sum-of-nat-expt-lens (x n)
  (if (endp x)
      0
      (+ (nat-expt (len (car x)) n)
         (sum-of-nat-expt-lens (cdr x) n))))

(defthm nat-expt-1+
  (implies (natp n)
           (equal (nat-expt (+ 1 x) (+ 1 n))
                  (+ (* x (nat-expt (+ 1 x) n))
                     (nat-expt (+ 1 x) n)))))

(defun sum-of-nat-expt-1+lens (x n)
  (if (endp x)
      0
      (+ (nat-expt (+ 1 (len (car x))) n)
         (sum-of-nat-expt-1+lens (cdr x) n))))

(defthm sum-of-nat-expt-lens-append
  (equal (sum-of-nat-expt-lens (append x y) n)
         (+ (sum-of-nat-expt-lens x n)
            (sum-of-nat-expt-lens y n))))

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

(defthm sum-of-nat-expt-lens-insert
  (equal (sum-of-nat-expt-lens (insert x y) n)
         (* (nat-expt (+ (len x) (len y)) n)
            (+ 1 (len y)))))

(defthm sum-of-nat-expt-lens-mappend-insert
  (implies (natp n)
           (equal (sum-of-nat-expt-lens (mappend-insert (list x) y) n)
                  (sum-of-nat-expt-1+lens y (+ 1 n)))))

(defthm len-sum-of-nextp-lens
  (equal (len x)
         (sum-of-nat-expt-lens x 0)))
(in-theory (disable len-sum-of-nextp-lens))

(defthm len-mappend-insert
  (equal (len (mappend-insert (list x) y))
         (sum-of-nat-expt-1+lens y 1))
  :hints (("Goal" :in-theory (enable len-sum-of-nextp-lens))))

(defun mapcar-len (x)
  (if (endp x)
      nil
      (cons (len (car x))
            (mapcar-len (cdr x)))))

(defun sum (x)
  (if (endp x)
      0
      (+ (car x)
         (sum (cdr x)))))

(defun mapcar-nat-expt (x i)
  (if (endp x)
      nil
      (cons (nat-expt (car x) i)
            (mapcar-nat-expt (cdr x) i))))

(defun seq (x n)
  (if (zp n)
      nil
      (cons x (seq x (1- n)))))

(defun mapcar-product (x y)
  (if (or (endp x) (endp y))
      nil
      (cons (* (car x) (car y))
            (mapcar-product (cdr x) (cdr y)))))

(defun mapcar-sum (x y)
  (if (or (endp x) (endp y))
      nil
      (cons (+ (car x) (car y))
            (mapcar-sum (cdr x) (cdr y)))))


(defthm sum-of-nat-expt-lens-equal-sum-mapcar-nat-expt-len
  (equal (sum-of-nat-expt-lens x n)
         (sum (mapcar-nat-expt (mapcar-len x) n))))

(defthm sum-of-nat-expt-1+lens-equal-sum-mapcar-nat-expt-1+-len
  (equal (sum-of-nat-expt-1+lens x n)
         (sum (mapcar-nat-expt (mapcar-sum (seq 1 (len x))
                                           (mapcar-len x))
                               n))))


(defthm nat-listp-mapcar-len
  (nat-listp (mapcar-len x)))

(defthm sum-mapcar-sum
  (implies (equal (len x) (len y))
           (equal (sum (mapcar-sum x y))
                  (+ (sum x)
                     (sum y)))))

(defthm len-mapcar-len
  (equal (len (mapcar-len x)) (len x)))

(defthm len-mapcar-nat-expt
  (equal (len (mapcar-nat-expt x n)) (len x)))

(defthm len-mapcar-product
  (implies (equal (len x) (len y))
           (equal (len (mapcar-product x y))
                  (len x))))

(defthm mapcar-nat-expt-0-one-seq
  (equal (mapcar-nat-expt x 0)
         (seq 1 (len x))))

(defthm mapcar-product-one-seq
  (implies (acl2-number-listp x)
           (equal (mapcar-product (seq 1 (len x)) x)
                  x)))

(defthm mapcar-product-mapcar-nat-expt-0
  (implies (and (acl2-number-listp x)
                (equal (len x) (len y)))
           (equal (mapcar-product (mapcar-nat-expt y 0)
                                  x)
                  x)))

(defthm sum-of-nat-expt-lens-equal-sum-mapcar-nat-expt-len/inverse
  (equal (sum (mapcar-nat-expt (mapcar-len x) n))
         (sum-of-nat-expt-lens x n)))


(defthm sum-of-nat-expt-1+lens-equal-sum-mapcar-nat-expt-1+-len/inverse
  (equal (sum (mapcar-nat-expt (mapcar-sum (seq 1 (len x))
                                           (mapcar-len x))
                               n))
         (sum-of-nat-expt-1+lens x n)))

(defthm sum-of-nat-expt-lens-mappend-insert/mapcar
  (implies (natp n)
           (equal (sum (mapcar-nat-expt (mapcar-len (mappend-insert (list x)
                                                                    y))
                                        n))
                  (sum (mapcar-nat-expt (mapcar-sum (seq 1 (len y))
                                                    (mapcar-len y))
                                        (+ 1 n)))))
  :hints (("Goal"  :in-theory (disable
                               sum-of-nat-expt-lens-equal-sum-mapcar-nat-expt-len
                               sum-of-nat-expt-1+lens-equal-sum-mapcar-nat-expt-1+-len))))

(in-theory (disable sum-of-nat-expt-lens-equal-sum-mapcar-nat-expt-len/inverse
                    sum-of-nat-expt-1+lens-equal-sum-mapcar-nat-expt-1+-len/inverse))

(defthm nat-expt-1
  (equal (nat-expt x 1)
         x))

(defthm mapcar-nat-expt-1
  (implies (true-listp x)
           (equal (mapcar-nat-expt x 1)
                  x)))

(defthm sum-mapcar-len-mappend-insert-lemma
  (equal (sum (mapcar-len x))
         (sum (mapcar-nat-expt (mapcar-len x) 1))))

(in-theory (disable sum-mapcar-len-mappend-insert-lemma))

(defthm len-seq
  (implies (natp n)
           (equal (len (seq x n))
                  n)))

(defthm sum-seq
  (implies (natp n)
           (equal (sum (seq x n))
                  (* x n))))

(defthm mapcar-distributivity
  (equal (* x (sum y))
         (sum (mapcar-product (seq x (len y))
                              y))))

(defthm len-mapcar-sum
  (implies (equal (len x) (len y))
           (equal (len (mapcar-sum x y))
                  (len x))))

(defthm mapcar-product-com
  (implies (equal (len x) (len y))
           (equal (mapcar-product x y)
                  (mapcar-product y x))))

(defthm mapcar-len-insert
  (equal (mapcar-len (insert x y))
         (seq (+ (len x) (len y))
              (+ 1 (len y)))))

(defun mapcar-len-mappend-insert (x)
  (if (endp x)
      nil
      (append (seq (+ 1 (len (car x)))
                   (+ 1 (len (car x))))
              (mapcar-len-mappend-insert (cdr x)))))

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

(defthm theorem-of-mapcar-len-mappend-insert
  (equal (mapcar-len (mappend-insert (list x) y))
         (mapcar-len-mappend-insert y)))

(defun sum-mapcar-len-mappend-insert (x)
  (if (endp x)
      0
      (+ (* (+ 1 (len (car x)))
            (+ 1 (len (car x))))
         (sum-mapcar-len-mappend-insert (cdr x)))))

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

(defthm theorem-of-sum-mapcar-len-mappend-insert
  (equal (sum (mapcar-len-mappend-insert x))
         (sum-mapcar-len-mappend-insert x)))

(defun seqp (x)
  (if (or (endp x)
          (endp (cdr x)))
      t
      (and (equal (car x)
                  (cadr x))
           (seqp (cdr x)))))

(defmacro same-len-p (x)
  `(seqp (mapcar-len ,x)))

(defthm sum-mapcar-len-mappend-insert-permutations
  (implies (same-len-p x)
           (equal (sum-mapcar-len-mappend-insert x)
                  (if (consp x)
                      (* (+ 1 (len (car x)))
                         (+ 1 (len (car x)))
                         (len x))
                      0))))

(defthm same-len-p-insert
  (implies (true-listp y)
           (same-len-p (insert x y))))

(defthm seqp-append
  (iff (seqp (append x y))
       (if (consp x)
           (if (consp y)
               (and (seqp x)
                    (seqp y)
                    (equal (car x) (car y)))
               (seqp x))
           (seqp y))))

(defthm car-seq
  (implies (consp (seq x n))
           (equal (car (seq x n)) x)))

(defthm car-mapcar-len-mappend-insert
  (implies (consp (mapcar-len-mappend-insert x))
           (equal (car (mapcar-len-mappend-insert x))
                  (+ 1 (len (car x))))))

(defthm seqp-seq
  (seqp (seq x n)))

(defthm car-append
  (equal (car (append x y))
         (if (consp x)
             (car x)
             (car y))))

(defthm same-mapcar-len-mappend-insert
  (implies (same-len-p x)
           (seqp (mapcar-len-mappend-insert x))))

(defthm same-len-p-permutations
  (same-len-p (permutations x)))

(defthm len-car-insert
  (equal (len (car (insert x y)))
         (+ (len x) (len y))))

(defthm len-car-mappend-insert
  (implies (and (consp (mappend-insert (list x) y))
                (same-len-p y))
           (equal (len (car (mappend-insert (list x) y)))
                  (+ 1 (len (car y))))))

(defthm len-car-permutations
  (implies (consp (permutations x))
           (equal (len (car (permutations x)))
                  (len x))))

(defthm len-permutations-lemma
  (equal (sum (mapcar-len (permutations x)))
         (* (len x) (len (permutations x)))))

(defun factorial (n)
  (if (zp n)
      1
      (* n (factorial (1- n)))))

(defthm len-permutations
  (equal (len (permutations x))
         (factorial (len x))))