expt - ACL2 Book

Included Books

other

(in-package "ACL2")

include-book

(include-book "building-blocks")

local

(local (include-book "../../support/top"))

local

(local (include-book "expt-helper"))

local

(local (include-book "types"))

other

(table acl2-defaults-table :state-ok t)

expt-type-prescription-rationalp-basetheorem

(defthm expt-type-prescription-rationalp-base
  (implies (rationalp x) (rationalp (expt x n)))
  :rule-classes (:type-prescription :generalize))

expt-type-prescription-integerp-basetheorem

(defthm expt-type-prescription-integerp-base
  (implies (and (<= 0 n) (integerp x)) (integerp (expt x n)))
  :rule-classes (:type-prescription :generalize))

expt-type-prescription-integerp-base-atheorem

(defthm expt-type-prescription-integerp-base-a
  (implies (and (integerp n) (< n 0) (integerp x) (< 1 x))
    (and (rationalp (expt x n)) (not (integerp (expt x n)))))
  :rule-classes (:type-prescription :generalize))

expt-type-prescription-integerp-base-btheorem

(defthm expt-type-prescription-integerp-base-b
  (implies (and (integerp n) (< n 0) (integerp x) (< x -1))
    (and (rationalp (expt x n)) (not (integerp (expt x n)))))
  :rule-classes (:type-prescription :generalize))

expt-type-prescription-non-0-basetheorem

(defthm expt-type-prescription-non-0-base
  (implies (and (acl2-numberp x) (not (equal x 0)))
    (and (acl2-numberp (expt x n)) (not (equal (expt x n) 0))))
  :rule-classes (:type-prescription :generalize))

expt-type-prescription-positive-basetheorem

(defthm expt-type-prescription-positive-base
  (implies (and (< 0 x) (rationalp x))
    (and (rationalp (expt x n)) (< 0 (expt x n))))
  :rule-classes (:type-prescription :generalize))

expt-type-prescription-nonnegative-basetheorem

(defthm expt-type-prescription-nonnegative-base
  (implies (and (<= 0 x) (rationalp x))
    (and (rationalp (expt x n)) (<= 0 (expt x n))))
  :rule-classes (:type-prescription :generalize))

integerp-/-expt-1theorem

(defthm integerp-/-expt-1
  (implies (and (integerp x) (< 1 x) (integerp n))
    (equal (integerp (/ (expt x n))) (<= n 0)))
  :rule-classes (:rewrite (:type-prescription :corollary (implies (and (integerp x) (< 1 x) (integerp n) (<= n 0))
        (integerp (/ (expt x n)))))
    (:generalize :corollary (implies (and (integerp x) (< 1 x) (integerp n) (<= n 0))
        (integerp (/ (expt x n)))))))

integerp-/-expt-2theorem

(defthm integerp-/-expt-2
  (implies (and (integerp x) (< x -1) (integerp n))
    (equal (integerp (/ (expt x n))) (<= n 0)))
  :rule-classes (:rewrite (:type-prescription :corollary (implies (and (integerp x) (< x -1) (integerp n) (<= n 0))
        (integerp (/ (expt x n)))))
    (:generalize :corollary (implies (and (integerp x) (< x -1) (integerp n) (<= n 0))
        (integerp (/ (expt x n)))))))

|(expt x 0)|theorem

(defthm |(expt x 0)| (equal (expt x 0) 1))

|(expt 0 n)|theorem

(defthm |(expt 0 n)|
  (equal (expt 0 n)
    (if (zip n)
      1
      0)))

|(expt x 1)|theorem

(defthm |(expt x 1)|
  (implies (acl2-numberp x) (equal (expt x 1) x)))

|(expt 1 n)|theorem

(defthm |(expt 1 n)| (equal (expt 1 n) 1))

|(expt x -1)|theorem

(defthm |(expt x -1)| (equal (expt x -1) (/ x)))

|(equal (expt x n) -1)|theorem

