Lean中如何仅对多个相同项中的单个项应用rw重写策略？

rw策略默认的匹配规则是替换目标中所有符合匹配条件的项。你使用的← mul_zero a对应等式为a * 0 = 0，反向重写的规则就是「将所有出现的0替换为a * 0」，你的初始目标⊢ 0 = 0中左右两侧都存在0，因此两个0会被同时替换，最终得到⊢ a * 0 = a * 0的结果。

有三种常用方式可以实现仅对单个匹配项重写：

• 使用nth_rw指定替换顺序：nth_rw的索引从1开始计数，对应匹配到的第N个项，仅替换左侧第一个0的写法为：

  nth_rw 1 [← mul_zero a]
  

• 使用conv模式精确定位作用域：可以直接指定操作等式的左侧或右侧，避免全局匹配，写法为：

  conv => lhs; rw ← mul_zero a
  

  其中lhs对应等式左侧，如需操作右侧可替换为rhs，对于更复杂的嵌套表达式，conv模式还可以逐级定位到目标子项进行操作，灵活性更高。
• 使用rw的occs参数指定匹配位置：直接在rw语句中传入参数限定匹配位置，写法为：

  rw ← mul_zero a { occs := occurrences.pos [1] }
  

内容的提问来源于stack exchange，提问作者Wheat Wizard