I was looking at the documentation of the `rewrite`

tactic and saw that it is possible to limit the number of rewrites by giving a `nat`

as a parameter.

How do we use it to actually limit the number of rewrites, though? I just wanted to figure out how it was meant to be used.

I thought it meant with an `H: a:bool = b:bool`

and goal `a = b -> a = a \/ b = b \/ a = a`

, rewriting with `1`

as the limit would make the goal `b = b -> a = a \/ b = b \/ a = a`

with only the first `a`

being replaced by `b`

. Is it not so?

I tried

```
Theorem foo' : forall a b : bool, a = b -> a = a \/ b = b \/ a = a.
Proof.
intros.
rewrite -> 1 H.
```

but it replaced all `a`

s with `b`

s and changed the goal from `a = b -> a = a \/ b = b \/ a = a`

to `b = b -> b = b \/ b = b \/ b = b`

.

Or is it applicable only when some sort of nesting is there?

You may rather be looking for `rewrite H at 1`

. `rewrite n H`

is equivalent to `rewrite H; rewrite H; ... ; rewrite H`

n times, and is useful for using universally quantified equations with different instantiations (each `rewrite`

uses only one instantiation).

The syntax for rewrite is given here as:

```
Tactic rewrite oriented_rewriter+, occurrences? by ltac_expr3?
```

where

```
oriented_rewriter ::= (-> | <-)? natural? (? | !)? one_term_with_bindings
```

Is the `n`

in the `rewrite n H`

syntax same as the `natural`

in `oriented_rewriter`

? The kind we can use with `?`

and `!`

like `1?`

and `2!`

?

Yes. Note that the `?| !`

is optional, so `rewrite n H`

is an instance where that punctuation is not used.

Thanks!

Ju-sh has marked this topic as resolved.

Last updated: Jun 18 2024 at 10:02 UTC