将nat的证明转换为非负整型的证明
将nat的证明转换为非负整型的证明
提问于 2020-12-14 16:33:29
我证明了一些相当微不足道的引理
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，我们应该能够得出0 ≤ z → p' z，其中p‘与p“相同”。然而，我甚至不知道如何在精益中阐述这一点，更不用说如何证明它了。
所以，问题是，这可以在精益中得到证明，人们应该如何去做呢？
回答 1
Stack Overflow用户
发布于 2020-12-14 16:51:27
这一点能在精益中得到证明吗
如果它是正确的数学，它可以在精益中得到证明。你需要给第二个引理一个不同于第一个引理的名字。
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的策略知道什么是真的，什么是假的。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/65285838
复制相关文章
相似问题
腾讯云开发者
