More sophisticated tactics

In this subsubsection and the following example, we discuss operations on tactics and tactics with parameters.

introduction of new variables:

When a rewrite introduces new free variables, they are automatically supplied with a numerical subscript as ``new'' variables. Something more complex may happen if the new variable is introduced inside an abstraction (bracketed) term; see below. The introduction of new variables can always be avoided by the use of parameterized versions of theorems which supply values to the new variables; see examples below.

(* example of introduction of new variables *)

- declareunary "-";            (* declare - as a
                               prefix operator *)
- axiom "INV" "?x + -?x" "0";

- s "0";
- rri "INV";                   (* rri = revruleintro 
                               applies converse of 
                               theorem *)

{INV <= 0}                     (* display *)
INV <= 0

- ex();

{?x_82 + - ?x_82}              (* note appearance 
?x_82 + - ?x_82                of new variables *)

control structures:

The special infix operators =>>, <<=, *> and <* allow one to apply a rewrite rule (or its converse) depending on whether the application of a preceding rewrite rule succeeded or failed.

The complex rewrite rules thm1 =>> thm2 and thm1 <<= ?thm2 have the effect of applying thm1 then applying thm2 (resp. its converse) only if the application of thm1 fails. (the handling of these infixes by Watson is quite different from their former handling by Mark2: a chain of alternatives applied to a term which Watson represents as (thm1 =>> thm2 =>> ... =>> thmn) => term was represented by Mark2 as thmn =>> ... thm2 =>> thm1 => term). The commands altruleintro (ari) and altrevruleintro (arri) introduce these ``alternative rule infixes'' (their use is illustrated in the examples below).

The complex rewrite rules thm1 *> thm2 and thm1 <* thm2 have the effect of first applying thm1, then applying thm2 only if the application of thm1 succeeded.

For either of the above kinds of operator, if the theorem thm1 happens to be a built-in operator (e.g., the abstraction and reduction tactics BIND and EVAL introduced below), thm1 is said to ``succeed'' if it makes a change in the target term, and ``fail'' otherwise. For theorems of the usual kind, success or failure depends on whether the appropriate side of the theorem matches the target term.

In the following example, we illustrate the application of =>> to fine-tune the behavior of a tactic. We prove a theorem which applies the identity of addition on either side.

(* a preliminary result *)

- s "?x+0";                (* displays suppressed *)
- ri "COMM"; ri "ZERO";
- prove "COMMZERO";

COMMZERO:  
?x + 0  =  
ZERO => COMM => ?x + 0
0                          (* no axiom was used 
                           in proving this, 
                           though some 
                           were mentioned *)

(* the tactic to apply identity on either side -- 
naive version *)

- s "?x+?y";
- ri "ZERO"; ri "COMMZERO"; 
- p "EITHERZERO";

EITHERZERO:  
?x + ?y  =  
COMMZERO => ZERO => ?x + ?y
0

(* the problem with this *)

- s "0+?x+0";
- ri "EITHERZERO"; ex();

{?x}                       (* the final display *)
?x

(* the difficulty is that successive applications 
of theorems cannot be relied upon to serve as 
alternatives; one may apply and then another after 
it in the list *)

(* we modify the tactic *)

- s "?x+?y";
- ri "ZERO"; ari "COMMZERO"; (* ari = 
                             altrevruleintro
                             introduces an 
                             alternative 
                             theorem to be
                             applied if COMM fails *)
- reprove "EITHERZERO";

EITHERZERO:  
?x + ?y  =  
(ZERO =>> COMMZERO) => ?x + ?y  (* note the 
                                syntactical 
0                               effect of ari *)

(* we repeat the test above *)

- s "0+?x+0";
- ri "EITHERZERO"; ex();

{?x + 0}                   (* the final display:  
?x + 0                     only one application 
                           of identity is made *)

tactics with parameters; operators as tactics

Watson allows the user to develop tactics with parameters, which may be used to pass terms or other theorems or tactics as data to a tactic. The prove command will take parameter lists built with the predeclared function application infix ``@'' and pairing infix ``,''; it will match the parameter list against actual embedded occurrences of the theorem, which needs to have parameters matching the original parameter list in order to be used successfully for rewriting. Watson also allows operators (prefix or infix) to be ``proved'' as (necessarily parameterized) tactics.

