binomial - ACL2 Book

Included Books

other

(in-package "ACL2")

local

(local (include-book "top"))

include-book

(include-book "factorial")

include-book

(include-book "sumlist")

choosefunction

(defun choose
  (k n)
  (if (and (integerp k) (integerp n) (<= 0 k) (<= k n))
    (/ (factorial n) (* (factorial k) (factorial (- n k))))
    0))

factorial-n/n-1theorem

(defthm factorial-n/n-1
  (implies (and (integerp n) (<= 1 n))
    (equal (* (factorial n) (/ (factorial (+ -1 n)))) n))
  :hints (("Goal" :expand ((factorial n)))))

local

(local (defthm factorial-n/n-1/x
    (implies (and (integerp n) (<= 1 n))
      (equal (* (factorial n) (/ (factorial (+ -1 n))) x) (* n x)))))

choose-reductiontheorem

(defthm choose-reduction
  (implies (and (integerp k) (integerp n) (< 0 k) (< k n))
    (equal (choose k n)
      (+ (choose (1- k) (1- n)) (choose k (1- n)))))
  :hints (("Subgoal 4'" :expand ((factorial n))))
  :rule-classes nil)

choose-mkfunction

(defun choose-mk
  (k n)
  (if (and (integerp k) (integerp n))
    (if (and (< 0 k) (< k n))
      (+ (choose-mk (1- k) (1- n)) (choose-mk k (1- n)))
      (if (and (<= 0 k) (<= k n))
        1
        0))
    0))

choose-mk-choosetheorem

(defthm choose-mk-choose
  (equal (choose-mk k n) (choose k n))
  :hints (("Goal" :induct (choose-mk k n)) ("Subgoal *1/1" :use (:instance choose-reduction)
      :in-theory (disable choose)))
  :rule-classes nil)

choose-is-non-negative-integertheorem

(defthm choose-is-non-negative-integer
  (and (integerp (choose k n)) (<= 0 (choose k n)))
  :hints (("Goal" :use (:instance choose-mk-choose)
     :in-theory (disable choose choose-mk)))
  :rule-classes (:rewrite :type-prescription))

binomial-expansionfunction

(defun binomial-expansion
  (x y k n)
  (declare (xargs :measure (nfix (1+ (- n k)))))
  (if (and (integerp k) (integerp n) (<= 0 k) (<= k n))
    (cons (* (choose k n) (expt x k) (expt y (- n k)))
      (binomial-expansion x y (1+ k) n))
    nil))

binomial-expansion-times-xfunction

(defun binomial-expansion-times-x
  (x y k n)
  (declare (xargs :measure (nfix (1+ (- n k)))))
  (if (and (integerp k) (integerp n) (<= 0 k) (<= k n))
    (cons (* (choose k n) (expt x (1+ k)) (expt y (- n k)))
      (binomial-expansion-times-x x y (1+ k) n))
    nil))

binomial-expansion-times-x-correcttheorem

(defthm binomial-expansion-times-x-correct
  (equal (* x (sumlist (binomial-expansion x y k n)))
    (sumlist (binomial-expansion-times-x x y k n)))
  :hints (("Goal" :in-theory (disable choose))))

binomial-expansion-times-yfunction

(defun binomial-expansion-times-y
  (x y k n)
  (declare (xargs :measure (nfix (1+ (- n k)))))
  (if (and (integerp k) (integerp n) (<= 0 k) (<= k n))
    (cons (* (choose k n) (expt x k) (expt y (1+ (- n k))))
      (binomial-expansion-times-y x y (1+ k) n))
    nil))

binomial-expansion-times-y-correcttheorem

(defthm binomial-expansion-times-y-correct
  (equal (* y (sumlist (binomial-expansion x y k n)))
    (sumlist (binomial-expansion-times-y x y k n)))
  :hints (("Goal" :in-theory (disable choose))))

binomial-expansion-trianglefunction

(defun binomial-expansion-triangle
  (x y k n)
  (declare (xargs :measure (nfix (1+ (- n k)))))
  (if (and (integerp k) (integerp n) (<= 0 k) (<= k n))
    (cons (* (choose k n) (expt x (1+ k)) (expt y (- n k)))
      (cons (* (choose k n) (expt x k) (expt y (1+ (- n k))))
        (binomial-expansion-triangle x y (1+ k) n)))
    nil))

binomial-expansion-times-x-plus-times-ytheorem

(defthm binomial-expansion-times-x-plus-times-y
  (equal (+ (sumlist (binomial-expansion-times-x x y k n))
      (sumlist (binomial-expansion-times-y x y k n)))
    (sumlist (binomial-expansion-triangle x y k n)))
  :hints (("Goal" :in-theory (disable choose expt))))

binomial-expansion-pascal-trianglefunction

(defun binomial-expansion-pascal-triangle
  (x y k n)
  (declare (xargs :measure (nfix (1+ (- n k)))))
  (if (and (integerp k) (integerp n) (<= 0 k))
    (if (< k n)
      (cons (* (choose k n) (expt x (1+ k)) (expt y (- n k)))
        (cons (* (choose (1+ k) n) (expt x (1+ k)) (expt y (- n k)))
          (binomial-expansion-pascal-triangle x y (1+ k) n)))
      (if (= k n)
        (list (* (choose k n) (expt x (1+ k)) (expt y (- n k))))
        nil))
    nil))

