Julin S (Dec 29 2021 at 14:11): 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?
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.
Julin S (Dec 29 2021 at 16:50):Thanks!
Notification Bot (Dec 29 2021 at 16:50):Ju-sh has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC