• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
      • Type-prescription
      • Rewrite
      • Meta
      • Linear
      • Definition
      • Clause-processor
        • Meta-extract
          • Def-meta-extract
          • Fn-get-def
        • Set-skip-meta-termp-checks
        • Make-summary-data
        • Clause-processor-tools
        • Set-skip-meta-termp-checks!
      • Tau-system
      • Forward-chaining
      • Equivalence
      • Congruence
      • Free-variables
      • Executable-counterpart
      • Induction
      • Type-reasoning
      • Compound-recognizer
      • Rewrite-quoted-constant
      • Elim
      • Well-founded-relation-rule
      • Built-in-clause
      • Well-formedness-guarantee
      • Patterned-congruence
      • Rule-classes-introduction
      • Guard-holders
      • Refinement
      • Type-set-inverter
      • Generalize
      • Corollary
      • Induction-heuristics
      • Backchaining
      • Default-backchain-limit
    • Proof-builder
    • Recursion-and-induction
    • Hons-and-memoization
    • Events
    • Parallelism
    • History
    • Programming
    • Operational-semantics
    • Real
    • Start-here
    • Debugging
    • Miscellaneous
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Meta-extract

Def-meta-extract

Generate macros and theorems convenient for using meta-extract with a given evaluator.

Using the meta-extract feature in proofs of meta rules and clause processors is fairly inconvenient when starting from scratch. Def-meta-extract generates a set of theorems for a given evaluator that are a more convenient starting point for reasoning about meta-extract.

Usage:

(defevaluator mx-ev mx-ev-lst
  ((typespec-check ts x)
   (if a b c)
   (equal a b)
   (not a)
   (iff a b)
   (implies a b)
   ...))   ;; other functions as needed for the application

(def-meta-extract mx-ev mx-ev-lst)

We will use the above invocation on mx-ev as an example; def-meta-extract should be applicable to any evaluator that supports the six functions listed in the defevaluator form above.

The above invocation of def-meta-extract produces two macros that expand to well-formed meta-extract hypotheses:

(mx-ev-meta-extract-contextual-facts a :mfc mfc :state state)
(mx-ev-meta-extract-global-facts :state state)

(Note: The keyword arguments listed default to the variable names mfc and state, which are usually the right arguments.)

The exact meta-extract hypotheses produced use a bad-guy function as the obj argument to the meta-extract function, and for the global macro, for the st argument to meta-extract-global-fact+, so that they effectively universally quantify them, as shown by the following two theorems:

Theorem: mx-ev-meta-extract-contextual-badguy-sufficient

(defthm mx-ev-meta-extract-contextual-badguy-sufficient
  (implies (mx-ev-meta-extract-contextual-facts a)
           (mx-ev (meta-extract-contextual-fact obj mfc state)
                  a)))

Theorem: mx-ev-meta-extract-global-badguy-sufficient

(defthm mx-ev-meta-extract-global-badguy-sufficient
  (implies (mx-ev-meta-extract-global-facts)
           (mx-ev (meta-extract-global-fact+ obj st state)
                  a)))

However, def-meta-extract proves several theorems for the given evaluator so that the user doesn't need to reason directly about invocations of meta-extract-contextual-fact and meta-extract-global-fact+. For example, to show that an invocation of meta-extract-formula is true under mx-ev, you could prove:

(implies (and (mx-ev (meta-extract-global-fact+ (list :formula name) st state) a)
              (equal (w st) (w state)))
         (mx-ev (meta-extract-formula name st) a))

But the following theorem proved by def-meta-extract obviates the need to reason directly about meta-extract-global-fact+ and provide the correct obj = (list :formula name) in this manner:

(implies (and (mx-ev-meta-extract-global-facts)
              (equal (w st) (w state)))
         (mx-ev (meta-extract-formula name st) a))

(Note: st, the state from which the formula is extracted, and state, the original state on which the metafunction or clause processor was invoked, may differ in the case of a clause processor because the clause processor can update state. As long as the w field (holding the ACL2 logical world) of the state is not updated, global facts can still be extracted from the state and assumed correct.)

List of theorems proved by def-meta-extract

Typset reasoning with mfc-ts

The following theorem allows the user to conclude that a typeset returned by mfc-ts correctly describes the type of a term:

Theorem: mx-ev-meta-extract-typeset

(defthm mx-ev-meta-extract-typeset
  (implies (mx-ev-meta-extract-contextual-facts a)
           (typespec-check (mfc-ts term mfc state :forcep nil)
                           (mx-ev term a)))
  :rule-classes ((:rewrite)))

Rewriting with mfc-rw and under substitution with mfc-rw+

