lean - 将 nat 的证明转化为非负整数的证明

Question

我证明了一些相当微不足道的引理

lemma two_ne_four_mul_any (n:ℕ) : 2 ≠ 2 * 2 * n

显然，这同样适用于非负整数、有理数、实数等:

lemma two_ne_four_mul_any (z:ℤ) (nonneg: 0 ≤ z): 2 ≠ 2 * 2 * z

一般来说，如果我们有一些 n:nat 的 p n，我们应该能够得出结论 0 ≤ z → p' z 其中p'与p“相同”。然而，我什至不知道如何在精益中表述这一点，更不用说如何证明它了。

那么，问题是，这能否在精益中得到证明，人们将如何去做？

Answer 1

can this be proven in Lean

如果它是正确的数学，它可以在精益中得到证明。不过，您需要为第二个引理指定一个与第一个引理不同的名称。

import tactic

lemma two_ne_four_mul_any (n:ℕ) : 2 ≠ 2 * 2 * n := sorry

lemma two_ne_four_mul_any' (z:ℤ) (nonneg: 0 ≤ z) : 2 ≠ 2 * 2 * z :=
begin
  -- get the natural
  rcases int.eq_coe_of_zero_le nonneg with ⟨n, rfl⟩,
  -- apply the lemma for naturals
  apply_mod_cast (two_ne_four_mul_any n)
end

这里你必须要小心一点——例如，自然数和整数的减法会产生不同的结果(例如，自然数中的 2-3=0 而整数中当然是 -1，所以如果 p n := n - 3 = 0 是关于自然数的陈述，那么 p 2 是正确的，但朴素的“相同”陈述对整数不正确)。 cast 策略知道什么是真实的，什么不是。