(in-package "ACL2")

(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)))

(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)))))))