cancel-terms-meta - ACL2 Book

Included Books

other

(in-package "ACL2")

include-book

(include-book "common-meta")

local

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

local

(local (include-book "cancel-terms-helper"))

other

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

local

(local (defthm hide-revealed
    (equal (hide x) x)
    :hints (("Goal" :expand (hide x)))))

info-list-entryfunction

(defun info-list-entry
  (piece pattern-fun val-fun)
  (cons (my-apply-1 pattern-fun piece)
    (cons (rfix (my-apply-1 val-fun piece)) piece)))

patternother

(defabbrev pattern (info-list-entry) (car info-list-entry))

valother

(defabbrev val (info-list-entry) (cadr info-list-entry))

pieceother

(defabbrev piece (info-list-entry) (cddr info-list-entry))

info-list-intersectfunction

(defun info-list-intersect
  (info-list1 info-list2 bin-op)
  (declare (xargs :hints (("Goal" :in-theory (enable assoc-pattern-matchp)))))
  (if (atom info-list1)
    nil
    (let ((temp (assoc-pattern-matchp (pattern (first info-list1))
           info-list2)))
      (if temp
        (cons (if (use-firstp (val (first info-list1)) (val temp) bin-op)
            (first info-list1)
            temp)
          (info-list-intersect (rest info-list1) info-list2 bin-op))
        (info-list-intersect (rest info-list1) info-list2 bin-op)))))

info-list1function

(defun info-list1
  (term pattern-fun val-fun bin-op)
  (if (and (consp term) (eq (ffn-symb term) bin-op))
    (cons (info-list-entry (arg1 term) pattern-fun val-fun)
      (info-list1 (arg2 term) pattern-fun val-fun bin-op))
    (list (info-list-entry term pattern-fun val-fun))))

info-listfunction

(defun info-list
  (term pattern-fun val-fun bin-op)
  (cond ((and (eq bin-op 'binary-*) (eq (fn-symb term) 'binary-+)) (let ((temp (info-list (arg2 term) pattern-fun val-fun bin-op)))
        (if temp
          (info-list-intersect (info-list1 (arg1 term) pattern-fun val-fun bin-op)
            temp
            bin-op)
          nil)))
    (t (info-list1 term pattern-fun val-fun bin-op))))

local

(local (in-theory (disable info-list)))

proveably-rationalfunction

