permutations: Add permutations.lisp file.

1 files changed, 346 insertions, 0 deletions

diff --git a/permutations.lisp b/permutations.lisp
new file mode 100644
index 0000000..d777d06
--- /dev/null
+++ b/permutations.lisp
@@ -0,0 +1,346 @@
+(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))))