Info file: acl2-doc-emacs.info, -*-Text-*- produced by `texinfo-format-buffer' from file `acl2-doc-emacs.texinfo' using `texinfmt.el' version 2.32 of 19 November 1993. This is documentation for ACL2 Version 1.9 Copyright (C) 1997 Computational Logic, Inc. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. You should have received a copy of the GNU General Public License along with this program; if not, write to the Free Software Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. Written by: Matt Kaufmann and J Strother Moore Computational Logic, Inc. 1717 West Sixth Street, Suite 290 Austin, TX 78703-4776 U.S.A.  File: acl2-doc-emacs.info, Node: BUILT-IN-CLAUSES, Next: COMPOUND-RECOGNIZER, Prev: RULE-CLASSES, Up: RULE-CLASSES BUILT-IN-CLAUSES to build a clause into the simplifier and measure and guard generating See *Note RULE-CLASSES:: for a general discussion of rule classes and how they are used to build rules from formulas. A :built-in-clause rule can be built from any formula other than propositional tautologies. Roughly speaking, the system uses the list of built-in clauses as the first method of proof when attacking a new goal. Any goal that is subsumed by a built in clause is proved "silently." ACL2 maintains a set of "built-in" clauses that are used to short-circuit certain theorem proving tasks. We discuss this at length below. When a theorem is given the rule class :built-in-clause ACL2 flattens the implies and and structure of the :corollary formula so as to obtain a set of formulas whose conjunction is equivalent to the given corollary. It then converts each of these to clausal form and adds each clause to the set of built-in clauses. For example, the following :corollary (regardless of the definition of abl) (and (implies (and (true-listp x) (not (equal x nil))) (< (acl2-count (abl x)) (acl2-count x))) (implies (and (true-listp x) (not (equal nil x))) (< (acl2-count (abl x)) (acl2-count x)))) will build in two clauses, {(not (true-listp x)) (equal x nil) (< (acl2-count (abl x)) (acl2-count x))} and {(not (true-listp x)) (equal nil x) (< (acl2-count (abl x)) (acl2-count x))}. We now give more background. Recall that a clause is a set of terms, implicitly representing the disjunction of the terms. Clause c1 is "subsumed" by clause c2 if some instance of c2 is a subset c1. For example, let c1 be {(not (consp l)) (equal a (car l)) (< (acl2-count (cdr l)) (acl2-count l))}. Then c1 is subsumed by c2, shown below, {(not (consp x)) ; second term omitted here (< (acl2-count (cdr x)) (acl2-count x))} because we can instantiate x in c2 with l to obtain a subset of c1. Observe that c1 is the clausal form of (implies (and (consp l) (not (equal a (car l)))) (< (acl2-count (cdr l)) (acl2-count l))), c2 is the clausal form of (implies (consp l) (< (acl2-count (cdr l)) (acl2-count l))) and the subsumption property just means that c1 follows trivially from c2 by instantiation. The set of built-in clauses is just a set of known theorems in clausal form. Any formula that is subsumed by a built-in clause is thus a theorem. If the set of built-in theorems is reasonably small, this little theorem prover is fast. ACL2 uses the "built-in clause check" in four places: (1) at the top of the iteration in the prover -- thus if a built-in clause is generated as a subgoal it will be recognized when that goal is considered, (2) within the simplifier so that no built-in clause is ever generated by simplification, (3) as a filter on the clauses generated to prove the termination of recursively defun'd functions and (4) as a filter on the clauses generated to verify the guards of a function. The latter two uses are the ones that most often motivate an extension to the set of built-in clauses. Frequently a given formalization problem requires the definition of many functions which require virtually identical termination and/or guard proofs. These proofs can be short-circuited by extending the set of built-in clauses to contain the most general forms of the clauses generated by the definitional schemes in use. The attentive user might have noticed that there are some recursive schemes, e.g., recursion by cdr after testing consp, that ACL2 just seems to "know" are ok, while for others it generates measure clauses to prove. Actually, it always generates measure clauses but then filters out any that pass the built-in clause check. When ACL2 is initialized, the clause justifying cdr recursion after a consp test is added to the set of built-in clauses. (That clause is c2 above.) Note that only a subsumption check is made; no rewriting or simplification is done. Thus, if we want the system to "know" that cdr recursion is ok after a negative atom test (which, by the definition of atom, is the same as a consp test), we have to build in a second clause. The subsumption algorithm does not "know" about commutative functions. Thus, for predictability, we have built in commuted versions of each clause involving commutative functions. For example, we build in both {(not (integerp x)) (< 0 x) (= x 0) (< (acl2-count (+ -1 x)) (acl2-count x))} and the commuted version {(not (integerp x)) (< 0 x) (= 0 x) (< (acl2-count (+ -1 x)) (acl2-count x))} so that the user need not worry whether to write (= x 0) or (= 0 x) in definitions. :built-in-clause rules added by the user can be enabled and disabled.  File: acl2-doc-emacs.info, Node: COMPOUND-RECOGNIZER, Next: CONGRUENCE, Prev: BUILT-IN-CLAUSES, Up: RULE-CLASSES COMPOUND-RECOGNIZER make a rule used by the typing mechanism See *Note 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 :compound-recognizer rule might be built is: Example: (implies (alistp x) When (alistp x) is assumed true, (true-listp x)) add the additional hypothesis that x is of primitive type true-listp. General Forms: (implies (fn x) concl) (implies (not (fn x)) concl) (and (implies (fn x) concl1) (implies (not (fn x)) concl2)) (iff (fn x) concl) (equal (fn x) concl) where fn is a Boolean valued function of one argument, x is a variable symbol, and the system can deduce some restriction on the primitive type of x from the assumption that concl holds. The third restriction is vague but one way to understand it is to weaken it a little to "and concl is a non-tautological conjunction or disjunction of the primitive type recognizers listed below." The primitive ACL2 types and a suitable primitive recognizing expression for each are listed below. type suitable primitive recognizer zero (equal x 0) negative integers (and (integerp x) (< x 0)) positive integers (and (integerp x) (> x 0)) negative ratio (and (rationalp x) (not (integerp x)) (< x 0)) positive ratio (and (rationalp x) (not (integerp x)) (> x 0)) complex rational (complex-rationalp x) nil (equal x nil) t (equal x t) other symbols (and (symbolp x) (not (equal x nil)) (not (equal x t))) proper conses (and (consp x) (true-listp x)) improper conses (and (consp x) (not (true-listp x))) strings (stringp x) characters (characterp x) Thus, a suitable concl to recognize the naturals would be (or (equal x 0) (and (integerp x) (> x 0))) but it turns out that we also permit (and (integerp x) (>= x 0)). Similarly, the true-lists could be specified by (or (equal x nil) (and (consp x) (true-listp x))) but we in fact allow (true-listp x). When time permits we will document more fully what is allowed or implement a macro that permits direct specification of the desired type in terms of the primitives. There are essentially four forms of :compound-recognizer rules, the last two general forms above being equivalent. We explain how such rules are used by considering the individual forms. Consider a rule of the first form, (implies (fn x) concl). The effect of such a rule is that when the rewriter assumes (fn x) true, as it would while diving through (if (fn x) xxx ...) to rewrite xxx, it restricts the type of x as specified by concl. However, when assuming (fn x) false, as necessary in (if (fn x) ... xxx), the rule permits no additional assumptions about the type of x. For example, if fn is primep, i.e., the predicate that recognizes prime numbers, then (implies (primep x) (and (integerp x) (>= x 0))) is a compound recognizer rule of the first form. When (primep x) is assumed true, the rewriter gains the additional information that x is a natural number. When (primep x) is assumed false, no additional information is gained -- since x may be a non-prime natural or may not even be a natural. The second general form addresses itself to the symmetric case, when assuming (fn x) false permits type restrictions on x but assuming (fn x) true permits no such restrictions. For example, if we defined exprp to be the recognizer for well-formed expressions for some language in which all symbols, numbers, character objects and strings were well-formed -- e.g., the well-formedness rules only put restrictions on expressions represented by consps -- then the theorem (implies (not (exprp x)) (consp x)) is a rule of the second form. Assuming (exprp x) true tells us nothing about the type of x; assuming it false tells us x is a consp. The third general form addresses itself to the case where one type may be deduced from (fn x) and a generally unrelated type may be deduced from its negation. If we modified the expression recognizer above so that character objects are illegal, then a rule of the third form is (and (implies (exprp x) (not (characterp x))) (implies (not (exprp x)) (or (consp x) (characterp x)))). Finally, rules of the fourth class address the case where fn recognizes all and only the objects whose type is described. In this case, fn is really just a new name for some "compound recognizers." The classic example is (booleanp x), which is just a handy combination of two primitive types: (iff (booleanp x) (or (equal x t) (equal x nil))). Often it is best to disable fn after proving that it is a compound recognizer, since (fn x) will not be recognized as a compound recognizer once it has been expanded. Every time you prove a new compound recognizer rule about fn it overrides all previously proved compound recognizer rules about fn. Thus, if you want to establish the type implied by (fn x) and you want to establish the type implied by (not (fn x)), you must prove a compound recognizer rule of the third or fourth forms. Proving a rule of the first form followed by one of the second only leaves the second fact in the data base. Compound recognizer rules can be disabled with the effect that older rules about fn, if any, are exposed. If you prove multiple compound recognizer rules for a function, you may see a *warning* message to the effect that the new rule is not as "restrictive" as the old. That is, the new rules do not give the rewriter strictly more type information than it already had. The new rule is stored anyway, overriding the old, if enabled. You may be playing subtle games with enabling or rewriting. But two other interpretions are more likely, we think. One is that you have forgotten about an earlier rule and should merely print it out to make sure it says what you know and then forget your new rule. The other is that you meant to give the system more information and the system has simply been unable to extract the intended type information from the term you placed in the conclusion of the new rule. Given our lack of specificity in saying how type information is extracted from rules, you can hardly blame yourself for this problem. Sorry. If you suspect you've been burned this way, you should rephrase the new rule in terms of the primitive recognizing expressions above and see if the warning is still given. It would also be helpful to let us see your example so we can consider it as we redesign this stuff. Compound recognizer rules are similar to :forward-chaining rules in that the system deduces new information from the act of assuming something true or false. If a compound recognizer rule were stored as a forward chaining rule it would have essentially the same effect as described, when it has any effect at all. The important point is that :forward-chaining rules, because of their more general and expensive form, are used "at the top level" of the simplification process: we forward chain from assumptions in the goal being proved. But compound recognizer rules are built in at the bottom-most level of the simplifier, where type reasoning is done. All that said, compound recognizer rules are a rather fancy, specialized mechanism. It may be more appropriate to create :forward-chaining rules instead of :compound-recognizer rules.  File: acl2-doc-emacs.info, Node: CONGRUENCE, Next: DEFINITION, Prev: COMPOUND-RECOGNIZER, Up: RULE-CLASSES CONGRUENCE the relations to maintain while simplifying arguments See *Note 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 :congruence rule might be built is: Example: (implies (set-equal x y) (iff (memb e x) (memb e y))). Also see *Note DEFCONG:: and see *Note EQUIVALENCE::. General Form: (implies (equiv1 xk xk-equiv) (equiv2 (fn x1... xk ...xn) (fn x1... xk-equiv ...xn))) where equiv1 and equiv2 are known equivalence relations, fn is an n-ary function symbol and the xi and xk-equiv are all distinct variables. The effect of such a rule is to record that the equiv2-equivalence of fn-expressions can be maintained if, while rewriting the kth argument position, equiv1-equivalence is maintained. See *Note EQUIVALENCE:: for a general discussion of the issues. We say that equiv2, above, is the "outside equivalence" in the rule and equiv1 is the "inside equivalence for the kth argument" The macro form (defcong equiv1 equiv2 (fn x1 ... x1) k) is an abbreviation for a defthm of rule-class :congruence that attempts to establish that equiv2 is maintained by maintaining equiv1 in fn's kth argument. The defcong macro automatically generates the general formula shown above. See *Note DEFCONG::. The memb example above tells us that (memb e x) is propositionally equivalent to (memb e y), provided x and y are set-equal. The outside equivalence is iff and the inside equivalence for the second argument is set-equal. If we see a memb expression in a propositional context, e.g., as a literal of a clause or test of an if (but not, for example, as an argument to cons), we can rewrite its second argument maintaining set-equality. For example, a rule stating the commutativity of append (modulo set-equality) could be applied in this context. Since equality is a refinement of all equivalence relations, all equality rules are always available. See *Note REFINEMENT::. All known :congruence rules about a given outside equivalence and fn can be used independently. That is, consider two :congruence rules with the same outside equivalence, equiv, and about the same function fn. Suppose one says that equiv1 is the inside equivalence for the first argument and the other says equiv2 is the inside equivalence for the second argument. Then (fn a b) is equiv (fn a' b') provided a is equiv1 to a' and b is equiv2 to b'. This is an easy consequence of the transitivity of equiv. It permits you to think independently about the inside equivalences. Furthermore, it is possible that more than one inside equivalence for a given argument slot will maintain a given outside equivalence. For example, (length a) is equal to (length a') if a and a' are related either by list-equal or by string-equal. You may prove two (or more) :congruence rules for the same slot of a function. The result is that the system uses a new, "generated" equivalence relation for that slot with the result that rules of both (or all) kinds are available while rewriting. :congruence rules can be disabled. For example, if you have two different inside equivalences for a given argument position and you find that the :rewrite rules for one are unexpectedly preventing the application of the desired rule, you can disable the rule that introduced the unwanted inside equivalence. More will be written about this as we develop the techniques.  File: acl2-doc-emacs.info, Node: DEFINITION, Next: ELIM, Prev: CONGRUENCE, Up: RULE-CLASSES DEFINITION make a rule that acts like a function definition Example: (implies (true-listp x) (equal (len x) (if (null x) 0 (if (null (cdr x)) 1 (len (cddr x)))))) General Form: (implies hyp (equiv (fn a1 ... an) body)) where equiv is an equivalence relation and fn is a function symbol other than if, hide or force. Such rules allow "alternative" definitions of fn to be proved as theorems but used as definitions. These rules are not true "definitions" in the sense that they (a) cannot introduce new function symbols and (b) do not have to be terminating recursion schemes. They are just conditional rewrite rules that are controlled the same way we control recursive definitions. We call these "definition rules" or "generalized definitions". Consider the general form above. Generalized definitions are stored among the :rewrite rules for the function "defined," fn above, but the procedure for applying them is a little different. During rewriting, instances of (fn a1 ... an) are replaced by corresponding instances of body provided the hyps can be established as for a :rewrite rule and the result of rewriting body satisfies the criteria for function expansion. There are two primary criteria, either of which permits expansion. The first is that the "recursive" calls of fn in the rewritten body have arguments that already occur in the goal conjecture. The second is that the "controlling" arguments to fn are simpler in the rewritten body. The notions of "recursive call" and "controllers" are complicated by the provisions for mutually recursive definitions. Consider a "clique" of mutually recursive definitions. Then a "recursive call" is a call to any function defined in the clique and an argument is a "controller" if it is involved in the measure that decreases in all recursive calls. These notions are precisely defined by the definitional principle and do not necessarily make sense in the context of generalized definitional equations as implemented here. But because the heuristics governing the use of generalized definitions require these notions, it is generally up to the user to specify which calls in body are to be considered recursive and what the controlling arguments are. This information is specified in the :clique and :controller-alist fields of the :definition rule class. The :clique field is the list of function symbols to be considered recursive calls of fn. In the case of a non-recursive definition, the :clique field is empty; in a singly recursive definition, it should consist of the singleton list containing fn; otherwise it should be a list of all of the functions in the mutually recursive clique with this definition of fn. If the :clique field is not provided it defaults to nil if fn does not occur as a function symbol in body and it defaults to the singleton list containing fn otherwise. Thus, :clique must be supplied by the user only when the generalized definition rule is to be treated as one of several in a mutually recursive clique. The :controller-alist is an alist that maps each function symbol in the :clique to a mask specifying which arguments are considered controllers. The mask for a given member of the clique, fn, must be a list of t's and nil's of length equal to the arity of fn. A t should be in each argument position that is considered a "controller" of the recursion. For a function admitted under the principle of definition, an argument controls the recursion if it is one of the arguments measured in the termination argument for the function. But in generalized definition rules, the user is free to designate any subset of the arguments as controllers. Failure to choose wisely may result in the "infinite expansion" of definitional rules but cannot render ACL2 unsound since the rule being misused is a theorem. If the :controller-alist is omitted it can sometimes be defaulted automatically by the system. If the :clique is nil, the :controller-alist defaults to nil. If the :clique is a singleton containing fn, the :controller-alist defaults to the controller alist computed by (defun fn args body). If the :clique contains more than one function, the user must supply the :controller-alist specifying the controllers for each function in the clique. This is necessary since the system cannot determine and thus cannot analyze the other definitional equations to be included in the clique. For example, suppose fn1 and fn2 have been defined one way and it is desired to make "alternative" mutually recursive definitions available to the rewriter. Then one would prove two theorems and store each as a :definition rule. These two theorems would exhibit equations "defining" fn1 and fn2 in terms of each other. No provision is here made for exhibiting these two equations as a system of equations. One is proved and then the other. It just so happens that the user intends them to be treated as mutually recursive definitions. To achieve this end, both :definition rules should specify the :clique (fn1 fn2) and should specify a suitable :controller-alist. If, for example, the new definition of fn1 is controlled by its first argument and the new definition of fn2 is controlled by its second and third (and they each take three arguments) then a suitable :controller-alist would be ((fn1 t nil nil) (fn2 nil t t)). The order of the pairs in the alist is unimportant, but there must be a pair for each function in the clique. Inappropriate heuristic advice via :clique and :controller-alist can cause "infinite expansion" of generalized definitions, but cannot render ACL2 unsound. Note that the actual definition of fn1 has the runic name (:definition fn1). The runic name of the alternative definition is (:definition lemma), where lemma is the name given to the event that created the generalized :definition rule. This allows theories to switch between various "definitions" of the functions. The definitional principle, defun, actually adds :definition rules. Thus the handling of generalized definitions is exactly the same as for "real" definitions because no distinction is made in the implementation. Suppose (fn x y) is defun'd to be body. Note that defun (or defuns or mutual-recursion) can compute the clique for fn from the syntactic presentation and it can compute the controllers from the termination analysis. Provided the definition is admissible, defun adds the :definition rule (equal (fn x y) body). Thus, (fn a b) will not be expanded unless (g a b) can be established.  File: acl2-doc-emacs.info, Node: ELIM, Next: EQUIVALENCE, Prev: DEFINITION, Up: RULE-CLASSES ELIM make a destructor elimination rule See *Note 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 an :elim rule might be built is: Example: (implies (consp x) when (car v) or (cdr v) appears (equal (cons (car x) (cdr x)) in a conjecture, and v is a x)) variable, consider replacing v by (cons a b), for two new variables a and b. General Form: (implies hyp (equal lhs x)) where x is a variable symbol and lhs contains one or more terms (called "destructor terms") of the form (fn v1 ... vn), where fn is a function symbol and the vi are distinct variable symbols, v1, ..., vn include all the variable symbols in the formula, no fn occurs in lhs in more than one destructor term, and all occurrences of x in lhs are inside destructor terms. To use an :elim rule, the theorem prover waits until a conjecture has been maximally simplified. If it then finds an instance of some destructor term (fn v1 ... vn) in the conjecture, where the instance for x is some variable symbol, vi, it instantiates the :elim formula as indicated by the destructor term matched, splits the conjecture into two goals, according to whether the instantiated hypothesis, hyp, holds, and in the case that it does, generalizes all the instantiated destructor terms in the conjecture to new variables and then replaces vi in the conjecture by the generalized instantiated lhs. At the moment, the best description of how ACL2 :elim rules are used may be found in the discussion of "ELIM Rules," pp 247 of A Computational Logic Handbook.  File: acl2-doc-emacs.info, Node: EQUIVALENCE, Next: FORWARD-CHAINING, Prev: ELIM, Up: RULE-CLASSES EQUIVALENCE mark a relation as an equivalence relation See *Note 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 :equivalence rule might be built is as follows. (We assume that r-equal has been defined.) Example: (and (booleanp (r-equal x y)) (r-equal x x) (implies (r-equal x y) (r-equal y x)) (implies (and (r-equal x y) (r-equal y z)) (r-equal x z))). Also see *Note DEFEQUIV::. General Form: (and (booleanp (equiv x y)) (equiv x x) (implies (equiv x y) (equiv y x)) (implies (and (equiv x y) (equiv y z)) (equiv x z))) except that the order of the conjuncts and terms and the choice of variable symbols is unimportant. The effect of such a rule is to identify equiv as an equivalence relation. Note that only Boolean 2-place function symbols can be treated as equivalence relations. See *Note CONGRUENCE:: and see *Note REFINEMENT:: for closely related concepts. The macro form (defequiv equiv) is an abbreviation for a defthm of rule-class :equivalence that establishes that equiv is an equivalence relation. It generates the formula shown above. See *Note DEFEQUIV::. When equiv is marked as an equivalence relation, its reflexivity, symmetry, and transitivity are built into the system in a deeper way than via :rewrite rules. More importantly, after equiv has been shown to be an equivalence relation, lemmas about equiv, e.g., (implies hyps (equiv lhs rhs)), when stored as :rewrite rules, cause the system to rewrite certain occurrences of (instances of) lhs to (instances of) rhs. Roughly speaking, an occurrence of lhs in the kth argument of some fn-expression, (fn ... lhs' ...), can be rewritten to produce (fn ... rhs' ...), provided the system "knows" that the value of fn is unaffected by equiv-substitution in the kth argument. Such knowledge is communicated to the system via "congruence lemmas." For example, suppose that r-equal is known to be an equivalence relation. The :congruence lemma (implies (r-equal s1 s2) (equal (fn s1 n) (fn s2 n))) informs the rewriter that, while rewriting the first argument of fn-expressions, it is permitted to use r-equal rewrite-rules. See *Note CONGRUENCE:: for details about :congruence lemmas. Interestingly, congruence lemmas are automatically created when an equivalence relation is stored, saying that either of the equivalence relation's arguments may be replaced by an equivalent argument. That is, if the equivalence relation is fn, we store congruence rules that state the following fact: (implies (and (fn x1 y1) (fn x2 y2)) (iff (fn x1 x2) (fn y1 y2))) Another aspect of equivalence relations is that of "refinement." We say equiv1 "refines" equiv2 iff (equiv1 x y) implies (equiv2 x y). :refinement rules permit you to establish such connections between your equivalence relations. The value of refinements is that if the system is trying to rewrite something while maintaining equiv2 it is permitted to use as a :rewrite rule any refinement of equiv2. Thus, if equiv1 is a refinement of equiv2 and there are equiv1 rewrite-rules available, they can be brought to bear while maintaining equiv2. See *Note REFINEMENT::. The system initially has knowledge of two equivalence relations, equality, denoted by the symbol equal, and propositional equivalence, denoted by iff. Equal is known to be a refinement of all equivalence relations and to preserve equality across all arguments of all functions. Typically there are five steps involved in introducing and using a new equivalence relation, equiv. (1) Define equiv, (2) prove the :equivalence lemma about equiv, (3) prove the :congruence lemmas that show where equiv can be used to maintain known relations, (4) prove the :refinement lemmas that relate equiv to known relations other than equal, and (5) develop the theory of conditional :rewrite rules that drive equiv rewriting. More will be written about this as we develop the techniques. For now, here is an example that shows how to make use of equivalence relations in rewriting. Among the theorems proved below is (defthm insert-sort-is-id (perm (insert-sort x) x)) Here perm is defined as usual with delete and is proved to be an equivalence relation and to be a congruence relation for cons and member. Then we prove the lemma (defthm insert-is-cons (perm (insert a x) (cons a x))) which you must think of as you would (insert a x) = (cons a x). Now prove (perm (insert-sort x) x). The base case is trivial. The induction step is (consp x) & (perm (insert-sort (cdr x)) (cdr x)) -> (perm (insert-sort x) x). Opening insert-sort makes the conclusion be (perm (insert (car x) (insert-sort (cdr x))) x). Then apply the induction hypothesis (rewriting (insert-sort (cdr x)) to (cdr x)), to make the conclusion be (perm (insert (car x) (cdr x)) x) Then apply insert-is-cons to get (perm (cons (car x) (cdr x)) x). But we know that (cons (car x) (cdr x)) is x, so we get (perm x x) which is trivial, since perm is an equivalence relation. Here are the events. (encapsulate ((lt (x y) t)) (local (defun lt (x y) (declare (ignore x y)) nil)) (defthm lt-non-symmetric (implies (lt x y) (not (lt y x))))) (defun insert (x lst) (cond ((atom lst) (list x)) ((lt x (car lst)) (cons x lst)) (t (cons (car lst) (insert x (cdr lst)))))) (defun insert-sort (lst) (cond ((atom lst) nil) (t (insert (car lst) (insert-sort (cdr lst)))))) (defun del (x lst) (cond ((atom lst) nil) ((equal x (car lst)) (cdr lst)) (t (cons (car lst) (del x (cdr lst)))))) (defun mem (x lst) (cond ((atom lst) nil) ((equal x (car lst)) t) (t (mem x (cdr lst))))) (defun perm (lst1 lst2) (cond ((atom lst1) (atom lst2)) ((mem (car lst1) lst2) (perm (cdr lst1) (del (car lst1) lst2))) (t nil))) (defthm perm-reflexive (perm x x)) (defthm perm-cons (implies (mem a x) (equal (perm x (cons a y)) (perm (del a x) y))) :hints (("Goal" :induct (perm x y)))) (defthm perm-symmetric (implies (perm x y) (perm y x))) (defthm mem-del (implies (mem a (del b x)) (mem a x))) (defthm perm-mem (implies (and (perm x y) (mem a x)) (mem a y))) (defthm mem-del2 (implies (and (mem a x) (not (equal a b))) (mem a (del b x)))) (defthm comm-del (equal (del a (del b x)) (del b (del a x)))) (defthm perm-del (implies (perm x y) (perm (del a x) (del a y)))) (defthm perm-transitive (implies (and (perm x y) (perm y z)) (perm x z))) (defequiv perm) (in-theory (disable perm perm-reflexive perm-symmetric perm-transitive)) (defcong perm perm (cons x y) 2) (defcong perm iff (mem x y) 2) (defthm atom-perm (implies (not (consp x)) (perm x nil)) :rule-classes :forward-chaining :hints (("Goal" :in-theory (enable perm)))) (defthm insert-is-cons (perm (insert a x) (cons a x))) (defthm insert-sort-is-id (perm (insert-sort x) x)) (defun app (x y) (if (consp x) (cons (car x) (app (cdr x) y)) y)) (defun rev (x) (if (consp x) (app (rev (cdr x)) (list (car x))) nil)) (defcong perm perm (app x y) 2) (defthm app-cons (perm (app a (cons b c)) (cons b (app a c)))) (defthm app-commutes (perm (app a b) (app b a))) (defcong perm perm (app x y) 1 :hints (("Goal" :induct (app y x)))) (defthm rev-is-id (perm (rev x) x)) (defun == (x y) (if (consp x) (if (consp y) (and (equal (car x) (car y)) (== (cdr x) (cdr y))) nil) (not (consp y)))) (defthm ==-symmetric (== x x)) (defthm ==-reflexive (implies (== x y) (== y x))) (defequiv ==) (in-theory (disable ==-symmetric ==-reflexive)) (defcong == == (cons x y) 2) (defcong == iff (consp x) 1) (defcong == == (app x y) 2) (defcong == == (app x y) 1) (defthm rev-rev (== (rev (rev x)) x))  File: acl2-doc-emacs.info, Node: FORWARD-CHAINING, Next: GENERALIZE, Prev: EQUIVALENCE, Up: RULE-CLASSES FORWARD-CHAINING make a rule to forward chain when a certain trigger arises See *Note 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 :forward-chaining rule might be built is: Example: (implies (and (p x) (r x)) when (p a) appears in a formula to be (q (f x))) simplified, try to establish (r a) and if successful, add (q (f a)) to the known assumptions To specify the triggering terms provide a non-empty list of terms as the value of the :trigger-terms field of the rule class object. General Form: Any theorem, provided an acceptable triggering term exists. Forward chaining rules are generated from the corollary term as follows. If that term has the form (implies hyp concl), then the let expressions in concl (formally, lambda expressions) are expanded away, and the result is treated as a conjunction, with one forward chaining rule with hypothesis hyp created for each conjunct. In the other case, where the corollary term is not an implies, we process it as we process the conclusion in the first case. The :trigger-terms field of a :forward-chaining rule class object should be a non-empty list of terms, if provided, and should have certain properties described below. If the :trigger-terms field is not provided, it defaults to the singleton list containing the "atom" of the first hypothesis of the formula. (The atom of (not x) is x; the atom of any other term is the term itself.) If there are no hypotheses and no :trigger-terms were provided, an error is caused. A triggering term is acceptable if it is not a variable, a quoted constant, a lambda application, a let-expression, or a not-expression, and every variable symbol in the conclusion of the theorem either occurs in the hypotheses or occurs in the trigger. :Forward-chaining rules are used by the simplifier before it begins to rewrite the literals of the goal. If any term in the goal is an instance of a trigger of some forward chaining rule, we try to establish the hypotheses of that forward chaining theorem (from the negation of the goal). To relieve a hypotheses we only use type reasoning, evaluation of ground terms, and presence among our known assumptions. We do not use rewriting. If all hypotheses are relieved, we add the instantiated conclusion to our known assumptions.  File: acl2-doc-emacs.info, Node: GENERALIZE, Next: INDUCTION, Prev: FORWARD-CHAINING, Up: RULE-CLASSES GENERALIZE make a rule to restrict generalizations See *Note 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 :generalize rule might be built is: Example: any theorem General Form: any theorem To use such a :generalize rule, the system waits until it has decided to generalize some term, term, by replacing it with some new variable v. If any :generalize formula can be instantiated so that some non-variable subterm becomes term, then that instance of the formula is added as a hypothesis. At the moment, the best description of how ACL2 :generalize rules are used may be found in the discussion of "Generalize Rules," pp 248 of A Computational Logic Handbook.  File: acl2-doc-emacs.info, Node: INDUCTION, Next: LINEAR, Prev: GENERALIZE, Up: RULE-CLASSES INDUCTION make a rule that suggests a certain induction Example: (:induction :corollary t ; the theorem proved is irrelevant! :pattern (* 1/2 i) :condition (and (integerp i) (>= i 0)) :scheme (recursion-by-sub2 i)) In ACL2, as in Nqthm, the functions in a conjecture "suggest" the inductions considered by the system. Because every recursive function must be admitted with a justification in terms of a measure that decreases in a well-founded way on a given set of "controlling" arguments, every recursive function suggests a dual induction scheme that "unwinds" the function from a given application. For example, since append (actually binary-append, but we'll ignore the distinction here) decomposes its first argument by successive cdrs as long as it is a non-nil true list, the induction scheme suggested by (append x y) has a base case supposing x to be either not a true list or to be nil and then has an induction step in which the induction hypothesis is obtained by replacing x by (cdr x). This substitution decreases the same measure used to justify the definition of append. Observe that an induction scheme is suggested by a recursive function application only if the controlling actuals are distinct variables, a condition that is sufficient to insure that the "substitution" used to create the induction hypothesis is indeed a substitution and that it drives down a certain measure. In particular, (append (foo x) y) does not suggest an induction unwinding append because the induction scheme suggested by (append x y) requires that we substitute (cdr x) for x and we cannot do that if x is not a variable symbol. Once ACL2 has collected together all the suggested induction schemes it massages them in various ways, combining some to simultaneously unwind certain cliques of functions and vetoing others because they "flaw" others. We do not further discuss the induction heuristics here; the interested reader should see Chapter XIV of A Computational Logic (Boyer and Moore, Academic Press, 1979) which represents a fairly complete description of the induction heuristics of ACL2. However, unlike Nqthm, ACL2 provides a means by which the user can elaborate the rules under which function applications suggest induction schemes. Such rules are called :induction rules. The definitional principle automatically creates an :induction rule, named (:induction fn), for each admitted recursive function, fn. It is this rule that links applications of fn to the induction scheme it suggests. Disabling (:induction fn) will prevent fn from suggesting the induction scheme derived from its recursive definition. It is possible for the user to create additional :induction rules by using the :induction rule class in defthm. Technically we are "overloading" defthm by using it in the creation of :induction rules because no theorem need be proved to set up the heuristic link represented by an :induction rule. However, since defthm is generally used to create rules and rule-class objects are generally used to specify the exact form of each rule, we maintain that convention and introduce the notion of an :induction rule. An :induction rule can be created from any lemma whatsoever. General Form of an :induction Lemma or Corollary: T General Form of an :induction rule-class: (:induction :pattern pat-term :condition cond-term :scheme scheme-term) where pat-term, cond-term, and scheme-term are all terms, pat-term is the application of a function symbol, fn, scheme-term is the application of a function symbol, rec-fn, that suggests an induction, and, finally, every free variable of cond-term and scheme-term is a free variable of pat-term. We actually check that rec-fn is either recursively defined -- so that it suggests the induction that is intrinsic to its recursion -- or else that another :induction rule has been proved linking a call of rec-fn as the :pattern to some scheme. The induction rule created is used as follows. When an instance of the :pattern term occurs in a conjecture to be proved by induction and the corresponding instance of the :condition term is known to be non-nil (by type reasoning alone), the corresponding instance of the :scheme term is created and the rule "suggests" the induction, if any, suggested by that term. If rec-fn is recursive, then the suggestion is the one that unwinds that recursion. Consider, for example, the example given above, (:induction :pattern (* 1/2 i) :condition (and (integerp i) (>= i 0)) :scheme (recursion-by-sub2 i)). In this example, we imagine that recursion-by-sub2 is the function: (defun recursion-by-sub2 (i) (if (and (integerp i) (< 1 i)) (recursion-by-sub2 (- i 2)) t)) Observe that this function recursively decomposes its integer argument by subtracting 2 from it repeatedly and stops when the argument is 1 or less. The value of the function is irrelevant; it is its induction scheme that concerns us. The induction scheme suggested by (recursion-by-sub2 i) is (and (implies (not (and (integerp i) (< 1 i))) ; base case (:p i)) (implies (and (and (integerp i) (< 1 i)) ; induction step (:p (- i 2))) (:p i))) We can think of the base case as covering two situations. The first is when i is not an integer. The second is when the integer i is 0 or 1. In the base case we must prove (:p i) without further help. The induction step deals with those integer i greater than 1, and inductively assumes the conjecture for i-2 while proving it for i. Let us call this scheme "induction on i by twos." Suppose the above :induction rule has been added. Then an occurrence of, say, (* 1/2 k) in a conjecture to be proved by induction would suggest, via this rule, an induction on k by twos, provided k was known to be a nonnegative integer. This is because the induction rule's :pattern is matched in the conjecture, its :condition is satisfied, and the :scheme suggested by the rule is that derived from (recursion-by-sub2 k), which is induction on k by twos. Similarly, the term (* 1/2 (length l)) would suggest no induction via this rule, even though the rule "fires" because it creates the :scheme (recursion-by-sub2 (length l)) which suggests no inductions unwinding recursion-by-sub2 (since the controlling argument of recursion-by-sub2 in this :scheme is not a variable symbol). Continuing this example one step further illustrates the utility of :induction rules. We could define the function recursion-by-cddr that suggests the induction scheme decomposing its consp argument two cdrs at a time. We could then add the :induction rule linking (* 1/2 (length x)) to (recursion-by-cddr x) and arrange for (* 1/2 (length l)) to suggest induction on l by cddr. Observe that :induction rules require no proofs to be done. Such a rule is merely a heuristic link between the :pattern term, which may occur in conjectures to be proved by induction, and the :scheme term, from which an induction scheme may be derived. Hence, when an :induction rule-class is specified in a defthm event, the theorem proved is irrelevant. The easiest theorem to prove is, of course, t. Thus, we suggest that when an :induction rule is to be created, the following form be used: (defthm name T :rule-classes ((:induction :pattern pat-term :condition cond-term :scheme scheme-term))) The name of the rule created is (:induction name). When that rune is disabled the heuristic link between pat-term and scheme-term is broken.  File: acl2-doc-emacs.info, Node: LINEAR, Next: LINEAR-ALIAS, Prev: INDUCTION, Up: RULE-CLASSES LINEAR make some arithmetic inequality rules See *Note 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 :linear rule might be built is: Example: (implies (and (eqlablep e) if inequality reasoning begins to (true-listp x)) consider how (length (member a b)) (>= (length x) compares to any other term, add to (length (member e x)))) set of known inequalities the fact that it is no larger than (length b), provided (eqlablep a) and (true-listp b) rewrite to t General Form: (and ... (implies (and ...hi...) (implies (and ...hk...) (and ... (rel lhs rhs) ...))) ...) Note: One :linear rule class object might create many linear arithmetic rules from the :corollary formula. To create the rules, we first flatten the and and implies structure of the formula, transforming it into a conjunction of formulas, each of the form (implies (and h1 ... hn) (rel lhs rhs)) where no hypothesis is a conjunction and rel is one of the inequality relations <, <=, =, /=, >, or >=. If necessary, the hypothesis of such a conjunct may be vacuous. We create a :linear rule for each such conjunct, if possible, and otherwise cause an error. Each rule has one or more "trigger terms" which may be specified by the user using the :trigger-terms field of the rule class or which may be defaulted to values chosen by the system. We discuss the determination of trigger terms after discussing how linear rules are used. :linear rules are used by a linear arithmetic decision procedure during rewriting. We describe the procedure very roughly here. Fundamental to the procedure is the notion of a linear polynomial inequality. A "linear polynomial" is a sum of terms, each of which is the product of a rational constant and an "unknown." The "unknown" is permitted to be 1 simply to allow a term in the sum to be constant. Thus, an example linear polynomial is 3*x + 7*a + 2; here x and a are the (interesting) unknowns. In our case, the unknowns need not be variable symbols. For example, (length x) might be used as an unknown in a linear polynomial. Thus, another linear polynomial is 3*(length x) + 7*a. A "linear polynomial inequality" is an inequality (either < or <=) relation between two linear polynomials. Certain linear polynomial inequalities can be combined by cross-multiplication and addition to permit the deduction of a third linear inequality polynomial with fewer unknowns. If this deduced inequality is manifestly false, a contradiction has been deduced from the assumed inequalities. For example, suppose we have three assumptions: p1: 3*x + 7*a < 4 p2: 3 < 2*x p3: 0 <= a. By cross-multiplying and adding the first two (that is, multiplying p1 by 2, p2 by 3 and adding the respective sides), we deduce the intermediate result p4: 6*x + 14*a + 9 < 8 + 6*x which, after cancellation, is p4: 14*a + 1 < 0. If we then cross-multiply and add p3 to p4, we get p5: 1 <= 0, a contradiction. Thus, we have proved that p1 and p2 imply the negation of p3. All of the unknowns of a polynomial must be eliminated by cancellation in order to produce a constant inequality. We can choose to eliminate the unknowns in any order. We eliminate them in term-order, largest unknowns first. (See *Note TERM-ORDER::.) Now suppose that this procedure does not produce a contradiction but instead yields a set of nontrivial inequalities. A contradiction might still be deduced if we could add to the set some additional inequalities allowing additional cancellation. That is where :linear lemmas come in. When the set of inequalities has stabilized under cross-multiplication and addition and no contradiction is produced, we search the data base of :linear rules for rules about the unknowns that are candidates for cancellation (i.e., are the largest unknowns in their respective inequalities). If the trigger term of some :linear rule can be instantiated to yield a candidate for cancellation, we so instantiate that rule, attempt to relieve the hypotheses with general-purpose rewriting, and, if successful, convert the concluding inequality into a polynomial inequality and add it to the set. This may let cancellation continue. See the discussion of "Linear Arithmetic Rules" pp 242 of A Computational Logic Handbook for more details. We now describe how the trigger terms are determined. Most of the time, the trigger terms are not specified by the user and are instead selected by the system. However, the user may specify the terms by including an explicit :trigger-terms field in the rule class, e.g., General Form of a Linear Rule Class: (:LINEAR :COROLLARY formula :TRIGGER-TERMS (term1 ... termk)) Each termi must be a term and must not be a variable, quoted constant, lambda application, let-expression or if-expression. In addition, each termi must be such that if all the variables in the term are instantiated and then the hypotheses of the corollary formula are relieved (possibly instantiating additional free variables), then all the variables in the concluding inequality are instantiated. We generate a linear rule for each conjuctive branch through the corollary and store each rule under each of the specified triggers. Thus, if the corollary formula contains several conjuncts, the variable restrictions on the termi must hold for each conjunct. Note: Problems may arise if you explicitly store a linear lemma under a trigger term that, when instantiated, is not the largest unknown in the instantiated concluding inequality. Suppose for example you store the linear rule (<= (fn i j) (/ i (* j j))) under the trigger term (fn i j). Then when the system "needs" an inequality about (fn a b), i.e., because (fn a b) is the largest unknown in some inequality in the set of assumed inequalities, it will appeal to the rule and deduce (<= (fn a b) (/ a (* b b))). However, the largest unknown in this inequality is (/ a (* b b)) and hence this inequality will not be used until that term is eliminated by cancellation with some other inequality. It is generally best to specify as a trigger term one of the "maximal" terms of the polynomial, as described below. If :trigger-terms is omitted the system computes a set of trigger terms. Each conjunct of the corollary formula may be given a unique set of triggers depending on the variables that occur in the conjunct and the addends that occur in the concluding inequality. In particular, the trigger terms for a conjunct is the list of all "maximal addends" in the concluding inequality. The "addends" of (+ x y) and (- x y) are the union of the addends of x and y. The addends of (- x) and (* n x), where n is a numeric constant, is in all cases just {x}. The addends of an inequality are the union of the addends of the left- and right-hand sides. The addends of any other term, x, is {x}. A term is maximal for a conjunct (implies hyps concl) of the corollary if (a) the term is a non-variable, non-quote, non-lambda application, non-let and non-if expression, (b) the term contains enough variables so that when they are instantiated and the hypotheses are relieved then all the variables in concl are instantiated, and (c) any instantiation of the term is always at least as "large" (see *Note TERM-ORDER:: for a description of the order used) as the corresponding instantiations of any other addend in concl.