show why a rule's pattern and the :target do not match

When a near miss break occurs (see `monitor`) the user
sees a message like this:

(1 Breaking (:REWRITE LEMMA) on (F (G A B) A '(A B C D ...)): The pattern in this rule failed to match the target. However, this is considered a NEAR MISS under the break criteria, (:CONDITION 'T :ABSTRACTION ...), specified when this rule was monitored. The following criterion is satisfied. * The :ABSTRACTION pattern provided in your monitor, ..., matches :TARGET.

It can be difficult to determine why the pattern of the rule, e.g., the

Included among the `brr-commands` is the

But in a near miss break, the situation is as follows. The prover has
tried to apply a rule that has been monitored with a break criterion meaning
``cause an interactive break when the target term (the term to currently
being rewritten) satisfies this criterion but the triggering pattern of the
rule fails to match the target term.'' When inside the resulting break, the
target term is given by the `brr` command `rule-classes`). The triggering pattern of a `rewrite` rule — the most common class of rule — is the left-hand
side of the concluding equality and can be obtained from within the break by
typing the `brr` command `rewrite-quoted-constant` rule is its right-hand side, but as
explained in `rewrite-quoted-constant`, the `linear` rule is
displayed by the

To understand the answer you have to understand how the ACL2 matching
algorithm works. The matching algorithm is given two terms,

The

The message displays the pattern in question and the target term, but it
also displays a version of the pattern in which the first unmatchable subterm
is replaced by the expression

The message goes on to show the mismatched subterms from the pattern and
the target, the substitution that was computed to match everything up to

So, for example, suppose the rule's

The ACL2 match algorithm attempted to match :LHS with :TARGET by finding a substitution, s, such that :LHS/s = :TARGET. That attempt failed when trying to match the subterm of :LHS marked <pat> in :LHS' below. :LHS: (F X (G X Y) (H X)) :LHS': (F X (G <pat> Y) (H X)) :TARGET: (F A (G B A) (H A)) Below we show the substitution, s, computed prior to the failure; the subterm of :LHS we're calling <pat>; the instantiated subterm, <pat>/s; and the corresponding subterm, <tar>, of :TARGET. s: ((X A)) <pat>: X <pat>/s: A <tar>: B For the rewriter to get past this failure the match algorithm must be able to extend substitution s to s' so that <pat>/s' is equal to <tar> and our match algorithm could not find such an extension.

Note that the substitution

When `compare-objects` on those objects. It can be hard to spot
how two large constants differ and

The command

But note that

- (a) a variable in the pattern has already been bound in the substitution (i.e., bound earlier in the matching process) to a term that is not identical to the corresponding term in the target, or
- (b) a term in the pattern has a different function symbol than the corresponding term the target.

So do not expect the