REFINEMENT

record that one equivalence relation refines another
Major Section:  RULE-CLASSES

See rule-classes for a general discussion of rule classes and how they are used to build rules from formulas. An example :corollary formula from which a :refinement rule might be built is:

Example:
(implies (bag-equal x y) (set-equal y x)).
Also see defrefinement.

General Form:
(implies (equiv1 x y) (equiv2 x y))
Equiv1 and equiv2 must be known equivalence relations. The effect of such a rule is to record that equiv1 is a refinement of equiv2. This means that equiv1 :rewrite rules may be used while trying to maintain equiv2. See equivalence for a general discussion of the issues.

The macro form (defrefinement equiv1 equiv2) is an abbreviation for a defthm of rule-class :refinement that establishes that equiv1 is a refinement of equiv2. See defrefinement.

Suppose we have the :rewrite rule

(bag-equal (append a b) (append b a))
which states that append is commutative modulo bag-equality. Suppose further we have established that bag-equality refines set-equality. Then when we are simplifying append expressions while maintaining set-equality we use append's commutativity property, even though it was proved for bag-equality.

Equality is known to be a refinement of all equivalence relations. The transitive closure of the refinement relation is maintained, so if set-equality, say, is shown to be a refinement of some third sense of equivalence, then bag-equality will automatially be known as a refinement of that third equivalence.

:refinement lemmas cannot be disabled. That is, once one equivalence relation has been shown to be a refinement of another, there is no way to prevent the system from using that information. Of course, individual :rewrite rules can be disabled.

More will be written about this as we develop the techniques.













































































REWRITE

make some :rewrite rules (possibly conditional ones)
Major Section:  RULE-CLASSES

See rule-classes for a general discussion of rule classes and how they are used to build rules from formulas. Example :corollary formulas from which :rewrite rules might be built are:

Example:
(equal (+ x y) (+ y x))            replace (+ a b) by (+ b a) provided
                                   certain heuristics approve the
                                   permutation.

(implies (true-listp x) replace (append a nil) by a, if (equal (append x nil) x)) (true-listp a) rewrites to t

(implies replace (member a (append b c)) by (and (eqlablep e) (member a (append c b)) in contexts (true-listp x) in which propositional equivalence (true-listp y)) is sufficient, provided (eqlablep a) (iff (member e (append x y)) (true-listp b) and (true-listp c) (member e (append y x)))) rewrite to t and the permutative heuristics approve

General Form: (and ... (implies (and ...hi...) (implies (and ...hk...) (and ... (equiv lhs rhs) ...))) ...)

Note: One :rewrite rule class object might create many rewrite rules from the :corollary formula. To create the rules, we first translate the formula (expanding all macros; also see trans). Next, we eliminate all lambdas; one may think of this step as simply substituting away every let, let*, and mv-let in the formula. We then flatten the and and implies structure of the formula, transforming it into a conjunction of formulas, each of the form
(implies (and h1 ... hn) concl)
where no hypothesis is a conjunction and concl is neither a conjunction nor an implication. If necessary, the hypothesis of such a conjunct may be vacuous. We then further coerce each concl into the form (equiv lhs rhs), where equiv is a known equivalence relation, by replacing any concl not of that form by (iff concl t). A concl of the form (not term) is considered to be of the form (iff term nil). By these steps we reduce the given :corollary to a sequence of conjuncts, each of which is of the form
(implies (and h1 ... hn)
         (equiv lhs rhs))
where equiv is a known equivalence relation. See equivalence for a general discussion of the introduction of new equivalence relations.

We create a :rewrite rule for each such conjunct, if possible, and otherwise cause an error. It is possible to create a rewrite rule from such a conjunct provided lhs is not a variable, a quoted constant, a let-expression, a lambda application, or an if-expression.

A :rewrite rule is used when any instance of the lhs occurs in a context in which the equivalence relation is operative. First, we find a substitution that makes lhs equal to the target term. Then we attempt to relieve the instantiated hypotheses of the rule. Hypotheses that are fully instantiated are relieved by recursive rewriting. Hypotheses that contain ``free variables'' (variables not assigned by the unifying substitution) are relieved by attempting to guess a suitable instance so as to make the hypothesis equal to some known assumption in the context of the target. If the hypotheses are relieved, and certain restrictions that prevent some forms of infinite regress are met (see loop-stopper), the target is replaced by the instantiated rhs, which is then recursively rewritten.

At the moment, the best description of how ACL2 :rewrite rules are used may be found in the discussion of ``Replacement Rules'' pp 234 of A Computational Logic Handbook.













































































TYPE-PRESCRIPTION

make a rule that specifies the type of a term
Major Section:  RULE-CLASSES

See rule-classes for a general discussion of rule classes and how they are used to build rules from formulas. Some example :corollary formulas from which :type-prescription rules might be built are:

Examples:
(implies                           (nth n lst) is of type characterp
 (and (character-listp lst)        provided the two hypotheses can
      (< n (length lst)))          be established by type reasoning
 (characterp (nth n lst))).

(implies (demodulize a lst 'value ans) is (and (atom a) either a nonnegative integer or (true-listp lst) of the same type as ans, provided (member-equal a lst)) the hyps can be established by type (or (and reasoning (integerp (demodulize a lst 'value ans)) (>= (demodulize a lst 'value ans) 0)) (equal (demodulize a lst 'value ans) ans))).

To specify the term whose type (see type-set) is described by the rule, provide that term as the value of the :typed-term field of the rule class object.

General Form:
(implies hyps
         (or type-restriction1-on-pat
             ...
             type-restrictionk-on-pat
             (equal pat var1)
             ...
             (equal pat varj)))
where pat is the application of some function symbol to some arguments, each type-restrictioni-on-pat is a term involving pat and containing no variables outside of the occurrences of pat, and each vari is one of the variables of pat. Generally speaking, the type-restriction terms ought to be terms that inform us as to the type of pat. Ideally, they should be ``primitive recognizing expressions'' about pat; see compound-recognizer.

If the :typed-term is not provided in the rule class object, it is computed heuristically by looking for a term in the conclusion whose type is being restricted. An error is caused if no such term is found.

Roughly speaking, the effect of adding such a rule is to inform the ACL2 typing mechanism that pat has the type described by the conclusion, when the hypotheses are true. In particular, the type of pat is within the union of the types described by the several disjuncts. The ``type described by'' (equal pat vari) is the type of vari.

More operationally, when asked to determine the type of a term that is an instance of pat, ACL2 will first attempt to establish the hypotheses. This is done by type reasoning alone, not rewriting! Of course, if some hypothesis is to be forced, it is so treated; see force and see case-split. Provided the hypotheses are established by type reasoning, ACL2 then unions the types described by the type-restrictioni-on-pat terms together with the types of those subexpressions of pat identified by the vari. The final type computed for a term is the intersection of the types implied by each applicable rule. Type prescription rules may be disabled.

Because only type reasoning is used to establish the hypotheses of :type-prescription rules, some care must be taken with the hypotheses. Suppose, for example, that the non-recursive function my-statep is defined as

  (defun my-statep (x)
    (and (true-listp x)
         (equal (length x) 2)))
and suppose (my-statep s) occurs as a hypothesis of a :type-prescription rule that is being considered for use in the proof attempt for a conjecture with the hypothesis (my-statep s). Since the hypothesis in the conjecture is rewritten, it will become the conjunction of (true-listp s) and (equal (length s) 2). Those two terms will be assumed to have type t in the context in which the :type-prescription rule is tried. But type reasoning will be unable to deduce that (my-statep s) has type t in this context. Thus, either my-statep should be disabled (see disable) during the proof attempt or else the occurrence of (my-statep s) in the :type-prescription rule should be replaced by the conjunction into which it rewrites.

While this example makes it clear how non-recursive predicates can cause problems, non-recursive functions in general can cause problems. For example, if (mitigate x) is defined to be (if (rationalp x) (1- x) x) then the hypothesis (pred (mitigate s)) in the conjecture will rewrite, opening mitigate and splitting the conjecture into two subgoals, one in which (rationalp s) and (pred (1- x)) are assumed and the other in which (not (rationalp s)) and (pred x) are assumed. But (pred (mitigate s)) will not be typed as t in either of these contexts. The moral is: beware of non-recursive functions occuring in the hypotheses of :type-prescription rules.

