remove-weak-inequalities

Included Books

other

(in-package "ACL2")

include-book

(include-book "building-blocks")

other

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

remove-weak-inequalities-fnfunction

(defun remove-weak-inequalities-fn
  (x y mfc state)
  (declare (xargs :guard t))
  (if (eq (present-in-hyps `(< ,Y ,X) (mfc-clause mfc)) 'positive)
    (let ((contradictionp (mfc-ap `(< ,Y ,X) mfc state)))
      (if (and (consp contradictionp)
          (consp (car contradictionp))
          (consp (caar contradictionp))
          (consp (cdaar contradictionp))
          (equal (len (access poly contradictionp :parents)) 1))
        t
        nil))
    nil))

remove-weak-inequalitiestheorem

(defthm remove-weak-inequalities
  (implies (and (syntaxp (rewriting-goal-literal x mfc state))
      (syntaxp (remove-weak-inequalities-fn x y mfc state))
      (<= x y))
    (<= x y)))

remove-strict-inequalities-fnfunction

(defun remove-strict-inequalities-fn
  (x y mfc state)
  (declare (xargs :guard t))
  (if (eq (present-in-hyps `(< ,X ,Y) (mfc-clause mfc)) 'negative)
    (let ((contradictionp (mfc-ap `(not (< ,X ,Y)) mfc state)))
      (if (and (consp contradictionp)
          (consp (car contradictionp))
          (consp (caar contradictionp))
          (consp (cdaar contradictionp))
          (equal (len (access poly contradictionp :parents)) 1))
        t
        nil))
    nil))

remove-strict-inequalitiestheorem

(defthm remove-strict-inequalities
  (implies (and (syntaxp (rewriting-goal-literal x mfc state))
      (syntaxp (remove-strict-inequalities-fn x y mfc state))
      (< x y))
    (< x y)))