lean - 是否有解决此类琐碎目标的策略(精益定理证明)？

Question

我是初学者，但遇到以下问题:

import tactic.linarith
import tactic.suggest

noncomputable theory
open_locale classical

lemma two_ne_four_mul_any (n:ℕ) : 2 ≠ 2 * 2 * n := begin
  cases n,
  linarith,
  rw mul_assoc,
  ???
end

现在的状态是:

n : ℕ
⊢ 2 ≠ 2 * (2 * n.succ)

它接缝如此微不足道，我认为一定有解决它的策略。但是 linarith、ring、simp、trivial 不起作用。

那么，我是否错过了一些重要的导入？

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

n : ℕ
⊢ 1 ≠ 2 * n.succ

希望一些更高级别的策略现在可以看到它是真的。但是，我不知道如何对等式两边进行一些运算。难道不能以某种方式将两边除以 2 吗？

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

⊢ 0 ≠ 2 * n + 1

希望在库中找到适用的引理。

Answer 1

linarith 知道线性算术，这是一个线性算术目标，但它被 nat.succ 的使用遮蔽了。如果您重写它，那么 linarith 将起作用。

example (n : ℕ): 2 ≠ 2 * (2 * n.succ) :=
by rw nat.succ_eq_add_one; linarith