如何仅对一个术语应用重写？

Question

在精益中，我有时想将一种rw策略应用于多个相同术语中的一个。例如我有一个目标

\n

\xe2\x8a\xa2 0 = 0\n

\n

我想要rw它

\n

\xe2\x8a\xa2 a * 0 = 0\n

\n

我也有

\n

mul_zero (a : mynat) :\n  a * 0 = 0\n

\n

现在我应该能够重写0to a * 0。然而尝试

\n

rw \xe2\x86\x90 zero_mul a,\n

\n

给我

\n

\xe2\x8a\xa2 a * 0 = a * 0\n

\n

这不是我想要的！

\n

精益这样做有什么原因吗？是否有某种方法可以将重写仅应用于一个术语？

\n

Answer 1

rw同时重写所有相同的术语。\n有一种不同的策略nth_rewrite只重写特定出现的术语。您需要 mathlib nth_rewrite，并且我不确定它是否在自然数游戏中可用。

\n

import tactic\nexample : 0 = 0 :=\nbegin\n  nth_rewrite 0 [\xe2\x86\x90 nat.mul_zero 2],\n  -- \xe2\x8a\xa2 2 * 0 = 0\nend\n

\n

Answer 2

您可以为此使用转换策略

\n

lemma a : 0 = 0 :=\nbegin\n  conv {\n    to_lhs, \n    rw \xe2\x86\x90 nat.mul_zero 2,\n  },\nend\n

\n

请参阅： https: //leanprover-community.github.io/extras/conv.html

\n