equalities

(in-package "ACL2")

(defsection fc
  :parents (arithmetic-1)
  :short "Identity macro — does nothing, you can safely ignore this."
  :long "<p>@(call fc) just expands to @('x').  This macro is a historic
artifact that was originally used in the @('arithmetic') library as a way to
experiment with using @(see force).</p>

@(def fc)"
  (defmacro fc (x) x))

(defsection basic-sum-normalization
  :parents (arithmetic-1)
  :short "Trivial normalization and cancellation rules for sums."
  (defthm commutativity-2-of-+
    (equal (+ x (+ y z)) (+ y (+ x z))))
  (defthm functional-self-inversion-of-minus
    (equal (- (- x)) (fix x)))
  (defthm distributivity-of-minus-over-+
    (equal (- (+ x y)) (+ (- x) (- y))))
  (defthm minus-cancellation-on-right
    (equal (+ x y (- x)) (fix y)))
  (defthm minus-cancellation-on-left
    (equal (+ x (- x) y) (fix y)))
  (defthm right-cancellation-for-+
    (equal (equal (+ x z) (+ y z)) (equal (fix x) (fix y))))
  (defthm left-cancellation-for-+
    (equal (equal (+ x y) (+ x z)) (equal (fix y) (fix z))))
  (defthm equal-minus-0
    (equal (equal 0 (- x)) (equal 0 (fix x))))
  (defthm inverse-of-+-as=0
    (equal (equal (- a b) 0) (equal (fix a) (fix b))))
  (defthm equal-minus-minus
    (equal (equal (- a) (- b)) (equal (fix a) (fix b))))
  (defthm fold-consts-in-+
    (implies (and (syntaxp (quotep x)) (syntaxp (quotep y)))
      (equal (+ x (+ y z)) (+ (+ x y) z)))))