(* an example of parameterized and operator theorems:
simple structural tactics *)

- declareopaque "^+";           (* variable operator 
                                declaration will be
                                explained below 
                                (sect. ??) *)
- s "?x^+?y";
- right(); ri "?thm";
- p "RIGHT@?thm";

RIGHT @ ?thm:  
?x ^+ ?y  =  
?x ^+ ?thm => ?y
0

(* a test *)

- s "?x+?y+?z";
- ri "RIGHT@COMM"; steps();

(RIGHT @ COMM) => ?x + ?y + ?z (* display of
?x + COMM => ?y + ?z           rewriting steps *)
?x + ?z + ?y

(* operators as theorems *)

- s "?x";
- ri "?thm1";
- ri "?thm2";
- p "?thm1**?thm2";

?thm1 ** ?thm2:  
?x  =  
?thm2 => ?thm1 => ?x
0

(* a test *)

- s "?x+?y+?z";
- ri "COMM**ASSOC"; ex();

{?y + ?z + ?x}                 (* final display *)
?y + ?z + ?x

The prefix operator !@ can be applied to a theorem whose application introduces new variables to produce a parameterized theorem to which values of these new variables can be supplied; the operator !$ applied to a theorem whose converse introduces new variables produces a parameterized theorem with the same effect as the converse of the original theorem.

In the following example, we develop a tactic converse of a theorem which eliminates variables using parameters and using the built-in operator !$.

(* parameterized converse theorem *)

- s "0";
- initializecounter();     (* initializes suffixes 
                           of new variables *)
- rri "INV"; ex();

{?x_1 + - ?x_1}            (* display *)
?x_1 + - ?x_1

- assign "?x_1" "?x";      (* rename new variable 
                           using global assignment *)
- prove "INV_INVERSE@?x";

INV_INVERSE @ ?x:  
0  =  
?x + - ?x
INV , 0

- s "0";
- ri "INV_INVERSE@3"; ex();

{3 + - 3}                  (* final display *)
3 + - 3

(* the same effect using a built in operator *)

- s "0";
- ri "(!$ INV)@3"; ex();

{3 + - 3}                  (* final display *)
3 + - 3

We close the section with a not altogether trivial example.

- declarepretheorem "ASSOCS";

- s "(?x+?y)+?z";
- ri "ASSOC"; ex();
- ri "ASSOCS";
- p "ASSOCS";

(* ASSOCS applies associativity 
as many times as possible at the top *)

ASSOCS:  
(?x + ?y) + ?z  =  
ASSOCS => ?x + ?y + ?z
ASSOC , 0

(* a test *)

- s "((?x+?y)+?z)+(?u+?v)+?w";
- ri "ASSOCS"; ex();

{?x + ?y + ?z + (?u + ?v) + ?w}  (* the final display *)
?x + ?y + ?z + (?u + ?v) + ?w

(* the full tactic *)

- declarepretheorem "ALLASSOCS";

- s "?x+?y";
- ri "ASSOCS"; ri "RIGHT@ALLASSOCS";
- p "ALLASSOCS";

ALLASSOCS:  
?x + ?y  =  
(RIGHT @ ALLASSOCS) => ASSOCS => ?x + ?y
0                              (* no axiom dependencies 
                               because no axiom was 
                               actually used to rewrite *)

(* test *)

s "(((?x+(?y+?z)+?w)+(?u+?v)+?w)+
                       ((?u+?v)+?w)+?e)+(?u+?v)+?e+?f";

{(((?x + (?y + ?z) + ?w) + (?u + ?v) + ?w) + ((?u 
            + ?v) + ?w) + ?e) + (?u + ?v) + ?e + ?f} 

(* duplication of displays suppressed *)

- ri "ALLASSOCS"; ex();

(* the final display -- intermediate and duplicate
displays suppressed *)

{?x + ?y + ?z + ?w + ?u + ?v + ?w + ?u + ?v + ?w + ?e 
   + ?u + ?v + ?e + ?f}