local

(local (defthm silly-inequality
    (implies (and (integerp k) (integerp n) (< k n))
      (<= (+ 1 k) n))))

local

(local (defthm choose-k-k
    (equal (choose k k)
      (if (and (integerp k) (<= 0 k))
        1
        0))))

local

(local (defthm expt-x-0 (equal (expt x 0) 1)))

local

(local (defthm binomial-expansion-triangle-x-y-k-1+k
    (equal (binomial-expansion-triangle x y (+ 1 k) k) nil)
    :hints (("Goal" :expand (binomial-expansion-triangle x y (+ 1 k) k)))))

local

(local (defthm binomial-expansion-triangle-x-y-k-k-lemma
    (equal (binomial-expansion-triangle x y k k)
      (if (and (integerp k) (<= 0 k))
        (list (expt x (1+ k)) (* (expt x k) y))
        nil))))

binomial-expansion-pascal-triangle-correcttheorem

(defthm binomial-expansion-pascal-triangle-correct
  (implies (and (integerp k) (integerp n) (<= 0 k) (<= k n))
    (equal (sumlist (binomial-expansion-triangle x y k n))
      (+ (* (choose k n) (expt x k) (expt y (1+ (- n k))))
        (sumlist (binomial-expansion-pascal-triangle x y k n)))))
  :hints (("Goal" :in-theory (disable choose
       expt
       right-unicity-of-1-for-expt
       expt-minus
       distributivity-of-expt-over-*
       exponents-multiply
       functional-commutativity-of-expt-/-base
       exponents-add
       exponents-add-for-nonneg-exponents)) ("Subgoal *1/5" :in-theory (disable choose expt))))

binomial-expansion-zerotheorem

(defthm binomial-expansion-zero
  (implies (< n k) (equal (binomial-expansion x y k n) nil)))

pascal-triangle-binomialtheorem

(defthm pascal-triangle-binomial
  (implies (and (integerp k) (integerp n) (<= 0 k))
    (equal (sumlist (binomial-expansion-pascal-triangle x y k n))
      (sumlist (binomial-expansion x y (1+ k) (1+ n)))))
  :hints (("Goal" :induct (binomial-expansion-pascal-triangle x y k n)
     :in-theory (disable choose
       expt
       right-unicity-of-1-for-expt
       expt-minus
       distributivity-of-expt-over-*
       exponents-multiply
       functional-commutativity-of-expt-/-base
       exponents-add
       exponents-add-for-nonneg-exponents)) ("Subgoal *1/1''" :use ((:instance choose-reduction (k (+ 1 k)) (n (+ 1 n)))))))

choose-0-ntheorem

(defthm choose-0-n
  (equal (choose 0 n)
    (if (and (integerp n) (<= 0 n))
      1
      0)))

binomial-theorem-induction-lemmatheorem

(defthm binomial-theorem-induction-lemma
  (implies (and (integerp n) (< 0 n))
    (equal (+ (* x (sumlist (binomial-expansion x y 0 (1- n))))
        (* y (sumlist (binomial-expansion x y 0 (1- n)))))
      (sumlist (binomial-expansion x y 0 n))))
  :hints (("Goal" :in-theory (disable expt))))

n-exptfunction

(defun n-expt
  (x n)
  (declare (xargs :guard (and (acl2-numberp x) (integerp n) (<= 0 n))))
  (if (and (integerp n) (< 0 n))
    (* x (n-expt x (1- n)))
    1))

local

(local (defthm distributivity-2
    (equal (* (+ x y) z) (+ (* x z) (* y z)))))

binomial-theorem-faketheorem

(defthm binomial-theorem-fake
  (implies (and (integerp n) (<= 0 n))
    (equal (n-expt (+ x y) n)
      (sumlist (binomial-expansion x y 0 n))))
  :hints (("Goal" :induct (n-expt x n)) ("Subgoal *1/1'" :in-theory (disable binomial-expansion))
    ("Subgoal *1/1'''" :by (:instance binomial-theorem-induction-lemma))))

n-expt-expttheorem

(defthm n-expt-expt
  (implies (and (integerp n) (<= 0 n))
    (equal (expt x n) (n-expt x n))))

binomial-theoremtheorem

(defthm binomial-theorem
  (implies (and (integerp n) (<= 0 n))
    (equal (expt (+ x y) n)
      (sumlist (binomial-expansion x y 0 n)))))

binomial-sum-commutestheorem

(defthm binomial-sum-commutes
  (implies (and (integerp n) (<= 0 n))
    (equal (sumlist (binomial-expansion x y 0 n))
      (sumlist (binomial-expansion y x 0 n))))
  :hints (("Goal" :use ((:instance binomial-theorem) (:instance binomial-theorem (x y) (y x)))
     :in-theory (disable binomial-theorem)))
  :rule-classes nil)