(defun proveably-rational
  (x mfc state)
  (equal (mfc-rw `(rationalp ,X) t t mfc state) *t*))

my-apply-2function

(defun my-apply-2
  (fun arg mfc state)
  (case fun
    (proveably-rational (proveably-rational arg mfc state))
    (true t)))

local

(local (in-theory (disable my-apply-2)))

cancelling-piecefunction

(defun cancelling-piece
  (piece bin-op)
  (if (eq bin-op 'binary-*)
    (if (eq (fn-symb piece) 'expt)
      `(expt (unary-/ ,(FARGN PIECE 1)) ,(FARGN PIECE 2))
      `(unary-/ ,PIECE))
    (cond ((eq (fn-symb piece) 'unary--) (fargn piece 1))
      ((and (eq (fn-symb piece) 'binary-*)
         (quotep (fargn piece 1))) `(binary-* ,(KWOTE (- (UNQUOTE (FARGN PIECE 1))))
          ,(FARGN PIECE 2)))
      (t `(unary-- ,PIECE)))))

local

(local (in-theory (disable cancelling-piece)))

strip-cancelling-piecefunction

(defun strip-cancelling-piece
  (cancelling-piece)
  (if (member-eq (fn-symb cancelling-piece)
      '(unary-- unary-/ expt))
    (strip-cancelling-piece (arg1 cancelling-piece))
    cancelling-piece))

first-matchfunction

(defun first-match
  (info-list1 info-list2 criterion bin-op mfc state)
  (if (endp info-list1)
    (mv nil nil nil)
    (let* ((temp (assoc-pattern-matchp (pattern (first info-list1))
           info-list2)) (use-first (if temp
            (use-firstp (val (first info-list1)) (val temp) bin-op)
            nil))
        (piece (if temp
            (if use-first
              (piece (first info-list1))
              (piece temp))
            nil))
        (pattern (if temp
            (if use-first
              (pattern (first info-list1))
              (pattern temp))
            nil))
        (cancelling-piece (if temp
            (cancelling-piece piece bin-op)
            nil)))
      (if (and temp (my-apply-2 criterion cancelling-piece mfc state))
        (mv t pattern cancelling-piece)
        (first-match (rest info-list1)
          info-list2
          criterion
          bin-op
          mfc
          state)))))

local

(local (in-theory (disable first-match)))

first-negative2function

(defun first-negative2
  (term pattern-fun val-fun criterion bin-op mfc state)
  (let ((val (rfix (my-apply-1 val-fun term))))
    (if (and (< val 0) (my-apply-2 criterion term mfc state))
      (mv t
        (my-apply-1 pattern-fun term)
        (cancelling-piece term bin-op))
      (mv nil nil nil))))

first-negative1function

(defun first-negative1
  (term pattern-fun val-fun criterion bin-op mfc state)
  (declare (xargs :hints (("Goal" :in-theory (disable first-negative2)))))
  (if (and (consp term) (eq (fn-symb term) bin-op))
    (mv-let (flag to-match cancelling-piece)
      (first-negative2 (arg1 term)
        pattern-fun
        val-fun
        criterion
        bin-op
        mfc
        state)
      (if flag
        (mv t to-match cancelling-piece)
        (first-negative1 (arg2 term)
          pattern-fun
          val-fun
          criterion
          bin-op
          mfc
          state)))
    (first-negative2 term
      pattern-fun
      val-fun
      criterion
      bin-op
      mfc
      state)))

first-negativefunction

(defun first-negative
  (term pattern-fun val-fun criterion bin-op mfc state)
  (if (and (eq bin-op 'binary-*) (eq (fn-symb term) 'binary-+))
    (mv-let (flag to-match cancelling-piece)
      (first-negative1 (arg1 term)
        pattern-fun
        val-fun
        criterion
        bin-op
        mfc
        state)
      (if flag
        (mv flag to-match cancelling-piece)
        (first-negative (arg2 term)
          pattern-fun
          val-fun
          criterion
          bin-op
          mfc
          state)))
    (first-negative1 term
      pattern-fun
      val-fun
      criterion
      bin-op
      mfc
      state)))

local

(local (in-theory (disable first-negative)))

hack957theorem

(defthm hack957
  (implies (equal (fix (eva term a)) 0)
    (equal (fix (eva (strip-cancelling-piece term) a)) 0)))

insert-zerofunction

(defun insert-zero
  (sub-term term)
  (cond ((or (null term) (variablep term) (fquotep term)) (if (equal sub-term term)
        ''0
        term))
    (t (case (ffn-symb term)
        ((binary-+ binary-*) (if (equal sub-term term)
            ''0
            (list (ffn-symb term)
              (insert-zero sub-term (arg1 term))
              (insert-zero sub-term (arg2 term)))))
        ((unary-- unary-/) (list (ffn-symb term) (insert-zero sub-term (arg1 term))))
        (expt (list (ffn-symb term)
            (insert-zero sub-term (arg1 term))
            (arg2 term)))
        (t (if (equal sub-term term)
            ''0
            term))))))

insert-zero-correct0theorem

(defthm insert-zero-correct0
  (implies (and (equal (fix (eva sub-term a)) 0)
      (not (acl2-numberp (eva term a))))
    (equal (eva (insert-zero sub-term term) a)
      (if (equal sub-term term)
        0
        (eva term a)))))

insert-zero-correctatheorem

(defthm insert-zero-correcta
  (implies (and (equal (fix (eva sub-term a)) 0)
      (case-split (acl2-numberp (eva term a))))
    (equal (eva (insert-zero sub-term term) a) (eva term a))))

local

(local (in-theory (disable strip-cancelling-piece insert-zero)))

new-term-nffunction

(defun new-term-nf
  (term new-piece pattern pattern-fun bin-op)
  (mv-let (flag new-term)
    (new-term term new-piece pattern pattern-fun bin-op)
    (declare (ignore flag))
    new-term))

good-argfunction

(defun good-arg
  (arg)
  (member-eq (fn-symb arg)
    '(binary-+ binary-* expt unary-- unary-/)))

test926theorem

(defthm test926
  (implies (good-arg term) (acl2-numberp (eva term a)))
  :rule-classes (:type-prescription))

local

(local (in-theory (disable good-arg)))

good-args-*function

(defun good-args-*
  (arg1 arg2)
  (cond ((or (null arg1) (null arg2)) nil)
    ((member-eq (fn-symb arg1) '(expt unary-- unary-/)) (not (equal arg2 ''0)))
    ((member-eq (fn-symb arg2) '(expt unary-- unary-/)) (not (equal arg1 ''0)))
    (t t)))

nil-not-good-args-*theorem

(defthm nil-not-good-args-*
  (and (not (good-args-* x nil)) (not (good-args-* nil x))))

good-args-+function

(defun good-args-+
  (arg1 arg2)
  (and (not (equal arg1 ''0)) (not (equal arg2 ''0))))

local

(local (in-theory (disable good-args-+ good-args-*)))

good-argsfunction

(defun good-args
  (arg1 arg2 bin-op)
  (and (or (good-arg arg1) (good-arg arg2))
    (if (eq bin-op 'binary-*)
      (good-args-* arg1 arg2)
      (good-args-+ arg1 arg2))))

make-cancelling-metamacro

(defmacro make-cancelling-meta
  (name bin-op rel pattern-fun val-fun criterion result)
  (let ((fn-name (intern-name (list name "-FN"))) (thm-name (intern-name (list name "-THM"))))
    `(progn (defun ,FN-NAME
        (term mfc state)
        (if (and (consp term) (eq (ffn-symb term) ,REL))
          (let ((arg1 (arg1 term)) (arg2 (arg2 term)))
            (if (good-args arg1 arg2 ,BIN-OP)
              (mv-let (flag pattern cancelling-piece)
                (let* ((info-list1 (info-list arg1 ,PATTERN-FUN ,VAL-FUN ,BIN-OP)) (info-list2 (if (null info-list1)
                        nil
                        (info-list arg2 ,PATTERN-FUN ,VAL-FUN ,BIN-OP))))
                  (first-match info-list1
                    info-list2
                    ,CRITERION
                    ,BIN-OP
                    mfc
                    state))
                (if flag
                  (let ((new-arg1 (new-term-nf arg1
                         cancelling-piece
                         pattern
                         ,PATTERN-FUN
                         ,BIN-OP)) (new-arg2 (new-term-nf arg2
                          cancelling-piece
                          pattern
                          ,PATTERN-FUN
                          ,BIN-OP)))
                    ,RESULT)
                  term))
              term))
          term))
      (defthm ,THM-NAME
        (equal (eva term a) (eva (,FN-NAME term mfc state) a))
        :rule-classes ((:meta :trigger-fns (,(UNQUOTE REL))))
        :otf-flg t)
      (local (in-theory (disable ,THM-NAME))))))

make-prefer-positives-metamacro

(defmacro make-prefer-positives-meta
  (name bin-op rel pattern-fun val-fun criterion result)
  (let ((fn-name (intern-name (list name "-FN"))) (thm-name (intern-name (list name "-THM"))))
    `(progn (defun ,FN-NAME
        (term mfc state)
        (if (and (consp term) (eq (ffn-symb term) ,REL))
          (let ((arg1 (arg1 term)) (arg2 (arg2 term)))
            (if (or (good-arg arg1) (good-arg arg2))
              (mv-let (flag pattern cancelling-piece)
                (mv-let (temp-flag temp-pattern temp-cancelling-piece)
                  (first-negative arg1
                    ,PATTERN-FUN
                    ,VAL-FUN
                    ,CRITERION
                    ,BIN-OP
                    mfc
                    state)
                  (if temp-flag
                    (mv temp-flag temp-pattern temp-cancelling-piece)
                    (first-negative arg2
                      ,PATTERN-FUN
                      ,VAL-FUN
                      ,CRITERION
                      ,BIN-OP
                      mfc
                      state)))
                (if flag
                  (let ((new-arg1 (new-term-nf arg1
                         cancelling-piece
                         pattern
                         ,PATTERN-FUN
                         ,BIN-OP)) (new-arg2 (new-term-nf arg2
                          cancelling-piece
                          pattern
                          ,PATTERN-FUN
                          ,BIN-OP)))
                    ,RESULT)
                  term))
              term))
          term))
      (defthm ,THM-NAME
        (equal (eva term a) (eva (,FN-NAME term mfc state) a))
        :rule-classes ((:meta :trigger-fns (,(UNQUOTE REL)))))
      (local (in-theory (disable ,THM-NAME))))))

addends-equal-resultmacro

(defmacro addends-equal-result
  nil
  '`(if (acl2-numberp ,ARG1)
    (if (acl2-numberp ,ARG2)
      (equal ,NEW-ARG1 ,NEW-ARG2)
      'nil)
    'nil))

addends-<-resultmacro

(defmacro addends-<-result nil '`(< ,NEW-ARG1 ,NEW-ARG2))

factors-equal-resultmacro

(defmacro factors-equal-result
  nil
  '`(if (acl2-numberp ,ARG1)
    (if (acl2-numberp ,ARG2)
      (if (not (equal (fix ,CANCELLING-PIECE) '0))
        (equal ,NEW-ARG1 ,NEW-ARG2)
        (equal ,(INSERT-ZERO (STRIP-CANCELLING-PIECE CANCELLING-PIECE) ARG1)
          ,(INSERT-ZERO (STRIP-CANCELLING-PIECE CANCELLING-PIECE) ARG2)))
      'nil)
    'nil))

factors-<-resultmacro

(defmacro factors-<-result
  nil
  '`(if (rationalp ,CANCELLING-PIECE)
    (if (not (equal ,CANCELLING-PIECE '0))
      (if (< '0 ,CANCELLING-PIECE)
        (< ,NEW-ARG1 ,NEW-ARG2)
        (< ,NEW-ARG2 ,NEW-ARG1))
      (< ,(INSERT-ZERO (STRIP-CANCELLING-PIECE CANCELLING-PIECE) ARG1)
        ,(INSERT-ZERO (STRIP-CANCELLING-PIECE CANCELLING-PIECE) ARG2)))
    ,TERM))

local

(local (in-theory (disable good-args)))

local

(local (in-theory (enable rewrite-linear-equalities-to-iff)))

local

(local (in-theory (enable good-args)))

local

(local (in-theory (disable cancelling-piece
      first-match
      new-term
      info-list
      my-apply-1)))

local

(local (in-theory (disable good-arg good-args-+ good-args-*)))

other

(make-cancelling-meta cancel-addends-equal
  'binary-+
  'equal
  'addend-pattern
  'addend-val
  'true
  (addends-equal-result))

other

(make-cancelling-meta cancel-addends-<
  'binary-+
  '<
  'addend-pattern
  'addend-val
  'true
  (addends-<-result))

other

(make-cancelling-meta cancel-factors-gather-exponents-equal
  'binary-*
  'equal
  'factor-pattern-gather-exponents
  'factor-val
  'true
  (factors-equal-result))

other

(make-cancelling-meta cancel-factors-scatter-exponents-equal
  'binary-*
  'equal
  'factor-pattern-scatter-exponents
  'factor-val
  'true
  (factors-equal-result))

other

(make-cancelling-meta cancel-factors-gather-exponents-<
  'binary-*
  '<
  'factor-pattern-gather-exponents
  'factor-val
  'proveably-rational
  (factors-<-result))

other

(make-cancelling-meta cancel-factors-scatter-exponents-<
  'binary-*
  '<
  'factor-pattern-scatter-exponents
  'factor-val
  'proveably-rational
  (factors-<-result))

other

(make-prefer-positives-meta prefer-positive-addends-equal
  'binary-+
  'equal
  'addend-pattern
  'addend-val
  'true
  (addends-equal-result))

other

(make-prefer-positives-meta prefer-positive-addends-<
  'binary-+
  '<
  'addend-pattern
  'addend-val
  'true
  (addends-<-result))

other

(make-prefer-positives-meta prefer-positive-factors-gather-exponents-equal
  'binary-*
  'equal
  'factor-pattern-gather-exponents
  'factor-val
  'true
  (factors-equal-result))

other

(make-prefer-positives-meta prefer-positive-factors-scatter-exponents-equal
  'binary-*
  'equal
  'factor-pattern-scatter-exponents
  'factor-val
  'true
  (factors-equal-result))

other

(make-prefer-positives-meta prefer-positive-factors-gather-exponents-<
  'binary-*
  '<
  'factor-pattern-scatter-exponents
  'factor-val
  'proveably-rational
  (factors-<-result))

other

(make-prefer-positives-meta prefer-positive-factors-scatter-exponents-<
  'binary-*
  '<
  'factor-pattern-scatter-exponents
  'factor-val
  'proveably-rational
  (factors-<-result))

other

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