A few examples should give enough of the flavor of tactic writing in the Nuprl context to permit the reader to build substantial tactics of his own. Our first example is a very simple one which encodes a frequently used pattern of reasoning, namely, case analysis. When called as a refinement tactic with an argument which is a union type (i.e., of the form A|B) cases will do a seq with its argument and then do an elim on the copy of the term which appears in the hypothesis list of the second subgoal. The effect is essentially to implement a derived rule of the form
>> T by cases 'A|B' >> A | B A >> T B >> Texcept that any of the subgoals which the auto--tactic manages to prove will not appear. (Note the use of the quotes to make text into an ML term.) The following is the implementation of the tactic.
let cases union_term = refine (seq [union_term] [`nil`]) THENL [IDTAC ;\pf. refine (union_elim (length (hypotheses pf)) `nil` `nil`) pf ] THEN TRY (COMPLETE immediate) ;;
The first refine above will do the seq rule; the `nil` argument means that the new hypothesis in the second subgoal generated will not have a tag. The two members of the list following the THENL are what will be applied to the two subgoals resulting from the seq. The first one simply leaves alone the introduced union term, and the second does the elimination. The only complication is that the rule constructor union_elim requires the number of the hypothesis to be eliminated as an argument; in this case it is the last one, so the length of the current hypothesis list is the required number. Since the length of the actual proof to which refine is applied is necessary, the second tactic in the list of tactics is actually a lambda term. Recall that the type of tactics is proof->proof list # validation. Therefore, if X is a piece of ML code which uses an identifier pf and which is of type tactic under the assumption that pf is of type proof, then pf.(X pf) is also a tactic. When it is applied to a proof pf will be bound to the proof, and then the tactic defined by X will be applied. In the last line an attempt is made to prove completely all of the unproved subgoals generated so far.
The next example illustrates some of the other functions available in the ML environment of Nuprl . Given an integer, bring_hyp returns a refinement tactic implementing the rule
>> T' by bring_hyp i >> T->T'where T is the type in hypothesis i. This is often useful when it is desired that the substitutions done by an elimination be done in a hypothesis also; using this tactic, doing the elimination and then doing an introduction accomplishes this.
Figure: The bring_hyp Tactic
Figure shows the implementation of this tactic. The function select takes an integer n and a list and returns the element of the list, and type_of_declaration breaks down a declaration into its two components and returns the second part. make_function_term takes an identifier x and terms A and B to a term x:A->B. Note that because of the intended purpose of the tactic no attempt is made to prove one of the generated subgoals.