diff options
| -rw-r--r-- | combinations.lisp | 43 |
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))))))) |