Def-fgl-boolean-constraint
Define a rule that recognizes constraints among FGL generated Boolean variables
When using FGL in a term-level style FGL
may generate new Boolean variables from terms that appear as IF tests.
Sometimes, the terms from which these variables are generated have
interdependent meanings. For example, if Boolean variable a represents
(logbitp 5 x) and Boolean variable b represents (integerp x), it
should be impossible for a to be true when b is false. However, by
default, the Boolean variables generated this way are unconstrained. When
this sort of interdependency among variables exists but is not accounted for,
it can cause FGL to find false counterexamples.
Def-fgl-boolean-constraint provides a mechanism to make such constraints
known to FGL. While symbolically executing a form, FGL maintains a constraint, a
Boolean formula known to always be true (under the evolving assignment of
Boolean variables to terms). A constraint rule generated by
def-fgl-boolean-constraint is triggered when a Boolean variable is
generated from an IF condition term and can cause the constraint to be updated
with a new conjunct.
A Boolean constraint rule is formulated as follows:
(def-fgl-boolean-constraint fgl-logbitp-implies-integerp
:bindings ((bit (logbitp n x))
(intp (integerp x)))
:body (implies bit intp)
;; optional arguments:
:syntaxp ...
:hints ...)
This generates a proof obligation:
(defthm fgl-logbitp-implies-integerp
(let ((bit (fgl-bool-fix (logbitp n x)))
(intp (fgl-bool-fix (integerp x))))
(implies bit intp))
:hints ...
:rule-classes nil)
(The optional :hints argument to def-fgl-boolean-constraint provides the
hints for the proof obligation.)
Once this rule is established, FGL will generate constraints as follows:
- When a Boolean variable a is generated from an IF condition matching
(logbitp n x), FGL will search for an existing generated Boolean variable
b whose IF condition was (integerp x) and, if it exists, add the
constraint (implies a b).
- Conversely, when a Boolean variable b is generated from an IF
condition matching (integerp x), FGL will search for existing generated
Boolean variables ai matching (logbitp n x), and for each of them,
add the constraint (implies ai b).
To show that this rule works, you can verify that the following events fail
prior to introducing the constraint rule above, but succeed after:
(def-fgl-thm foo1
:hyp t
:concl (if (integerp x) t (not (logbitp n x)))
:g-bindings nil
:rule-classes nil)
(def-fgl-thm foo2
:hyp t
:concl (if (logbitp n x) (integerp x) t)
:g-bindings nil
:rule-classes nil)
