## Stream: Coq users

### Topic: ✔ rewrite tactic with nat argument

#### Julin S (Dec 29 2021 at 14:11):

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?

#### Li-yao (Dec 29 2021 at 14:17):

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).

#### Julin S (Dec 29 2021 at 16:08):

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!`?

#### Li-yao (Dec 29 2021 at 16:09):

Yes. Note that the `?| !` is optional, so `rewrite n H` is an instance where that punctuation is not used.

Thanks!

#### Notification Bot (Dec 29 2021 at 16:50):

Ju-sh has marked this topic as resolved.

Last updated: Jan 31 2023 at 14:03 UTC