simplify - ACL2 Book

Included Books

other

(in-package "ACL2")

include-book

(include-book "common")

local

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

local

(local (include-book "basic"))

other

(table acl2-defaults-table :state-ok t)

local

(local (defthm rewrite-equal-<-to-iff-<
    (equal (equal (< a b) (< c d)) (iff (< a b) (< c d)))))

local

(local (encapsulate nil
    (local (include-book "../../support/top"))
    (defthm equal-*-/-1
      (equal (equal (* (/ x) y) z)
        (if (equal (fix x) 0)
          (equal z 0)
          (and (acl2-numberp z) (equal (fix y) (* x z))))))
    (defthm equal-*-/-2
      (equal (equal (* y (/ x)) z)
        (if (equal (fix x) 0)
          (equal z 0)
          (and (acl2-numberp z) (equal (fix y) (* z x))))))))

local

(local (encapsulate nil
    (local (include-book "../../support/top"))
    (defthm equal-*-1
      (implies (not (equal (fix x) 0))
        (equal (equal (* x y) (* x z)) (equal (fix y) (fix z)))))
    (defthm equal-*-2
      (implies (not (equal (fix x) 0))
        (equal (equal (* y x) (* z x)) (equal (fix y) (fix z)))))))

simplify-terms-such-as-ax+bx-rel-0-fnfunction

