是否有解决此类琐碎目标的策略（精益定理证明）？

Question

我是一个初学者，我遇到了以下问题：

\n

import tactic.linarith\nimport tactic.suggest\n\nnoncomputable theory\nopen_locale classical\n\nlemma two_ne_four_mul_any (n:\xe2\x84\x95) : 2 \xe2\x89\xa0 2 * 2 * n := begin\n  cases n,\n  linarith,\n  rw mul_assoc,\n  ???\nend\n

\n

现在的状态是：

\n

n : \xe2\x84\x95\n\xe2\x8a\xa2 2 \xe2\x89\xa0 2 * (2 * n.succ)\n

\n

它看起来如此微不足道，以至于我认为必须有一种策略来解决它。但 linarith、ring、simpl、trivial 不起作用。

\n

那么，我是否错过了一些重要的内容？

\n

我还尝试使用现有的引理来解决这个问题。第一步我想达到：

\n

n : \xe2\x84\x95\n\xe2\x8a\xa2 1 \xe2\x89\xa0 2 * n.succ\n

\n

希望某些更高级别的策略现在能够看到这是真的。但是，我不知道如何对方程两边进行一些操作。两边都除以2不是应该有可能吗？

\n

我的计划是继续将 rhs 更改为 2*(n+1) 和 2n+2，也许目标是

\n

\xe2\x8a\xa2 0 \xe2\x89\xa0 2 * n + 1\n

\n

希望在图书馆找到适用的引理。

\n

Answer 1

linarith知道线性算术，这是一个线性算术目标，但它被 的使用所掩盖nat.succ。如果你重写它那就linarith行了。

\n

example (n : \xe2\x84\x95): 2 \xe2\x89\xa0 2 * (2 * n.succ) :=\nby rw nat.succ_eq_add_one; linarith\n

\n