basic

other

(in-package "ACL2")

local

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

local

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

include-book

(include-book "building-blocks")

default-expt-1theorem

(defthm default-expt-1
  (implies (not (acl2-numberp x))
    (equal (expt x n)
      (if (zip n)
        1
        0))))

default-expt-2theorem

(defthm default-expt-2
  (implies (case-split (not (integerp n)))
    (equal (expt x n) 1)))

|(+ y x)|theorem

(defthm |(+ y x)| (equal (+ y x) (+ x y)))

|(+ y (+ x z))|theorem

(defthm |(+ y (+ x z))| (equal (+ y (+ x z)) (+ x (+ y z))))

|(+ (+ x y) z)|theorem

(defthm |(+ (+ x y) z)| (equal (+ (+ x y) z) (+ x (+ y z))))

|(+ 0 x)|theorem

(defthm |(+ 0 x)|
  (implies (acl2-numberp x) (equal (+ 0 x) x)))

|(- (- x))|theorem

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

|(- (+ x y))|theorem

(defthm |(- (+ x y))| (equal (- (+ x y)) (+ (- x) (- y))))

|(* y x)|theorem

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

|(* y (* x z))|theorem

(defthm |(* y (* x z))| (equal (* y (* x z)) (* x (* y z))))

|(* (* x y) z)|theorem

(defthm |(* (* x y) z)| (equal (* (* x y) z) (* x (* y z))))

|(* 1 x)|theorem

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

|(* 0 x)|theorem

(defthm |(* 0 x)| (equal (* 0 x) 0))

|(* -1 x)|theorem

(defthm |(* -1 x)| (equal (* -1 x) (- x)))

|(/ (/ x))|theorem

(defthm |(/ (/ x))|
  (implies (acl2-numberp x) (equal (/ (/ x)) x)))

|(/ (* x y))|theorem

(defthm |(/ (* x y))| (equal (/ (* x y)) (* (/ x) (/ y))))

|(* x (+ y z))|theorem

(defthm |(* x (+ y z))|
  (equal (* x (+ y z)) (+ (* x y) (* x z))))

local

(local (in-theory (disable distributivity)))

|(* (+ x y) z)|theorem

(defthm |(* (+ x y) z)|
  (equal (* (+ x y) z) (+ (* x z) (* y z))))

|(* a (/ a))|theorem

(defthm |(* a (/ a))|
  (implies (acl2-numberp x)
    (equal (* x (/ x))
      (if (equal x 0)
        0
        1))))

|(* a (/ a) b)|theorem

(defthm |(* a (/ a) b)|
  (implies (and (acl2-numberp x) (acl2-numberp y))
    (equal (* x (/ x) y)
      (if (equal x 0)
        0
        y))))

|(* x (- y))|theorem

(defthm |(* x (- y))|
  (implies (syntaxp (not (quotep y)))
    (equal (* x (- y)) (- (* x y)))))

|(* (- x) y)|theorem

(defthm |(* (- x) y)|
  (implies (syntaxp (not (quotep x)))
    (equal (* (- x) y) (- (* x y)))))

|(- (* c x))|theorem

(defthm |(- (* c x))|
  (implies (syntaxp (quotep c))
    (equal (- (* c x)) (* (- c) x))))

|(/ (- x))|theorem

(defthm |(/ (- x))|
  (implies (syntaxp (not (quotep x)))
    (equal (/ (- x)) (- (/ x)))))

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-non-0-basetheorem

(defthm expt-type-prescription-non-0-base
  (implies (and (acl2-numberp x) (not (equal x 0)))
    (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)) (< 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)) (<= 0 (expt x n)))
  :rule-classes (:type-prescription :generalize))

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

(defthm |(equal (expt x n) 0)|
  (implies (and (acl2-numberp x) (integerp n))
    (equal (equal (expt x n) 0)
      (and (equal x 0) (not (equal n 0))))))

|(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 x c)|theorem

(defthm |(expt x c)|
  (implies (and (syntaxp (quotep c)) (integerp c) (not (equal c 0)))
    (equal (expt x c)
      (cond ((< c 0) (* (/ x) (expt x (+ c 1))))
        (t (* x (expt x (- c 1)))))))
  :hints (("Goal" :in-theory (disable expt))))

|(expt x (- n))|theorem

