A target indicates where a rewrite is to be applied. Targets are given by the grammar:

[target]      ::= in [hyp] at [occurrences]
                  in [hyp]                   (shorthand for: in hyp at 0)

[targets]     ::= [target] ...
                  [epsilon]                  (shorthand for: in concl at 0)
                  at [occurrences]           (shorthand for: in concl at [occurrences])

[occurrences] ::= [numbers]                  (rewrite the indicated hit numbers)
                  pos [numbers]              (rewrite the indicated term positions)
                  all                        (rewrite all hits)

In a [short-target] (as in reduce) the in can be omitted.

Hit numbers are counted in a pre-order, left-to-right traversal starting at 0. Hits are counted anew for each application, so if a rewrite eliminates a hit, then using that rewrite on the first two hits would be occurrences 0 0 (not 0 1). The testRewrite tool can assist in counting hits.

Term positions are also counted in a pre-order, left-to-right traversal starting at 0. Position counts are affected by the fact that paths are stored in spinal notation, so in x y z, position 0 is x y z, position 1 is y, and position 2 is z. There is no specific position for x or x y, but all rewrites will act on the prefix of a path so 0 will do. The showPosition tool can assist in counting positions.

When a hypothesis is rewritten, only earlier hypotheses are available to the rewrite. Thus, for example, a hypothetical equality can only be used to rewrite a later hypothesis. Similarly, any hypotheses used to satisfy typing obligations that are incurred by a rewrite must appear before the hypothesis being rewritten.

Capturing bindings

Some rewrites take a set of binders using the syntax within [captures]. These binders are used when rewriting beneath bindings. If n binders are supplied, the innermost n bindings are captured at the site of a prospective rewrite, and are given the supplied names. Those names can be used in terms that are supplied to the rewrite.

If the within [captures] syntax is omitted, the captures list is taken to be empty.


In the above rewrites, the term being replaced cannot have an evar head. That is, it must not be an evar, nor an elim starting from an evar.

Relations supported by unaugmented Istari include eq (_ = _ : _), eqtp (_ = _ : type), eeqtp (<:>), subtype (<:), iff (<->), and arrow. Note that arrows in an equation are interpreted as antecedents for the relation, not as the relation itself. Thus, to rewrite using arrow, one should use the synonym implies, which unfolds to arrow. Other relations can be supported by adding to the rewriter’s weakening and compatibility tables.

Rewriting tactics

Rewriting tools


When the rewriter searches for terms matching its target, it employs one of three levels of strictness:

Rewrites using -> and <- use intermediate matching, while the variants --> and <-- use strict matching. Intermediate matching is normally preferred because of its better flexibility, but sometimes strict matching is preferable. Consider the goal:

P (0 + 1 + x)

Rewriting this goal with -> Nat.plus_assoc will fail, because its target is E1 + E2 + E3 while the goal, up to beta equivalence, is P (1 + x). Unification cannot uniquely solve the constraint E1 + E2 = 1. One can resolve this by giving the arguments explicitly, as in -> Nat.plus_assoc 0 1 x, but that is more verbose.

Alternatively, --> Nat.plus_assoc works without explicit arguments. That is because it does not respect beta-equivalence, so each evar’s binding is uniquely determined.

Delayed typechecking

Note that rewriting takes place before typechecking. This can affect what hits the rewriter finds. For example, consider the lemma:

min_eq_l : forall (m n : nat) . m <= n -> min m n = m : nat

Suppose H : (x <= y) and one rewrites using -> min_eq_l _ _ H. Istari generates evars to fill in the underscores, say E1 and E2. Since typechecking has not taken place yet when the rewriter runs, those evars have not yet unified with x and y. Thus, the rewriter looks for terms it can unify with min E1 E2, not with min x y. The former could easily hit more often than the latter.

The user can account for this behavior by choosing an appropriate hit number, or by rewriting using -> min_eq_l x y H.

(This behavior is intended because the user always has the option to deal with typechecking subgoals manually, using rewriteRaw for example. It would be confusing if the rewriter behaved differently when doing so.)