unit-propagation-correct

(in-package "LRAT")

(include-book "truth-monotone")

(include-book "unit-propagation-monotone")

(include-book "unit-propagation-implies-unsat")

(defthm not-conflicting-literalsp-implies-negate-is-not-member
  (implies (and (member lit a)
      (not (conflicting-literalsp a))
      (literal-listp a))
    (not (member (negate lit) a))))

(defthm not-conflicting-literalsp-implies-negate-is-not-member-subset
  (implies (and (subsetp a1 a2)
      (member lit a2)
      (not (conflicting-literalsp a2))
      (literal-listp a2))
    (not (member (negate lit) a1))))

(defthm subsetp-union-equal-2
  (implies (subsetp x z)
    (subsetp x (union$ y z))))

(defthm not-conflicting-literalsp-subsetp
  (implies (and (subsetp a1 a2)
      (literal-listp a2)
      (not (conflicting-literalsp a2)))
    (not (conflicting-literalsp a1))))

(defthm union-preserves-subsetp-2
  (implies (subsetp y z)
    (subsetp (union$ x y)
      (union$ x z))))

(defthm conflicting-literalsp-preserved-by-union-equal-cons-2
  (implies (and (not (conflicting-literalsp (union$ a1 a2)))
      (literalp lit)
      (not (member (negate lit) a1))
      (not (member (negate lit) a2)))
    (not (conflicting-literalsp (union$ a1 (cons lit a2))))))

(defthm conflicting-literalsp-union-when-member
  (implies (and (literal-listp a1)
      (not (conflicting-literalsp a1))
      (literal-listp a2)
      (not (conflicting-literalsp a2))
      (member lit a1))
    (iff (conflicting-literalsp (union-equal a1 (cons lit a2)))
      (conflicting-literalsp (union-equal a1 a2))))
  :hints (("Goal" :induct (union-equal a1 a2)
     :restrict ((not-conflicting-literalsp-implies-negate-is-not-member-subset ((a2 (union-equal (cdr a1)
             (cons (car a1) a2))))) (not-conflicting-literalsp-subsetp ((a2 (union-equal (cdr a1)
              (cons (car a1) a2)))))))))

(encapsulate nil
  (local (defthm evaluate-clause-union-equal-cons-2
      (implies (and (not (member-equal lit clause))
          (equal (evaluate-clause clause
              (union-equal assignment
                (cons lit y)))
            t))
        (equal (evaluate-clause clause
            (union-equal assignment y))
          t))))
  (local (defthm not-conflicting-literalsp-union-lemma
      (implies (and (literal-listp clause)
          (literal-listp y)
          (not (conflicting-literalsp clause))
          (not (conflicting-literalsp (union-equal assignment y)))
          (not (equal (evaluate-clause clause
                (union-equal assignment y))
              t)))
        (not (conflicting-literalsp (union-equal assignment
              (negate-clause-or-assignment-rec clause y)))))))
  (local (defthm evaluate-clause-union-equal-nil
      (equal (evaluate-clause clause
          (union-equal x nil))
        (evaluate-clause clause x))))
  (local (defthm conflicting-literalsp-union-equal-nil
      (iff (conflicting-literalsp (union-equal x nil))
        (conflicting-literalsp x))))
  (defthm not-conflicting-literalsp-union
    (implies (and (literal-listp clause)
        (not (conflicting-literalsp clause))
        (not (conflicting-literalsp assignment))
        (not (equal (evaluate-clause clause assignment)
            t)))
      (not (conflicting-literalsp (union-equal assignment
            (negate-clause-or-assignment clause)))))
    :hints (("Goal" :in-theory (enable negate-clause-or-assignment)))))

(defthm clause-or-assignment-p-union
  (implies (and (clause-or-assignment-p clause)
      (clause-or-assignment-p assignment)
      (not (equal (evaluate-clause clause assignment)
          t)))
    (clause-or-assignment-p (union$ assignment
        (negate-clause-or-assignment clause))))
  :hints (("Goal" :in-theory (enable clause-or-assignment-p))))

(defthm subsetp-union-1
  (subsetp x (union$ x y)))

(defthm unit-propagation-correct-1
  (implies (formula-truep formula assignment)
    (formula-truep formula
      (union$ assignment
        (negate-clause-or-assignment clause))))
  :hints (("Goal" :restrict ((truth-monotone ((a1 assignment))))))
  :rule-classes nil)

(defthm unit-propagation-correct-2
  (implies (and (formula-p formula)
      (clause-or-assignment-p clause)
      (clause-or-assignment-p assignment)
      (equal (unit-propagation formula
          indices
          (negate-clause-or-assignment clause))
        t)
      (not (equal (evaluate-clause clause assignment)
          t)))
    (equal (unit-propagation formula
        indices
        (union$ assignment
          (negate-clause-or-assignment clause)))
      t))
  :rule-classes nil)

(defthm unit-propagation-correct
  (implies (and (formula-p formula)
      (clause-or-assignment-p clause)
      (clause-or-assignment-p assignment)
      (formula-truep formula assignment)
      (equal (unit-propagation formula
          indices
          (negate-clause-or-assignment clause))
        t))
    (equal (evaluate-clause clause assignment)
      t))
  :hints (("Goal" :do-not-induct t
     :use (unit-propagation-correct-1 unit-propagation-correct-2)
     :in-theory (disable formula-p subsetp-union-equal-2))))