(defsection basic-product-normalization
  :parents (arithmetic-1)
  :short "Trivial normalization and cancellation rules for products."
  (defthm commutativity-2-of-*
    (equal (* x (* y z)) (* y (* x z)))
    :hints (("Goal" :use (:functional-instance commutativity-2-of-op
         (equiv equal)
         (pred (lambda (x) t))
         (op binary-*)))))
  (defthm functional-self-inversion-of-/
    (equal (/ (/ x)) (fix x))
    :hints (("Goal" :use (:functional-instance involution-of-inv
         (equiv equal)
         (pred (lambda (x) (and (acl2-numberp x) (not (equal x 0)))))
         (op binary-*)
         (id (lambda nil 1))
         (inv unary-/)))))
  (defthm distributivity-of-/-over-*
    (equal (/ (* x y)) (* (/ x) (/ y)))
    :hints (("Goal" :use (:functional-instance distributivity-of-inv-over-op
         (equiv equal)
         (pred (lambda (x) (and (acl2-numberp x) (not (equal x 0)))))
         (op binary-*)
         (id (lambda nil 1))
         (inv unary-/)))))
  (defthm /-cancellation-on-right
    (implies (and (fc (acl2-numberp x)) (fc (not (equal x 0))))
      (equal (* x y (/ x)) (fix y)))
    :hints (("Goal" :use (:functional-instance inv-cancellation-on-right
         (equiv equal)
         (pred (lambda (x) (and (acl2-numberp x) (not (equal x 0)))))
         (op binary-*)
         (id (lambda nil 1))
         (inv unary-/)))))
  (defthm /-cancellation-on-left
    (implies (and (fc (acl2-numberp x)) (fc (not (equal 0 x))))
      (equal (* x (/ x) y) (fix y)))
    :hints (("Goal" :use /-cancellation-on-right)))
  (local (defthm right-cancellation-for-*-lemma
      (implies (and (equal (* x z) (* y z))
          (acl2-numberp z)
          (not (equal 0 z))
          (acl2-numberp x)
          (acl2-numberp y))
        (equal (equal x y) t))
      :hints (("Goal" :use (:functional-instance right-cancellation-for-op
           (equiv equal)
           (pred (lambda (x) (and (acl2-numberp x) (not (equal x 0)))))
           (op binary-*)
           (id (lambda nil 1))
           (inv unary-/))))))
  (defthm right-cancellation-for-*
    (equal (equal (* x z) (* y z))
      (or (equal 0 (fix z)) (equal (fix x) (fix y)))))
  (defthm left-cancellation-for-*
    (equal (equal (* z x) (* z y))
      (or (equal 0 (fix z)) (equal (fix x) (fix y)))))
  (defthm zero-is-only-zero-divisor
    (equal (equal (* x y) 0)
      (or (equal (fix x) 0) (equal (fix y) 0))))
  (defthm equal-*-x-y-x
    (equal (equal (* x y) x)
      (or (equal x 0) (and (equal y 1) (acl2-numberp x))))
    :hints (("Goal" :use ((:instance right-cancellation-for-* (z x) (x y) (y 1))))))
  (defthm equal-*-x-y-y
    (equal (equal (* x y) y)
      (or (equal y 0) (and (equal x 1) (acl2-numberp y))))
    :hints (("Goal" :use ((:instance right-cancellation-for-* (z y) (x x) (y 1))))))
  (local (defthm equal-/-lemma
      (implies (and (acl2-numberp x) (acl2-numberp y) (equal (* x y) 1))
        (equal y (/ x)))
      :rule-classes nil
      :hints (("Goal" :use (:functional-instance uniqueness-of-op-inverses
           (equiv equal)
           (pred (lambda (x) (and (acl2-numberp x) (not (equal x 0)))))
           (op binary-*)
           (id (lambda nil 1))
           (inv unary-/))))))
  (defthm equal-/
    (implies (and (fc (acl2-numberp x)) (fc (not (equal 0 x))))
      (equal (equal (/ x) y) (equal 1 (* x y))))
    :hints (("Goal" :use equal-/-lemma)))
  (defthm numerator-nonzero-forward
    (implies (not (equal (numerator r) 0))
      (and (not (equal r 0)) (acl2-numberp r)))
    :rule-classes ((:forward-chaining :trigger-terms ((numerator r)))))
  (encapsulate nil
    (local (defthm uniqueness-of-*-inverses-lemma
        (equal (equal (* x y) 1)
          (and (not (equal x 0)) (acl2-numberp x) (equal y (/ x))))))
    (defthm uniqueness-of-*-inverses
      (equal (equal (* x y) 1)
        (and (not (equal (fix x) 0)) (equal y (/ x))))
      :hints (("Goal" :in-theory (disable equal-/)))))
  (in-theory (disable uniqueness-of-*-inverses))
  (theory-invariant (not (and (active-runep '(:rewrite uniqueness-of-*-inverses))
        (active-runep '(:rewrite equal-/)))))
  (encapsulate nil
    (local (defthm equal-/-/-lemma
        (implies (and (fc (acl2-numberp a))
            (fc (acl2-numberp b))
            (fc (not (equal a 0)))
            (fc (not (equal b 0))))
          (equal (equal (/ a) (/ b)) (equal a b)))
        :hints (("Goal" :use ((:instance (:theorem (implies (and (fc (acl2-numberp a))
                    (fc (acl2-numberp b))
                    (fc (not (equal a 0)))
                    (fc (not (equal b 0))))
                  (implies (equal a b) (equal (/ a) (/ b)))))
              (a (/ a))
              (b (/ b))))))
        :rule-classes nil))
    (defthm equal-/-/
      (equal (equal (/ a) (/ b)) (equal (fix a) (fix b)))
      :hints (("Goal" :use equal-/-/-lemma :in-theory (disable equal-/)))))
  (defthm equal-*-/-1
    (implies (and (acl2-numberp x) (not (equal x 0)))
      (equal (equal (* (/ x) y) z)
        (and (acl2-numberp z) (equal (fix y) (* x z))))))
  (defthm equal-*-/-2
    (implies (and (acl2-numberp x) (not (equal x 0)))
      (equal (equal (* y (/ x)) z)
        (and (acl2-numberp z) (equal (fix y) (* z x))))))
  (defthm fold-consts-in-*
    (implies (and (syntaxp (quotep x)) (syntaxp (quotep y)))
      (equal (* x (* y z)) (* (* x y) z))))
  (defthm times-zero (equal (* 0 x) 0)))

(defsection basic-products-with-negations
  :parents (arithmetic-1)
  :short "Rules for normalizing products with negative factors, and reciprocals
of negations."
  (local (defthm functional-commutativity-of-minus-*-right-lemma
      (implies (and (fc (acl2-numberp x)) (fc (acl2-numberp y)))
        (equal (* x (- y)) (- (* x y))))
      :hints (("Goal" :use (:functional-instance functional-commutativity-of-minus-times-right
           (equiv equal)
           (pred acl2-numberp)
           (plus binary-+)
           (times binary-*)
           (zero (lambda nil 0))
           (minus unary--))))
      :rule-classes nil))
  (defthm functional-commutativity-of-minus-*-right
    (equal (* x (- y)) (- (* x y)))
    :hints (("Goal" :use functional-commutativity-of-minus-*-right-lemma)))
  (defthm functional-commutativity-of-minus-*-left
    (equal (* (- x) y) (- (* x y))))
  (defthm reciprocal-minus
    (equal (/ (- x)) (- (/ x)))
    :hints (("Goal" :cases ((and (fc (acl2-numberp x)) (fc (not (equal x 0)))))))))

(defsection basic-rational-identities
  :parents (arithmetic-1 numerator denominator)
  :short "Basic cancellation rules for @('numerator') and @('denominator') terms."
  :long "<p>See also @(see more-rational-identities) for additional reductions
involving @('numerator') and @('denominator') terms.</p>"
  (local (defthm numerator-integerp-lemma-1
      (implies (rationalp x)
        (equal (* (* (numerator x) (/ (denominator x))) (denominator x))
          (numerator x)))
      :rule-classes nil
      :hints (("Goal" :in-theory (disable rational-implies2)))))
  (local (defthm numerator-integerp-lemma
      (implies (and (rationalp x)
          (equal (* (numerator x) (/ (denominator x))) x))
        (equal (numerator x) (* x (denominator x))))
      :rule-classes nil
      :hints (("Goal" :use (numerator-integerp-lemma-1)
         :in-theory (disable rational-implies2)))))
  (defthm numerator-when-integerp
    (implies (integerp x) (equal (numerator x) x))
    :hints (("Goal" :in-theory (disable rational-implies2)
       :use ((:instance lowest-terms (r x) (q 1) (n (denominator x))) rational-implies2
         numerator-integerp-lemma))))
  (defthm integerp==>denominator=1
    (implies (integerp x) (equal (denominator x) 1))
    :hints (("Goal" :use (rational-implies2 numerator-when-integerp)
       :in-theory (disable rational-implies2))))
  (defthm equal-denominator-1
    (equal (equal (denominator x) 1)
      (or (integerp x) (not (rationalp x))))
    :hints (("Goal" :use (rational-implies2 completion-of-denominator)
       :in-theory (disable rational-implies2))))
  (defthm *-r-denominator-r
    (equal (* r (denominator r))
      (if (rationalp r)
        (numerator r)
        (fix r)))
    :hints (("Goal" :use ((:instance rational-implies2 (x r)))
       :in-theory (disable rational-implies2))))
  (defthm /r-when-abs-numerator=1
    (and (implies (equal (numerator r) 1)
        (equal (/ r) (denominator r)))
      (implies (equal (numerator r) -1)
        (equal (/ r) (- (denominator r)))))
    :hints (("Goal" :use ((:instance rational-implies2 (x r)))
       :in-theory (disable rational-implies2)))))

(defsection basic-expt-type-rules
  :parents (arithmetic-1 expt)
  :short "Rules about when @('expt') produces integers, positive numbers, etc."
  (defthm expt-type-prescription-rationalp
    (implies (rationalp r) (rationalp (expt r i)))
    :rule-classes (:type-prescription :generalize))
  (defthm expt-type-prescription-positive
    (implies (and (< 0 r) (real/rationalp r)) (< 0 (expt r i)))
    :rule-classes (:type-prescription :generalize))
  (defthm expt-type-prescription-nonzero
    (implies (and (fc (acl2-numberp r)) (not (equal r 0)))
      (not (equal 0 (expt r i))))
    :rule-classes (:type-prescription :generalize))
  (defthm expt-type-prescription-integerp
    (implies (and (<= 0 i) (integerp r)) (integerp (expt r i)))
    :rule-classes (:type-prescription :generalize))
  (in-theory (disable rationalp-expt-type-prescription
      expt-type-prescription-non-zero-base)))

(defsection basic-expt-normalization
  :parents (arithmetic-1 expt)
  :short "Basic rules for normalizing and simplifying exponents."
  (defthm right-unicity-of-1-for-expt
    (equal (expt r 1) (fix r))
    :hints (("Goal" :expand (expt r 1))))
  (defthm expt-minus (equal (expt r (- i)) (/ (expt r i))))
  (defthm exponents-add-for-nonneg-exponents
    (implies (and (<= 0 i) (<= 0 j) (fc (integerp i)) (fc (integerp j)))
      (equal (expt r (+ i j)) (* (expt r i) (expt r j)))))
  (encapsulate nil
    (local (defthm exponents-add-negative-negative
        (implies (and (integerp i) (integerp j) (< i 0) (< j 0))
          (equal (expt r (+ i j)) (* (expt r i) (expt r j))))
        :rule-classes nil))
    (local (defthm exponents-add-positive-negative
        (implies (and (integerp i)
            (integerp j)
            (acl2-numberp r)
            (not (equal r 0))
            (< 0 i)
            (< j 0))
          (equal (expt r (+ i j)) (* (expt r i) (expt r j))))
        :hints (("Goal" :expand (expt r (+ i j))))
        :rule-classes nil))
    (defthm exponents-add
      (implies (and (syntaxp (not (and (quotep i)
                (integerp (cadr i))
                (or (equal (cadr i) 1) (equal (cadr i) -1)))))
          (syntaxp (not (and (quotep j)
                (integerp (cadr j))
                (or (equal (cadr j) 1) (equal (cadr j) -1)))))
          (not (equal 0 r))
          (fc (acl2-numberp r))
          (fc (integerp i))
          (fc (integerp j)))
        (equal (expt r (+ i j)) (* (expt r i) (expt r j))))
      :hints (("Goal" :use (exponents-add-negative-negative exponents-add-positive-negative
           (:instance exponents-add-positive-negative (i j) (j i)))))))
  (defthm exponents-add-unrestricted
    (implies (and (not (equal 0 r))
        (fc (acl2-numberp r))
        (fc (integerp i))
        (fc (integerp j)))
      (equal (expt r (+ i j)) (* (expt r i) (expt r j)))))
  (in-theory (disable exponents-add-unrestricted))
  (defthm distributivity-of-expt-over-*
    (equal (expt (* a b) i) (* (expt a i) (expt b i))))
  (defthm expt-1 (equal (expt 1 x) 1))
  (defthm exponents-multiply
    (implies (and (fc (integerp i)) (fc (integerp j)))
      (equal (expt (expt r i) j) (expt r (* i j))))
    :hints (("Goal" :cases ((not (acl2-numberp r)) (equal r 0)))))
  (defthm functional-commutativity-of-expt-/-base
    (equal (expt (/ r) i) (/ (expt r i))))
  (defthm equal-constant-+
    (implies (syntaxp (and (quotep c1) (quotep c2)))
      (equal (equal (+ c1 x) c2)
        (if (acl2-numberp c2)
          (if (acl2-numberp x)
            (equal x (- c2 c1))
            (equal (fix c1) c2))
          nil)))))