		Search-engine friendly clone of the ACL2 documentation.

Event-macro-applicability-condition-utilities

Evmac-appcond-theorem

Generate a theorem event for an applicability condition.

Signature
(evmac-appcond-theorem appcond hints names-to-avoid print ctx state) → (mv event thm-name new-hints updated-names-to-avoid)
Arguments: appcond — Guard (evmac-appcondp appcond).; hints — Guard (evmac-input-hints-p hints).; names-to-avoid — Guard (symbol-listp names-to-avoid).; print — Guard (evmac-input-print-p print).
Returns: event — Type (pseudo-event-formp event).; thm-name — Type (symbolp thm-name).; new-hints — Type (evmac-input-hints-p new-hints), given (evmac-input-hints-p hints).; updated-names-to-avoid — Type (symbol-listp updated-names-to-avoid), given (symbol-listp names-to-avoid).

We generate a name for the theorem that is not in the world and that is distinct from the given list of names to avoid; the latter are names not yet in the world, but are names of other events that will be added to the world together with this theorem, and that therefore must be all distinct. We return an updated list of names to avoid that includes the new name, so that future calls of this function, or of other event-generating code, can use the updated list to avoid conflicts with this new name. The new theorem name is also returned as a result as a convenience (it could be extracted from the returned event instead); the event macro may reference this name in generated proofs (see evmac-appcond-theorem-list for more discussion on this). The theorem name is the same as the keyword that names the applicability condition, if fresh, otherwise $ characters are appended to it until it is fresh. The theorem name is in the "ACL2" package, which seems like a good general choice; the event macro, or the application where the event macro is used, may be in an arbitrary package.

We untranslate the formula so that it is more readable if printed on the screen. The use of untranslate forces this function and its callers into program mode. An alternative could be to use a more limited, logic-mode untranslation.

If the event macro's hints are an alist from keywords to true lists, we extract the ones associated to the applicability conditions (if any, otherwise we get nil) and use those to prove the theorem; we also remove the pair from the alist, and return the updated alist. By threading the hints alist through calls of this functions, one for each applicability condition, at the end the event macro can detect if there were unused hints (e.g. for applicability conditions that were not actually present), and issue a warning or error in that case (see evmac-ensure-no-extra-hints). If the event macro's hints are not an alist from keywords to true lists, we use those in their entirety to prove the theorem, and we return them unchanged.

The theorem has no rule classes, because it is meant to be referenced in :use hints in proofs generated by the event macro. Not having rule classes avoids any restrictions on the formula, such as having a conclusion (equal var ...) for a rewrite rule.

The theorem is wrapped into try-event in order to provide a terser error message if the proof fails. This wrapping is not performed if :print is :all, to avoid the suppression of the error output done by try-event. This causes the print levels to be not quite ``monotonic'', in the sense that :print :all will not print the custom error message passed to try-event. This choice may be revisited at some point.

This function also takes a print specifier as input, meant to be one of the inputs of the event macro. This is used to determine whether events that show progress messages should be generated or not. Since this is a binary choice, the input of this function could be a boolean flag instead of a print specifier. However, having a print specifier makes things more modular (e.g. if print specifiers are extended with more options in the future). If an event macro does not have a print specifier input (perhaps yet), the caller of this function can still set one adequate to whether progress messages must be shown or not.

The returned event, which consists of the theorem and the optional show-progress events, is local (to the encapsulate that the event macro expands to). This is why the exact name of the theorem is not too important, so long as it is valid and does not clash with others. If an event macro should generate (some of) its applicability conditions as persistent events, the best course of action is to still use this function to generate local theorems with no rule classes, and then do another pass over such applicability conditions to generate non-local theorems with the same formulas, without hints (thus keeping the history ``clean'') and with the desired names and rule classes. These non-local theorems can be easily proved via :by hints: to avoid their appearance in the history, the theorems with the desired names can be introduced twice, once locally with the :by hints, and once non-locally and redundantly without hints. Perhaps there should be a utility to do this, if the task becomes common among event macros.

So this function generates a little more than just a theorem event, because of the surrounding things generated. However, those surrounding things are auxiliary: it is still, mainly, a theorem event.

