2

我是一个初学者，我坚持以下几点：

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

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

4

1 回答 1

4

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

example (n : ℕ): 2 ≠ 2 * (2 * n.succ) :=
by rw nat.succ_eq_add_one; linarith
于 2020-12-12T17:26:20.277 回答