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

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

所以，问题是，这可以在精益中得到证明吗？如何去做呢？

Answer 1

这可以在精益中得到证明吗

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

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什么不是。