trivial-ancestors-check

Included Books

top

other

(in-package "ACL2")

include-book

(include-book "xdoc/top" :dir :system)

local

(local (in-theory (disable mv-nth equal-mod-commuting)))

check-assumed-true-or-falsefunction

(defun check-assumed-true-or-false
  (lit lit-atm ancestors)
  (declare (xargs :guard (and (pseudo-termp lit)
        (pseudo-termp lit-atm)
        (ancestor-listp ancestors))))
  (cond ((endp ancestors) (mv nil nil))
    ((ancestor-binding-hyp-p (car ancestors)) (check-assumed-true-or-false lit lit-atm (cdr ancestors)))
    ((equal-mod-commuting lit
       (access ancestor (car ancestors) :lit)
       nil) (mv t t))
    ((equal-mod-commuting lit-atm
       (access ancestor (car ancestors) :atm)
       nil) (mv t nil))
    (t (check-assumed-true-or-false lit lit-atm (cdr ancestors)))))

check-assumed-true-or-false-oktheorem

(defthmd check-assumed-true-or-false-ok
  (mv-let (present true)
    (check-assumed-true-or-false lit lit-atm ancestors)
    (implies (and present true)
      (member-equal-mod-commuting lit
        (strip-ancestor-literals ancestors)
        nil))))

in-theory

(in-theory (disable check-assumed-true-or-false))

trivial-ancestors-checkfunction

(defun trivial-ancestors-check
  (lit ancestors tokens)
  (declare (xargs :guard (and (pseudo-termp lit)
        (ancestor-listp ancestors)
        (true-listp tokens)))
    (ignorable tokens))
  (cond ((endp ancestors) (mv nil nil))
    (t (mv-let (not-flg lit-atm)
        (strip-not lit)
        (declare (ignore not-flg))
        (check-assumed-true-or-false lit lit-atm ancestors)))))

trivial-ancestors-check-oktheorem

(defthmd trivial-ancestors-check-ok
  (mv-let (present true)
    (trivial-ancestors-check lit ancestors tokens)
    (implies (and present true)
      (member-equal-mod-commuting lit
        (strip-ancestor-literals ancestors)
        nil)))
  :hints (("Goal" :in-theory (enable check-assumed-true-or-false-ok))))

in-theory

(in-theory (disable trivial-ancestors-check))

local

(local (defattach (ancestors-check trivial-ancestors-check)
    :system-ok t
    :hints (("goal" :in-theory '(trivial-ancestors-check-ok)))))

use-trivial-ancestors-checkmacro

(defmacro use-trivial-ancestors-check
  nil
  '(local (defattach (ancestors-check trivial-ancestors-check)
      :system-ok t
      :hints (("goal" :in-theory '(trivial-ancestors-check-ok))))))

other

(defxdoc use-trivial-ancestors-check
  :short "Override ACL2's built-in ancestors check heuristic with a simpler and less surprising one."
  :parents (proof-automation)
  :long "<p>Usage: as an embeddable event,</p>

@({
 (include-book "tools/trivial-ancestors-check" :dir :system)
 (use-trivial-ancestors-check)
 })
<p>or</p>
@({
 (local (include-book "tools/trivial-ancestors-check" :dir :system))
 (local (use-trivial-ancestors-check)).
 })

<p>(Note: @('use-trivial-ancestors-check') expands to a local event, but you
can still wrap it in local, in which case the trivial-ancestors-check book may
be included locally.)</p>

<p>ACL2 has a heuristic called @('ancestors-check') which it uses to
prevent loops in backchaining during rewriting.  The @('ancestors'), in this
context, are the sequence of hyps we have backchained to in order to get to the
one we are currently trying to relieve.  Among other things, ACL2's built in
ancestors check decides whether the current hyp is more complicated than any
ancestral hyp, and gives up on backchaining if so.  Occasionally this can cause
a rewriting strategy to mysteriously fail to work.  Fortunately, ACL2 allows
its default ancestors check to be replaced by an attachment.</p>

<p>Running @('(use-trivial-ancestors-check)') replaces the default ancestors
check with one that does much less: it only checks whether the current hyp
occurs, exactly or negated, in the ancestors, and doesn't try to prevent
backchaining to more complicated hyps.</p>

<p>This could cause rewriting to fail due to a chain of increasingly
complicated hyps.  But when we tried replacing ACL2's default heuristic with
this new one, we only found a couple of examples in the regression where this
was the case, and these were due to (in our view) bad rules.  So in practice,
this seems to be fairly undisruptive.</p>")

other

(defpointer trivial-ancestors-check
  use-trivial-ancestors-check)