From e7c237de367db261b80b60588ac89926345751aa Mon Sep 17 00:00:00 2001 From: Masaya Tojo Date: Sun, 5 Sep 2021 01:36:57 +0900 Subject: len-combinations: Add len-combinations-factorial theorem. --- combinations.lisp | 43 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 43 insertions(+) (limited to 'combinations.lisp') 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))))))) -- cgit v1.2.3