Stream: Coq users

Topic: ✔ rewrite tactic with nat argument


view this post on Zulip 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 as with bs 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?

view this post on Zulip 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).

view this post on Zulip 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!?

view this post on Zulip 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.

view this post on Zulip Julin S (Dec 29 2021 at 16:50):

Thanks!

view this post on Zulip 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