From 975418f4c2e1520649196458d3211e6ef9ec531a Mon Sep 17 00:00:00 2001 From: Masaya Tojo Date: Wed, 1 Sep 2021 23:12:41 +0900 Subject: Add combinations.lisp file. --- combinations.lisp | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) create mode 100644 combinations.lisp (limited to 'combinations.lisp') diff --git a/combinations.lisp b/combinations.lisp new file mode 100644 index 0000000..1867923 --- /dev/null +++ b/combinations.lisp @@ -0,0 +1,28 @@ +(defun cons-all (e x) + (declare (xargs :guard (true-listp x))) + (if (endp x) + nil + (cons (cons e (car x)) + (cons-all e (cdr x))))) + +(defun combinations (x n) + (declare (xargs :guard (and (true-listp x) + (natp n)))) + (cond + ((zp n) (list nil)) + ((endp x) nil) + (t + (append (cons-all (car x) + (combinations (cdr x) (- n 1))) + (combinations (cdr x) n))))) + +(defun comb (n k) + (cond + ((zp k) 1) + ((zp n) 0) + (t (+ (comb (- n 1) k) + (comb (- n 1) (- k 1)))))) + +(defthm len-combinations + (equal (len (combinations x n)) + (comb (len x) n))) -- cgit v1.2.3