The following six theorems allow the user to conclude that a call of mfc-rw returns an equivalent term, or that a call of mfc-rw+ returns a term equivalent to the substitution of alist into term, with the equivalence given by the equiv-info argument provided (nil for equality, t for iff, or the name of an equivalence relation):

Theorem: mx-ev-meta-extract-rw-equal

(defthm mx-ev-meta-extract-rw-equal
  (implies (mx-ev-meta-extract-contextual-facts a)
           (equal (mx-ev (mfc-rw term obj nil mfc state
                                 :forcep nil)
                         a)
                  (mx-ev (sublis-var nil term) a)))
  :rule-classes ((:rewrite)))

Theorem: mx-ev-meta-extract-rw-iff

(defthm mx-ev-meta-extract-rw-iff
  (implies (mx-ev-meta-extract-contextual-facts a)
           (iff (mx-ev (mfc-rw term obj t mfc state
                               :forcep nil)
                       a)
                (mx-ev (sublis-var nil term) a)))
  :rule-classes ((:rewrite)))

Theorem: mx-ev-meta-extract-rw-equiv

(defthm mx-ev-meta-extract-rw-equiv
  (implies (and (mx-ev-meta-extract-contextual-facts a)
                equiv (not (equal equiv t))
                (symbolp equiv)
                (getprop equiv 'coarsenings
                         nil 'current-acl2-world
                         (w state)))
           (mx-ev (cons equiv
                        (cons (sublis-var nil term)
                              (cons (mfc-rw term obj equiv mfc state
                                            :forcep nil)
                                    'nil)))
                  a))
  :rule-classes ((:rewrite)))

Theorem: mx-ev-meta-extract-rw+-equal

(defthm mx-ev-meta-extract-rw+-equal
  (implies (mx-ev-meta-extract-contextual-facts a)
           (equal (mx-ev (mfc-rw+ term alist obj nil mfc state
                                  :forcep nil)
                         a)
                  (mx-ev (sublis-var alist term) a)))
  :rule-classes ((:rewrite)))

Theorem: mx-ev-meta-extract-rw+-iff

(defthm mx-ev-meta-extract-rw+-iff
  (implies (mx-ev-meta-extract-contextual-facts a)
           (iff (mx-ev (mfc-rw+ term alist obj t mfc state
                                :forcep nil)
                       a)
                (mx-ev (sublis-var alist term) a)))
  :rule-classes ((:rewrite)))

Theorem: mx-ev-meta-extract-rw+-equiv

(defthm mx-ev-meta-extract-rw+-equiv
 (implies
    (and (mx-ev-meta-extract-contextual-facts a)
         equiv (not (equal equiv t))
         (symbolp equiv)
         (getprop equiv 'coarsenings
                  nil 'current-acl2-world
                  (w state)))
    (mx-ev (cons equiv
                 (cons (sublis-var alist term)
                       (cons (mfc-rw+ term alist obj equiv mfc state
                                      :forcep nil)
                             'nil)))
           a))
 :rule-classes ((:rewrite)))

Detecting linear arithmetic contradictions with mfc-ap

The following theorem allows the user to conclude that a term is false under the given environment a when mfc-ap returns t indicating a linear arithmetic contradiction:

Theorem: mx-ev-meta-extract-mfc-ap

(defthm mx-ev-meta-extract-mfc-ap
  (implies (and (mx-ev-meta-extract-contextual-facts a)
                (mx-ev term a))
           (not (mfc-ap term mfc state :forcep nil)))
  :rule-classes ((:rewrite)))

Proving terms true with mfc-relieve-hyp

Theorem: mx-ev-meta-extract-relieve-hyp

(defthm mx-ev-meta-extract-relieve-hyp
  (implies
       (and (mx-ev-meta-extract-contextual-facts a)
            (not (mx-ev (sublis-var alist hyp) a)))
       (not (mfc-relieve-hyp hyp alist rune target bkptr mfc state
                             :forcep nil)))
  :rule-classes ((:rewrite)))

Looking up formulas by name using meta-extract-formula

(Note: meta-extract-formula can be used to look up a theorem, definition of a defined function, or constraint of a constrained function.)

Theorem: mx-ev-meta-extract-formula

(defthm mx-ev-meta-extract-formula
  (implies (and (mx-ev-meta-extract-global-facts)
                (equal (w st) (w state)))
           (mx-ev (meta-extract-formula name st)
                  a))
  :rule-classes ((:rewrite)))

Looking up rewrite rules from a lemmas property

The following two theorems conclude that a rewrite rule extracted from a function's lemmas property is valid (the second somewhat more explicitly than the first):

Theorem: mx-ev-meta-extract-lemma-term

(defthm mx-ev-meta-extract-lemma-term
  (implies (and (mx-ev-meta-extract-global-facts)
                (member rule (fgetprop fn 'lemmas nil (w st)))
                (equal (w st) (w state)))
           (mx-ev (rewrite-rule-term rule) a))
  :rule-classes ((:rewrite)))

Theorem: mx-ev-meta-extract-lemma

(defthm mx-ev-meta-extract-lemma
  (implies (and (mx-ev-meta-extract-global-facts)
                (member rule (fgetprop fn 'lemmas nil (w st)))
                (not (eq (access rewrite-rule rule :subclass)
                         'meta))
                (mx-ev (conjoin (access rewrite-rule rule :hyps))
                       a)
                (equal (w st) (w state)))
           (mx-ev (cons (access rewrite-rule rule :equiv)
                        (cons (access rewrite-rule rule :lhs)
                              (cons (access rewrite-rule rule :rhs)
                                    'nil)))
                  a))
  :rule-classes ((:rewrite)))

Calling a function with magic-ev-fncall

Theorem: mx-ev-meta-extract-fncall

(defthm mx-ev-meta-extract-fncall
  (mv-let (erp val)
          (magic-ev-fncall fn arglist st t nil)
    (implies (and (mx-ev-meta-extract-global-facts)
                  (equal (w st) (w state))
                  (not erp)
                  (logicp fn (w st)))
             (equal val
                    (mx-ev (cons fn (kwote-lst arglist))
                           nil))))
  :rule-classes ((:rewrite)))

Evaluating a term with magic-ev or termlist with magic-ev-lst

Theorem: mx-ev-meta-extract-magic-ev

(defthm mx-ev-meta-extract-magic-ev
  (mv-let (erp val)
          (magic-ev x alist st hard-errp aokp)
    (implies (and (mx-ev-meta-extract-global-facts)
                  (equal (w st) (w state))
                  (not erp)
                  (equal hard-errp t)
                  (equal aokp nil)
                  (pseudo-termp x))
             (equal val (mx-ev x alist))))
  :rule-classes ((:rewrite)))

Theorem: mx-ev-meta-extract-magic-ev-lst

(defthm mx-ev-meta-extract-magic-ev-lst
  (mv-let (erp val)
          (magic-ev-lst x alist st hard-errp aokp)
    (implies (and (mx-ev-meta-extract-global-facts)
                  (equal (w st) (w state))
                  (not erp)
                  (equal hard-errp t)
                  (equal aokp nil)
                  (pseudo-term-listp x))
             (equal val (mx-ev-lst x alist))))
  :rule-classes ((:rewrite)))

Looking up a function definition with fn-get-def

The following theorem allows a function call to be expaneded to its body when the function definition is successfully looked up in the world with fn-get-def. Note: The term (mv-nth 0 (fn-get-def ...)) indicating success of the fn-get-def call is rewritten to the call of fn-check-def:

Theorem: mx-ev-meta-extract-fn-check-def

(defthm mx-ev-meta-extract-fn-check-def
  (implies (and (fn-check-def fn st formals body)
                (mx-ev-meta-extract-global-facts)
                (equal (w st) (w state))
                (equal (len args) (len formals)))
           (equal (mx-ev (cons fn args) a)
                  (mx-ev body
                         (pairlis$ formals (mx-ev-lst args a)))))
  :rule-classes ((:rewrite)))

Technical lemmas about pairing formals with actuals

The following three theorems may help in reasoning about expansions of function calls and lambdas:

Theorem: mx-ev-lst-of-pairlis

(defthm mx-ev-lst-of-pairlis
  (implies (and (no-duplicatesp keys)
                (symbol-listp keys)
                (not (member nil keys)))
           (equal (mx-ev-lst keys (pairlis$ keys vals))
                  (take (len keys) vals)))
  :rule-classes ((:rewrite)))

Theorem: mx-ev-lst-of-pairlis-append-rest

(defthm mx-ev-lst-of-pairlis-append-rest
 (implies (and (no-duplicatesp keys)
               (symbol-listp keys)
               (not (member nil keys)))
          (equal (mx-ev-lst keys (append (pairlis$ keys vals) rest))
                 (take (len keys) vals)))
 :rule-classes ((:rewrite)))

Theorem: mx-ev-lst-of-pairlis-append-head-rest

(defthm mx-ev-lst-of-pairlis-append-head-rest
 (implies (and (no-duplicatesp keys)
               (alistp head)
               (not (intersectp keys (strip-cars head)))
               (symbol-listp keys)
               (not (member nil keys)))
          (equal (mx-ev-lst keys
                            (append head (pairlis$ keys vals) rest))
                 (take (len keys) vals)))
 :rule-classes ((:rewrite)))