Filtering...

expo-proofs

books/rtl/rel9/arithmetic/expo-proofs

Included Books

negative-syntaxp power2p unary-divide arith2 integerp fl expt e0-ordinal common-factor-defuns common-factor
other
(in-package "ACL2")
include-book
(include-book "negative-syntaxp")
include-book
(include-book "power2p")
include-book
(include-book "unary-divide")
include-book
(include-book "arith2")
include-book
(include-book "integerp")
local
(local (include-book "fl"))
local
(local (include-book "expt"))
local
(local (in-theory (enable expt-minus)))
flfunction
(defund fl
  (x)
  (declare (xargs :guard (real/rationalp x)))
  (floor x 1))
include-book
(include-book "../../../ordinals/e0-ordinal")
other
(set-well-founded-relation e0-ord-<)
expo-measurefunction
(defun expo-measure
  (x)
  (cond ((not (rationalp x)) 0)
    ((< x 0) '(2 . 0))
    ((< x 1) (cons 1 (fl (/ x))))
    (t (fl x))))
expofunction
(defund expo
  (x)
  (declare (xargs :guard t :measure (expo-measure x)))
  (cond ((or (not (rationalp x)) (equal x 0)) 0)
    ((< x 0) (expo (- x)))
    ((< x 1) (1- (expo (* 2 x))))
    ((< x 2) 0)
    (t (1+ (expo (/ x 2))))))
expo-integer-typetheorem
(defthm expo-integer-type
  (integerp (expo x))
  :rule-classes :type-prescription)
in-theory
(in-theory (disable (:type-prescription expo)))
expo-of-not-rationalptheorem
(defthm expo-of-not-rationalp
  (implies (not (rationalp x)) (equal (expo x) 0))
  :hints (("Goal" :in-theory (enable expo))))
expo-minustheorem
(defthmd expo-minus
  (equal (expo (* -1 x)) (expo x))
  :hints (("Goal" :in-theory (enable expo))))
expo-minus-erictheorem
(defthm expo-minus-eric
  (implies (syntaxp (negative-syntaxp x))
    (equal (expo x) (expo (* -1 x))))
  :hints (("Goal" :in-theory (enable expo-minus))))
other
(theory-invariant (not (and (or (active-runep '(:rewrite expo-minus))
        (active-runep '(:rewrite expo-minus-eric)))
      (active-runep '(:definition expo))))
  :key expo-minus-invariant)
local
(local (in-theory (disable expo-minus expo-minus-eric)))
expo-lower-boundtheorem
(defthm expo-lower-bound
  (implies (and (rationalp x) (not (equal x 0)))
    (<= (expt 2 (expo x)) (abs x)))
  :rule-classes :linear :hints (("goal" :in-theory (enable expo expt-split))))
expo-lower-postheorem
(defthm expo-lower-pos
  (implies (and (< 0 x) (rationalp x))
    (<= (expt 2 (expo x)) x))
  :rule-classes :linear)
local
(local (defthm expo-upper-bound-old
    (implies (and (rationalp x) (not (equal x 0)))
      (< (abs x) (expt 2 (1+ (expo x)))))
    :rule-classes :linear :hints (("Goal" :in-theory (set-difference-theories (enable expo expt-split) 'nil)
       :cases ((equal x 0))))))
expo-upper-boundtheorem
(defthm expo-upper-bound
  (implies (rationalp x) (< (abs x) (expt 2 (1+ (expo x)))))
  :rule-classes :linear :hints (("Goal" :use (expo-upper-bound-old))))
expo-upper-postheorem
(defthm expo-upper-pos
  (implies (rationalp x) (< x (expt 2 (1+ (expo x)))))
  :rule-classes :linear)
local
(local (defthm expo-unique-2
    (implies (and (rationalp x)
        (not (equal x 0))
        (integerp n)
        (> n (expo x)))
      (> (expt 2 n) (abs x)))
    :rule-classes nil
    :hints (("Goal" :in-theory (disable abs)
       :use ((:instance expt-weak-monotone (n (1+ (expo x))) (m n)))))))
local
(local (defthm expo-unique-1
    (implies (and (rationalp x)
        (not (equal x 0))
        (integerp n)
        (< n (expo x)))
      (<= (expt 2 (1+ n)) (abs x)))
    :rule-classes nil
    :hints (("Goal" :in-theory (disable abs)
       :use ((:instance expt-weak-monotone (n (1+ n)) (m (expo x))))))))
expo-uniquetheorem
(defthm expo-unique
  (implies (and (<= (expt 2 n) (abs x))
      (< (abs x) (expt 2 (1+ n)))
      (rationalp x)
      (integerp n))
    (equal n (expo x)))
  :rule-classes nil
  :hints (("Goal" :in-theory (disable abs)
     :use ((:instance expo-unique-1) (:instance expo-unique-2)))))
expo-monotonetheorem
(defthmd expo-monotone
  (implies (and (<= (abs x) (abs y))
      (case-split (rationalp x))
      (case-split (not (equal x 0)))
      (case-split (rationalp y)))
    (<= (expo x) (expo y)))
  :rule-classes :linear :hints (("Goal" :use ((:instance expo-unique-2 (n (expo x)) (x y))))))
expo-2**ntheorem
(defthm expo-2**n
  (implies (integerp n) (equal (expo (expt 2 n)) n))
  :hints (("Goal" :use ((:instance expo-unique (x (expt 2 n))) (:instance expt-strong-monotone (m (1+ n)))))))
expo-halftheorem
(defthm expo-half
  (implies (and (case-split (rationalp x))
      (case-split (not (equal x 0))))
    (equal (expo (* 1/2 x)) (+ -1 (expo x))))
  :hints (("Goal" :in-theory (enable expo expt))))
expo-doubletheorem
(defthm expo-double
  (implies (and (case-split (rationalp x))
      (case-split (not (equal x 0))))
    (equal (expo (* 2 x)) (+ 1 (expo x))))
  :hints (("Goal" :in-theory (set-difference-theories (enable expo expt) '(expo-minus)))))
other
(theory-invariant (incompatible (:rewrite expo-half) (:definition expo))
  :key expo-half-loops-with-defn-expo)
other
(theory-invariant (incompatible (:rewrite expo-double) (:definition expo))
  :key expo-double-loops-with-defn-expo)
expo-shifttheorem
(defthm expo-shift
  (implies (and (rationalp x) (not (equal x 0)) (integerp n))
    (equal (expo (* (expt 2 n) x)) (+ n (expo x))))
  :hints (("Goal" :in-theory (e/d (expt) nil))))
expo-shift-alttheorem
(defthm expo-shift-alt
  (implies (and (rationalp x) (not (equal x 0)) (integerp n))
    (equal (expo (* x (expt 2 n))) (+ n (expo x))))
  :hints (("Goal" :use expo-shift :in-theory (e/d nil (expo-shift)))))
include-book
(include-book "common-factor-defuns")
get-expt-factorsfunction
(defun get-expt-factors
  (factor-list)
  (declare (xargs :guard (true-listp factor-list)))
  (if (endp factor-list)
    nil
    (let* ((factor (car factor-list)))
      (if (and (consp factor)
          (or (and (equal (car factor) 'expt)
              (consp (cdr factor))
              (equal (cadr factor) ''2))
            (and (equal (car factor) 'unary-/)
              (consp (cdr factor))
              (consp (cadr factor))
              (equal (caadr factor) 'expt)
              (consp (cdadr factor))
              (equal (cadadr factor) ''2))))
        (cons factor (get-expt-factors (cdr factor-list)))
        (get-expt-factors (cdr factor-list))))))
find-common-expt-factors-to-cancelfunction
(defun find-common-expt-factors-to-cancel
  (expr)
  (declare (xargs :guard (and (pseudo-termp expr))))
  (get-expt-factors (remove-cancelling-factor-pairs (find-common-factors-in-sum-of-products expr))))
bind-k-to-common-expt-factorsfunction
(defund bind-k-to-common-expt-factors
  (expr)
  (declare (xargs :guard-hints (("Goal" :use (:instance remove-cancelling-factor-pairs-preserves-true-listp
           (l (my-intersection-equal (find-common-factors-in-sum-of-products lhs)
               (find-common-factors-in-sum-of-products rhs))))))
      :guard (and (pseudo-termp expr))))
  (let* ((common-factor-list (find-common-expt-factors-to-cancel expr)))
    (if (endp common-factor-list)
      nil
      (list (cons 'k
          (make-product-from-list-of-factors common-factor-list))))))
power2p-rewritetheorem
(defthmd power2p-rewrite
  (equal (power2p x) (equal x (expt 2 (expo x))))
  :hints (("Goal" :in-theory (set-difference-theories (enable power2p expt-split expt-between-one-and-two)
       '(power2p-shift)))))
in-theory
(in-theory (disable expo-2**n))
expo-expt2theorem
(defthm expo-expt2
  (equal (expo (expt 2 i))
    (if (integerp i)
      i
      0))
  :hints (("goal" :in-theory (enable expt))))
power2p-expt2-itheorem
(defthm power2p-expt2-i
  (power2p (expt 2 i))
  :hints (("Goal" :in-theory (enable expt power2p))))
power2p-shift-specialtheorem
(defthm power2p-shift-special
  (equal (power2p (* (expt 2 i) x)) (power2p x))
  :hints (("Goal" :in-theory (set-difference-theories (enable expt-split) 'nil))))
expo-expt2-inversetheorem
(defthm expo-expt2-inverse
  (equal (expo (/ (expt 2 i)))
    (if (integerp i)
      (- i)
      0))
  :hints (("goal" :in-theory (disable expo-expt2)
     :use (:instance expo-expt2 (i (- i))))))
expo-/-power2ptheorem
(defthmd expo-/-power2p
  (implies (power2p x) (equal (expo (/ x)) (- (expo x))))
  :hints (("Goal" :in-theory (set-difference-theories (enable power2p)
       '(power2p-shift expo-expt2 expo-expt2-inverse)))))
expo-/-power2p-alttheorem
(defthm expo-/-power2p-alt
  (implies (and (syntaxp (power2-syntaxp x)) (force (power2p x)))
    (equal (expo (/ x)) (- (expo x))))
  :hints (("Goal" :in-theory (e/d (expo-/-power2p) (expo-expt2 expo-expt2-inverse)))))
expo-shift-generaltheorem
(defthm expo-shift-general
  (implies (and (bind-free (bind-k-to-common-expt-factors x) (k))
      (syntaxp (not (equal k x)))
      (force (power2p k))
      (case-split (rationalp x))
      (case-split (not (equal x 0))))
    (equal (expo x) (+ (expo k) (expo (* (/ k) x)))))
  :hints (("goal" :in-theory (enable power2p-rewrite)
     :use (:instance expo-shift (n (- (expo k)))))))
other
(theory-invariant (incompatible (:rewrite expo-shift-general)
    (:rewrite expt-inverse))
  :key expt-shift-general-can-loop-with-expt-inverse)
expo>=theorem
(defthm expo>=
  (implies (and (<= (expt 2 n) x) (rationalp x) (integerp n))
    (<= n (expo x)))
  :otf-flg t
  :rule-classes :linear :hints (("goal" :use ((:instance expo-monotone (x (expt 2 n)) (y x))))))
expo<=theorem
(defthm expo<=
  (implies (and (< x (* 2 (expt 2 n)))
      (< 0 x)
      (rationalp x)
      (integerp n))
    (<= (expo x) n))
  :rule-classes :linear :hints (("goal" :in-theory (enable expt-split)
     :use (expo-lower-bound (:instance expt-weak-monotone (n (1+ n)) (m (expo x)))))))
in-theory
(in-theory (disable expo<= expo>=))
local
(local (in-theory (enable expo-minus)))
expo-of-integerencapsulate
(encapsulate nil
  (local (defthm expo-of-non-negative-integerp
      (implies (and (integerp x) (>= x 0)) (>= (expo x) 0))
      :hints (("Goal" :use ((:instance expo>= (x x) (n 0)))))))
  (defthm expo-of-integer
    (implies (integerp x) (<= 0 (expo x)))
    :hints (("Goal" :in-theory (disable expo-of-non-negative-integerp)
       :use ((:instance expo-of-non-negative-integerp (x x)) (:instance expo-of-non-negative-integerp (x (- x))))))
    :rule-classes (:rewrite)))
expo-of-integer-typetheorem
(defthm expo-of-integer-type
  (implies (integerp x)
    (and (integerp (expo x)) (<= 0 (expo x))))
  :rule-classes ((:type-prescription :typed-term (expo x))))
local
(local (in-theory (disable expo-minus)))
local
(local (include-book "common-factor"))
local
(local (defthm expo-unique-1
    (implies (and (rationalp x)
        (not (equal x 0))
        (integerp n)
        (< n (expo x)))
      (<= (expt 2 (1+ n)) (abs x)))
    :rule-classes nil
    :hints (("Goal" :in-theory (disable expo abs)
       :use ((:instance expt-weak-monotone (n (1+ n)) (m (expo x))))))))
local
(local (defthm expo-unique-2-alt
    (implies (and (rationalp x) (integerp n) (> n (expo x)))
      (> (expt 2 n) (abs x)))
    :rule-classes nil
    :hints (("Goal" :in-theory (disable expo abs)
       :use ((:instance expt-weak-monotone (n (1+ (expo x))) (m n)))))))
expo-unique-erictheorem
(defthmd expo-unique-eric
  (implies (and (<= (expt 2 n) (abs x))
      (< (abs x) (expt 2 (1+ n)))
      (rationalp x)
      (integerp n))
    (equal (expo x) n))
  :hints (("goal" :in-theory (disable expo abs)
     :use ((:instance expo-unique-1) (:instance expo-unique-2)))))
expo-unique-eric-2theorem
(defthm expo-unique-eric-2
  (implies (and (<= (expt 2 n) (abs x))
      (< (abs x) (expt 2 (1+ n)))
      (rationalp x)
      (integerp n))
    (equal (equal (expo x) n) t))
  :hints (("goal" :in-theory (disable expo abs)
     :use ((:instance expo-unique)))))
expo-equality-reduce-to-boundstheorem
(defthm expo-equality-reduce-to-bounds
  (implies (and (case-split (rationalp x)) (case-split (integerp n)))
    (equal (equal (expo x) n)
      (if (equal 0 x)
        (equal 0 n)
        (and (<= (expt 2 n) (abs x)) (< (abs x) (expt 2 (1+ n)))))))
  :hints (("goal" :in-theory (disable expo abs) :cases ((equal x 0)))))
in-theory
(in-theory (disable expo-equality-reduce-to-bounds))
expo-shift-constanttheorem
(defthm expo-shift-constant
  (implies (and (syntaxp (quotep k))
      (equal k (expt 2 (expo k)))
      (rationalp x)
      (not (equal x 0)))
    (equal (expo (* k x)) (+ (expo k) (expo x))))
  :hints (("Goal" :in-theory (disable)
     :use (:instance expo-shift (n (expo k))))))
expo-comparison-rewrite-to-boundtheorem
(defthm expo-comparison-rewrite-to-bound
  (implies (and (syntaxp (not (power2-syntaxp x)))
      (case-split (not (equal 0 x)))
      (integerp k)
      (case-split (rationalp x)))
    (equal (< (expo x) k) (< (abs x) (expt 2 k))))
  :otf-flg t
  :hints (("Goal" :use ((:instance expo-monotone (x (expt 2 k)) (y x)) (:instance expo-monotone (y (expt 2 k)) (x x))))))
expo-comparison-rewrite-to-bound-2theorem
(defthm expo-comparison-rewrite-to-bound-2
  (implies (and (syntaxp (not (power2-syntaxp x)))
      (case-split (not (equal 0 x)))
      (integerp k)
      (case-split (rationalp x)))
    (equal (< k (expo x)) (<= (expt 2 (+ k 1)) (abs x))))
  :otf-flg t
  :hints (("Goal" :in-theory (disable expo-comparison-rewrite-to-bound)
     :use ((:instance expo-monotone (x (expt 2 (+ 1 k))) (y x)) (:instance expo-monotone (y (expt 2 (+ 1 k))) (x x))))))
expo-bound-erictheorem
(defthm expo-bound-eric
  (implies (case-split (rationalp x))
    (and (equal (< (* 2 (expt 2 (expo x))) x) nil)
      (equal (< x (* 2 (expt 2 (expo x)))) t)
      (equal (< (expt 2 (+ 1 (expo x))) x) nil)
      (equal (< x (expt 2 (+ 1 (expo x)))) t)))
  :hints (("goal" :in-theory (set-difference-theories (enable expt-split) 'nil)
     :use expo-upper-bound)))
expo-/-notpower2ptheorem
(defthm expo-/-notpower2p
  (implies (and (not (power2p x))
      (case-split (not (equal x 0)))
      (<= 0 x)
      (case-split (rationalp x)))
    (equal (expo (/ x)) (+ -1 (- (expo x)))))
  :hints (("Goal" :in-theory (set-difference-theories (enable power2p expt-split expo-equality-reduce-to-bounds)
       '(power2p-shift expo-shift-constant)))))
in-theory
(in-theory (disable expo-/-notpower2p))
in-theory
(in-theory (disable power2p-shift-special))
expt-comparetheorem
(defthm expt-compare
  (implies (and (syntaxp (and (power2-syntaxp lhs) (power2-syntaxp rhs)))
      (case-split (power2p lhs))
      (case-split (power2p rhs)))
    (equal (< lhs rhs) (< (expo lhs) (expo rhs))))
  :hints (("goal" :in-theory (set-difference-theories (enable power2p-rewrite)
       '(expo-comparison-rewrite-to-bound-2 power2p-shift))
     :use (:instance expt-strong-monotone
       (m (expo lhs))
       (n (expo rhs)))))
  :otf-flg t)
expt-comparetheorem
(defthm expt-compare
  (implies (and (syntaxp (and (power2-syntaxp lhs) (power2-syntaxp rhs)))
      (case-split (power2p lhs))
      (case-split (power2p rhs)))
    (equal (< lhs rhs) (< (expo lhs) (expo rhs))))
  :hints (("goal" :in-theory (set-difference-theories (enable power2p-rewrite expt)
       '(power2p-shift))
     :use (:instance expt-strong-monotone
       (m (expo lhs))
       (n (expo rhs)))))
  :otf-flg t)
expt-compare-equaltheorem
(defthm expt-compare-equal
  (implies (and (syntaxp (and (power2-syntaxp lhs) (power2-syntaxp rhs)))
      (case-split (power2p lhs))
      (case-split (power2p rhs)))
    (equal (equal lhs rhs) (equal (expo lhs) (expo rhs))))
  :hints (("Goal" :in-theory (set-difference-theories (enable power2p-rewrite expt)
       '(power2p-shift)))))
power2-integertheorem
(defthm power2-integer
  (implies (and (syntaxp (power2-syntaxp x)) (force (power2p x)))
    (equal (integerp x) (<= 0 (expo x))))
  :hints (("Goal" :use (:instance expt2-integer (i (expo x)))
     :in-theory (set-difference-theories (enable power2p-rewrite expt)
       '(power2p-shift expt2-integer)))))
expo-shift-16theorem
(defthm expo-shift-16
  (implies (and (case-split (integerp n))
      (case-split (rationalp x))
      (case-split (not (equal x 0))))
    (equal (expo (* (/ (expt 2 n)) x)) (+ (- n) (expo x)))))
expo-lower-bound-2theorem
(defthm expo-lower-bound-2
  (implies (and (case-split (rationalp x))
      (case-split (<= 0 x))
      (case-split (not (equal x 0))))
    (<= (expt 2 (expo x)) x))
  :rule-classes :linear)
expo-upper-bound-tighttheorem
(defthmd expo-upper-bound-tight
  (implies (integerp x)
    (<= (abs x) (+ -1 (expt 2 (1+ (expo x))))))
  :hints (("Goal" :use (expo-upper-bound)))
  :rule-classes :linear)
expo-x+a*2**ktheorem
(defthm expo-x+a*2**k
  (implies (and (< (expo x) k)
      (< 0 a)
      (integerp a)
      (case-split (<= 0 x))
      (case-split (integerp k))
      (case-split (rationalp x)))
    (equal (expo (+ x (* a (expt 2 k))))
      (expo (* a (expt 2 k)))))
  :hints (("goal" :in-theory (e/d (expt-split) nil)
     :use ((:instance expo-lower-bound (x (* a (expt 2 k)))) (:instance expo-upper-bound-tight (x a))
       (:instance expo-unique
         (x (+ x (* a (expt 2 k))))
         (n (expo (* a (expt 2 k))))))))
  :otf-flg t)
expo-x+2**ktheorem
(defthm expo-x+2**k
  (implies (and (< (expo x) k)
      (<= 0 x)
      (case-split (integerp k))
      (case-split (rationalp x)))
    (equal (expo (+ x (expt 2 k))) k))
  :hints (("Goal" :use (:instance expo-x+a*2**k (a 1)))))
local
(local (defthmd between-0-and-1-means-not-integerp
    (implies (and (< 0 x) (< x 1)) (not (integerp x)))))
expo-times-2-not-a-factortheorem
(defthm expo-times-2-not-a-factor
  (implies (rationalp x)
    (equal (integerp (* 1/2 x (/ (expt 2 (expo x)))))
      (equal 0 x)))
  :hints (("Goal" :in-theory (enable expt-minus expt-split)
     :use (expo-lower-bound expo-upper-bound
       (:instance between-0-and-1-means-not-integerp
         (x (* 1/2 (abs x) (expt 2 (* -1 (expo x))))))))))
local
(local (defthmd between-1-and-2-means-not-integerp
    (implies (and (< 1 x) (< x 2)) (not (integerp x)))))
local
(local (defthm expo-a-factor-means-power2-helper
    (implies (and (<= 0 x) (rationalp x))
      (equal (integerp (* x (/ (expt 2 (expo x)))))
        (or (equal 0 x) (power2p (abs x)))))
    :otf-flg t
    :hints (("Goal" :in-theory (e/d (expt-minus expt-split power2p-rewrite)
         (expo-bound-eric))
       :use (expo-lower-bound expo-upper-bound
         (:instance between-1-and-2-means-not-integerp
           (x (* x (/ (expt 2 (expo x)))))))))))
expo-a-factor-means-power2theorem
(defthm expo-a-factor-means-power2
  (implies (acl2-numberp x)
    (equal (integerp (* x (/ (expt 2 (expo x)))))
      (or (equal 0 x) (power2p (abs x)))))
  :hints (("Goal" :in-theory (enable expo-minus-eric)
     :use ((:instance expo-a-factor-means-power2-helper (x x)) (:instance expo-a-factor-means-power2-helper (x (- x)))))))