the guard proof obligation
Major Section:  OTHER

See verify-guards, and see guard for a discussion of guards. Also see verify-guards-formula for a utility provided for viewing the guard proof obligation, without proof. Guard-obligation is a lower level function for use in system programs, not typically appropriate for most ACL2 users. If you simply want to see the guard proof obligations, see verify-guards-formula.

Example Form:
(guard-obligation 'foo nil 'top-level state)
(guard-obligation '(if (consp x) (foo (car x)) t) nil 'my-function state)

General Forms:
(guard-obligation name guard-debug ctx state)
(guard-obligation term guard-debug ctx state)
where the first argument is either the name of a function or theorem or is a non-variable term that may be in untranslated form; guard-debug is typically nil but may be t (see guard-debug); ctx is a context (typically, a symbol used in error and warning messages); and state references the ACL2 state.

If you want to obtain the formula but you don't care about the so-called ``tag tree'':

(mv-let (erp val state)
        (guard-obligation x guard-debug 'top-level state)
        (if erp
           ( .. code for handling error case, e.g., name is undefined .. )
          (let ((cl-set (cadr val))) ; to be proved for guard verification
            ( .. code using cl-set, which is a list of clauses,
                 implicitly conjoined, each of which is viewed as
                 a disjunction .. ))))

The form (guard-obligation x guard-debug ctx state) evaluates to a triple (mv erp val state), where erp is nil unless there is an error, and state is the ACL2 state. Suppose erp is nil. Then val is the keyword :redundant if the corresponding verify-guards event would be redundant; see redundant-events. Otherwise, val is a tuple (list* names cl-set ttree), where: names is (cons :term xt) if x is not a variable, where xt is the translated form of x; and otherwise is a list containing x along with, if x is defined in a mutual-recursion, any other functions defined in the same mutual-recursion nest; cl-set is a list of lists of terms, viewed as a conjunction of clauses (each viewed (as a disjunction); and ttree is an assumption-free tag-tree that justifies cl-set. (The notion of ``tag-tree'' may probably be ignored except for system developers.)

Guard-obligation is typically used for function names or non-variable terms, but as for verify-guards, it may also be applied to theorem names.

See the source code for verify-guards-formula for an example of how to use guard-obligation.