expt-proofs - ACL2 Book

Included Books

ground-zero negative-syntaxp predicate fp2 numerator denominator integerp fl arith2 top even-odd

other

(in-package "ACL2")

natpfunction

(defun natp
  (x)
  (declare (xargs :guard t))
  (and (integerp x) (<= 0 x)))

flfunction

(defund fl
  (x)
  (declare (xargs :guard (real/rationalp x)))
  (floor x 1))

include-book

(include-book "ground-zero")

include-book

(include-book "negative-syntaxp")

local

(local (include-book "predicate"))

local

(local (include-book "fp2"))

local

(local (include-book "numerator"))

local

(local (include-book "denominator"))

local

(local (include-book "integerp"))

local

(local (include-book "fl"))

local

(local (include-book "arith2"))

a16encapsulate

(encapsulate nil
  (local (include-book "../../../arithmetic/top"))
  (defthm a16
    (equal (expt (* a b) i) (* (expt a i) (expt b i)))
    :hints (("Goal" :in-theory (enable distributivity-of-expt-over-*))))
  (defthmd expt-split
    (implies (and (integerp i)
        (integerp j)
        (case-split (acl2-numberp r))
        (case-split (not (equal r 0))))
      (equal (expt r (+ i j)) (* (expt r i) (expt r j))))
    :hints (("Goal" :in-theory (enable expt)))))

other

