rw expression IN expression

Question

说，我需要:

rw ← nat.mul_one (d+d),

但是在整个目标中有多个(d+d)。我可以这样做吗:

rw ← nat.mul_one (d+d) in (5+(d+d)),

使得(d+d)只在括号中的完整表达式为5+(d+d)匹配的地方被重写?

Answer 1

您可以尝试mathlib的nth_rewrite或rw的可选occs参数。例如:

如果⊢ (d + d) + 5 * (d + d) + 2 * (d + d) = 8 * (d + d)，那么nth_rewrite ←nat.mul_one (d + d) 1应该工作，rw ←nat.mul_one (d + d) { occs := occurrences.pos [2]}也应该工作(注意nth_rewrite是零索引，而rw是1索引)。

你也可以使用conv，但我不建议这样做;在上面的例子中，conv是conv { congr, congr, congr, skip, rw ←nat.mul_one (d + d) }。

Answer 2

您可以在这里了解conv模式的乐趣，它使您能够进行有针对性的重写，或者您可以使用这里记录的nth_rewrite策略，它将让您精确地选择要更改的d+d中的哪个。