Because of the freedom one has in forming the conclusion of a type-prescription, we have to use heuristics to recover the pattern, pat, whose type is being specified. In some cases our heuristics may not identify the intended term and the :type-prescription rule will be rejected as illegal because the conclusion is not of the correct form. When this happens you may wish to specify the pat directly. This may be done by using a suitable rule class token. In particular, when the token :type-prescription is used it means ACL2 is to compute pat with its heuristics; otherwise the token should be of the form (:type-prescription :typed-term pat), where pat is the term whose type is being specified.

The defun event may generate a :type-prescription rule. Suppose fn is the name of the function concerned. Then (:type-prescription fn) is the rune given to the type-prescription, if any, generated for fn by defun. (The trivial rule, saying fn has unknown type, is not stored, but defun still allocates the rune and the corollary of this rune is known to be t.)













































































TYPE-SET-INVERTER

exhibit a new decoding for an ACL2 type-set
Major Section:  RULE-CLASSES

See rule-classes for a general discussion of rule classes and how they are used to build rules from formulas.

Example Rule Class:
(:type-set-inverter 
  :corollary (equal (and (counting-number x) (not (equal x 0)))
                    (and (integerp x) (< x 0)))
  :type-set 2)

General Forms of Rule Class: :type-set-inverter, or (:type-set-inverter :type-set n)

General Form of Theorem or Corollary: (EQUAL new-expr old-expr)

where n is a type-set (see type-set) and old-expr is the term containing x as a free variable that ACL2 currently uses to recognize type-set n. For a given n, the exact form of old-expr is generated by
(convert-type-set-to-term 'x n (ens state) (w state) nil)].

If the :type-set field of the rule-class is omitted, we attempt to compute it from the right-hand side, old-expr, of the corollary. That computation is done by type-set-implied-by-term (see type-set). However, it is possible that the type-set we compute from lhs does not have the required property that when inverted with convert-type-set-to-term the result is lhs. If you omit :type-set and an error is caused because lhs has the incorrect form, you should manually specify both :type-set and the lhs generated by convert-type-set-to-term.

The rule generated will henceforth make new-expr be the term used by ACL2 to recognize type-set n. If this rule is created by a defthm event named name then the rune of the rule is (:type-set-inverter name) and by disabling that rune you can prevent its being used to decode type-sets.

Type-sets are inverted when forced assumptions are turned into formulas to be proved. In their internal form, assumptions are essentially pairs consisting of a context and a goal term, which was forced. Abstractly a context is just a list of hypotheses which may be assumed while proving the goal term. But actually contexts are alists which pair terms with type-sets, encoding the current hypotheses. For example, if the original conjecture contained the hypothesis (integerp x) then the context used while working on that conjecture will include the assignment to x of the type-set *ts-integer*.













































































WELL-FOUNDED-RELATION

show that a relation is well-founded on a set
Major Section:  RULE-CLASSES

See rule-classes for a general discussion of rule classes and how they are used to build rules from formulas. An example :corollary formula from which a :well-founded-relation rule might be built is as follows. (Of course, the functions pairp, lex2p, and ordinate would have to be defined first.)

Example:
(and (implies (pairp x) (e0-ordinalp (ordinate x)))
     (implies (and (pairp x)
                   (pairp y)
                   (lex2p x y))
              (e0-ord-< (ordinate x) (ordinate y))))
The above example 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) (E0-ORDINALP (fn x)))      ; Property 1
     (IMPLIES (AND (mp x)                       ; Property 2
                   (mp y)
                   (rel x y))
              (E0-ORD-< (fn x) (fn y)))),
or
(AND (E0-ORDINALP (fn x))                       ; Property 1
     (IMPLIES (rel x y)                         ; Property 2
              (E0-ORD-< (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 hyptheses in the second conjunct both produce unrecognized forms. The requirement that each fn be proved well-founded at most once insures 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.

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 e0-ordinalp.) 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 e0-ord-<. (See e0-ord-<.) 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 insured 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 (mp . 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-default-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 e0-ord-<.

Finally, though it is probably obvious, we now show that defun-goal-1 and defun-goal-2 are sufficient to insure 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 e0-ord-<
                 :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
(e0-ordinalp (fn (m x)))                        ; *1
and
(implies (test x)                               ; *2
         (e0-ord-< (fn (m (step x))) (fn (m x)))).
But *1 can be proved by instantiating property-1 to get
(implies (mp (m x)) (e0-ordinalp (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)))
         (e0-ord-< (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))
         (e0-ord-< (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.