From 7a8fe5e2716b4c84d390a96d6dfd56a124017559 Mon Sep 17 00:00:00 2001 From: Masaya Tojo Date: Fri, 13 Aug 2021 01:00:21 +0900 Subject: permutations: Remove useless theorems and fucntions. --- permutations.lisp | 131 ++++++++++-------------------------------------------- 1 file changed, 24 insertions(+), 107 deletions(-) diff --git a/permutations.lisp b/permutations.lisp index 7c01dc3..66ecc74 100644 --- a/permutations.lisp +++ b/permutations.lisp @@ -1,5 +1,3 @@ -(local (include-book "arithmetic/top-with-meta" :dir :system)) - (defun insert (x y) (if (endp y) (list x) @@ -19,58 +17,39 @@ (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) +(defun sum-of-lens (x) (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))))) + (+ (len (car x)) + (sum-of-lens (cdr x))))) -(defun sum-of-nat-expt-1+lens (x n) +(defun sum-of-1+lens (x) (if (endp x) 0 - (+ (nat-expt (+ 1 (len (car x))) n) - (sum-of-nat-expt-1+lens (cdr x) n)))) + (+ (+ 1 (len (car x))) + (sum-of-1+lens (cdr x))))) -(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 sum-of-lens-append + (equal (sum-of-lens (append x y)) + (+ (sum-of-lens x) + (sum-of-lens y)))) (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) +(defthm sum-of-lens-insert + (equal (sum-of-lens (insert x y)) + (* (+ (len x) (len y)) (+ 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-insert + (equal (len (insert x y)) + (+ 1 (len y)))) (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)))) + (sum-of-1+lens y))) (defun mapcar-len (x) (if (endp x) @@ -84,12 +63,6 @@ (+ (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 @@ -107,16 +80,14 @@ (cons (+ (car x) (car y)) (mapcar-sum (cdr x) (cdr y))))) +(defthm sum-of-lens-equal-sum-mapcar-len + (equal (sum-of-lens x) + (sum (mapcar-len x)))) -(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 sum-of-1+lens-equal-sum-1+-len + (equal (sum-of-1+lens x) + (sum (mapcar-sum (seq 1 (len x)) + (mapcar-len x))))) (defthm nat-listp-mapcar-len (nat-listp (mapcar-len x))) @@ -130,70 +101,16 @@ (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)) -- cgit v1.2.3