(theory-invariant (not (and (active-runep '(:rewrite expt-split))
      (active-runep '(:rewrite a15))))
  :key expt-split-invariant)

other

(theory-invariant (not (and (active-runep '(:rewrite expt-split))
      (active-runep '(:definition expt))))
  :key expt-split-invariant-2)

expt-2-positive-rational-typetheorem

(defthm expt-2-positive-rational-type
  (and (rationalp (expt 2 i)) (< 0 (expt 2 i)))
  :hints (("Goal" :in-theory (enable expt)))
  :rule-classes (:rewrite (:type-prescription :typed-term (expt 2 i))))

expt-2-positive-integer-typetheorem

(defthm expt-2-positive-integer-type
  (implies (<= 0 i)
    (and (integerp (expt 2 i)) (< 0 (expt 2 i))))
  :hints (("Goal" :in-theory (enable expt)))
  :rule-classes (:type-prescription))

expt-2-integerptheorem

(defthm expt-2-integerp
  (implies (<= 0 i) (integerp (expt 2 i))))

expt-2-type-lineartheorem

(defthm expt-2-type-linear
  (implies (<= 0 i) (<= 1 (expt 2 i)))
  :rule-classes ((:linear :trigger-terms ((expt 2 i)))))

encapsulate

(encapsulate nil
  (local (defthm expt-strong-monotone-1
      (implies (and (integerp n) (integerp k) (> k 0))
        (< (expt 2 n) (expt 2 (+ n k))))
      :hints (("Goal" :in-theory (enable expt)))
      :rule-classes nil))
  (defthmd expt-strong-monotone
    (implies (and (integerp n) (integerp m))
      (equal (< (expt 2 n) (expt 2 m)) (< n m)))
    :hints (("Goal" :use ((:instance expt-strong-monotone-1 (k (- m n))) (:instance expt-strong-monotone-1 (k (- n m)) (n m)))))))

expt2-integertheorem

(defthm expt2-integer
  (implies (case-split (integerp i))
    (equal (integerp (expt 2 i)) (<= 0 i)))
  :hints (("Goal" :use (:instance expt-strong-monotone (n i) (m 0)))))

expt-strong-monotone-lineartheorem

(defthmd expt-strong-monotone-linear
  (implies (and (< n m)
      (case-split (integerp n))
      (case-split (integerp m)))
    (< (expt 2 n) (expt 2 m)))
  :rule-classes ((:linear :match-free :all))
  :hints (("Goal" :use expt-strong-monotone)))

expt-weak-monotonetheorem

(defthmd expt-weak-monotone
  (implies (and (integerp n) (integerp m))
    (equal (<= (expt 2 n) (expt 2 m)) (<= n m)))
  :hints (("Goal" :use (expt-strong-monotone (:instance expt-strong-monotone (m n) (n m))))))

expt-weak-monotone-lineartheorem

(defthmd expt-weak-monotone-linear
  (implies (and (<= n m)
      (case-split (integerp n))
      (case-split (integerp m)))
    (<= (expt 2 n) (expt 2 m)))
  :rule-classes ((:linear :match-free :all))
  :hints (("Goal" :use (expt-strong-monotone (:instance expt-strong-monotone (m n) (n m))))))

expt-between-one-and-twotheorem

(defthmd expt-between-one-and-two
  (implies (and (<= 1 (expt 2 i)) (< (expt 2 i) 2))
    (equal (expt 2 i) 1))
  :hints (("goal" :in-theory (enable expt zip)) ("subgoal *1/7" :use (:instance expt-weak-monotone (n (+ i 1)) (m 0)))))

expt-with-i-non-integertheorem

(defthm expt-with-i-non-integer
  (implies (not (integerp i)) (equal (expt r i) 1))
  :hints (("Goal" :in-theory (enable expt))))

expt-minus-helpertheorem

(defthmd expt-minus-helper
  (equal (expt r (* -1 i)) (/ (expt r i)))
  :otf-flg t
  :hints (("Goal" :cases ((integerp i) (and (not (integerp i)) (acl2-numberp i)))
     :in-theory (enable expt))))

expt-minustheorem

(defthmd expt-minus
  (implies (syntaxp (negative-syntaxp i))
    (equal (expt r i) (/ (expt r (* -1 i)))))
  :hints (("Goal" :in-theory (enable expt-minus-helper expt-split))))

local

(local (in-theory (enable expt-minus)))

expt-inversetheorem

(defthmd expt-inverse
  (equal (/ (expt 2 i)) (expt 2 (* -1 i))))

other

(theory-invariant (not (and (active-runep '(:rewrite expt-minus))
      (active-runep '(:rewrite expt-inverse))))
  :key expt-minus-invariant)

a15theorem

(defthmd a15
  (implies (and (rationalp i)
      (not (equal i 0))
      (integerp j1)
      (integerp j2))
    (and (equal (* (expt i j1) (expt i j2)) (expt i (+ j1 j2)))
      (equal (* (expt i j1) (* (expt i j2) x))
        (* (expt i (+ j1 j2)) x))))
  :hints (("Goal" :in-theory (enable expt-split))))

expt-r-0theorem

(defthm expt-r-0
  (equal (expt r 0) 1)
  :hints (("Goal" :in-theory (enable expt))))

expt-0-itheorem

(defthm expt-0-i
  (implies (and (case-split (integerp i))
      (case-split (not (equal 0 i))))
    (equal (expt 0 i) 0))
  :hints (("Goal" :in-theory (enable expt))))

in-theory

(in-theory (disable (:executable-counterpart expt)))

other

(set-compile-fns t)

expt-executefunction

(defun expt-execute (r i) (expt r i))

expt-execute-rewritetheorem

(defthm expt-execute-rewrite
  (implies (and (syntaxp (and (quotep r) (quotep i) (< (abs (cadr i)) 1000))))
    (equal (expt r i) (expt-execute r i))))

expt2-constants-collect-special-1theorem

(defthm expt2-constants-collect-special-1
  (implies (and (syntaxp (and (quotep i1) (quotep i2)))
      (case-split (rationalp y))
      (case-split (integerp i1))
      (case-split (integerp i2)))
    (equal (* (expt 2 i1) (/ (expt 2 i2)) y)
      (* (expt 2 (- i1 i2)) y)))
  :hints (("Goal" :in-theory (set-difference-theories (enable expt-split) 'nil))))

expt2-constants-collect-special-2theorem

(defthm expt2-constants-collect-special-2
  (implies (and (syntaxp (and (quotep i1) (quotep i2)))
      (case-split (integerp i1))
      (case-split (integerp i2)))
    (equal (* (expt 2 i1) (/ (expt 2 i2))) (expt 2 (- i1 i2))))
  :hints (("Goal" :in-theory (set-difference-theories (enable expt-split) 'nil))))

expt2-constants-collect-special-4theorem

(defthm expt2-constants-collect-special-4
  (implies (and (syntaxp (and (quotep i1) (quotep i2)))
      (case-split (rationalp y))
      (case-split (integerp i1))
      (case-split (integerp i2)))
    (equal (* (/ (expt 2 i2)) (expt 2 i1) y)
      (* (expt 2 (- i1 i2)) y)))
  :hints (("Goal" :in-theory (set-difference-theories (enable expt-split) 'nil))))

expt2-constants-collect-special-5theorem

(defthm expt2-constants-collect-special-5
  (implies (and (syntaxp (and (quotep i1) (quotep i2)))
      (case-split (integerp i1))
      (case-split (integerp i2)))
    (equal (* (/ (expt 2 i2)) (expt 2 i1)) (expt 2 (- i1 i2))))
  :hints (("Goal" :in-theory (set-difference-theories (enable expt-split) 'nil))))

expt2-constants-collect-special-6theorem

(defthm expt2-constants-collect-special-6
  (implies (and (syntaxp (and (quotep i1) (quotep i2)))
      (case-split (rationalp x))
      (case-split (integerp i1))
      (case-split (integerp i2)))
    (equal (* (expt 2 i2) x (expt 2 i1))
      (* (expt 2 (+ i1 i2)) x)))
  :hints (("Goal" :in-theory (set-difference-theories (enable expt-split) 'nil))))

expt2-constants-collect-special-3theorem

(defthm expt2-constants-collect-special-3
  (implies (and (syntaxp (and (quotep i1) (quotep i2)))
      (case-split (rationalp x))
      (case-split (integerp i1))
      (case-split (integerp i2)))
    (equal (equal (* x (expt 2 i1)) (expt 2 i2))
      (equal x (expt 2 (- i2 i1)))))
  :hints (("Goal" :in-theory (set-difference-theories (enable expt-split) 'nil))))

expt2-1-to-1theorem

(defthm expt2-1-to-1
  (implies (and (integerp i1) (integerp i2))
    (equal (equal (expt 2 i1) (expt 2 i2)) (equal i1 i2)))
  :hints (("Goal" :use ((:instance expt-strong-monotone (n i1) (m i2)) (:instance expt-strong-monotone (n i2) (m i1))))))

expt-eventheorem

(defthm expt-even
  (implies (and (< 0 i) (case-split (integerp i)))
    (integerp (* 1/2 (expt 2 i))))
  :hints (("goal" :in-theory (enable expt))))

expt-quotient-integerptheorem

(defthm expt-quotient-integerp
  (implies (and (<= j i)
      (case-split (integerp i))
      (case-split (integerp j)))
    (integerp (* (expt 2 i) (/ (expt 2 j)))))
  :rule-classes (:rewrite :type-prescription)
  :hints (("Goal" :in-theory (e/d (expt-split) (expt-2-integerp))
     :use (:instance expt-2-positive-integer-type (i (- i j))))))

expt-quotient-integerp-alttheorem

(defthm expt-quotient-integerp-alt
  (implies (and (<= j i)
      (case-split (integerp i))
      (case-split (integerp j)))
    (integerp (* (/ (expt 2 j)) (expt 2 i))))
  :rule-classes (:rewrite :type-prescription))

expt-prod-integer-3-termstheorem

(defthm expt-prod-integer-3-terms
  (implies (and (integerp n) (<= 0 (+ i j)) (integerp i) (integerp j))
    (integerp (* (expt 2 i) (expt 2 j) n)))
  :hints (("Goal" :in-theory (enable a15))))

expt2-inverse-integertheorem

(defthm expt2-inverse-integer
  (implies (case-split (integerp i))
    (equal (integerp (/ (expt 2 i))) (<= i 0)))
  :hints (("Goal" :in-theory (disable expt2-integer)
     :use (:instance expt2-integer (i (- i))))))

expt-prod-integer-3-terms-2theorem

(defthm expt-prod-integer-3-terms-2
  (implies (and (<= 0 (+ i (- j) (- l)))
      (integerp i)
      (integerp j)
      (integerp l))
    (integerp (* (expt 2 i) (/ (expt 2 j)) (/ (expt 2 l)))))
  :hints (("Goal" :in-theory (set-difference-theories (enable a15 expt-inverse)
       '(expt-minus)))))

expt2-inverse-eventheorem

(defthm expt2-inverse-even
  (implies (case-split (integerp i))
    (equal (integerp (* 1/2 (/ (expt 2 i)))) (<= (+ 1 i) 0)))
  :otf-flg t
  :hints (("Goal" :in-theory (set-difference-theories (enable expt-split)
       '(expt2-integer expt2-inverse-integer))
     :use (:instance expt2-integer (i (+ -1 (- i)))))))

expt-2-split-product-indextheorem

(defthmd expt-2-split-product-index
  (implies (and (syntaxp (not (quotep i)))
      (case-split (rationalp r))
      (case-split (integerp i)))
    (equal (expt r (* 2 i)) (* (expt r i) (expt r i))))
  :hints (("Goal" :in-theory (disable expt-split)
     :use (:instance expt-split (i i) (j i)))))

expt-bigger-than-itheorem

(defthm expt-bigger-than-i
  (implies (integerp i) (< i (expt 2 i)))
  :hints (("Goal" :in-theory (enable expt))))

expt-compare-with-doubletheorem

(defthmd expt-compare-with-double
  (implies (and (integerp x) (integerp i))
    (equal (< (* 2 x) (expt 2 i)) (< x (expt 2 (+ -1 i)))))
  :hints (("Goal" :in-theory (enable expt-split))))

expt-2-reduce-leading-constant-gentheorem

(defthmd expt-2-reduce-leading-constant-gen
  (implies (case-split (integerp (+ k d)))
    (equal (expt 2 (+ k d))
      (* (expt 2 (fl k)) (expt 2 (+ (mod k 1) d)))))
  :hints (("Goal" :in-theory (set-difference-theories (enable mod) '(expt-split))
     :use (:instance expt-split (r 2) (i (fl k)) (j (+ (mod k 1) d))))))

expt-2-reduce-leading-constanttheorem

(defthmd expt-2-reduce-leading-constant
  (implies (and (syntaxp (and (quotep k) (or (>= (cadr k) 1) (< (cadr k) 0))))
      (case-split (integerp (+ k d))))
    (equal (expt 2 (+ k d))
      (* (expt 2 (fl k)) (expt 2 (+ (mod k 1) d)))))
  :hints (("Goal" :in-theory (set-difference-theories (enable) '(expt-split))
     :use (expt-2-reduce-leading-constant-gen (:instance expt-split (r 2) (i (fl k)) (j (+ (mod k 1) d)))))))

expt-combinetheorem

(defthmd expt-combine
  (implies (and (case-split (rationalp r))
      (case-split (not (equal r 0)))
      (case-split (integerp i1))
      (case-split (integerp i2)))
    (and (equal (* (expt r i1) (expt r i2)) (expt r (+ i1 i2)))
      (equal (* (expt r i1) (* (expt r i2) x))
        (* (expt r (+ i1 i2)) x))))
  :hints (("goal" :in-theory (enable a15))))

expt-with-small-ntheorem

(defthm expt-with-small-n
  (implies (<= n 0) (<= (expt 2 n) 1))
  :hints (("Goal" :use (:instance expt-weak-monotone (m 0))))
  :rule-classes (:linear))

local

(local (include-book "even-odd"))

even-not-equal-oddtheorem

(defthmd even-not-equal-odd
  (implies (and (evenp x) (oddp y)) (not (equal x y)))
  :hints (("Goal" :in-theory (enable oddp))))

expt-2-is-not-oddtheorem

(defthm expt-2-is-not-odd
  (implies (and (evenp x) (< 0 i) (integerp i))
    (equal (equal (expt 2 i) (+ 1 x)) nil))
  :hints (("Goal" :in-theory (enable evenp oddp even-not-equal-odd)))
  :otf-flg t)

a14theorem

(defthm a14
  (and (implies (and (integerp i) (<= 0 i) (<= 0 j))
      (and (integerp (expt i j)) (<= 0 (expt i j))))
    (implies (and (rationalp i) (not (equal i 0)))
      (not (equal (expt i j) 0))))
  :hints (("Goal" :in-theory (enable expt)))
  :rule-classes ((:type-prescription :corollary (implies (and (integerp i) (<= 0 i) (<= 0 j))
       (and (integerp (expt i j)) (<= 0 (expt i j))))) (:type-prescription :corollary (implies (and (rationalp i) (not (equal i 0)))
        (not (equal (expt i j) 0))))))

expt-with-product-exponenttheorem

(defthmd expt-with-product-exponent
  (implies (and (syntaxp (not (quotep i))) (case-split (integerp i)))
    (equal (expt 2 (* 2 i)) (* (expt 2 i) (expt 2 i))))
  :hints (("Goal" :in-theory (enable a15))))

natp-expttheorem

(defthmd natp-expt
  (implies (natp n)
    (and (integerp (expt 2 n)) (< 0 (expt 2 n))))
  :rule-classes (:type-prescription :rewrite))

expt-exceeds-another-by-more-than-1theorem

(defthm expt-exceeds-another-by-more-than-1
  (implies (and (<= 0 i) (<= 0 j) (integerp i) (integerp j))
    (implies (< (+ 1 i) j) (< (+ 1 (expt 2 i)) (expt 2 j))))
  :hints (("Goal" :in-theory (enable expt-split)
     :use (:instance expt-strong-monotone (n (+ 1 i)) (m j)))))

expt-exceeds-2theorem

(defthm expt-exceeds-2
  (implies (and (< i j) (<= 0 i) (<= 0 j) (integerp i) (integerp j))
    (<= (+ 1 (expt 2 i)) (expt 2 j)))
  :rule-classes (:rewrite :linear)
  :hints (("Goal" :use (:instance expt-strong-monotone (n i) (m j)))))

expt-with-i-non-integer-specialtheorem

(defthm expt-with-i-non-integer-special
  (implies (not (integerp i))
    (equal (expt 2 (+ -1 i))
      (if (acl2-numberp i)
        1
        1/2))))