len-combinations: Add len-combinations-factorial theorem.

1 files changed, 43 insertions, 0 deletions

diff --git a/combinations.lisp b/combinations.lisp
index 1867923..93c3b67 100644
--- a/combinations.lisp
+++ b/combinations.lisp
@@ -26,3 +26,46 @@
 (defthm len-combinations
   (equal (len (combinations x n))
          (comb (len x) n)))
+
+(defun factorial (n)
+  (if (zp n)
+      1
+      (* n (factorial (- n 1)))))
+
+(include-book "arithmetic/top" :dir :system)
+
+(defthm comb-zero
+  (implies (and (natp n)
+                (natp k)
+                (< n k))
+           (equal (comb n k) 0)))
+
+(defthm comb-1
+  (implies (natp n)
+           (equal (comb n 1) n)))
+
+(defthm comb-factorial-lemma
+  (implies (natp n)
+           (equal (* n (+ -1 n) x)
+                  (+ (* (+ -1 n) x)
+                     (* (+ -1 n) (+ -1 n) x))))
+  :rule-classes nil)
+
+(defthm comb-factorial
+  (implies (natp n)
+           (equal (comb n k)
+                  (cond ((zp k) 1)
+                        ((< n k) 0)
+                        (t (/ (factorial n)
+                              (* (factorial (- n k))
+                                 (factorial k)))))))
+  :hints (("Subgoal *1/4.2'" :use (:instance comb-factorial-lemma
+                                             (x (factorial (+ -2 n)))))))
+
+(defthm len-combination-factorial
+  (equal (len (combinations x k))
+         (cond ((zp k) 1)
+               ((< (len x) k) 0)
+               (t (/ (factorial (len x))
+                     (* (factorial (- (len x) k))
+                        (factorial k)))))))