		Search-engine friendly clone of the ACL2 documentation.

Boolean-assert-all

Boolean-assert-all-lifting

Lifting of the circuit to a predicate.

The shallowly embedded predicate is defined as the conjunction, for each value, of the predicate of the boolean-assert circuit.

To prove the lifting theorem, i.e. the correspondence with the deep embedding, first we prove a theorem about the constraints in the body. This is where the induction is facilitated by the construction that takes an arbitrary list of variables, as mentioned in boolean-assert-all-circuit-body. We induct simultaneously on the list of variables and list of values. It is important to assume that the list of variables has no duplicates, so that the omap built via omap::from-lists has no overwriting, and instead associates corresponding elements of the lists. To have a sufficient induction hypothesis, we need to generalize the theorem to a generic assignment asg, assumed to include at least the one built via omap::from-lists. The lifting theorem says that the list of recursively constructed constraints is satisfied iff the shallowly embedded boolean-assert-all predicate holds. We use the rule pfcs::constraint-satp-to-definition-satp to turn the satisfaction of each constraint into the satisfaction of the definition of the boolean-assert circuit, which lets us use the lifting theorem definition-satp-to-boolean-assert-pred for that circuit.

Using that theorem, we can prove the lifting theorem for the circuit. Note that we prove it for a generic number of variables n = (len xs), and we assume that the definitions defs include the definition of the circuit determined by that n as parameter. We can use the rule pfcs::constraint-relation-nofreevars-satp because the circuit has no free variables, so we don't need to deal with the existential quantification.

Definitions and Theorems

Function: boolean-assert-all-pred

(defun boolean-assert-all-pred (xs p)
  (or (endp xs)
      (and (boolean-assert-pred (car xs) p)
           (boolean-assert-all-pred (cdr xs) p))))

Theorem: constraint-list-satp-to-boolean-assert-all-circuit-body

(defthm constraint-list-satp-to-boolean-assert-all-circuit-body
 (implies
      (and (equal (pfcs::lookup-definition (pfname "boolean_assert")
                                           defs)
                  (boolean-assert-circuit))
           (primep prime)
           (name-listp xs-vars)
           (no-duplicatesp-equal xs-vars)
           (pfield::fe-listp xs-vals prime)
           (equal (len xs-vars) (len xs-vals))
           (pfcs::assignmentp asg)
           (pfcs::assignment-wfp asg prime)
           (omap::submap (omap::from-lists xs-vars xs-vals)
                         asg))
      (equal (pfcs::constraint-list-satp
                  (boolean-assert-all-circuit-body xs-vars)
                  defs asg prime)
             (boolean-assert-all-pred xs-vals prime))))

Theorem: definition-satp-to-boolean-assert-all

(defthm definition-satp-to-boolean-assert-all
 (implies
  (and
   (equal
     (pfcs::lookup-definition (pfname "boolean_assert_all" (len xs))
                              defs)
     (boolean-assert-all-circuit (len xs)))
   (equal (pfcs::lookup-definition (pfname "boolean_assert")
                                   defs)
          (boolean-assert-circuit))
   (primep prime)
   (pfield::fe-listp xs prime))
  (equal
       (pfcs::definition-satp (pfname "boolean_assert_all" (len xs))
                              defs xs prime)
       (boolean-assert-all-pred xs prime))))