Well-founded-relation-rule
Show that a relation is well-founded on a set
See rule-classes for a general discussion of rule classes,
including how they are used to build rules from formulas and a discussion of
the various keywords in a rule class description.
Example:
(defthm lex2p-is-well-founded-relation
(and (implies (pairp x) (o-p (ordinate x)))
(implies (and (pairp x)
(pairp y)
(lex2p x y))
(o< (ordinate x) (ordinate y))))
:rule-classes :well-founded-relation)
The example above creates a :well-founded-relation rule, where of
course the functions pairp, lex2p, and ordinate would have to
be defined first. It establishes that lex2p is a well-founded relation
on pairps. We explain and give details below.
Exactly two general forms are recognized:
General Forms
(AND (IMPLIES (mp x) (O-P (fn x))) ; Property 1
(IMPLIES (AND (mp x) ; Property 2
(mp y)
(rel x y))
(O< (fn x) (fn y)))),
or
(AND (O-P (fn x)) ; Property 1
(IMPLIES (rel x y) ; Property 2
(O< (fn x) (fn y))))
where mp, fn, and rel are function symbols, x and
y are distinct variable symbols, and no other :well-founded-relation
theorem about fn has been proved. When the second general form is used,
we act as though the first form were used with mp being the function that
ignores its argument and returns t. The discussion below therefore
considers only the first general form.
Note: We are very rigid when checking that the submitted formula is of one
of these forms. For example, in the first form, we insist that all the
conjuncts appear in the order shown above. Thus, interchanging the two
properties in the top-level conjunct or rearranging the hypotheses in the
second conjunct both produce unrecognized forms. The requirement that each
fn be proved well-founded at most once ensures that for each well-founded
relation, fn, there is a unique mp that recognizes the domain on
which rel is well-founded. We impose this requirement simply so that
rel can be used as a short-hand when specifying the well-founded
relations to be used in definitions; otherwise the specification would have to
indicate which mp was to be used.
We also insist that the new ordering be embedded into the ordinals as
handled by o-p and o< and not some into previously admitted
user-defined well-founded set and relation. This restriction should pose no
hardship. If mp and rel were previously shown to be well-founded
via the embedding fn, and you know how to embed some new set and relation
into mp and rel, then by composing fn with your new embedding
and using the previously proved well-founded relation lemma you can embed the
new set and relation into the ordinals.
Mp is a predicate that recognizes the objects that are supposedly
ordered in a well-founded way by rel. We call such an object an
``mp-measure'' or simply a ``measure'' when mp is understood.
Property 1 tells us that every measure can be mapped into an ACL2 ordinal.
(See o-p.) This mapping is performed by fn. Property 2 tells us
that if the measure x is smaller than the measure y according to
rel then the image of x under fn is a smaller than that of
y, according to the well-founded relation o<. (See o<.)
Thus, the general form of a :well-founded-relation formula establishes
that there exists a rel-order preserving embedding (namely via fn)
of the mp-measures into the ordinals. We can thus conclude that rel
is well-founded on mp-measures.
Such well-founded relations are used in the admissibility test for
recursive functions, in particular, to show that the recursion terminates. To
illustrate how such information may be used, consider a generic function
definition
(defun g (x) (if (test x) (g (step x)) (base x))).
If rel has been shown to be well-founded on mp-measures, then
g's termination can be ensured by finding a measure, (m x), with the
property that m produces a measure:
(mp (m x)), ; Defun-goal-1
and that the argument to g gets smaller (when measured by m and
compared by rel) in the recursion,
(implies (test x) (rel (m (step x)) (m x))). ; Defun-goal-2
If rel is selected as the :well-founded-relation to be used in
the definition of g, the definitional principal will generate and attempt
to prove defun-goal-1 and defun-goal-2 to justify g. We show
later why these two goals are sufficient to establish the termination of
g. Observe that neither the ordinals nor the embedding, fn, of the
mp-measures into the ordinals is involved in the goals generated by the
definitional principal.
Suppose now that a :well-founded-relation theorem has been proved for
mp and rel. How can rel be ``selected as the
:well-founded-relation'' by defun? There are two ways. First,
an xargs keyword to the defun event allows the specification
of a :well-founded-relation. Thus, the definition of g above might
be written
(defun g (x)
(declare (xargs :well-founded-relation rel))
(if (test x) (g (step x)) (base x)))
Alternatively, rel may be specified as the
:default-well-founded-relation in ACL2-defaults-table by
executing the event
(set-well-founded-relation rel).
When a defun event does not explicitly specify the relation in its
xargs the default relation is used. When ACL2 is initialized, the
default relation is o<.
Finally, though it is probably obvious, we now show that defun-goal-1
and defun-goal-2 are sufficient to ensure the termination of g
provided property-1 and property-2 of mp and rel have been
proved. To this end, assume we have proved defun-goal-1 and
defun-goal-2 as well as property-1 and property-2 and we show
how to admit g under the primitive ACL2 definitional principal (i.e.,
using only the ordinals). In particular, consider the definition event
(defun g (x)
(declare (xargs :well-founded-relation o<
:measure (fn (m x))))
(if (test x) (g (step x)) (base x)))
Proof that g is admissible: To admit the definition of g above we
must prove
(o-p (fn (m x))) ; *1
and
(implies (test x) ; *2
(o< (fn (m (step x))) (fn (m x)))).
But *1 can be proved by instantiating property-1 to get
(implies (mp (m x)) (o-p (fn (m x)))),
and then relieving the hypothesis with defun-goal-1, (mp (m
x)).
Similarly, *2 can be proved by instantiating property-2 to get
(implies (and (mp (m (step x)))
(mp (m x))
(rel (m (step x)) (m x)))
(o< (fn (m (step x))) (fn (m x))))
and relieving the first two hypotheses by appealing to two instances of
defun-goal-1, thus obtaining
(implies (rel (m (step x)) (m x))
(o< (fn (m (step x))) (fn (m x)))).
By chaining this together with defun-goal-2,
(implies (test x)
(rel (m (step x)) (m x)))
we obtain *2. Q.E.D.
Subtopics
- Nat-list-<
- An alternate well-founded-relation that allows lists of naturals to
be used directly as measures.
