		Search-engine friendly clone of the ACL2 documentation.

Atc-function-and-loop-generation

Atc-gen-loop-measure-fn

Generate a measure function for a recursive target function.

Signature
(atc-gen-loop-measure-fn fn names-to-avoid state) → (mv event name formals updated-names-to-avoid)
Arguments: fn — Guard (symbolp fn).; names-to-avoid — Guard (symbol-listp names-to-avoid).
Returns: event — Type (pseudo-event-formp event).; name — Type (symbolp name).; formals — Type (symbol-listp formals).; updated-names-to-avoid — Type (symbol-listp updated-names-to-avoid), given (symbol-listp names-to-avoid).

The correctness theorem for a loop involves the measure of the loop function. The measure may be a complex term. An early version of ATC was using the measure terms directly in the generated theorems, but that caused proof failures sometimes, due to ACL2 sometimes modifying those measure terms during a proof (e.g. due to equalities involving measure subterms arising from case analyses): after the terms were modified, some of the generated theorems about the measure terms no longer apply, making the proof fail. Thus, we ``protect'' the measure terms from modifications by generating functions for them, and using those functions in the generated theorems.

The code of this ACL2 function generates a measure function for the recursive target function fn. The funcion is not guard-verified, because its is only logical. It is important that we take, as formal parameters of the generated measure function, only the variables that occur in the measure term. This facilitates the generation of the loop function's termination theorem expressed over the generated measure function.

Definitions and Theorems

Function: atc-gen-loop-measure-fn

(defun atc-gen-loop-measure-fn (fn names-to-avoid state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (and (symbolp fn)
                              (symbol-listp names-to-avoid))))
  (declare (xargs :guard (irecursivep+ fn (w state))))
  (let ((__function__ 'atc-gen-loop-measure-fn))
    (declare (ignorable __function__))
    (b* ((wrld (w state))
         (name (packn-pos (list 'measure-of- fn) fn))
         ((mv name names-to-avoid)
          (fresh-logical-name-with-$s-suffix name 'function
                                             names-to-avoid wrld))
         ((when (eq name 'quote))
          (raise "Internal error: name is QUOTE.")
          (mv '(_) nil nil nil))
         (measure-term (measure+ fn wrld))
         (measure-vars (all-vars measure-term))
         ((mv & event)
          (evmac-generate-defun
               name
               :formals measure-vars
               :body (untranslate$ measure-term nil state)
               :verify-guards nil
               :enable nil)))
      (mv event
          name measure-vars names-to-avoid))))

Theorem: pseudo-event-formp-of-atc-gen-loop-measure-fn.event

(defthm pseudo-event-formp-of-atc-gen-loop-measure-fn.event
  (b* (((mv acl2::?event
            ?name ?formals ?updated-names-to-avoid)
        (atc-gen-loop-measure-fn fn names-to-avoid state)))
    (pseudo-event-formp event))
  :rule-classes :rewrite)

Theorem: symbolp-of-atc-gen-loop-measure-fn.name

(defthm symbolp-of-atc-gen-loop-measure-fn.name
  (b* (((mv acl2::?event
            ?name ?formals ?updated-names-to-avoid)
        (atc-gen-loop-measure-fn fn names-to-avoid state)))
    (symbolp name))
  :rule-classes :rewrite)

Theorem: symbol-listp-of-atc-gen-loop-measure-fn.formals

(defthm symbol-listp-of-atc-gen-loop-measure-fn.formals
  (b* (((mv acl2::?event
            ?name ?formals ?updated-names-to-avoid)
        (atc-gen-loop-measure-fn fn names-to-avoid state)))
    (symbol-listp formals))
  :rule-classes :rewrite)

Theorem: symbol-listp-of-atc-gen-loop-measure-fn.updated-names-to-avoid

(defthm
     symbol-listp-of-atc-gen-loop-measure-fn.updated-names-to-avoid
  (implies (symbol-listp names-to-avoid)
           (b* (((mv acl2::?event
                     ?name ?formals ?updated-names-to-avoid)
                 (atc-gen-loop-measure-fn fn names-to-avoid state)))
             (symbol-listp updated-names-to-avoid)))
  :rule-classes :rewrite)

Theorem: atc-gen-loop-measure-fn-name-not-quote

(defthm atc-gen-loop-measure-fn-name-not-quote
  (b* (((mv acl2::?event
            ?name ?formals ?updated-names-to-avoid)
        (atc-gen-loop-measure-fn fn names-to-avoid state)))
    (not (equal name 'quote))))