Definitions and Theorems

Function: evmac-appcond-theorem

(defun evmac-appcond-theorem
       (appcond hints names-to-avoid print ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (evmac-appcondp appcond)
                             (evmac-input-hints-p hints)
                             (symbol-listp names-to-avoid)
                             (evmac-input-print-p print))))
 (let ((__function__ 'evmac-appcond-theorem))
  (declare (ignorable __function__))
  (b*
   ((wrld (w state))
    ((evmac-appcond appcond) appcond)
    ((mv thm-name updated-names-to-avoid)
     (fresh-logical-name-with-$s-suffix
          (intern-in-package-of-symbol (symbol-name appcond.name)
                                       (pkg-witness "ACL2"))
          nil names-to-avoid wrld))
    (thm-formula (untranslate$ appcond.formula t state))
    ((mv thm-hints new-hints)
     (if (keyword-truelist-alistp hints)
         (mv (cdr (assoc-eq appcond.name hints))
             (remove-assoc-eq appcond.name hints))
       (mv hints hints)))
    (thm-event
     (cons
      'defthm
      (cons
       thm-name
       (cons
           thm-formula
           (cons ':rule-classes
                 (cons 'nil
                       (and thm-hints (list :hints thm-hints))))))))
    (error-msg
     (msg
       "The proof of the ~x0 applicability condition fails:~%~X12~|"
       appcond.name thm-formula nil))
    (try?-thm-event (if (eq print :all)
                        thm-event
                      (try-event thm-event ctx t nil error-msg)))
    (show-progress-p (member-eq print '(:info :all)))
    (progress-start?
     (and
      show-progress-p
      (cons
       (cons
        'cw-event
        (cons
         '"~%Attempting to prove the ~x0 ~
                                 applicability condition:~%~X12~|"
         (cons (cons 'quote (cons appcond.name 'nil))
               (cons (cons 'quote (cons thm-formula 'nil))
                     '(nil)))))
       'nil)))
    (progress-end? (and show-progress-p
                        '((cw-event "Done.~%"))))
    (event
     (cons 'local
           (cons (cons 'progn
                       (append progress-start?
                               (cons try?-thm-event progress-end?)))
                 'nil))))
   (mv event thm-name
       new-hints updated-names-to-avoid))))

Theorem: pseudo-event-formp-of-evmac-appcond-theorem.event

(defthm pseudo-event-formp-of-evmac-appcond-theorem.event
  (b*
    (((mv ?event ?thm-name
          ?new-hints ?updated-names-to-avoid)
      (evmac-appcond-theorem appcond
                             hints names-to-avoid print ctx state)))
    (pseudo-event-formp event))
  :rule-classes :rewrite)

Theorem: symbolp-of-evmac-appcond-theorem.thm-name

(defthm symbolp-of-evmac-appcond-theorem.thm-name
  (b*
    (((mv ?event ?thm-name
          ?new-hints ?updated-names-to-avoid)
      (evmac-appcond-theorem appcond
                             hints names-to-avoid print ctx state)))
    (symbolp thm-name))
  :rule-classes :rewrite)

Theorem: evmac-input-hints-p-of-evmac-appcond-theorem.new-hints

(defthm evmac-input-hints-p-of-evmac-appcond-theorem.new-hints
 (implies
   (evmac-input-hints-p hints)
   (b*
    (((mv ?event ?thm-name
          ?new-hints ?updated-names-to-avoid)
      (evmac-appcond-theorem appcond
                             hints names-to-avoid print ctx state)))
    (evmac-input-hints-p new-hints)))
 :rule-classes :rewrite)

Theorem: symbol-listp-of-evmac-appcond-theorem.updated-names-to-avoid

(defthm symbol-listp-of-evmac-appcond-theorem.updated-names-to-avoid
 (implies
   (symbol-listp names-to-avoid)
   (b*
    (((mv ?event ?thm-name
          ?new-hints ?updated-names-to-avoid)
      (evmac-appcond-theorem appcond
                             hints names-to-avoid print ctx state)))
    (symbol-listp updated-names-to-avoid)))
 :rule-classes :rewrite)