(defun simplify-terms-such-as-ax+bx-rel-0-fn
  (sum)
  (declare (xargs :guard t))
  (if (eq (fn-symb sum) 'binary-+)
    (let ((common-factors (common-factors (factors (arg1 sum)) (arg2 sum))))
      (if common-factors
        (let ((common (make-product common-factors)) (remainder (remainder common-factors sum)))
          (list (cons 'common common) (cons 'remainder remainder)))
        nil))
    nil))

simplify-terms-such-as-ax+bx-=-0theorem

(defthm simplify-terms-such-as-ax+bx-=-0
  (implies (and (bind-free (simplify-terms-such-as-ax+bx-rel-0-fn sum)
        (common remainder))
      (acl2-numberp common)
      (acl2-numberp remainder)
      (equal sum (* common remainder)))
    (equal (equal sum 0)
      (or (equal common 0) (equal remainder 0)))))

simplify-terms-such-as-ax+bx-<-0-rational-remaindertheorem

(defthm simplify-terms-such-as-ax+bx-<-0-rational-remainder
  (implies (and (bind-free (simplify-terms-such-as-ax+bx-rel-0-fn sum)
        (common remainder))
      (acl2-numberp common)
      (real/rationalp remainder)
      (equal sum (* common remainder)))
    (equal (< sum 0)
      (cond ((< common 0) (< 0 remainder))
        ((< 0 common) (< remainder 0))
        (t nil)))))

simplify-terms-such-as-ax+bx-<-0-rational-commontheorem

(defthm simplify-terms-such-as-ax+bx-<-0-rational-common
  (implies (and (bind-free (simplify-terms-such-as-ax+bx-rel-0-fn sum)
        (common remainder))
      (real/rationalp common)
      (acl2-numberp remainder)
      (equal sum (* common remainder)))
    (equal (< sum 0)
      (cond ((< common 0) (< 0 remainder))
        ((< 0 common) (< remainder 0))
        (t nil))))
  :hints (("Goal" :use (:instance simplify-terms-such-as-ax+bx-<-0-rational-remainder
       (common remainder)
       (remainder common)))))

simplify-terms-such-as-0-<-ax+bx-rational-remaindertheorem

(defthm simplify-terms-such-as-0-<-ax+bx-rational-remainder
  (implies (and (bind-free (simplify-terms-such-as-ax+bx-rel-0-fn sum)
        (common remainder))
      (acl2-numberp common)
      (real/rationalp remainder)
      (equal sum (* common remainder)))
    (equal (< 0 sum)
      (cond ((< 0 common) (< 0 remainder))
        ((< common 0) (< remainder 0))
        (t nil)))))

simplify-terms-such-as-0-<-ax+bx-rational-commontheorem

(defthm simplify-terms-such-as-0-<-ax+bx-rational-common
  (implies (and (bind-free (simplify-terms-such-as-ax+bx-rel-0-fn sum)
        (common remainder))
      (real/rationalp common)
      (acl2-numberp remainder)
      (equal sum (* common remainder)))
    (equal (< 0 sum)
      (cond ((< 0 common) (< 0 remainder))
        ((< common 0) (< remainder 0))
        (t nil))))
  :hints (("Goal" :use (:instance simplify-terms-such-as-0-<-ax+bx-rational-remainder
       (common remainder)
       (remainder common)))))

addend-valfunction

(defun addend-val
  (addend)
  (declare (xargs :guard t))
  (cond ((variablep addend) (list 0 1 0))
    ((constant-p addend) (let ((val (unquote addend)))
        (if (rationalp val)
          (list 0 0 (abs val))
          (list 0 0 1))))
    ((eq (ffn-symb addend) 'unary--) (addend-val (arg1 addend)))
    ((and (eq (ffn-symb addend) 'binary-*)
       (constant-p (arg1 addend))) (let ((val (unquote (arg1 addend))))
        (if (rationalp val)
          (list (abs val) 0 0)
          (list 1 0 0))))
    (t (list 0 1 0))))

addend-info-entryfunction

(defun addend-info-entry
  (x)
  (declare (xargs :guard t))
  (list (addend-pattern x) (addend-val x) x))

addend-info-listfunction

(defun addend-info-list
  (x)
  (declare (xargs :guard t))
  (if (eq (fn-symb x) 'binary-+)
    (cons (addend-info-entry (arg1 x))
      (addend-info-list (arg2 x)))
    (list (addend-info-entry x))))

local

(local (encapsulate nil
    (local (defthm temp-1 (good-val-triple-p (addend-val x))))
    (defthm addend-info-list-thm
      (info-list-p (addend-info-list x)))))

assoc-addendfunction

(defun assoc-addend
  (x info-list)
  (declare (xargs :guard (info-list-p info-list)))
  (cond ((endp info-list) nil)
    ((matching-addend-patterns-p x (caar info-list)) (car info-list))
    (t (assoc-addend x (cdr info-list)))))

first-match-in-addend-info-listsfunction

(defun first-match-in-addend-info-lists
  (info-list1 info-list2 mfc state)
  (declare (xargs :guard (and (info-list-p info-list1) (info-list-p info-list2))
      :guard-hints (("Goal" :in-theory (disable good-val-triple-p negate-match val-<)))))
  (if (endp info-list1)
    nil
    (let ((temp (assoc-addend (car (car info-list1)) info-list2)))
      (if temp
        (cond ((and (val-< (cadr (car info-list1)) (cadr temp))
             (stable-under-rewriting-sums (negate-match (caddr (car info-list1)))
               mfc
               state)) (list (cons 'x (negate-match (caddr (car info-list1))))))
          ((stable-under-rewriting-sums (negate-match (caddr temp))
             mfc
             state) (list (cons 'x (negate-match (caddr temp)))))
          (t (first-match-in-addend-info-lists (cdr info-list1)
              info-list2
              mfc
              state)))
        (first-match-in-addend-info-lists (cdr info-list1)
          info-list2
          mfc
          state)))))

find-matching-addendsfunction

(defun find-matching-addends
  (lhs rhs mfc state)
  (declare (xargs :guard t :verify-guards nil))
  (let* ((info-list1 (addend-info-list lhs)) (info-list2 (if info-list1
          (addend-info-list rhs)
          nil)))
    (if info-list2
      (first-match-in-addend-info-lists info-list1
        info-list2
        mfc
        state)
      nil)))

other

(verify-guards find-matching-addends)

simplify-sums-equaltheorem

(defthm simplify-sums-equal
  (implies (and (syntaxp (not (quotep lhs)))
      (syntaxp (not (quotep rhs)))
      (syntaxp (in-term-order-+ lhs mfc state))
      (syntaxp (in-term-order-+ rhs mfc state))
      (acl2-numberp lhs)
      (acl2-numberp rhs)
      (bind-free (find-matching-addends lhs rhs mfc state) (x)))
    (equal (equal lhs rhs) (equal (+ x lhs) (+ x rhs)))))

local

(local (in-theory (disable simplify-sums-equal)))

simplify-sums-<theorem

(defthm simplify-sums-<
  (implies (and (syntaxp (not (quotep lhs)))
      (syntaxp (not (quotep rhs)))
      (syntaxp (in-term-order-+ lhs mfc state))
      (syntaxp (in-term-order-+ rhs mfc state))
      (acl2-numberp lhs)
      (acl2-numberp rhs)
      (bind-free (find-matching-addends lhs rhs mfc state) (x)))
    (equal (< lhs rhs) (< (+ x lhs) (+ x rhs)))))

local

(local (in-theory (disable simplify-sums-<)))

negative-addend-pfunction

(defun negative-addend-p
  (x)
  (declare (xargs :guard t))
  (or (and (eq (fn-symb x) 'unary--)
      (or (variablep (arg1 x))
        (not (equal (ffn-symb (arg1 x)) 'unary--))))
    (and (eq (fn-symb x) 'binary-*)
      (rational-constant-p (arg1 x))
      (< (unquote (arg1 x)) 0))))

find-negative-addend1function

(defun find-negative-addend1
  (x mfc state)
  (declare (xargs :guard t))
  (cond ((not (eq (fn-symb x) 'binary-+)) (if (and (negative-addend-p x)
          (stable-under-rewriting-sums (negate-match x) mfc state))
        (list (cons 'x (negate-match x)))
        nil))
    ((and (negative-addend-p (arg1 x))
       (stable-under-rewriting-sums (negate-match (arg1 x))
         mfc
         state)) (list (cons 'x (negate-match (arg1 x)))))
    ((eq (fn-symb (arg2 x)) 'binary-+) (find-negative-addend1 (arg2 x) mfc state))
    ((and (negative-addend-p (arg2 x))
       (stable-under-rewriting-sums (negate-match (arg2 x))
         mfc
         state)) (list (cons 'x (negate-match (arg2 x)))))
    (t nil)))

find-negative-addendfunction

(defun find-negative-addend
  (lhs rhs mfc state)
  (declare (xargs :guard t))
  (let ((temp1 (find-negative-addend1 lhs mfc state)))
    (if temp1
      temp1
      (let ((temp2 (find-negative-addend1 rhs mfc state)))
        (if temp2
          temp2
          nil)))))

prefer-positive-addends-equaltheorem

(defthm prefer-positive-addends-equal
  (implies (and (acl2-numberp lhs)
      (acl2-numberp rhs)
      (syntaxp (in-term-order-+ lhs mfc state))
      (syntaxp (in-term-order-+ rhs mfc state))
      (syntaxp (or (equal (fn-symb lhs) 'binary-+)
          (equal (fn-symb rhs) 'binary-+)))
      (bind-free (find-negative-addend lhs rhs mfc state) (x)))
    (equal (equal lhs rhs) (equal (+ x lhs) (+ x rhs)))))

local

(local (in-theory (disable prefer-positive-addends-equal)))

prefer-positive-addends-<theorem

(defthm prefer-positive-addends-<
  (implies (and (acl2-numberp lhs)
      (acl2-numberp rhs)
      (syntaxp (in-term-order-+ lhs mfc state))
      (syntaxp (in-term-order-+ rhs mfc state))
      (syntaxp (or (equal (fn-symb lhs) 'binary-+)
          (equal (fn-symb rhs) 'binary-+)))
      (bind-free (find-negative-addend lhs rhs mfc state) (x)))
    (equal (< lhs rhs) (< (+ x lhs) (+ x rhs)))))

local

(local (in-theory (disable prefer-positive-addends-<)))

simplify-products-gather-exponents-equaltheorem

(defthm simplify-products-gather-exponents-equal
  (implies (and (acl2-numberp lhs)
      (acl2-numberp rhs)
      (syntaxp (not (quotep lhs)))
      (syntaxp (not (quotep rhs)))
      (syntaxp (in-term-order-* lhs mfc state))
      (syntaxp (in-term-order-* rhs mfc state))
      (bind-free (find-matching-factors-gather-exponents lhs rhs mfc state)
        (x))
      (syntaxp (not (equal x ''1)))
      (syntaxp (not (equal x ''-1)))
      (case-split (acl2-numberp x))
      (case-split (not (equal x 0))))
    (equal (equal lhs rhs) (equal (* x lhs) (* x rhs)))))

local

(local (in-theory (disable simplify-products-gather-exponents-equal)))

simplify-products-gather-exponents-<theorem

(defthm simplify-products-gather-exponents-<
  (implies (and (acl2-numberp lhs)
      (acl2-numberp rhs)
      (syntaxp (not (quotep lhs)))
      (syntaxp (not (quotep rhs)))
      (syntaxp (in-term-order-* lhs mfc state))
      (syntaxp (in-term-order-* rhs mfc state))
      (bind-free (find-rational-matching-factors-gather-exponents lhs
          rhs
          mfc
          state)
        (x))
      (syntaxp (not (equal x ''1)))
      (syntaxp (not (equal x ''-1)))
      (case-split (real/rationalp x))
      (case-split (not (equal x 0))))
    (equal (< lhs rhs)
      (cond ((< 0 x) (< (* x lhs) (* x rhs)))
        (t (< (* x rhs) (* x lhs)))))))

local

(local (in-theory (disable simplify-products-gather-exponents-<)))

simplify-products-scatter-exponents-equaltheorem

(defthm simplify-products-scatter-exponents-equal
  (implies (and (acl2-numberp lhs)
      (acl2-numberp rhs)
      (syntaxp (not (quotep lhs)))
      (syntaxp (not (quotep rhs)))
      (syntaxp (in-term-order-* lhs mfc state))
      (syntaxp (in-term-order-* rhs mfc state))
      (bind-free (find-matching-factors-scatter-exponents lhs rhs mfc state)
        (x))
      (syntaxp (not (equal x ''1)))
      (syntaxp (not (equal x ''-1)))
      (case-split (acl2-numberp x))
      (case-split (not (equal x 0))))
    (equal (equal lhs rhs) (equal (* x lhs) (* x rhs)))))

local

(local (in-theory (disable simplify-products-scatter-exponents-equal)))

simplify-products-scatter-exponents-<theorem

(defthm simplify-products-scatter-exponents-<
  (implies (and (acl2-numberp lhs)
      (acl2-numberp rhs)
      (syntaxp (not (quotep lhs)))
      (syntaxp (not (quotep rhs)))
      (syntaxp (in-term-order-* lhs mfc state))
      (syntaxp (in-term-order-* rhs mfc state))
      (bind-free (find-rational-matching-factors-scatter-exponents lhs
          rhs
          mfc
          state)
        (x))
      (syntaxp (not (equal x ''1)))
      (syntaxp (not (equal x ''-1)))
      (case-split (real/rationalp x))
      (case-split (not (equal x 0))))
    (equal (< lhs rhs)
      (cond ((< 0 x) (< (* x lhs) (* x rhs)))
        (t (< (* x rhs) (* x lhs)))))))

local

(local (in-theory (disable simplify-products-scatter-exponents-<)))

find-divisive-factor-scatter-exponents2function

(defun find-divisive-factor-scatter-exponents2
  (x mfc state)
  (declare (xargs :guard t))
  (cond ((or (variablep x) (fquotep x)) nil)
    ((eq (ffn-symb x) 'unary--) (find-divisive-factor-scatter-exponents2 (arg1 x) mfc state))
    ((eq (ffn-symb x) 'unary-/) (if (stable-under-rewriting-products (invert-match x) mfc state)
        (list (cons 'x (invert-match x)))
        nil))
    ((eq (ffn-symb x) 'expt) (cond ((eq (fn-symb (arg1 x)) 'unary-/) (if (stable-under-rewriting-products (invert-match x) mfc state)
            (list (cons 'x (invert-match x)))
            nil))
        ((and (quotep (arg1 x))
           (consp (cdr (arg1 x)))
           (not (integerp (cadr (arg1 x))))
           (rationalp (cadr (arg1 x)))
           (eql (numerator (cadr (arg1 x))) 1)) (if (stable-under-rewriting-products (invert-match x) mfc state)
            (list (cons 'x (invert-match x)))
            nil))
        ((eq (fn-symb (arg2 x)) 'unary--) (if (stable-under-rewriting-products (invert-match x) mfc state)
            (list (cons 'x (invert-match x)))
            nil))
        ((and (eq (fn-symb (arg2 x)) 'binary-*)
           (rational-constant-p (arg1 (arg2 x)))
           (< (unquote (arg1 (arg2 x))) 0)) (if (stable-under-rewriting-products (invert-match x) mfc state)
            (list (cons 'x (invert-match x)))
            nil))
        (t nil)))
    ((eq (ffn-symb x) 'binary-*) (let ((temp (find-divisive-factor-scatter-exponents2 (arg1 x) mfc state)))
        (if temp
          temp
          (find-divisive-factor-scatter-exponents2 (arg2 x) mfc state))))
    (t nil)))

find-divisive-factor-scatter-exponents1function

(defun find-divisive-factor-scatter-exponents1
  (x mfc state)
  (declare (xargs :guard t))
  (cond ((or (variablep x) (fquotep x)) nil)
    ((eq (ffn-symb x) 'binary-+) (let ((temp (find-divisive-factor-scatter-exponents2 (arg1 x) mfc state)))
        (if temp
          temp
          (find-divisive-factor-scatter-exponents1 (arg2 x) mfc state))))
    (t (find-divisive-factor-scatter-exponents2 x mfc state))))

find-divisive-factor-scatter-exponentsfunction

(defun find-divisive-factor-scatter-exponents
  (lhs rhs mfc state)
  (declare (xargs :guard t))
  (let ((temp1 (find-divisive-factor-scatter-exponents1 lhs mfc state)))
    (if temp1
      temp1
      (let ((temp2 (find-divisive-factor-scatter-exponents1 rhs mfc state)))
        (if temp2
          temp2
          nil)))))

prefer-positive-exponents-scatter-exponents-equaltheorem

(defthm prefer-positive-exponents-scatter-exponents-equal
  (implies (and (acl2-numberp lhs)
      (acl2-numberp rhs)
      (syntaxp (in-term-order-* lhs mfc state))
      (syntaxp (in-term-order-* rhs mfc state))
      (bind-free (find-divisive-factor-scatter-exponents lhs rhs mfc state)
        (x))
      (syntaxp (not (equal x ''1)))
      (syntaxp (not (equal x ''-1)))
      (case-split (acl2-numberp x))
      (case-split (not (equal x 0))))
    (equal (equal lhs rhs) (equal (* x lhs) (* x rhs)))))

find-rational-divisive-factor-scatter-exponents2function

(defun find-rational-divisive-factor-scatter-exponents2
  (x mfc state)
  (declare (xargs :guard t))
  (cond ((or (variablep x) (fquotep x)) nil)
    ((eq (ffn-symb x) 'unary--) (find-rational-divisive-factor-scatter-exponents2 (arg1 x)
        mfc
        state))
    ((eq (ffn-symb x) 'unary-/) (if (and (proveably-real/rational 'x `((x . ,X)) mfc state)
          (stable-under-rewriting-products (invert-match x) mfc state))
        (list (cons 'x (invert-match x)))
        nil))
    ((eq (ffn-symb x) 'expt) (cond ((eq (fn-symb (arg1 x)) 'unary-/) (if (and (proveably-real/rational 'x `((x . ,X)) mfc state)
              (stable-under-rewriting-products (invert-match x) mfc state))
            (list (cons 'x (invert-match x)))
            nil))
        ((and (quotep (arg1 x))
           (consp (cdr (arg1 x)))
           (not (integerp (cadr (arg1 x))))
           (rationalp (cadr (arg1 x)))
           (eql (numerator (cadr (arg1 x))) 1)) (if (and (proveably-real/rational 'x `((x . ,X)) mfc state)
              (stable-under-rewriting-products (invert-match x) mfc state))
            (list (cons 'x (invert-match x)))
            nil))
        ((eq (fn-symb (arg2 x)) 'unary--) (if (and (proveably-real/rational 'x `((x . ,X)) mfc state)
              (stable-under-rewriting-products (invert-match x) mfc state))
            (list (cons 'x (invert-match x)))
            nil))
        ((and (eq (fn-symb (arg2 x)) 'binary-*)
           (rational-constant-p (arg1 (arg2 x)))
           (< (unquote (arg1 (arg2 x))) 0)) (if (and (proveably-real/rational 'x `((x . ,X)) mfc state)
              (stable-under-rewriting-products (invert-match x) mfc state))
            (list (cons 'x (invert-match x)))
            nil))
        (t nil)))
    ((eq (ffn-symb x) 'binary-*) (let ((temp (find-rational-divisive-factor-scatter-exponents2 (arg1 x)
             mfc
             state)))
        (if temp
          temp
          (find-rational-divisive-factor-scatter-exponents2 (arg2 x)
            mfc
            state))))
    (t nil)))

find-rational-divisive-factor-scatter-exponents1function

(defun find-rational-divisive-factor-scatter-exponents1
  (x mfc state)
  (declare (xargs :guard t))
  (cond ((or (variablep x) (fquotep x)) nil)
    ((eq (ffn-symb x) 'binary-+) (let ((temp (find-rational-divisive-factor-scatter-exponents2 (arg1 x)
             mfc
             state)))
        (if temp
          temp
          (find-rational-divisive-factor-scatter-exponents1 (arg2 x)
            mfc
            state))))
    (t (find-rational-divisive-factor-scatter-exponents2 x
        mfc
        state))))

find-rational-divisive-factor-scatter-exponentsfunction

(defun find-rational-divisive-factor-scatter-exponents
  (lhs rhs mfc state)
  (declare (xargs :guard t))
  (let ((temp1 (find-rational-divisive-factor-scatter-exponents1 lhs
         mfc
         state)))
    (if temp1
      temp1
      (let ((temp2 (find-rational-divisive-factor-scatter-exponents1 rhs
             mfc
             state)))
        (if temp2
          temp2
          nil)))))

prefer-positive-exponents-scatter-exponents-<theorem

(defthm prefer-positive-exponents-scatter-exponents-<
  (implies (and (acl2-numberp lhs)
      (acl2-numberp rhs)
      (syntaxp (in-term-order-* lhs mfc state))
      (syntaxp (in-term-order-* rhs mfc state))
      (bind-free (find-rational-divisive-factor-scatter-exponents lhs
          rhs
          mfc
          state)
        (x))
      (syntaxp (not (equal x ''1)))
      (syntaxp (not (equal x ''-1)))
      (case-split (real/rationalp x))
      (case-split (not (equal x 0))))
    (equal (< lhs rhs)
      (cond ((< 0 x) (< (* x lhs) (* x rhs)))
        (t (< (* x rhs) (* x lhs)))))))

prefer-positive-exponents-scatter-exponents-<-2theorem

(defthm prefer-positive-exponents-scatter-exponents-<-2
  (implies (and (real/rationalp lhs)
      (real/rationalp rhs)
      (syntaxp (in-term-order-* lhs mfc state))
      (syntaxp (in-term-order-* rhs mfc state))
      (bind-free (find-divisive-factor-scatter-exponents lhs rhs mfc state)
        (x))
      (syntaxp (not (equal x ''1)))
      (syntaxp (not (equal x ''-1)))
      (case-split (acl2-numberp x))
      (case-split (not (equal x 0))))
    (equal (< lhs rhs)
      (cond ((< 0 x) (< (* x lhs) (* x rhs)))
        (t (< (* x rhs) (* x lhs))))))
  :hints (("Goal" :in-theory (enable big-helper-2))))