common-factor - ACL2 Book

Included Books

meta-times-equal meta-plus-equal meta-plus-lessp common-factor-defuns predicate fp2 product

other

(in-package "ACL2")

include-book

(include-book "../../../meta/meta-times-equal")

include-book

(include-book "../../../meta/meta-plus-equal")

include-book

(include-book "../../../meta/meta-plus-lessp")

include-book

(include-book "common-factor-defuns")

mult-both-sides-of-equaltheorem

(defthm mult-both-sides-of-equal
  (implies (and (case-split (acl2-numberp a))
      (case-split (acl2-numberp b))
      (case-split (acl2-numberp c)))
    (equal (equal (* a c) (* b c))
      (if (equal c 0)
        t
        (equal a b))))
  :rule-classes nil)

commutativity-2-of-*theorem

(defthm commutativity-2-of-*
  (equal (* x (* y z)) (* y (* x z))))

inverse-of-*-2theorem

(defthm inverse-of-*-2
  (implies (and (case-split (acl2-numberp x))
      (case-split (not (equal x 0))))
    (equal (* x (* (/ x) y)) (fix y)))
  :hints (("Goal" :cases ((acl2-numberp x)))))

cancel-common-factors-in-equaltheorem

(defthm cancel-common-factors-in-equal
  (implies (and (bind-free (bind-k-to-common-factors lhs rhs) (k))
      (case-split (not (equal 0 k)))
      (case-split (acl2-numberp k))
      (case-split (acl2-numberp lhs))
      (case-split (acl2-numberp rhs)))
    (equal (equal lhs rhs) (equal (* (/ k) lhs) (* (/ k) rhs))))
  :hints (("Goal" :use (:instance mult-both-sides-of-equal
       (a lhs)
       (b rhs)
       (c (/ k))))))

local

(local (include-book "predicate"))

local

(local (include-book "fp2"))

cancel-in-prods-<theorem

(defthm cancel-in-prods-<
  (implies (and (rationalp a) (rationalp b) (rationalp c))
    (equal (< (* a b) (* a c))
      (if (equal 0 a)
        nil
        (if (> a 0)
          (< b c)
          (> b c))))))

cancel-common-factors-in-<theorem

(defthm cancel-common-factors-in-<
  (implies (and (bind-free (bind-k-to-common-factors lhs rhs) (k))
      (syntaxp (not (equal lhs rhs)))
      (case-split (not (equal 0 k)))
      (case-split (rationalp k))
      (case-split (rationalp lhs))
      (case-split (rationalp rhs)))
    (equal (< lhs rhs)
      (if (< 0 k)
        (< (* (/ k) lhs) (* (/ k) rhs))
        (if (equal 0 k)
          nil
          (< (* (/ k) rhs) (* (/ k) lhs))))))
  :hints (("Goal" :use (:instance cancel-in-prods-< (a lhs) (b rhs) (c (/ k))))))

find-common-factors-to-cancel-1function

(defun find-common-factors-to-cancel-1
  (expr)
  (declare (xargs :guard (and (pseudo-termp expr))))
  (remove-cancelling-factor-pairs (find-common-factors-in-sum-of-products expr)))

bind-k-to-common-factors-1function

(defund bind-k-to-common-factors-1
  (expr)
  (declare (xargs :guard-hints (("Goal" :use (:instance remove-cancelling-factor-pairs-preserves-true-listp
           (l (find-common-factors-in-sum-of-products expr)))))
      :guard (and (pseudo-termp expr))))
  (let* ((common-factor-list (find-common-factors-to-cancel-1 expr)))
    (if (endp common-factor-list)
      nil
      (list (cons 'k
          (make-product-from-list-of-factors common-factor-list))))))

local

(local (include-book "product"))

cancel-common-factors-in-equal-with-0theorem

(defthm cancel-common-factors-in-equal-with-0
  (implies (and (bind-free (bind-k-to-common-factors-1 rhs) (k))
      (syntaxp (not (equal k rhs)))
      (case-split (not (equal 0 k)))
      (case-split (rationalp k))
      (case-split (rationalp lhs))
      (case-split (rationalp rhs)))
    (equal (equal 0 rhs)
      (or (equal 0 k) (equal 0 (* (/ k) rhs))))))