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?
Theorem foo' : forall a b : bool, a = b -> a = a \/ b = b \/ a = a. Proof. intros. rewrite -> 1 H.
but it replaced all
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?
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?
oriented_rewriter ::= (-> | <-)? natural? (? | !)? one_term_with_bindings
n in the
rewrite n H syntax same as the
oriented_rewriter? The kind we can use with
Yes. Note that the
?| ! is optional, so
rewrite n H is an instance where that punctuation is not used.
Ju-sh has marked this topic as resolved.
Last updated: Jan 31 2023 at 14:03 UTC