(defthm |(equal (expt x n) -1)|
  (implies (and (integerp n) (real/rationalp x))
    (equal (equal (expt x n) -1) (and (equal x -1) (oddp n)))))

|(equal (expt x n) 0)|theorem

(defthm |(equal (expt x n) 0)|
  (implies (and (integerp n) (real/rationalp x))
    (equal (equal (expt x n) 0)
      (and (equal x 0) (not (equal n 0))))))

|(equal (expt x n) 1)|theorem

(defthm |(equal (expt x n) 1)|
  (implies (and (integerp n)
      (real/rationalp x)
      (syntaxp (rewriting-goal-literal x mfc state)))
    (equal (equal (expt x n) 1)
      (or (zip n) (equal x 1) (and (equal x -1) (evenp n))))))

p-o-2-g-fnfunction

(defun p-o-2-g-fn
  (c)
  (let ((x (power-of-2-generalized c)))
    (if x
      (list (cons 'x (kwote x)))
      nil)))

|(equal (expt 2 n) c)|theorem

(defthm |(equal (expt 2 n) c)|
  (implies (and (bind-free (p-o-2-g-fn c) (x))
      (integerp x)
      (equal (expt 2 x) c)
      (integerp n))
    (equal (equal (expt 2 n) c) (equal n x))))

|(expt (+ x y) 2)|theorem

(defthm |(expt (+ x y) 2)|
  (implies (syntaxp (rewriting-goal-literal x mfc state))
    (equal (expt (+ x y) 2) (+ (expt x 2) (* 2 x y) (expt y 2))))
  :hints (("Goal" :expand (expt (+ x y) 2))))

|(expt (+ x y) 3)|theorem

(defthm |(expt (+ x y) 3)|
  (implies (syntaxp (rewriting-goal-literal x mfc state))
    (equal (expt (+ x y) 3)
      (+ (expt x 3)
        (* 3 (expt x 2) y)
        (* 3 x (expt y 2))
        (expt y 3))))
  :hints (("Goal" :expand ((expt (+ x y) 3) (expt (+ x y) 2)))))

|(expt c (* d n))|theorem

(defthm |(expt c (* d n))|
  (implies (and (syntaxp (quotep c))
      (integerp c)
      (syntaxp (quotep d))
      (integerp d)
      (integerp n))
    (equal (expt c (* d n)) (expt (expt c d) n))))

|(expt (/ x) n)|theorem

(defthm |(expt (/ x) n)|
  (equal (expt (/ x) n) (expt x (- n))))

|(/ (expt x n))|theorem

(defthm |(/ (expt x n))|
  (equal (/ (expt x n)) (expt x (- n))))

|(expt 1/c n)|theorem

(defthm |(expt 1/c n)|
  (implies (and (syntaxp (quotep x))
      (syntaxp (rationalp (unquote x)))
      (syntaxp (not (integerp (unquote x))))
      (syntaxp (< (abs x) 1)))
    (equal (expt x n) (expt (/ x) (- n)))))

|(expt (- x) n)|theorem

(defthm |(expt (- x) n)|
  (implies (and (syntaxp (rewriting-goal-literal x mfc state))
      (syntaxp (mostly-negative-addends-p x mfc state))
      (integerp n))
    (equal (expt x n)
      (if (evenp n)
        (expt (- x) n)
        (- (expt (- x) n)))))
  :hints (("Goal" :use ((:instance expt-negative-base-even-exponent-a (i n) (r x)) (:instance expt-negative-base-odd-exponent-a (i n) (r x))))))

|(expt (- c) n)|theorem

(defthm |(expt (- c) n)|
  (implies (and (syntaxp (rewriting-goal-literal c mfc state))
      (syntaxp (rational-constant-p c))
      (integerp n))
    (equal (expt (- c) n)
      (if (evenp n)
        (expt c n)
        (- (expt c n))))))

other

(theory-invariant (if (active-runep '(:definition arith-5-active-flag))
    (and (active-runep '(:rewrite |(expt (/ x) n)|))
      (active-runep '(:rewrite |(/ (expt x n))|))
      (active-runep '(:rewrite |(expt 1/c n)|))
      (active-runep '(:rewrite |(expt (- x) n)|))
      (active-runep '(:rewrite |(expt (- c) n)|)))
    t)
  :error nil)

|(expt (* x y) n)|theorem

(defthm |(expt (* x y) n)|
  (equal (expt (* x y) n) (* (expt x n) (expt y n))))

|(expt (expt x m) n)|theorem

(defthm |(expt (expt x m) n)|
  (implies (and (integerp m) (integerp n))
    (equal (expt (expt x m) n) (expt x (* m n)))))

|(expt x (+ m n))|theorem

(defthm |(expt x (+ m n))|
  (implies (and (syntaxp (rewriting-goal-literal x mfc state))
      (integerp m)
      (integerp n))
    (equal (expt x (+ m n))
      (if (equal (+ m n) 0)
        1
        (* (expt x m) (expt x n))))))

|(expt x (+ m n)) non-zero (+ m n)|theorem

(defthm |(expt x (+ m n)) non-zero (+ m n)|
  (implies (and (integerp m) (integerp n) (not (equal (+ m n) 0)))
    (equal (expt x (+ m n)) (* (expt x m) (expt x n)))))

|(expt x (+ m n)) non-zero x|theorem

(defthm |(expt x (+ m n)) non-zero x|
  (implies (and (acl2-numberp x)
      (not (equal x 0))
      (integerp m)
      (integerp n))
    (equal (expt x (+ m n)) (* (expt x m) (expt x n)))))

|(integerp (expt x n))|theorem

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

|(< (expt x n) (expt x m))|theorem

(defthm |(< (expt x n) (expt x m))|
  (implies (and (real/rationalp x) (< 1 x) (integerp m) (integerp n))
    (equal (< (expt x m) (expt x n)) (< m n))))

|(equal (expt x m) (expt x n))|theorem

(defthm |(equal (expt x m) (expt x n))|
  (implies (and (real/rationalp x)
      (not (equal x -1))
      (not (equal x 0))
      (not (equal x 1))
      (integerp m)
      (integerp n))
    (equal (equal (expt x m) (expt x n)) (equal m n))))

expt-exceeds-another-by-more-than-ytheorem

(defthm expt-exceeds-another-by-more-than-y
  (implies (and (real/rationalp x)
      (< 1 x)
      (integerp m)
      (integerp n)
      (<= 0 m)
      (<= 0 n)
      (< m n)
      (real/rationalp y)
      (< (+ y 1) x))
    (< (+ y (expt x m)) (expt x n))))

expt-2-n-is-eventheorem

(defthm expt-2-n-is-even
  (implies (and (integerp n) (integerp m))
    (equal (equal (expt 2 n) (+ 1 (expt 2 m)))
      (and (equal n 1) (equal m 0)))))

odd-expt-thmtheorem

(defthm odd-expt-thm
  (implies (and (integerp man) (integerp exp) (<= exp 0))
    (equal (< man (expt 2 exp)) (<= man 0))))

expt-x->-xtheorem

(defthm expt-x->-x
  (implies (and (< 1 x) (< 1 n) (real/rationalp x) (integerp n))
    (< x (expt x n)))
  :rule-classes (:rewrite :linear))

expt-x->=-xtheorem

(defthm expt-x->=-x
  (implies (and (<= 1 x) (< 1 n) (real/rationalp x) (integerp n))
    (<= x (expt x n)))
  :rule-classes (:rewrite :linear))

expt-is-increasing-for-base->-1theorem

(defthm expt-is-increasing-for-base->-1
  (implies (and (< m n)
      (< 1 x)
      (integerp m)
      (integerp n)
      (real/rationalp x))
    (< (expt x m) (expt x n)))
  :rule-classes ((:rewrite) (:linear :match-free :once)))

expt-is-decreasing-for-pos-base-<-1theorem

(defthm expt-is-decreasing-for-pos-base-<-1
  (implies (and (< m n)
      (< 0 x)
      (< x 1)
      (integerp m)
      (integerp n)
      (real/rationalp x))
    (< (expt x n) (expt x m)))
  :rule-classes ((:rewrite) (:linear :match-free :once)))

expt-is-weakly-increasing-for-base->-1theorem

(defthm expt-is-weakly-increasing-for-base->-1
  (implies (and (<= m n)
      (<= 1 x)
      (integerp m)
      (integerp n)
      (real/rationalp x))
    (<= (expt x m) (expt x n)))
  :rule-classes ((:rewrite) (:linear :match-free :once)))

expt-is-weakly-decreasing-for-pos-base-<-1theorem

(defthm expt-is-weakly-decreasing-for-pos-base-<-1
  (implies (and (<= m n)
      (< 0 x)
      (<= x 1)
      (integerp m)
      (integerp n)
      (real/rationalp x))
    (<= (expt x n) (expt x m)))
  :rule-classes ((:rewrite) (:linear :match-free :once)))

expt->-1-onetheorem

(defthm expt->-1-one
  (implies (and (< 1 x) (< 0 n) (real/rationalp x) (integerp n))
    (< 1 (expt x n)))
  :rule-classes :linear)

expt->=-1-onetheorem

(defthm expt->=-1-one
  (implies (and (<= 1 x) (<= 0 n) (real/rationalp x) (integerp n))
    (<= 1 (expt x n)))
  :rule-classes :linear)

expt->-1-twotheorem

(defthm expt->-1-two
  (implies (and (< 0 x)
      (< x 1)
      (< n 0)
      (real/rationalp x)
      (integerp n))
    (< 1 (expt x n)))
  :rule-classes :linear)

expt->=-1-twotheorem

(defthm expt->=-1-two
  (implies (and (< 0 x)
      (<= x 1)
      (<= n 0)
      (real/rationalp x)
      (integerp n))
    (<= 1 (expt x n)))
  :rule-classes :linear)

expt-<-1-onetheorem

(defthm expt-<-1-one
  (implies (and (< 0 x)
      (< x 1)
      (< 0 n)
      (real/rationalp x)
      (integerp n))
    (< (expt x n) 1))
  :rule-classes :linear)

expt-<=-1-onetheorem

(defthm expt-<=-1-one
  (implies (and (<= 0 x)
      (<= x 1)
      (<= 0 n)
      (real/rationalp x)
      (integerp n))
    (<= (expt x n) 1))
  :hints (("Goal" :cases ((equal x 0) (equal x 1))))
  :rule-classes :linear)

expt-<-1-twotheorem

(defthm expt-<-1-two
  (implies (and (< 1 x) (< n 0) (real/rationalp x) (integerp n))
    (< (expt x n) 1))
  :rule-classes :linear)

expt-<=-1-twotheorem

(defthm expt-<=-1-two
  (implies (and (<= 1 x) (<= n 0) (real/rationalp x) (integerp n))
    (<= (expt x n) 1))
  :rule-classes :linear)

mfc-pot-lstfunction

(defun mfc-pot-lst
  (mfc)
  (access metafunction-context mfc :simplify-clause-pot-lst))

mfc-ptfunction

(defun mfc-pt
  (mfc)
  (let ((rcnst (access metafunction-context mfc :rcnst)))
    (access rewrite-constant rcnst :pt)))

bounds-for-expt-linear-fns-1function

(defun bounds-for-expt-linear-fns-1
  (n mfc state)
  (declare (xargs :mode :program))
  (declare (ignore state))
  (if (equal (fn-symb n) 'unary--)
    (let ((bounds-polys (bounds-polys-with-var n (mfc-pot-lst mfc) (mfc-pt mfc))))
      (mv-let (lbd lbd-rel lbd-ttree ubd ubd-rel ubd-ttree)
        (extract-bounds bounds-polys)
        (declare (ignore lbd-ttree ubd-ttree))
        (mv lbd lbd-rel ubd ubd-rel)))
    (let ((bounds-polys (bounds-polys-with-var n (mfc-pot-lst mfc) (mfc-pt mfc))))
      (mv-let (lbd lbd-rel lbd-ttree ubd ubd-rel ubd-ttree)
        (extract-bounds bounds-polys)
        (declare (ignore lbd-ttree ubd-ttree))
        (mv lbd lbd-rel ubd ubd-rel)))))

bounds-for-expt-linear-fnsfunction

(defun bounds-for-expt-linear-fns
  (n mfc state)
  (declare (xargs :mode :program))
  (cond ((quotep n) (mv nil nil nil nil))
    ((symbolp n) (bounds-for-expt-linear-fns-1 n mfc state))
    ((equal (fn-symb n) 'binary-+) (mv nil nil nil nil))
    ((equal (fn-symb n) 'unary--) (mv-let (lbd lbd-rel ubd ubd-rel)
        (bounds-for-expt-linear-fns-1 (arg1 n) mfc state)
        (mv (if ubd
            (- ubd)
            nil)
          ubd-rel
          (if lbd
            (- lbd)
            nil)
          lbd-rel)))
    ((and (equal (fn-symb n) 'binary-*)
       (quotep (arg1 n))
       (equal (unquote (arg1 n)) 0)) (mv nil nil nil nil))
    ((and (equal (fn-symb n) 'binary-*)
       (quotep (arg1 n))
       (rationalp (unquote (arg1 n)))
       (< 0 (unquote (arg1 n)))) (mv-let (lbd lbd-rel ubd ubd-rel)
        (bounds-for-expt-linear-fns-1 (arg2 n) mfc state)
        (let ((x (/ (unquote (arg1 n)))))
          (mv (if lbd
              (/ lbd x)
              nil)
            lbd-rel
            (if ubd
              (/ ubd x)
              nil)
            ubd-rel))))
    ((and (equal (fn-symb n) 'binary-*)
       (quotep (arg1 n))
       (rationalp (unquote (arg1 n)))
       (< (unquote (arg1 n)) 0)) (mv-let (lbd lbd-rel ubd ubd-rel)
        (bounds-for-expt-linear-fns-1 (arg2 n) mfc state)
        (let ((x (/ (unquote (arg1 n)))))
          (mv (if ubd
              (- (/ ubd x))
              nil)
            ubd-rel
            (if lbd
              (- (/ lbd x))
              nil)
            lbd-rel))))
    (t (bounds-for-expt-linear-fns-1 n mfc state))))

expt-linear-upper-<-fnfunction

(defun expt-linear-upper-<-fn
  (n mfc state)
  (declare (xargs :mode :program))
  (mv-let (lbd lbd-rel ubd ubd-rel)
    (bounds-for-expt-linear-fns n mfc state)
    (declare (ignore lbd lbd-rel))
    (cond ((and (equal ubd-rel '<) (integerp ubd)) (list (cons 'd (kwote ubd))))
      (t nil))))

expt-linear-upper-<=-fnfunction

(defun expt-linear-upper-<=-fn
  (n mfc state)
  (declare (xargs :mode :program))
  (mv-let (lbd lbd-rel ubd ubd-rel)
    (bounds-for-expt-linear-fns n mfc state)
    (declare (ignore lbd lbd-rel))
    (cond ((and (equal ubd-rel '<=) (integerp ubd)) (list (cons 'd (kwote ubd))))
      ((and (equal ubd-rel '<) (integerp ubd)) nil)
      ((real/rationalp ubd) (list (cons 'd (kwote (floor ubd 1)))))
      (t nil))))

expt-linear-lower-<-fnfunction

(defun expt-linear-lower-<-fn
  (n mfc state)
  (declare (xargs :mode :program))
  (mv-let (lbd lbd-rel ubd ubd-rel)
    (bounds-for-expt-linear-fns n mfc state)
    (declare (ignore ubd ubd-rel))
    (cond ((and (equal lbd-rel '<) (integerp lbd)) (list (cons 'd (kwote lbd))))
      (t nil))))

expt-linear-lower-<=-fnfunction

(defun expt-linear-lower-<=-fn
  (n mfc state)
  (declare (xargs :mode :program))
  (mv-let (lbd lbd-rel ubd ubd-rel)
    (bounds-for-expt-linear-fns n mfc state)
    (declare (ignore ubd ubd-rel))
    (cond ((and (equal lbd-rel '<=) (integerp lbd)) (list (cons 'd (kwote lbd))))
      ((and (equal lbd-rel '<) (integerp lbd)) nil)
      ((real/rationalp lbd) (list (cons 'd (kwote (+ 1 (floor lbd 1))))))
      (t nil))))

expt-linear-upper-<theorem

(defthm expt-linear-upper-<
  (implies (and (syntaxp (rational-constant-p c))
      (real/rationalp c)
      (< 1 c)
      (bind-free (expt-linear-upper-<-fn n mfc state) (d))
      (integerp d)
      (< n d)
      (integerp n))
    (< (expt c n) (expt c d)))
  :rule-classes ((:linear :trigger-terms ((expt c n)))))

expt-linear-upper-<=theorem

(defthm expt-linear-upper-<=
  (implies (and (syntaxp (rational-constant-p c))
      (real/rationalp c)
      (< 1 c)
      (bind-free (expt-linear-upper-<=-fn n mfc state) (d))
      (integerp d)
      (<= n d)
      (integerp n))
    (<= (expt c n) (expt c d)))
  :rule-classes ((:linear :trigger-terms ((expt c n)))))

expt-linear-lower-<theorem

(defthm expt-linear-lower-<
  (implies (and (syntaxp (rational-constant-p c))
      (real/rationalp c)
      (< 1 c)
      (bind-free (expt-linear-lower-<-fn n mfc state) (d))
      (integerp d)
      (< d n)
      (integerp n))
    (< (expt c d) (expt c n)))
  :rule-classes ((:linear :trigger-terms ((expt c n)))))

expt-linear-lower-<=theorem

(defthm expt-linear-lower-<=
  (implies (and (syntaxp (rational-constant-p c))
      (real/rationalp c)
      (< 1 c)
      (bind-free (expt-linear-lower-<=-fn n mfc state) (d))
      (integerp d)
      (<= d n)
      (integerp n))
    (<= (expt c d) (expt c n)))
  :rule-classes ((:linear :trigger-terms ((expt c n)))))

expt-type-prescription-negative-base-even-exponenttheorem

(defthm expt-type-prescription-negative-base-even-exponent
  (implies (and (< x 0)
      (rationalp x)
      (integerp n)
      (integerp (* 1/2 n)))
    (and (rationalp (expt x n)) (< 0 (expt x n))))
  :rule-classes (:type-prescription :generalize))

expt-type-prescription-negative-base-odd-exponenttheorem

(defthm expt-type-prescription-negative-base-odd-exponent
  (implies (and (< x 0)
      (rationalp x)
      (integerp n)
      (not (integerp (* 1/2 n))))
    (and (rationalp (expt x n)) (< (expt x n) 0)))
  :rule-classes (:type-prescription :generalize))

expt-type-prescription-nonpositive-base-even-exponenttheorem

(defthm expt-type-prescription-nonpositive-base-even-exponent
  (implies (and (<= x 0)
      (rationalp x)
      (integerp n)
      (integerp (* 1/2 n)))
    (and (rationalp (expt x n)) (<= 0 (expt x n))))
  :rule-classes (:type-prescription :generalize)
  :hints (("Goal" :use ((:instance expt-type-prescription-negative-base-even-exponent-a)))))

expt-type-prescription-nonpositive-base-odd-exponenttheorem

(defthm expt-type-prescription-nonpositive-base-odd-exponent
  (implies (and (<= x 0)
      (rationalp x)
      (integerp n)
      (not (integerp (* 1/2 n))))
    (and (rationalp (expt x n)) (<= (expt x n) 0)))
  :rule-classes (:type-prescription :generalize)
  :hints (("Goal" :use ((:instance expt-type-prescription-negative-base-odd-exponent-a)))))