(defthm |(expt x (- n))|
  (implies (syntaxp (negative-addends-p n))
    (equal (expt x n) (/ (expt x (- 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 (equal (numerator x) 1)))
    (equal (expt x n) (/ (expt (/ x) n)))))

|(expt (- x) n)|theorem

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

power-of-2-helperfunction

(defun power-of-2-helper
  (x)
  (declare (xargs :mode :program))
  (cond ((not (integerp x)) 0)
    ((<= x 2) 1)
    (t (1+ (power-of-2-helper (/ x 2))))))

power-of-2function

(defun power-of-2
  (x)
  (declare (xargs :mode :program))
  (list (cons 'c (kwote (power-of-2-helper (unquote x))))))

|(expt 2^i n)|theorem

(defthm |(expt 2^i n)|
  (implies (and (integerp n)
      (syntaxp (quotep x))
      (syntaxp (not (equal x ''1)))
      (syntaxp (not (equal x ''2)))
      (bind-free (power-of-2 x) (c))
      (integerp c)
      (equal (expt 2 c) x))
    (equal (expt x n) (expt 2 (* c n)))))

|(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 (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 x|theorem

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

|(equal (/ x) 0)|theorem

(defthm |(equal (/ x) 0)|
  (implies (acl2-numberp x)
    (equal (equal (/ x) 0) (equal x 0))))

|(equal (- x) 0)|theorem

(defthm |(equal (- x) 0)|
  (implies (and (syntaxp (negative-addends-p x)) (acl2-numberp x))
    (equal (equal x 0) (equal (- x) 0))))

|(equal (/ x) (/ y))|theorem

(defthm |(equal (/ x) (/ y))|
  (implies (and (acl2-numberp x) (acl2-numberp y))
    (equal (equal (/ x) (/ y)) (equal x y))))

|(equal (- x) (- y))|theorem

(defthm |(equal (- x) (- y))|
  (implies (and (syntaxp (negative-addends-p x))
      (syntaxp (negative-addends-p y))
      (acl2-numberp x)
      (acl2-numberp y))
    (equal (equal x y) (equal (- x) (- y)))))

|(< (/ x) 0)|theorem

(defthm |(< (/ x) 0)|
  (implies (rationalp x) (equal (< (/ x) 0) (< x 0))))

|(< 0 (/ x))|theorem

(defthm |(< 0 (/ x))|
  (implies (rationalp x) (equal (< 0 (/ x)) (< 0 x))))

|(< (- x) 0)|theorem

(defthm |(< (- x) 0)|
  (implies (syntaxp (negative-addends-p x))
    (equal (< x 0) (< 0 (- x)))))

|(< 0 (- x))|theorem

(defthm |(< 0 (- x))|
  (implies (syntaxp (negative-addends-p x))
    (equal (< 0 x) (< (- x) 0))))

|(< (- x) (- y))|theorem

(defthm |(< (- x) (- y))|
  (implies (and (syntaxp (negative-addends-p x))
      (syntaxp (negative-addends-p y)))
    (equal (< x y) (< (- y) (- x)))))

|(equal (+ c x) d)|theorem

(defthm |(equal (+ c x) d)|
  (implies (and (syntaxp (quotep c))
      (acl2-numberp c)
      (acl2-numberp x)
      (syntaxp (quotep d))
      (acl2-numberp d)
      (syntaxp (not (equal (fn-symb x) 'binary-+))))
    (equal (equal (+ c x) d) (equal x (- d c)))))

|(equal (+ c x y) d)|theorem

(defthm |(equal (+ c x y) d)|
  (implies (and (syntaxp (quotep c))
      (acl2-numberp c)
      (acl2-numberp x)
      (syntaxp (quotep d))
      (syntaxp (not (equal (unquote d) 0)))
      (acl2-numberp d))
    (equal (equal (+ c x y) d) (equal (+ x y) (- d c)))))

|(equal (+ c x) (+ d y))|theorem

(defthm |(equal (+ c x) (+ d y))|
  (implies (and (syntaxp (quotep c))
      (acl2-numberp c)
      (acl2-numberp x)
      (syntaxp (quotep d))
      (acl2-numberp d)
      (acl2-numberp y)
      (< c d))
    (equal (equal (+ c x) (+ d y)) (equal x (+ (- d c) y)))))

|(equal (+ d x) (+ c y))|theorem

(defthm |(equal (+ d x) (+ c y))|
  (implies (and (syntaxp (quotep c))
      (acl2-numberp c)
      (acl2-numberp x)
      (syntaxp (quotep d))
      (acl2-numberp d)
      (acl2-numberp y)
      (< c d))
    (equal (equal (+ d x) (+ c y)) (equal (+ (- d c) x) y))))

local

(local (defthm equal-to-iff
    (equal (equal (< a b) (< x y)) (iff (< a b) (< x y)))))

|(< (+ c x) d)|theorem

(defthm |(< (+ c x) d)|
  (implies (and (syntaxp (quotep c))
      (acl2-numberp c)
      (acl2-numberp x)
      (syntaxp (quotep d))
      (acl2-numberp d)
      (syntaxp (not (equal (fn-symb x) 'binary-+))))
    (equal (< (+ c x) d) (< x (- d c)))))

|(< (+ c x y) d)|theorem

(defthm |(< (+ c x y) d)|
  (implies (and (syntaxp (quotep c))
      (acl2-numberp c)
      (acl2-numberp x)
      (syntaxp (quotep d))
      (syntaxp (not (equal (unquote d) 0)))
      (acl2-numberp d))
    (equal (< (+ c x y) d) (< (+ x y) (- d c)))))

|(< (+ c x) (+ d y))|theorem

(defthm |(< (+ c x) (+ d y))|
  (implies (and (syntaxp (quotep c))
      (acl2-numberp c)
      (acl2-numberp x)
      (syntaxp (quotep d))
      (acl2-numberp d)
      (acl2-numberp y)
      (< c d))
    (equal (< (+ c x) (+ d y)) (< x (+ (- d c) y)))))

|(< (+ d x) (+ c y))|theorem

(defthm |(< (+ d x) (+ c y))|
  (implies (and (syntaxp (quotep c))
      (acl2-numberp c)
      (acl2-numberp x)
      (syntaxp (quotep d))
      (acl2-numberp d)
      (acl2-numberp y)
      (< c d))
    (equal (< (+ d x) (+ c y)) (< (+ (- d c) x) y))))

|(< d (+ c x))|theorem

(defthm |(< d (+ c x))|
  (implies (and (syntaxp (quotep c))
      (acl2-numberp c)
      (acl2-numberp x)
      (syntaxp (quotep d))
      (acl2-numberp d)
      (syntaxp (not (equal (fn-symb x) 'binary-+))))
    (equal (< d (+ c x)) (< (- d c) x))))

|(< d (+ c x y))|theorem

(defthm |(< d (+ c x y))|
  (implies (and (syntaxp (quotep c))
      (acl2-numberp c)
      (acl2-numberp x)
      (syntaxp (quotep d))
      (syntaxp (not (equal (unquote d) 0)))
      (acl2-numberp d))
    (equal (< d (+ c x y)) (< (- d c) (+ x y)))))

|(equal (* x y) 0)|theorem

(defthm |(equal (* x y) 0)|
  (implies (and (rationalp x) (rationalp y))
    (equal (equal (* x y) 0) (or (equal x 0) (equal y 0)))))

|(< (* x y) 0)|theorem

(defthm |(< (* x y) 0)|
  (implies (and (syntaxp (rewriting-goal-literal x mfc state))
      (rationalp x)
      (rationalp y))
    (equal (< (* x y) 0)
      (cond ((equal x 0) nil)
        ((equal y 0) nil)
        ((< x 0) (< 0 y))
        ((< 0 x) (< y 0))))))

|(< 0 (* x y))|theorem

(defthm |(< 0 (* x y))|
  (implies (and (syntaxp (rewriting-goal-literal x mfc state))
      (rationalp x)
      (rationalp y))
    (equal (< 0 (* x y))
      (cond ((equal x 0) nil)
        ((equal y 0) nil)
        ((< x 0) (< y 0))
        ((< 0 x) (< 0 y))))))

expt-x->-xtheorem

(defthm expt-x->-x
  (implies (and (< 1 x) (< 1 n) (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) (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)
      (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)
      (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)
      (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)
      (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) (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) (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) (rationalp x) (integerp n))
    (< (expt x n) 1))
  :rule-classes :linear)

expt-<-1-twotheorem

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

|(+ (if a b c) x)|theorem

(defthm |(+ (if a b c) x)|
  (equal (+ (if a
        b
        c)
      x)
    (if a
      (+ b x)
      (+ c x))))

|(+ x (if a b c))|theorem

(defthm |(+ x (if a b c))|
  (equal (+ x
      (if a
        b
        c))
    (if a
      (+ x b)
      (+ x c))))

|(- (if a b c))|theorem

(defthm |(- (if a b c))|
  (equal (- (if a
        b
        c))
    (if a
      (- b)
      (- c))))

|(* (if a b c) x)|theorem

(defthm |(* (if a b c) x)|
  (equal (* (if a
        b
        c)
      x)
    (if a
      (* b x)
      (* c x))))

|(* x (if a b c))|theorem

(defthm |(* x (if a b c))|
  (equal (* x
      (if a
        b
        c))
    (if a
      (* x b)
      (* x c))))

|(/ (if a b c))|theorem

(defthm |(/ (if a b c))|
  (equal (/ (if a
        b
        c))
    (if a
      (/ b)
      (/ c))))

|(expt (if a b c) x)|theorem

(defthm |(expt (if a b c) x)|
  (equal (expt (if a
        b
        c)
      x)
    (if a
      (expt b x)
      (expt c x))))

|(expt x (if a b c))|theorem

(defthm |(expt x (if a b c))|
  (equal (expt x
      (if a
        b
        c))
    (if a
      (expt x b)
      (expt x c))))

|(equal x (if a b c))|theorem

(defthm |(equal x (if a b c))|
  (equal (equal x
      (if a
        b
        c))
    (if a
      (equal x b)
      (equal x c))))

|(equal (if a b c) x)|theorem

(defthm |(equal (if a b c) x)|
  (equal (equal (if a
        b
        c)
      x)
    (if a
      (equal b x)
      (equal c x))))

|(< x (if a b c))|theorem

(defthm |(< x (if a b c))|
  (equal (< x
      (if a
        b
        c))
    (if a
      (< x b)
      (< x c))))

|(< (if a b c) x)|theorem

(defthm |(< (if a b c) x)|
  (equal (< (if a
        b
        c)
      x)
    (if a
      (< b x)
      (< c x))))

Included Books