7.14 Tacticals

7.14 Tacticals

We describe in this section how to combine the tactics provided by the system to write synthetic proof scripts called tacticals. The tacticals are built using tactic operators we present below.

7.14.1 Idtac

The constant Idtac is the identity tactic: it leaves any goal unchanged.

7.14.2 Fail

The tactic Fail is the always-failing tactic: it does not solve any goal (may it may be useful for defining other tacticals).

7.14.3 Do num tactic

This tactic operator repeats num times the tactic tactic. It fails when it is not possible to repeat num times the tactic.

7.14.4 tactic1 Orelse tactic2

The tactical tactic1 Orelse tactic2 tries to apply tactic1 and, in case of a failure, applies tactic2. It associates to the left.

7.14.5 Repeat tactic

This tactic operator repeats tactic as long as it does not fail.

7.14.6 tactic1 ; tactic2

This tactic operator is a generalized composition for sequencing. The tactical tactic1 ; tactic2 first applies tactic1 and then applies tactic2 to any subgoal generated by tactic1. ; associates to the left.

7.14.7 tactic0; [ tactic1 | ...| tacticn ]

This tactic operator is a generalization of the precedent tactics operator. The tactical tactic0 ; [ tactic1 | ...| tacticn ] first applies tactic0 and then applies tactici to the i-th subgoal generated by tactic0. It fails if n is not the exact number of remaining subgoals.

7.14.8 Try tactic

This tactic operator applies tactic tactic, and catches the possible failure of tactic. It never fails.

7.14.9 Info tactic

This is not really a tactical. For elementary tactics, this is equivalent to tactic. For complex tactic like Auto, it displays the operations performed by the tactic.

7.14.10 Abstract tactic

From outside, typing Abstract tactic is the same that typing tactic. Internally it saves an auxiliary lemma called ident_subproofn where ident is the name of the current goal and n is choosen so that this is a fresh name.

This tactical is useful with tactics such Omega or Discriminate that generate big proof terms. With that tool the user can avoid the explosion at time of the Save command without having to cut ``by hand'' the proof in smaller lemmas.


Variants:
  1. Abstract tactic using ident.
    Give explicitly the name of the auxiliary lemma.


Retrieved by Memoweb from http://pauillac.inria.fr/coq/doc/node.1.2.13.html at 8/10/98