7.5 Conversion tactics

This set of tactics implements different restricted usages of the ``Conv''rule given in section 4.3.

7.5.1 `Change` term

This tactic applies to any goal. It implements the rule ``Conv''given in section 4.3. Change U replaces the current goal T with a U providing that U is well-formed and that T and U are convertible.

Error messages:

convert-concl rule passed non-converting term

7.5.2 `Cbv` flag₁ ...flag_n, `Lazy` flag₁ ...flag_n and `Compute`

These parameterized reduction tactics apply to any goal and perform the normalization of the goal according to the specified flags. Since the reduction considered in Coq include b (reduction of functional application), d (unfolding of transparent constants, see 5.2.5) and i (reduction of Cases, Fix and CoFix expressions), every flag is one of Beta, Delta, Iota, [ident₁...ident_k] and -[ident₁...ident_k]. The last two flags give the list of constants to unfold, or the list of constants not to unfold. These two flags can occur only after the Delta flag. The goal may be normalized with two strategies: lazy (Lazy tactic), or call-by-value (Cbv tactic).

The lazy strategy is a call-by-need strategy, with sharing of reductions: the arguments of a function call are partially evaluated only when necessary, but if an argument is used several times, it is computed only once. This reduction is efficient for reducing expressions with dead code. For instance, the proofs of a proposition $_T x. P(x) reduce to a pair of a witness t, and a proof that t verifies the predicate P. Most of the time, t may be computed without computing the proof of P(t), thanks to the lazy strategy.

The call-by-value strategy is the one used in ML languages: the arguments of a function call are evaluated first, using a weak reduction (no reduction under the l-abstractions). Despite the lazy strategy always performs fewer reductions than the call-by-value strategy, the latter should be preferred for evaluating purely computational expressions (i.e. with few dead code).

Variants:

Compute
This tactic is an alias for Cbv Beta Delta Iota.

Error messages:

Delta must be specified before
A list of constants appeared before the Delta flag.

7.5.3 `Red`

This tactic applies to a goal which have form (x:T1)...(xk:Tk)(c t1 ...tn) where c is a constant. If c is transparent then it replaces c with its definition (say t) and then reduces (t t1 ...tn) according to bi-reduction rules.

Error messages:

Term not reducible

7.5.4 `Hnf`

This tactic applies to any goal. It replaces the current goal with its head normal form according to the bdi-reduction rules. Hnf does not produce a real head normal form but either a product or an applicative term in head normal form or a variable.

Example: The term (n:nat)(plus (S n) (S n)) is not reduced by Hnf.

Remark: The d rule will only be applied to transparent constants (i.e. which have not been frozen with an Opaque command; see section 5.2.4).

7.5.5 `Simpl`

This tactic applies to any goal. The tactic Simpl first applies bi-reduction rule. Then it expands transparent constants and tries to reduce T' according, once more, to bi rules. But when the i rule is not applicable then possible d-reductions are not applied. For instance trying to use Simpl on (plus n O)=n will change nothing.

7.5.6 `Unfold` ident

This tactic applies to any goal. The argument ident must be the name of a defined transparent constant (see section 1.3.2 and 5.2.5). The tactic Unfold applies the d rule to each occurrence of ident in the current goal and then replaces it with its bi-normal form.

Warning: If the constant is opaque, nothing will happen and no warning is printed.
Error messages:

ident does not occur

Variants:

Unfold ident₁ ...ident_n
Replaces simultaneously ident₁, ..., ident_n with their definitions and replaces the current goal with its bi normal form.
Unfold num₁¹ ...num_i¹ ident₁ ...num₁ⁿ...num_jⁿ ident_n
The lists num₁¹, ..., num_i¹ and num₁ⁿ, ..., num_jⁿ are to specify the occurrences of ident₁, ..., ident_n to be unfolded. Occurrences are located from left to right in the linear notation of terms.

Error message: bad occurrence numbers of ident_i

7.5.7 `Fold` term

This tactic applies to any goal. term is reduced using the Red tactic. Every occurrence of the resulting term in the goal is then substituted for term.

Variants:

Fold term₁ ...term_n
Equivalent to Fold term₁;...; Fold term_n.

7.5.8 `Pattern` term

This command applies to any goal. The argument term must be a free subterm of the current goal. The command Pattern performs b-expansion (the inverse of b-reduction) of the current goal (say T) by

replacing all occurrences of term in T with a fresh variable
abstracting this variable
applying the abstracted goal to term

For instance, if the current goal T is (P t) when t does not occur in P then Pattern t transforms it into ([x:A](P x) t). This command has to be used, for instance, when an Apply command fails on matching.

Variants:

Pattern num₁ ...num_n term
Only the occurrences num₁ ...num_n of term will be considered for b-expansion. Occurrences are located from left to right.
Pattern num₁¹ ...num_i¹ term₁ ...num₁^m ...num_j^m term_m
Will process occurrences num₁¹, ..., num_i¹ of term₁, ..., num₁^m, ..., num_j^m of term_m starting from term_m. Starting from a goal (P t₁...t_m) with the t_i which do not occur in P, the tactic Pattern t₁...t_m generates the equivalent goal ([x₁:A₁]...[x_m:A_m](P x₁...x_m) t₁...t_m).
If t_i occurs in one of the generated types A_j these occurrences will also be considered and possibly abstracted.

7.5.9 Conversion tactics applied to hypotheses

conv_tactic in ident₁ ...ident_n
Applies the conversion tactic conv_tactic to the hypotheses ident₁, ..., ident_n. The tactic conv_tactic is any of the conversion tactics listed in this section.

Error messages:

No such hypothesis.

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